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

At: trivial-arrows
k:, L: List. k-1- > L^k (i:||L||. L[i] < k)
By:
Auto
THEN
All (Unfold `arrows`)
THEN
ExRepD
Generated subgoals:

11. 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		8 steps
 
21. 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||
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)		8 steps

About:
listintnatural_numbersubtractless_thanfunctionequalimpliesallexists

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