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). Fin(St) (n:. #(St)=n ) pos_states

Thm* Auto:Automata(Alph;St), l:Alph*. ( < St,l,s. Auto(s,l) > :lInitialState(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

Thm* Alph,St:Type, A:Automata(Alph;St), l:Alph*. (Result(A)l) St compute_list_wf

Thm* Alph,States:Type, a:Automata(Alph;States). FinalState(a) States DA_fin_wf

Thm* Alph,States:Type, a:Automata(Alph;States). InitialState(a) States DA_init_wf

Thm* Alph,States:Type, a:Automata(Alph;States). a StatesAlphStates DA_act_wf