Nuprl - Proof: trivial-arrows 2 1 2

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

At: trivial-arrows 2 1 2

1. k:
2. L: List
3. i: ||L||
4. L[i] < k
5. n:
6. k-1n
7. G: {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||
8. increasing(x.x;L[i])

s:L[i] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(x.x;s)) = i

By: Auto THEN Inst Thm* n,m:, f:(nm). Inj(n; m; f) nm [k;L[i];x.s[x]]

Generated subgoal:

1 9. s: L[i] List
10. ||s|| = k
11. x,y:||s||. x < y s[x] < s[y]
Inj(k; L[i]; x.s[x]) 2 steps

About:

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