Definitions
array
1
Doc
At:
array
el
wfp
1
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
a:
[T]Array
5.
a.l = i
6.
a.u = j
7.
k:
{i..j
}
a[k]
T
By:
Unfold `array` 4
THEN
Analyze 4
THEN
Analyze 5
Generated subgoal:
1
4.
n:
5.
m:
{n...}
6.
a2:
{n..m
}
T
7.
< n,m,a2 > .l = i
8.
< n,m,a2 > .u = j
9.
k:
{i..j
}
< n,m,a2 > [k]
T