Inj(
k; (k-1); 
x.s[x])
k-1 
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))
(k-1) List
x,y:||s||. x < y s[x] < s[y]
||L||
n,m:, f:(nm). Inj(n; m; f) nm
[k;k-1;x.s[x]]
| 1 | Inj(k; (k-1); x.s[x]) | 1 step |
| 2 | 7. kk-1 | 1 step |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |
 |