PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: empty lang dec 1 1 1 2 1 2
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((k.l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))(t))
By: Reduce 0
Generated subgoal:

1 Dec(l:{l:(Alph*)| ||l|| = t }. LangOf(Auto)(l))

About:
applylambdaexistssetlistequal
intuniversefunctionnatural_numberimpliesadd