PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: empty lang dec 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. n:
6. f: nSt
7. g: Stn
8. InvFuns(n; St; f; g)
9. l: Alph*
10. FinalState(Auto)((Action(Auto):lInitialState(Auto)))

InvFuns(St; n; g; f)
By: BackThru Thm* f:(AB), g:(BA). InvFuns(A; B; f; g) InvFuns(B; A; g; f)
Generated subgoals:

None

About:
natural_numberuniverseallfunctionimplieslistassertapply