Definitions
array
1
Doc
At:
array
shift
wf
1
1
1
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
n:
5.
m1:
{n...}
6.
a2:
{n..m1
}
T
7.
< n,m1,a2 > .l = i
8.
< n,m1,a2 > .u = j
9.
m:
n+m
m1+m
By:
SupInf
Generated subgoals:
None
}
T
n+m
m1+m