R[c] List20. ||s|| = k
21.
x,y:||s||. x < y 
s[x] < s[y]
G(map(f;s)) ||L||
List
List
k
i:||L||. 0 < L[i] R[i]- > L[i--]^k
n
n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }
||L||
||R||
R[c](n-1)
s:R[c] List. ||s|| = k-1 (x,y:||s||. x < y s[x] < s[y]) G(map(f;s) @ [(n-1)]) = c
G:({s:(R[c] List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L[c--]||).
c@0:||L[c--]||, f:(L[c--][c@0]R[c]).
increasing(f;L[c--][c@0])
& (s:L[c--][c@0] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c@0)
(
s. G(map(f;s))) {s:(R[c] List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L[c--]||
L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L||
0)
| 1 | 19. s: R[c] List 20. ||s|| = k 21. x,y:||s||. x < y s[x] < s[y] G(map(f;s)) ||L|| | 1 step |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |