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