:: 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 Th1: :: FSM_3:1
for
i,
k,
l being
Nat st
i >= k + l holds
i >= k
theorem :: FSM_3:2
theorem Th3: :: FSM_3:3
theorem Th4: :: FSM_3:4
theorem Th5: :: FSM_3:5
theorem Th6: :: FSM_3:6
theorem Th7: :: FSM_3:7
theorem Th8: :: FSM_3:8
theorem Th9: :: FSM_3:9
theorem Th10: :: FSM_3:10
theorem :: FSM_3:11
canceled;
theorem Th12: :: 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 :
Def1:
:: 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 Def1 defines _bool FSM_3:def 1 :
theorem Th13: :: FSM_3:13
theorem Th14: :: FSM_3:14
:: deftheorem Def2 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 :
Def3:
:: 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 Def3 defines _bool FSM_3:def 3 :
theorem Th15: :: FSM_3:15
:: deftheorem defines left-Lang FSM_3:def 4 :
theorem Th16: :: FSM_3:16
:: deftheorem Def5 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 :
Def6:
:: 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 Def6 defines _bool FSM_3:def 6 :
theorem Th17: :: FSM_3:17
:: deftheorem defines right-Lang FSM_3:def 7 :
theorem Th18: :: FSM_3:18
:: deftheorem defines Lang FSM_3:def 8 :
theorem Th19: :: FSM_3:19
theorem Th20: :: FSM_3:20
theorem :: FSM_3:21
theorem :: FSM_3:22
theorem Th23: :: FSM_3:23
theorem Th24: :: FSM_3:24
theorem Th25: :: FSM_3:25
:: deftheorem Def9 defines chop FSM_3:def 9 :
theorem Th26: :: FSM_3:26
theorem Th27: :: FSM_3:27
theorem Th28: :: FSM_3:28
theorem Th29: :: FSM_3:29
theorem Th30: :: FSM_3:30
theorem Th31: :: FSM_3:31
theorem Th32: :: FSM_3:32
theorem Th33: :: FSM_3:33
theorem Th34: :: FSM_3:34
theorem Th35: :: FSM_3:35
theorem Th36: :: FSM_3:36
theorem Th37: :: FSM_3:37
theorem Th38: :: FSM_3:38
theorem Th39: :: FSM_3:39
theorem :: FSM_3:40
theorem :: FSM_3:41