|
concat_arrays [n:nat, m:nat, T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory defines the concatenation operator o for arrays
%
%------------------------------------------------------------------------
BEGIN
IMPORTING below_arrays
a_n: VAR below_array[n,T]
a_m: VAR below_array[m,T]
nm : VAR below(n+m)
o(a_n, a_m): below_array[n+m,T] = (LAMBDA nm: IF nm < n THEN a_n(nm)
ELSE a_m(nm - n)
ENDIF)
i: VAR below(n)
j: VAR {i: int | i >= n AND i < n+m}
concat_array_bot0: THEOREM m = 0 IMPLIES a_n o a_m = a_n
concat_array_top0: THEOREM n = 0 IMPLIES a_n o a_m = a_m
concat_array_bot : THEOREM (a_n o a_m)(i) = a_n(i)
concat_array_top : THEOREM (a_n o a_m)(j) = a_m(j-n)
END concat_arrays
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
