|
caret_arrays [N:nat, T: TYPE]: THEORY
BEGIN
IMPORTING below_arrays, empty_array_def
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
¤ Dauer der Verarbeitung: 0.16 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.
|
