PrintForm
Definitions
automata
7
Sections
AutomataTheory
Doc
At:
empty
lang
dec
1
1
1
2
1
1
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))
Fin(
(n+1))
By:
BackThru
Thm*
n:
. Fin(
n)
Generated subgoals:
None
About:
f:(n
St). Bij(n; St; f)l:Alph*. LangOf(Auto)(l)) 
(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))l:Alph*. LangOf(Auto)(l)) 
(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))
Fin((n+1))
n:. Fin(n)
