Nuprl - Proof: length le 1 2 1 1 1

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

At: length le 1 2 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. 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

a1 = a2

By: SupposeNot THEN Unfold `no_repeats` 4 THEN InstHyp [a1;a2] 4

Generated subgoal:

1 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 1 step

About:

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