| array_seg |
Def a[i..j] == < i,j,2of(2of(a)) >
Thm*  i: , j:{i...}, a:[T]Array{i..j }, m:{i..j}, n:{m..j}.
a[m..n]  [T]Array{m..n}
|
| p_array |
Def [T]Array{i..j} == {a:[T]Array | a.l = i & a.u = j}
Thm* T:Type{i}, i:, j:{i...}. [T]Array{i..j} Type{[i']}
|
| array |
Def [T]Array == n: m:{n...}{n..m}  T
Thm* T:Type{i}. [T]Array Type{[i']}
|
| int_seg |
Def {i..j} == {k:| i  k < j}
Thm* m,n:. {m..n} Type
|
| int_upper |
Def {i...} == {j:| ij}
Thm* n:. {n...} Type
|
| array_ub |
Def a.u == 1of(2of(a))
Thm* a:[T]Array . a.u
|
| pi2 |
Def 2of(t) == t.2
Thm* B:(AType), p:a:AB(a). 2of(p) B(1of(p))
|
| array_lb |
Def a.l == 1of(a)
Thm* a:[T]Array . a.l
|
| lelt |
Def i j < k == ij & j < k
|
| le |
Def AB ==  B < A
Thm* i,j:. ij Prop
|
| pi1 |
Def 1of(t) == t.1
Thm* B:(AType), p:a:AB(a). 1of(p) A
|
| not |
Def A == A   False
Thm* (A) Prop
|