A: VAR below_array[N,T]
m, n: VAR nat
p: VAR [nat, below[N]]
^(A, p): below_array[LET (m, n) = p IN IF m > n THEN 0 ELSE n - m + 1 ENDIF,T] = LET (m, n) = p IN IF m <= n THEN (LAMBDA (x: below[n-m+1]): A(x + m)) ELSE empty_array ENDIF
i,j,k: VAR below(N)
caret_all : LEMMA N > 0 IMPLIES A^(0,N-1) = A
caret_ii_0: LEMMA (A^(i,i))(0) = A(i)
caret_elim: LEMMA i <= j AND k < i - j + 1 IMPLIES (A ^ (i, j))(k) = A(j+k)
END caret_arrays
¤ 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.0.12Bemerkung:
(vorverarbeitet)
¤
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.
