At:
length le
1
2
1
1
1
1
1.
T: Type
2.
A: T List
3.
B: T List
4.
i,j:
. i < ||A|| 
j < ||A|| 
i = j A[i] = A[j]
5.
x:T. (x 
A) (x B)
6.
f: i:||A||
j:||B||
A[i] = B[j]
7.
a1: ||A||
8.
a2: ||A||
9.
j: ||B||
10.
z1: A[a1] = B[j]
11.
j1: ||B||
12.
z2: A[a2] = B[j]
13.
j = j1
14.
a1 = a2
15.
A[a1] = A[a2]
a1 = a2
By:
Analyze -1
Generated subgoals:
None
About:
