At: reach aux 1 1 1 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. Fin(S.car)
5. n: 
6. f: n
Alph
7. g: Alphn
8. InvFuns(n; Alph; f; g)
9. n1:
10. f1: n1S.car
11. g1: S.carn1
12. InvFuns(n1; S.car; f1; g1)
13. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||
n1+1 }| y[(||y||-1)] = si }
14. 
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)
By: InstConcl [RL]
Generated subgoals:None
About:
