Nuprl - Proof: length le 1 2 1

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

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

1of(f(a1)) = 1of(f(a2)) a1 = a2

By: GenConclAtAddr [1;2;1] THEN Thin -1 THEN Analyze -1 THEN Reduce 0 THEN GenConclAtAddr [1;3;1] THEN Thin -1 THEN Analyze -1 THEN Reduce 0

Generated subgoal:

1 9. j: ||B||
10. z1: A[a1] = B[j]
11. j1: ||B||
12. z2: A[a2] = B[j1]
j = j1 a1 = a2 3 steps

About:

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