Nuprl - Proof: arrows wf 1

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

At: arrows wf 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]

map(f;s) {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }

By: Analyze THEN Try (Complete Auto) THEN RWW Thm* f:(AB), as:A List. ||map(f;as)|| = ||as|| 0 THEN RWW Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) 0

Generated subgoal:

1 13. x: ||s||
14. y: ||s||
15. x < y
f(s[x]) < f(s[y]) 1 step

About:

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