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
False ; b.bs' b = a 
T 
mem_f(T;a;bs')
(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
Thm* f:(T
). Fin(T) (fL:T*. t:T. f(t) mem_f(T;t;fL)) bool_listify
Thm* S:ActionSet(Alph), s:S.car.
Fin(Alph)
Fin(S.car)
(BL:S.car*. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = s))
back_listify
Thm* Fin(T) (TL:T*. t:T. mem_f(T;t;TL)) fin_listify
In prior sections: list 3 autom det automata