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

At: trivial-arrows 1 1 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))
4. s: {s:((k-1) List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }
||L||

By:
Analyze -1
THEN
Analyze -1


Generated subgoal:

14. s: (k-1) List
5. ||s|| = k
6. x,y:||s||. x < y s[x] < s[y]
||L||
3 steps

About:
listitintnatural_numbersubtractless_thansetfunction
equalmemberimpliesandallexists

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