Selected Objects
| COM | ARRAY_DEFS | [T]Array : type of all arrays of type T.
[T]Array{i..j-} : Those arrays with start index i and
end index j-1.
e.g. a[i], a[i+1], ..., a[j-1]
NIL |
| DEF | array | [T]Array == n:  m:{n...}{n..m }  T |
| DEF | array_lb | a.l == 1of(a) |
| DEF | array_ub | a.u == 1of(2of(a)) |
| DEF | p_array | [T]Array{i..j} == {a:[T]Array | a.l = i & a.u = j} |
| THM | p_array_properties |  i:, j:{i...}, a:[T]Array{i..j}. a.l = i & a.u = j |
| DEF | array_el | a[i] == 2of(2of(a))(i) |
| DEF | array_seg | a[i..j] == < i,j,2of(2of(a)) > |
| DEF | array_shift | a[++i] == < (a.l+i),(a.u+i),( j.a[(j-i)]) > |
| DEF | array_append | arr1 @ arr2 == < arr1.l,arr2.u,(i.if i < arr1.u arr1[i] ; arr2[i] fi) > |