Auto:Automata(Alph;St)
, l:x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)). Auto(l)
accept_list_qwf
== FinalState(DA)(Result(DA)l)
Thm* Auto:Automata(Alph;St)
, l:x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)). Auto(l)
accept_list_qwf