:: Equivalence of Epsilon, Nondeterministic [Finite] Automata and Deterministic [Finite] Automata
:: by Micha{\l} Trybulec
::
:: Received May 25, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem LmNat1: :: FSM_3:1
for
i,
k,
l being
Nat st
i >= k + l holds
i >= k
theorem :: FSM_3:2
theorem ThTS3i: :: FSM_3:3
theorem LmXSeq10: :: FSM_3:4
theorem LmXSeq20: :: FSM_3:5
theorem LmSeq30: :: FSM_3:6
theorem ThTS3j: :: FSM_3:7
theorem ThLex10: :: FSM_3:8
theorem ThLex20: :: FSM_3:9
theorem ThLex30: :: FSM_3:10
theorem ThTS10: :: FSM_3:11
theorem ThDet20: :: FSM_3:12
definition
let E be non
empty set ;
let F be
Subset of
(E ^omega );
let TS be non
empty transition-system of
F;
func _bool TS -> strict transition-system of
Lex E means :
DefBool:
:: FSM_3:def 1
( the
carrier of
it = bool the
carrier of
TS & ( for
S being
Subset of
TS for
w being
Element of
E ^omega for
T being
Subset of
TS holds
(
[[S,w],T] in the
Tran of
it iff (
len w = 1 &
T = w -succ_of S,
TS ) ) ) );
existence
ex b1 being strict transition-system of Lex E st
( the carrier of b1 = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of b1 iff ( len w = 1 & T = w -succ_of S,TS ) ) ) )
uniqueness
for b1, b2 being strict transition-system of Lex E st the carrier of b1 = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of b1 iff ( len w = 1 & T = w -succ_of S,TS ) ) ) & the carrier of b2 = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of b2 iff ( len w = 1 & T = w -succ_of S,TS ) ) ) holds
b1 = b2
end;
:: deftheorem DefBool defines _bool FSM_3:def 1 :
theorem ThBool5: :: FSM_3:13
theorem ThBool10: :: FSM_3:14
:: deftheorem defDetSA defines deterministic FSM_3:def 2 :
definition
let E be non
empty set ;
let F be
Subset of
(E ^omega );
let SA be non
empty semiautomaton of
F;
func _bool SA -> strict semiautomaton of
Lex E means :
DefBoolSA:
:: FSM_3:def 3
(
transition-system(# the
carrier of
it,the
Tran of
it #)
= _bool transition-system(# the
carrier of
SA,the
Tran of
SA #) & the
InitS of
it = {((<%> E) -succ_of the InitS of SA,SA)} );
existence
ex b1 being strict semiautomaton of Lex E st
( transition-system(# the carrier of b1,the Tran of b1 #) = _bool transition-system(# the carrier of SA,the Tran of SA #) & the InitS of b1 = {((<%> E) -succ_of the InitS of SA,SA)} )
uniqueness
for b1, b2 being strict semiautomaton of Lex E st transition-system(# the carrier of b1,the Tran of b1 #) = _bool transition-system(# the carrier of SA,the Tran of SA #) & the InitS of b1 = {((<%> E) -succ_of the InitS of SA,SA)} & transition-system(# the carrier of b2,the Tran of b2 #) = _bool transition-system(# the carrier of SA,the Tran of SA #) & the InitS of b2 = {((<%> E) -succ_of the InitS of SA,SA)} holds
b1 = b2
;
end;
:: deftheorem DefBoolSA defines _bool FSM_3:def 3 :
theorem ThSA10: :: FSM_3:15
:: deftheorem defines left-Lang FSM_3:def 4 :
theorem ThLeft10: :: FSM_3:16
:: deftheorem defDetA defines deterministic FSM_3:def 5 :
definition
let E be non
empty set ;
let F be
Subset of
(E ^omega );
let A be non
empty automaton of
F;
func _bool A -> strict automaton of
Lex E means :
defBoolA:
:: FSM_3:def 6
(
semiautomaton(# the
carrier of
it,the
Tran of
it,the
InitS of
it #)
= _bool semiautomaton(# the
carrier of
A,the
Tran of
A,the
InitS of
A #) & the
FinalS of
it = { Q where Q is Element of it : Q meets the FinalS of A } );
existence
ex b1 being strict automaton of Lex E st
( semiautomaton(# the carrier of b1,the Tran of b1,the InitS of b1 #) = _bool semiautomaton(# the carrier of A,the Tran of A,the InitS of A #) & the FinalS of b1 = { Q where Q is Element of b1 : Q meets the FinalS of A } )
uniqueness
for b1, b2 being strict automaton of Lex E st semiautomaton(# the carrier of b1,the Tran of b1,the InitS of b1 #) = _bool semiautomaton(# the carrier of A,the Tran of A,the InitS of A #) & the FinalS of b1 = { Q where Q is Element of b1 : Q meets the FinalS of A } & semiautomaton(# the carrier of b2,the Tran of b2,the InitS of b2 #) = _bool semiautomaton(# the carrier of A,the Tran of A,the InitS of A #) & the FinalS of b2 = { Q where Q is Element of b2 : Q meets the FinalS of A } holds
b1 = b2
;
end;
:: deftheorem defBoolA defines _bool FSM_3:def 6 :
theorem ThA10: :: FSM_3:17
:: deftheorem defines right-Lang FSM_3:def 7 :
theorem ThRight10: :: FSM_3:18
:: deftheorem defines Lang FSM_3:def 8 :
theorem ThLang5: :: FSM_3:19
theorem ThLang10: :: FSM_3:20
theorem :: FSM_3:21
theorem :: FSM_3:22
theorem ThTS3h: :: FSM_3:23
theorem ThTS3g: :: FSM_3:24
theorem ThTS3e: :: FSM_3:25
:: deftheorem defCut defines chop FSM_3:def 9 :
theorem ThTS3k'b: :: FSM_3:26
theorem ThTS3k'a: :: FSM_3:27
theorem ThTS3k: :: FSM_3:28
theorem ThTS3: :: FSM_3:29
theorem ThSucc19: :: FSM_3:30
theorem ThTS38: :: FSM_3:31
theorem ThTS39: :: FSM_3:32
theorem ThSA39: :: FSM_3:33
theorem ThA20: :: FSM_3:34
theorem ThA30: :: FSM_3:35
theorem ThA38: :: FSM_3:36
theorem ThA39: :: FSM_3:37
theorem ThA40: :: FSM_3:38
theorem ThLang20: :: FSM_3:39
theorem :: FSM_3:40
theorem :: FSM_3:41