At:
length less
2
1
1
1
1
1.
T: Type
2.
A: T List
3.
B: T List
4.
no_repeats(T;A)
5.
x:T. (x 
A) 
(x B)
6.
x: T
7.
(x A)
8.
i: 
9.
i < ||B||
10.
x = B[i]
11.
f: k:||A||
j:||B||
A[k] = B[j] & j = i
12.
k: ||A||
13.
j: ||B||
14.
z1: A[k] = B[j] & j = i
15.
f(k) = < j,z1 > j:||B||A[k] = B[j] & j = i
if j < 
i
j else j-1 fi (||B||-1)
By:
SplitOnConclITE
Generated subgoals:
None
About:
