At: empty lang dec 1 1 1 2 1 2 1 4
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. n: 
6.
f:(
n
St). 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)
10. Dec(
t:{l:(Alph*)| ||l|| = t }. (
l.LangOf(Auto)(l))(t))
Dec(
l:{l:(Alph*)| ||l|| = t }. LangOf(Auto)(l))
By: Reduce 10
Generated subgoals:None
About: