1 | 18. ( s. G(map(f;s))) {s:( R[c] List)| ||s|| = k & ( x,y: ||s||. x < y  s[x] < s[y]) }  ||L[c--]|| 19. c@0: ||L[c--]||, f@0:( L[c--][c@0]  R[c]).
increasing(f@0;L[c--][c@0])
& ( s: L[c--][c@0] List.
||s|| = k  ( x,y: ||s||. x < y  s[x] < s[y])  G(map(f;map(f@0;s))) = c@0) 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) | 72 steps |