:: Equivalence of Epsilon, Nondeterministic [Finite] Automata and Deterministic [Finite] Automata
:: by Micha{\l} Trybulec
::
:: Copyright (c) 2009-2019 Association of Mizar Users

:: Preliminaries - Natural Numbers
theorem Th1: :: FSM_3:1
for i, k, l being Nat st i >= k + l holds
i >= k
proof end;

:: Preliminaries - Sequences
theorem :: FSM_3:2
for a, b being FinSequence st ( a ^ b = a or b ^ a = a ) holds
b = {}
proof end;

theorem Th3: :: FSM_3:3
for k being Nat
for p, q being FinSequence st k in dom p & (len p) + 1 = len q holds
k + 1 in dom q
proof end;

:: Preliminaries - XFinSequences and Words in E^omega
theorem Th4: :: FSM_3:4
for E being non empty set
for u being Element of E ^omega st len u = 1 holds
ex e being Element of E st
( <%e%> = u & e = u . 0 )
proof end;

theorem Th5: :: FSM_3:5
for E being non empty set
for u being Element of E ^omega
for k being Nat st k <> 0 & len u <= k + 1 holds
ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )
proof end;

theorem Th6: :: FSM_3:6
for x, y being set
for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds
( x = y & p = q )
proof end;

theorem Th7: :: FSM_3:7
for E being non empty set
for u being Element of E ^omega st len u > 0 holds
ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1
proof end;

:: Preliminaries - Lex
registration
let E be non empty set ;
cluster Lex E -> non empty ;
coherence
not Lex E is empty
proof end;
end;

theorem Th8: :: FSM_3:8
for E being non empty set holds not <%> E in Lex E
proof end;

theorem Th9: :: FSM_3:9
for E being non empty set
for u being Element of E ^omega holds
( u in Lex E iff len u = 1 )
proof end;

theorem Th10: :: FSM_3:10
for E being non empty set
for u, v being Element of E ^omega st u <> v & u in Lex E & v in Lex E holds
for w being Element of E ^omega holds
( not u ^ w = v & not w ^ u = v )
proof end;

:: Transition Systems over Lex(E)
theorem Th11: :: FSM_3:11
for E being non empty set
for TS being transition-system over Lex E st the Tran of TS is Function holds
TS is deterministic
proof end;

:: Powerset Construction for Transition Systems
:: This is a construction that limits new transitions to single character ones.
definition
let E be non empty set ;
let F be Subset of ();
let TS be non empty transition-system over F;
func _bool TS -> strict transition-system over 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 over 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) ) ) ) )
proof end;
uniqueness
for b1, b2 being strict transition-system over 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
proof end;
end;

:: deftheorem Def1 defines _bool FSM_3:def 1 :
for E being non empty set
for F being Subset of ()
for TS being non empty transition-system over F
for b4 being strict transition-system over Lex E holds
( b4 = _bool TS iff ( the carrier of b4 = 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 b4 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) ) );

registration
let E be non empty set ;
let F be Subset of ();
let TS be non empty transition-system over F;
coherence
( not _bool TS is empty & _bool TS is deterministic )
proof end;
end;

registration
let E be non empty set ;
let F be Subset of ();
let TS be non empty finite transition-system over F;
coherence
_bool TS is finite
proof end;
end;

theorem Th12: :: FSM_3:12
for x, y being set
for E being non empty set
for e being Element of E
for F being Subset of ()
for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds
x,<%e%> ==>. y, <%> E, _bool TS
proof end;

theorem Th13: :: FSM_3:13
for X being set
for E being non empty set
for w being Element of E ^omega
for F being Subset of ()
for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
proof end;

:: Semiautomata
definition
let E be non empty set ;
let F be Subset of ();
attr c3 is strict ;
struct semiautomaton over F -> transition-system over F;
aggr semiautomaton(# carrier, Tran, InitS #) -> semiautomaton over F;
sel InitS c3 -> Subset of the carrier of c3;
end;

definition
let E be non empty set ;
let F be Subset of ();
let SA be semiautomaton over F;
attr SA is deterministic means :Def2: :: FSM_3:def 2
( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 );
end;

:: deftheorem Def2 defines deterministic FSM_3:def 2 :
for E being non empty set
for F being Subset of ()
for SA being semiautomaton over F holds
( SA is deterministic iff ( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 ) );

registration
let E be non empty set ;
let F be Subset of ();
existence
ex b1 being semiautomaton over F st
( b1 is strict & not b1 is empty & b1 is finite & b1 is deterministic )
proof end;
end;

registration
let E be non empty set ;
let F be Subset of ();
let SA be non empty semiautomaton over F;
cluster transition-system(# the carrier of SA, the Tran of SA #) -> non empty ;
coherence
not transition-system(# the carrier of SA, the Tran of SA #) is empty
;
end;

definition
let E be non empty set ;
let F be Subset of ();
let SA be non empty semiautomaton over F;
func _bool SA -> strict semiautomaton over 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 over 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))} )
proof end;
uniqueness
for b1, b2 being strict semiautomaton over 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 :
for E being non empty set
for F being Subset of ()
for SA being non empty semiautomaton over F
for b4 being strict semiautomaton over Lex E holds
( b4 = _bool SA iff ( transition-system(# the carrier of b4, the Tran of b4 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b4 = {((<%> E) -succ_of ( the InitS of SA,SA))} ) );

registration
let E be non empty set ;
let F be Subset of ();
let SA be non empty semiautomaton over F;
coherence
( not _bool SA is empty & _bool SA is deterministic )
proof end;
end;

theorem Th14: :: FSM_3:14
for E being non empty set
for F being Subset of ()
for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA
proof end;

registration
let E be non empty set ;
let F be Subset of ();
let SA be non empty finite semiautomaton over F;
coherence
_bool SA is finite
proof end;
end;

:: Left-languages
definition
let E be non empty set ;
let F be Subset of ();
let SA be non empty semiautomaton over F;
let Q be Subset of SA;
func left-Lang Q -> Subset of () equals :: FSM_3:def 4
{ w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ;
coherence
{ w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } is Subset of ()
proof end;
end;

:: deftheorem defines left-Lang FSM_3:def 4 :
for E being non empty set
for F being Subset of ()
for SA being non empty semiautomaton over F
for Q being Subset of SA holds left-Lang Q = { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ;

theorem Th15: :: FSM_3:15
for E being non empty set
for w being Element of E ^omega
for F being Subset of ()
for SA being non empty semiautomaton over F
for Q being Subset of SA holds
( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )
proof end;

:: Automata
definition
let E be non empty set ;
let F be Subset of ();
attr c3 is strict ;
struct automaton over F -> semiautomaton over F;
aggr automaton(# carrier, Tran, InitS, FinalS #) -> automaton over F;
sel FinalS c3 -> Subset of the carrier of c3;
end;

definition
let E be non empty set ;
let F be Subset of ();
let A be automaton over F;
attr A is deterministic means :Def5: :: FSM_3:def 5
semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic ;
end;

:: deftheorem Def5 defines deterministic FSM_3:def 5 :
for E being non empty set
for F being Subset of ()
for A being automaton over F holds
( A is deterministic iff semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic );

registration
let E be non empty set ;
let F be Subset of ();
cluster non empty finite strict deterministic for automaton over F;
existence
ex b1 being automaton over F st
( b1 is strict & not b1 is empty & b1 is finite & b1 is deterministic )
proof end;
end;

registration
let E be non empty set ;
let F be Subset of ();
let A be non empty automaton over F;
cluster transition-system(# the carrier of A, the Tran of A #) -> non empty ;
coherence
not transition-system(# the carrier of A, the Tran of A #) is empty
;
cluster semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) -> non empty ;
coherence
not semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is empty
;
end;

definition
let E be non empty set ;
let F be Subset of ();
let A be non empty automaton over F;
func _bool A -> strict automaton over 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 over 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 } )
proof end;
uniqueness
for b1, b2 being strict automaton over 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 :
for E being non empty set
for F being Subset of ()
for A being non empty automaton over F
for b4 being strict automaton over Lex E holds
( b4 = _bool A iff ( semiautomaton(# the carrier of b4, the Tran of b4, the InitS of b4 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b4 = { Q where Q is Element of b4 : Q meets the FinalS of A } ) );

registration
let E be non empty set ;
let F be Subset of ();
let A be non empty automaton over F;
coherence
( not _bool A is empty & _bool A is deterministic )
proof end;
end;

theorem Th16: :: FSM_3:16
for E being non empty set
for F being Subset of ()
for A being non empty automaton over F holds the carrier of () = bool the carrier of A
proof end;

registration
let E be non empty set ;
let F be Subset of ();
let A be non empty finite automaton over F;
coherence
_bool A is finite
proof end;
end;

:: Languages Accepted by Automata
definition
let E be non empty set ;
let F be Subset of ();
let A be non empty automaton over F;
let Q be Subset of A;
func right-Lang Q -> Subset of () equals :: FSM_3:def 7
{ w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ;
coherence
{ w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } is Subset of ()
proof end;
end;

:: deftheorem defines right-Lang FSM_3:def 7 :
for E being non empty set
for F being Subset of ()
for A being non empty automaton over F
for Q being Subset of A holds right-Lang Q = { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ;

theorem Th17: :: FSM_3:17
for E being non empty set
for w being Element of E ^omega
for F being Subset of ()
for A being non empty automaton over F
for Q being Subset of A holds
( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )
proof end;

definition
let E be non empty set ;
let F be Subset of ();
let A be non empty automaton over F;
func Lang A -> Subset of () equals :: FSM_3:def 8
{ u where u is Element of E ^omega : ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A )
}
;
coherence
{ u where u is Element of E ^omega : ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A )
}
is Subset of ()
proof end;
end;

:: deftheorem defines Lang FSM_3:def 8 :
for E being non empty set
for F being Subset of ()
for A being non empty automaton over F holds Lang A = { u where u is Element of E ^omega : ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A )
}
;

theorem Th18: :: FSM_3:18
for E being non empty set
for w being Element of E ^omega
for F being Subset of ()
for A being non empty automaton over F holds
( w in Lang A iff ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) )
proof end;

theorem Th19: :: FSM_3:19
for E being non empty set
for w being Element of E ^omega
for F being Subset of ()
for A being non empty automaton over F holds
( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A )
proof end;

theorem :: FSM_3:20
for E being non empty set
for F being Subset of ()
for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A
proof end;

theorem :: FSM_3:21
for E being non empty set
for F being Subset of ()
for A being non empty automaton over F holds Lang A = right-Lang the InitS of A
proof end;

theorem Th22: :: FSM_3:22
for E being non empty set
for e being Element of E
for u being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for R being RedSequence of ==>.-relation TS st (R . 1) 2 = <%e%> ^ u & (R . (len R)) 2 = <%> E & not (R . 2) 2 = <%e%> ^ u holds
(R . 2) 2 = u
proof end;

theorem Th23: :: FSM_3:23
for E being non empty set
for u being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for R being RedSequence of ==>.-relation TS st (R . 1) 2 = u & (R . (len R)) 2 = <%> E holds
len R > len u
proof end;

theorem Th24: :: FSM_3:24
for E being non empty set
for u, v being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for R being RedSequence of ==>.-relation TS st (R . 1) 2 = u ^ v & (R . (len R)) 2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v )
proof end;

definition
let E be non empty set ;
let u, v be Element of E ^omega ;
func chop (u,v) -> Element of E ^omega means :Def9: :: FSM_3:def 9
for w being Element of E ^omega st w ^ v = u holds
it = w if ex w being Element of E ^omega st w ^ v = u
otherwise it = u;
existence
( ( ex w being Element of E ^omega st w ^ v = u implies ex b1 being Element of E ^omega st
for w being Element of E ^omega st w ^ v = u holds
b1 = w ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b1 being Element of E ^omega st b1 = u ) )
proof end;
uniqueness
for b1, b2 being Element of E ^omega holds
( ( ex w being Element of E ^omega st w ^ v = u & ( for w being Element of E ^omega st w ^ v = u holds
b1 = w ) & ( for w being Element of E ^omega st w ^ v = u holds
b2 = w ) implies b1 = b2 ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) & b1 = u & b2 = u implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of E ^omega holds verum
;
end;

:: deftheorem Def9 defines chop FSM_3:def 9 :
for E being non empty set
for u, v, b4 being Element of E ^omega holds
( ( ex w being Element of E ^omega st w ^ v = u implies ( b4 = chop (u,v) iff for w being Element of E ^omega st w ^ v = u holds
b4 = w ) ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ( b4 = chop (u,v) iff b4 = u ) ) );

theorem Th25: :: FSM_3:25
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
proof end;

theorem Th26: :: FSM_3:26
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds
==>.-relation TS reduces [x,u],[y,v]
proof end;

theorem Th27: :: FSM_3:27
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st x,u ^ w ==>* y,v ^ w,TS holds
x,u ==>* y,v,TS
proof end;

theorem Th28: :: FSM_3:28
for E being non empty set
for u, v being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for p, q being Element of TS st p,u ^ v ==>* q,TS holds
ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS )
proof end;

theorem Th29: :: FSM_3:29
for X being set
for E being non empty set
for v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)
proof end;

theorem Th30: :: FSM_3:30
for E being non empty set
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)}
proof end;

theorem Th31: :: FSM_3:31
for X being set
for E being non empty set
for v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}
proof end;

theorem Th32: :: FSM_3:32
for X being set
for E being non empty set
for w being Element of E ^omega
for SA being non empty semiautomaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))}
proof end;

