Definitions
array
1
Doc
At:
array
shift
wf
1
2
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
a:
[T]Array
5.
a.l = i & a.u = j
6.
m:
a[++m].l = i+m & a[++m].u = j+m
By:
Analyze 4
THEN
Analyze 5
THEN
Repeat (Unfolds [`array_shift`;`array_lb`;`array_ub`] 0)
THEN
Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 0
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+m = i+m & m1+m = j+m