6. f:
n
Alph7. g: Alph
n8. InvFuns(
n; Alph; f; g)
RL:S.car*. 
s:S.car. (w:Alph*. (S:w
si) = s) 
mem_f(S.car;s;RL) RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)f:(AB). Bij(A; B; f)) (A ~ B))
-1
| 1 | 5. n: 6. f: nAlph7. g: Alph n8. InvFuns( n; Alph; f; g) RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL) |
About:
 |  |  |  |  |