r,k:, L,R: List. 2k ||R|| = ||L|| (i:||L||. 0 < L[i] R[i]- > L[i--]^k) r- > R^k-1 r+1- > L^k

1

1. r: 2. k: 3. L: List 4. R: List 5. 2k 6. ||R|| = ||L|| 7. i:||L||. 0 < L[i] R[i]- > L[i--]^k 8. r- > R^k-1 9. n: 10. r+1n 11. 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)

98 steps

About: