k:
(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l)
l:Alph*. LangOf(Auto)(l)(n+1)8. l: {l:(Alph*)| ||l|| = k }
LangOf(Auto) 
Alph*
Propf:(nSt). Bij(n; St; f) (l:Alph*. LangOf(Auto)(l)) 
(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))| 1 | 7. k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l) l:Alph*. LangOf(Auto)(l) |
| 2 | 7. k: (n+1) 8. l: {l:(Alph*)| ||l|| = k } LangOf(Auto) Alph*Prop |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |