S:ActionSet(Alph), sL:S.car*.
Fin(Alph) 
Fin(S.car)
(
TBL:S.car*.
s:S.car. mem_f(S.car;s;TBL) 
(w:Alph*. mem_f(S.car;(S:w
s);sL)))
total_back_listify
s) == if null(L)
s else S.act(hd(L),(S:tl(L)s)) fi (recursive)
Thm* S:ActionSet(Alph), sL:S.car*.
Fin(Alph)
Fin(S.car)
(TBL:S.car*.
s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL)))
total_back_listify
In prior sections: action sets det automata