seq_def[T: TYPE]: THEORY BEGIN finite_seq: TYPE = [# l: nat, seq: [below[l] -> T] #] fs, fs1, fs2, fs3: VAR finite_seq m, n: VAR nat fin_seq(n): TYPE = {fs | l(fs) = n} fseq(fs): [below[l(fs)] -> T] = seq(fs) CONVERSION fseq o(fs1, fs2): finite_seq = LET l1 = l(fs1), lsum = l1 + l(fs2) IN (# l := lsum, seq := (LAMBDA (n:below[lsum]): IF n < l1 THEN seq(fs1)(n) ELSE seq(fs2)(n-l1) ENDIF) #); emptyarr(x: below[0]): T emptyseq: fin_seq(0) = (# l := 0, seq := emptyarr #) ; p: VAR [nat, nat] ; ^(fs: finite_seq, (p: [nat, below(l(fs))])): fin_seq(IF proj_1(p) > proj_2(p) THEN 0 ELSE proj_2(p)-proj_1(p)+1 ENDIF) = LET (m, n) = p IN IF m > n THEN emptyseq ELSE (# l := n-m+1, seq := (LAMBDA (x: below[n-m+1]): seq(fs)(x + m)) #) ENDIF ; rev(fs): finite_seq = (# l := l(fs), seq := (LAMBDA (i: below(l(fs))): seq(fs)(l(fs)-1-i)) #) %% ^(fs: finite_seq, (p: [m: nat, {n: nat | n >= m AND n < l(fs)}])): %% fin_seq(proj_2(p)-proj_1(p)+1) = %% LET (m, n) = p IN %% (# l := n-m+1, %% seq := (LAMBDA (x: below[n-m+1]): seq(fs)(x + m)) #) ; % % % ^^(fs, p): finite_seq = % LET (m, n) = p % IN IF m > n OR m >= l(fs) % THEN emptyseq % ELSE LET len = IF n < l(fs) THEN n - m + 1 % ELSE l(fs) - m ENDIF % IN (# l := len, % seq := (LAMBDA (x: below[len]): seq(fs)(x + m)) #) % ENDIF ; % % i,j: VAR nat % extractors_eq: LEMMA j < l(fs) IMPLIES fs^(i,j) = fs^^(i,j) END seq_def