PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: empty lang dec 1 1 1 1 2 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. k: (n+1)
8. l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l)

l:Alph*. LangOf(Auto)(l)

By: Analyze 8

Generated subgoal:

18. l: {l:(Alph*)| ||l|| = k }
9. LangOf(Auto)(l)
l:Alph*. LangOf(Auto)(l)


About:
existslistapplyuniversefunction
natural_numberaddsetequalint