theorem Th33: :: FSM_3:33
for x being set
for E being non empty set
for A being non empty automaton over (Lex E) \/ {(<%> E)}
for P being Subset of A st x in the FinalS of A & x in P holds
P in the FinalS of ()
proof end;

theorem Th34: :: FSM_3:34
for X being set
for E being non empty set
for A being non empty automaton over (Lex E) \/ {(<%> E)} st X in the FinalS of () holds
X meets the FinalS of A
proof end;

theorem Th35: :: FSM_3:35
for E being non empty set
for A being non empty automaton over (Lex E) \/ {(<%> E)} holds the InitS of () = {((<%> E) -succ_of ( the InitS of A,A))}
proof end;

theorem Th36: :: FSM_3:36
for X being set
for E being non empty set
for w being Element of E ^omega
for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},()) = {(w -succ_of (X,A))}
proof end;

theorem Th37: :: FSM_3:37
for E being non empty set
for w being Element of E ^omega
for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ( the InitS of (),()) = {(w -succ_of ( the InitS of A,A))}
proof end;

theorem Th38: :: FSM_3:38
for E being non empty set
for A being non empty automaton over (Lex E) \/ {(<%> E)} holds Lang A = Lang ()
proof end;

theorem :: FSM_3:39
for E being non empty set
for A being non empty automaton over (Lex E) \/ {(<%> E)} ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA
proof end;

theorem :: FSM_3:40
for E being non empty set
for FA being non empty finite automaton over (Lex E) \/ {(<%> E)} ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA
proof end;