Nuprl - Proof: trivial-arrows 2 2

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

At: trivial-arrows 2 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. f: L[i]n

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

By: Auto THEN Analyze THEN Try (Complete Auto) THEN RWO Thm* f:(AB), as:A List. ||map(f;as)|| = ||as|| 0 THEN RWO Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) 0 THEN AllHyps (h. FwdThru Thm* k:, f:(k). increasing(f;k) (x,y:k. x < y f(x) < f(y)) [h]) THEN BackThru -1 THEN EasyHyp

Generated subgoals:

None

About:

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