Definitions
array
1
Doc
At:
array
shift
wf
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
a:
[T]Array
5.
a.l = i & a.u = j
6.
m:
a[++m]
[T]Array
By:
Unfolds [`array`;`array_shift`] 0
THEN
Analyze 4
THEN
Analyze 5
Generated subgoal:
1
4.
n:
5.
m1:
{n...}
6.
a2:
{n..m1
}
T
7.
< n,m1,a2 > .l = i & < n,m1,a2 > .u = j
8.
m:
< ( < n,m1,a2 > .l+m),( < n,m1,a2 > .u+m),(
j. < n,m1,a2 > [(j-m)]) >
n:
m:{n...}
{n..m
}
T