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. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. n:
6. n ~ St
7. l: Alph*
8. FinalState(Auto)((Action(Auto):lInitialState(Auto)))

f:(Stn), g:(nSt). InvFuns(St; n; f; g)
By: Unfold `one_one_corr` 6
Generated subgoal:

16. f:(nSt), g:(Stn). InvFuns(n; St; f; g)
7. l: Alph*
8. FinalState(Auto)((Action(Auto):lInitialState(Auto)))
f:(Stn), g:(nSt). InvFuns(St; n; f; g)

About:
existsfunctionnatural_numberuniverselistassertapply