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 empty_array_def[T: TYPE]: THEORY BEGIN IMPORTING below_arrays empty_array: below_array[0,T] % (LAMBDA (x: below[0]): epsilon! (t:T): true) ; END empty_array_def