PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach dec 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. Fin(St)
6. s: St
7. RL:St*. s:St. (w:Alph*. (Result(Auto)w) = s) mem_f(St;s;RL)

Dec(w:Alph*. (Result(Auto)w) = s)
By:
Analyze -1
THEN
RWH (HypC -1) 0
Generated subgoal:

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

About:
existslistequaluniverseall