:: Equivalence of Epsilon, Nondeterministic [Finite] Automata and Deterministic [Finite] Automata
:: by Micha{\l} Trybulec
::
:: Received May 25, 2009
:: Copyright (c) 2009-2021 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 (E ^omega);
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 b₁ being strict transition-system over Lex E st
( the carrier of b₁ = 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 b₁ iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict transition-system over Lex E st the carrier of b₁ = 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 b₁ iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) & the carrier of b₂ = 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 b₂ iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) holds
b₁ = b₂

proof end;

end;

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

registration

let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;

cluster _bool TS -> non empty strict deterministic ;

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 (E ^omega);
let TS be non empty finite transition-system over F;

cluster _bool TS -> finite strict ;

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 (E ^omega)
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 (E ^omega)
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 (E ^omega);
attr c₃ is strict ;
struct semiautomaton over F -> transition-system over F;
aggr semiautomaton(# carrier, Tran, InitS #) -> semiautomaton over F;
sel InitS c₃ -> Subset of the carrier of c₃;

end;

definition

let E be non empty set ;
let F be Subset of (E ^omega);
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 (E ^omega)
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 (E ^omega);

cluster non empty finite strict deterministic for semiautomaton over F;

existence
ex b₁ being semiautomaton over F st
( b₁ is strict & not b₁ is empty & b₁ is finite & b₁ is deterministic )

proof end;

end;

registration

let E be non empty set ;
let F be Subset of (E ^omega);
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 (E ^omega);
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 b₁ being strict semiautomaton over Lex E st
( transition-system(# the carrier of b₁, the Tran of b₁ #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b₁ = {((<%> E) -succ_of ( the InitS of SA,SA))} )

proof end;

uniqueness
for b₁, b₂ being strict semiautomaton over Lex E st transition-system(# the carrier of b₁, the Tran of b₁ #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b₁ = {((<%> E) -succ_of ( the InitS of SA,SA))} & transition-system(# the carrier of b₂, the Tran of b₂ #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b₂ = {((<%> E) -succ_of ( the InitS of SA,SA))} holds
b₁ = b₂ ;

end;

:: deftheorem Def3 defines _bool FSM_3:def 3 :
for E being non empty set
for F being Subset of (E ^omega)
for SA being non empty semiautomaton over F
for b₄ being strict semiautomaton over Lex E holds
( b₄ = _bool SA iff ( transition-system(# the carrier of b₄, the Tran of b₄ #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b₄ = {((<%> E) -succ_of ( the InitS of SA,SA))} ) );

registration

let E be non empty set ;
let F be Subset of (E ^omega);
let SA be non empty semiautomaton over F;

cluster _bool SA -> non empty strict deterministic ;

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 (E ^omega)
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 (E ^omega);
let SA be non empty finite semiautomaton over F;

cluster _bool SA -> finite strict ;

coherence
_bool SA is finite

proof end;

end;

:: Left-languages

definition

let E be non empty set ;
let F be Subset of (E ^omega);
let SA be non empty semiautomaton over F;
let Q be Subset of SA;

func left-Lang Q -> Subset of (E ^omega) 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 (E ^omega)

proof end;

end;

:: deftheorem defines left-Lang FSM_3:def 4 :
for E being non empty set
for F being Subset of (E ^omega)
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 (E ^omega)
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 (E ^omega);
attr c₃ is strict ;
struct automaton over F -> semiautomaton over F;
aggr automaton(# carrier, Tran, InitS, FinalS #) -> automaton over F;
sel FinalS c₃ -> Subset of the carrier of c₃;

end;

definition

let E be non empty set ;
let F be Subset of (E ^omega);
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 (E ^omega)
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 (E ^omega);

cluster non empty finite strict deterministic for automaton over F;

existence
ex b₁ being automaton over F st
( b₁ is strict & not b₁ is empty & b₁ is finite & b₁ is deterministic )

proof end;

end;

registration

let E be non empty set ;
let F be Subset of (E ^omega);
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 (E ^omega);
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 b₁ being strict automaton over Lex E st
( semiautomaton(# the carrier of b₁, the Tran of b₁, the InitS of b₁ #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b₁ = { Q where Q is Element of b₁ : Q meets the FinalS of A } )

proof end;

uniqueness
for b₁, b₂ being strict automaton over Lex E st semiautomaton(# the carrier of b₁, the Tran of b₁, the InitS of b₁ #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b₁ = { Q where Q is Element of b₁ : Q meets the FinalS of A } & semiautomaton(# the carrier of b₂, the Tran of b₂, the InitS of b₂ #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b₂ = { Q where Q is Element of b₂ : Q meets the FinalS of A } holds
b₁ = b₂ ;

end;

:: deftheorem Def6 defines _bool FSM_3:def 6 :
for E being non empty set
for F being Subset of (E ^omega)
for A being non empty automaton over F
for b₄ being strict automaton over Lex E holds
( b₄ = _bool A iff ( semiautomaton(# the carrier of b₄, the Tran of b₄, the InitS of b₄ #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b₄ = { Q where Q is Element of b₄ : Q meets the FinalS of A } ) );

registration

let E be non empty set ;
let F be Subset of (E ^omega);
let A be non empty automaton over F;

cluster _bool A -> non empty strict deterministic ;

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 (E ^omega)
for A being non empty automaton over F holds the carrier of (_bool A) = bool the carrier of A

proof end;

registration

let E be non empty set ;
let F be Subset of (E ^omega);
let A be non empty finite automaton over F;

cluster _bool A -> finite strict ;

coherence
_bool A is finite

proof end;

end;

:: Languages Accepted by Automata

definition

let E be non empty set ;
let F be Subset of (E ^omega);
let A be non empty automaton over F;
let Q be Subset of A;

func right-Lang Q -> Subset of (E ^omega) 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 (E ^omega)

proof end;

end;

:: deftheorem defines right-Lang FSM_3:def 7 :
for E being non empty set
for F being Subset of (E ^omega)
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 (E ^omega)
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 (E ^omega);
let A be non empty automaton over F;

func Lang A -> Subset of (E ^omega) 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 (E ^omega)

proof end;

end;

:: deftheorem defines Lang FSM_3:def 8 :
for E being non empty set
for F being Subset of (E ^omega)
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 (E ^omega)
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 (E ^omega)
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 (E ^omega)
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 (E ^omega)
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 b₁ being Element of E ^omega st
for w being Element of E ^omega st w ^ v = u holds
b₁ = w ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b₁ being Element of E ^omega st b₁ = u ) )

proof end;

uniqueness
for b₁, b₂ 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
b₁ = w ) & ( for w being Element of E ^omega st w ^ v = u holds
b₂ = w ) implies b₁ = b₂ ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) & b₁ = u & b₂ = u implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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, b₄ being Element of E ^omega holds
( ( ex w being Element of E ^omega st w ^ v = u implies ( b₄ = chop (u,v) iff for w being Element of E ^omega st w ^ v = u holds
b₄ = w ) ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ( b₄ = chop (u,v) iff b₄ = 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 (_bool A)

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 (_bool A) 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 (_bool A) = {((<%> 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))},(_bool 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 (_bool A),(_bool A)) = {(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 (_bool A)

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;