Nuprl - Proof: length less 1

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

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]

k:||A||. j:||B||. A[k] = B[j] & j = i

By: Analyze 0 THEN InstHyp [A[k]] 5

Generated subgoals:

1 11. k: ||A||
(A[k] A) 1 step

2 11. k: ||A||
12. (A[k] B)
j:||B||. A[k] = B[j] & j = i 3 steps

About:

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

1	11. `k:` `\|\|A\|\|` `(A[k] A)`	1 step

2	11. `k:` `\|\|A\|\|` 12. `(A[k] B)` `j:\|\|B\|\|. A[k] = B[j] & j = i`	3 steps