PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: empty lang dec 1 1 1 1 1 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). Bij(n; St; f)
7. l: Alph*
8. FinalState(Auto)((Action(Auto):lInitialState(Auto)))

0 < n
By: RWH (LemmaC Thm* (f:(AB). Bij(A; B; f)) (A ~ B)) 6
Generated subgoal:

16. n ~ St
7. l: Alph*
8. FinalState(Auto)((Action(Auto):lInitialState(Auto)))
0 < n

About:
less_thannatural_numberuniverseexistsfunctionlistassertapply