2. S: ActionSet(Alph)
3. si: S.car
4. Fin(S.car)
5. Fin(Alph)
RL:S.car*. 
s:S.car. (w:Alph*. (S:w
si) = s) 
mem_f(S.car;s;RL) Alph:Type, S:ActionSet(Alph), si:S.car.
Fin(S.car) 
Fin(Alph) (RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL))| 1 | 1. Alph: Type 2. S: ActionSet(Alph) 3. si: S.car 4. Fin(S.car) 5. Fin(Alph) RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL) |
About:
 |  |  |  |  |  |