i,j:
(n+1). i < j & (
i.f((S:([1]
i)
s)))(i) = (i.f((S:([1]i)s)))(j) 
n
L:
*. (S:Ls) = q & (
k:. 
L = n0n1(k)))
ng:(nS.car). InvFuns(S.car; n; f; g)k:. (S:n0n1(k)s) = q L:*. (S:Ls) = q & (k:. L = n0n1(k))n:{1...}, m:{n+1...}, f:(mn). i,j:m. i < j & f(i) = f(j)
[n;n+1;i.f((S:([1]i)s))]| 1 | 8. i,j:(n+1). i < j & (i.f((S:([1]i)s)))(i) = (i.f((S:([1]i)s)))(j) n L:*. (S:Ls) = q & (k:. L = n0n1(k)) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |