Nuprl - Proof: arrows wf 1 1

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

At: arrows wf 1 1

1. r:
2. k:
3. L: List
4. n:
5. rn
6. G: {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||
7. c: ||L||
8. f: L[c]n
9. increasing(f;L[c])
10. s: L[c] List
11. ||s|| = k
12. x,y:||s||. x < y s[x] < s[y]
13. x: ||s||
14. y: ||s||
15. x < y

f(s[x]) < f(s[y])

By: FwdThru Thm* k:, f:(k). increasing(f;k) (x,y:k. x < y f(x) < f(y)) [9] THEN BackThru -1 THEN EasyHyp

Generated subgoals:

None

About:

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