Auto:Automata(Alph;St).
Fin(Alph) 
Fin(St) (s:St. Dec(
w:Alph*. (Result(Auto)w) = s))
reach_dec
InitialState(DA) else 
DA((Result(DA)tl(l)),hd(l)) fi
(recursive)
Thm* Auto:Automata(Alph;St).
Fin(Alph) Fin(St) (s:St. Dec(w:Alph*. (Result(Auto)w) = s))
reach_dec
Thm* Auto:Automata(Alph;St).
Fin(St) & Fin(Alph)
(RL:St*. s:St. (w:Alph*. (Result(Auto)w) = s) 
mem_f(St;s;RL))
reach_list
Thm* Auto:Automata(Alph;St), l:Alph*.
( < St,
l,s. Auto(s,l) > :l
InitialState(Auto)) = (Result(Auto)l)
action_auto
Thm* Auto:Automata(Alph;St)
, l:x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)). Auto(l)
accept_list_qwf
Thm* Auto:Automata(Alph;St), x,y,z:Alph*.
(Result(Auto)x) = (Result(Auto)y)
(Result(Auto)z @ x) = (Result(Auto)z @ y)
compute_l_inv
Thm* Auto:Automata(Alph;St)
, l:x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)). (Result(Auto)l) St
compute_list_qwf