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