Definitions
array
1
Doc
At:
array
shift
wf
1
1
1
1
2
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:
10.
j1:
{(n+m)..(m1+m)
}
n
j1-m
By:
SupInf
Generated subgoals:
None
}
T}
n
j1-m