n
S.car7. InvFuns(S.car;
n; f; g)8.
k:. (S:n0n1(k)
s) = q9. i:
(n+1)10. j:
(n+1)11. i < j
12. f((S:([1]
i)s)) = f((S:([1]j)s))
L:
*. (S:Ls) = q & (k:. 
L = n0n1(k)))
ng:(nS.car). InvFuns(S.car; n; f; g)k:. (S:n0n1(k)s) = q(n+1)(n+1)i)s)) = f((S:([1]j)s)) L:*. (S:Ls) = q & (k:. L = n0n1(k))| 1 | 6. g: nS.car 7. InvFuns(S.car; n; f; g)8. k:. (S:n0n1(k)s) = q9. i: (n+1)10. j: (n+1)11. i < j 12. f((S:([1] i)s)) = f((S:([1]j)s)) L:*. (S:Ls) = q & (k:. L = n0n1(k)) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |