List

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))

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

1

4. c: ||L|| 5. f: L[c](k-1) 6. increasing(f;L[c]) 7. s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) (s.)(map(f;s)) = c L[c] < k

1 step

About: