| array_append |
Def arr1 @ arr2 == < arr1.l,arr2.u,( i.if i < arr1.u arr1[i] ; arr2[i] fi) >
Thm*  i: , j:{i...}, k:{j...}, a:[T]Array{i..j }, b:[T]Array{j..k}.
a @ b  [T]Array{i..k}
|
| 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_upper |
Def {i...} == {j:| i j}
Thm* n:. {n...} Type
|
| array_lb |
Def a.l == 1of(a)
Thm* a:[T]Array . a.l
|
| array_ub |
Def a.u == 1of(2of(a))
Thm* a:[T]Array . a.u
|
| array_el |
Def a[i] == 2of(2of(a))(i)
Thm* i:, j:{i...}, a:[T]Array{i..j}, k:{i..j}. a[k] T
Thm* a:[T]Array , i:{a.l..a.u}. a[i] T
|
| int_seg |
Def {i..j} == {k:| i k < j}
Thm* m,n:. {m..n} Type
|
| 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
|
| pi2 |
Def 2of(t) == t.2
Thm* B:(AType), p:a:AB(a). 2of(p) B(1of(p))
|
| not |
Def A == A   False
Thm* (A) Prop
|