Nuprl - Proof: length less 1 2 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]
11. k: ||A||
12. i1:
13. i1 < ||B||
14. A[k] = B[i1]

i1 = i

By: ParallelOp 7 THEN Unfold `l_member` 0 THEN InstConcl [k]

Generated subgoal:

1 7. i:
8. i < ||B||
9. x = B[i]
10. k: ||A||
11. i1:
12. i1 < ||B||
13. A[k] = B[i1]
14. i1 = i
x = A[k] 1 step

About:

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