PrintForm
Definitions
automata
7
Sections
AutomataTheory
Doc
At:
empty
lang
dec
1
1
1
1
2
1
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.
k:
(n+1)
8.
l:
{l:(Alph*)| ||l|| = k }
9.
LangOf(Auto)(l)
l:Alph*. LangOf(Auto)(l)
By:
Witness l
Generated subgoal:
1
10.
l1:
Alph*
LangOf(Auto)
Alph*
Prop
About:
LangOf(Auto) 
Alph*
Prop
f:(nSt). Bij(n; St; f)(n+1) l:Alph*. LangOf(Auto)(l) LangOf(Auto) Alph*Prop
