(13steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: length less
T:Type, A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T. (x A) & (x B)) ||A|| < ||B||
By:
Auto
THEN
ExRepD
THEN
Analyze -1
THEN
ExRepD
THEN
Assert (k:||A||. j:||B||. A[k] = B[j] & j = i)
Generated subgoals:

11. 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]
k:||A||. j:||B||. A[k] = B[j] & j = i		5 steps
 
21. 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. k:||A||. j:||B||. A[k] = B[j] & j = i
||A|| < ||B||		7 steps

About:
listintnatural_numberless_thanuniverseequalimpliesandallexists

(13steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc