Nuprl - Pf empty_lang

PrintForm Definitions automata 7 Sections AutomataTheory Doc

1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. n:
6. f:(nSt). Bij(n; St; f)

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

By: Assert ((l:Alph*. LangOf(Auto)(l)) (k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l)))

Generated subgoals:

1 (l:Alph*. LangOf(Auto)(l)) (k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))

2 7. (l:Alph*. LangOf(Auto)(l)) (k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))
Dec(l:Alph*. LangOf(Auto)(l))

About:

1	`(l:Alph. LangOf(Auto)(l)) (k:(n+1), l:{l:(Alph)\| \|\|l\|\| = k }. LangOf(Auto)(l))`
2	7. `(l:Alph. LangOf(Auto)(l)) (k:(n+1), l:{l:(Alph)\| \|\|l\|\| = k }. LangOf(Auto)(l))` `Dec(l:Alph*. LangOf(Auto)(l))`