PrintForm
Definitions
automata
7
Sections
AutomataTheory
Doc
At:
empty
lang
dec
1
1
1
1
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)
(
l:Alph*. FinalState(Auto)(Result(Auto)l))
(
k:
(n+1), l:{l:(Alph*)| ||l|| = k }. FinalState(Auto)(Result(Auto)l))
By:
RWH (LemmaC
Thm*
Auto:Automata(Alph;St), l:Alph*. (Result(Auto)l) = (Action(Auto):l
InitialState(Auto))) 0
Generated subgoal:
1
(
l:Alph*. FinalState(Auto)((Action(Auto):l
InitialState(Auto))))
(
k:
(n+1), l:{l:(Alph*)| ||l|| = k }. FinalState(Auto)((Action(Auto):l
InitialState(Auto))))
About: