Nuprl - Proof: trivial-arrows 1

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

At: trivial-arrows 1

1. k:
2. L: List
3. n:. k-1n (G:({s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||). c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c))

i:||L||. L[i] < k

By: InstHyp [k-1;s.] -1 THEN Try (Complete Auto)

Generated subgoals:

1 (s.) {s:((k-1) List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L|| 5 steps

2 4. c:||L||, f:(L[c](k-1)). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) (s.)(map(f;s)) = c)
i:||L||. L[i] < k 2 steps

About:

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