At:
length less2121
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.
a1: ||A||
13.
a2: ||A||
14.
j: ||B||
15.
z1: A[a1] = B[j] & j = i
16.
j1: ||B||
17.
z2: A[a2] = B[j1] & j1 = i
if j < i j else j-1 fi = if j1 < i j1 else j1-1 fi (||B||-1) a1 = a2
By:
RepeatFor 2 SplitOnConclITE
THEN
SupposeNot
THEN
Unfold `no_repeats` 4
THEN
InstHyp [a1;a2] 4
THEN
Analyze -1
THEN
SubstFor A[a1] 0
THEN
SubstFor A[a2] 0
THEN
Analyze
Generated subgoals:
x:T. (x 
A) 
(x 
(x 
j:
A[k] = B[j] & 
if j < 
i
j else j-1 fi = if j1 < 
