PrintForm Definitions det automata Sections AutomataTheory Doc

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

RL:St*. s:St. (w:Alph*. (Result(Auto)w) = s) mem_f(St;s;RL)
By: Inst Thm* S:ActionSet(Alph), si:S.car. Fin(S.car) Fin(Alph) (RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)) [Alph; < St,a:Alph. s:St. Auto(s,a) > ;InitialState(Auto)]
Generated subgoals:

1 < St,a:Alph. s:St. Auto(s,a) > ActionSet(Alph)
2 < St,a:Alph. s:St. Auto(s,a) > .car Type
3 Fin( < St,a:Alph. s:St. Auto(s,a) > .car)
46. RL: < St,a:Alph. s:St. Auto(s,a) > .car*. s: < St,a:Alph. s:St. Auto(s,a) > .car. (w:Alph*. ( < St,a:Alph. s:St. Auto(s,a) > :wInitialState(Auto)) = s) mem_f( < St,a:Alph. s:St. Auto(s,a) > .car;s;RL)
RL:St*. s:St. (w:Alph*. (Result(Auto)w) = s) mem_f(St;s;RL)

About:
existslistallequalpairapplyuniversemember