Nuprl - Proof: length less 2 1

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

At: length less 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. 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

f:(||A||(||B||-1)). Inj(||A||; (||B||-1); f)

By: RenameVar `f' -1 THEN Unfolds [`all`;`exists`] -1 THEN InstConcl [k.if 1of(f(k)) < i 1of(f(k)) else 1of(f(k))-1 fi] THEN Try (Complete Auto)

Generated subgoals:

1 11. f: k:||A||j:||B||A[k] = B[j] & j = i
(k.if 1of(f(k)) < i 1of(f(k)) else 1of(f(k))-1 fi) ||A||(||B||-1) 3 steps

2 11. f: k:||A||j:||B||A[k] = B[j] & j = i
Inj(||A||; (||B||-1); k.if 1of(f(k)) < i 1of(f(k)) else 1of(f(k))-1 fi) 2 steps

About:

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