PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach dec 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. Fin(St)
6. s: St

Dec(w:Alph*. (Result(Auto)w) = s)
By: Inst Thm* Auto:Automata(Alph;St). Fin(St) & Fin(Alph) (RL:St*. s:St. (w:Alph*. (Result(Auto)w) = s) mem_f(St;s;RL)) [Alph;St;Auto]
Generated subgoal:

17. RL:St*. s:St. (w:Alph*. (Result(Auto)w) = s) mem_f(St;s;RL)
Dec(w:Alph*. (Result(Auto)w) = s)

About:
existslistequaluniverse