PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach list 1 4 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(St)
5. Fin(Alph)
6. RL:St*. s:St. (w:Alph*. ( < St,a:Alph. s:St. Auto(s,a) > :wInitialState(Auto)) = s) mem_f(St;s;RL)

RL:St*. s:St. (w:Alph*. (Result(Auto)w) = s) mem_f(St;s;RL)
By: RWH (LemmaC Thm* Auto:Automata(Alph;St), l:Alph*. ( < St,l,s. Auto(s,l) > :lInitialState(Auto)) = (Result(Auto)l)) -1
Generated subgoals:

None

About:
existslistallequaluniversepairapply