PrintForm Definitions automata 7 Sections AutomataTheory Doc

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

Dec(l:{l:(Alph*)| ||l|| = t }. LangOf(Auto)(l))
By: Inst Thm* R:(TProp). Fin(T) & (t:T. Dec(R(t))) Dec(t:T. R(t)) [{l:(Alph*)| ||l|| = t };l.LangOf(Auto)(l)]
Generated subgoals:

110. l: {l:(Alph*)| ||l|| = t }
LangOf(Auto) Alph*Prop
2 Fin({l:(Alph*)| ||l|| = t })
310. t1: {l:(Alph*)| ||l|| = t }
Dec((l.LangOf(Auto)(l))(t1))
410. Dec(t:{l:(Alph*)| ||l|| = t }. (l.LangOf(Auto)(l))(t))
Dec(l:{l:(Alph*)| ||l|| = t }. LangOf(Auto)(l))

About:
existssetlistequalintapplyuniverseall
functionpropimpliesandlambdanatural_numberaddmember