| array_shift |
Def a[++i] == < (a.l+i),(a.u+i),( j.a[(j-i)]) >
Thm*  i: , j:{i...}, a:[T]Array{i..j }, m:. a[++m]  [T]Array{i+m..j+m}
|
| 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
|
| array_ub |
Def a.u == 1of(2of(a))
Thm* a:[T]Array . a.u
|
| array_lb |
Def a.l == 1of(a)
Thm* a:[T]Array . a.l
|
| pi2 |
Def 2of(t) == t.2
Thm* B:(A  Type), p:a:A B(a). 2of(p) B(1of(p))
|
| pi1 |
Def 1of(t) == t.1
Thm* B:(AType), p:a:AB(a). 1of(p) A
|