Definitions
array
1
Doc
At:
array
append
wf
1
1
2
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
k:
{j...}
5.
n1:
6.
m1:
{n1...}
7.
a2:
{n1..m1
}
T
8.
n1 = i
9.
m1 = j
10.
n:
11.
m:
{n...}
12.
b2:
{n..m
}
T
13.
n = j
14.
m = k
n1 = i & m = k
By:
Auto
Generated subgoals:
None
}
T}T
n1 = i & m = k