PrintForm
Definitions
automata
7
Sections
AutomataTheory
Doc
At:
empty
lang
dec
1
1
1
2
1
3
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.
Dec(
t:
(n+1). (
k.
l:{l:(Alph*)| ||l|| = k
}. LangOf(Auto)(l))(t))
Dec(
k:
(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))
By:
Reduce 8
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))t:(n+1). (
k.l:{l:(Alph*)| ||l|| = k 
}. LangOf(Auto)(l))(t))
Dec(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))
