PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: empty lang dec 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. Fin(St)

Dec(l:Alph*. LangOf(Auto)(l))
By:
Unfold `finite` 5
THEN
Analyze 5
Generated subgoal:

15. n:
6. f:(nSt). Bij(n; St; f)
Dec(l:Alph*. LangOf(Auto)(l))

About:
existslistapplyuniverse