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


begin

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

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

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
proofend;

:: 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 &amp; e = u . 0 )
proofend;

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 &amp; len u <= k + 1 holds
ex v1, v2 being Element of E ^omega st
( len v1 <= k &amp; len v2 <= k &amp; u = v1 ^ v2 )
proofend;

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

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
proofend;

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

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

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 )
proofend;

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

:: 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
proofend;

:: 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 &amp; ( 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 &amp; 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 &amp; ( 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 &amp; T = w -succ_of (S,TS) ) ) ) )
proofend;
uniqueness
 for b1, b2 being strict transition-system over Lex E st the carrier of b1 = bool the carrier of TS &amp; ( 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 &amp; T = w -succ_of (S,TS) ) ) ) &amp; the carrier of b2 = bool the carrier of TS &amp; ( 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 &amp; T = w -succ_of (S,TS) ) ) ) holds
b1 = b2
proofend;
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 b4 being strict transition-system over Lex E holds
( b4 = _bool TS iff ( the carrier of b4 = bool the carrier of TS &amp; ( 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 &amp; 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 &amp; _bool TS is deterministic )
proofend;
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
proofend;
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
proofend;

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 )
proofend;

:: Semiautomata
definition
let E be non empty set ;
let F be Subset of (E ^omega);
attrc3 is strict ;
struct semiautomaton over F ->  transition-system over F;
aggrsemiautomaton(# 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 (E ^omega);
let SA be semiautomaton over F;
attrSA is deterministic  means :Def2: :: FSM_3:def 2
( transition-system(# the carrier of SA, the Tran of SA #) is deterministic &amp; 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 &amp; 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 b1 being semiautomaton over F st
( b1 is strict &amp; not b1 is empty &amp; b1 is finite &amp; b1 is deterministic )
proofend;
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 #) &amp; 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 #) &amp; the InitS of b1 = {((<%> E) -succ_of ( the InitS of SA,SA))} )
proofend;
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 #) &amp; the InitS of b1 = {((<%> E) -succ_of ( the InitS of SA,SA))} &amp; transition-system(# the carrier of b2, the Tran of b2 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) &amp; 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 (E ^omega)
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 #) &amp; the InitS of b4 = {((<%> 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 &amp; _bool SA is deterministic )
proofend;
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
proofend;

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
proofend;
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)
proofend;
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) )
proofend;

:: Automata
definition
let E be non empty set ;
let F be Subset of (E ^omega);
attrc3 is strict ;
struct automaton over F ->  semiautomaton over F;
aggrautomaton(# 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 (E ^omega);
let A be automaton over F;
attrA 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 b1 being automaton over F st
( b1 is strict &amp; not b1 is empty &amp; b1 is finite &amp; b1 is deterministic )
proofend;
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 #) &amp; 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 #) &amp; the FinalS of b1 =  {  Q where Q is Element of b1 : Q meets the FinalS of A  }  )
proofend;
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 #) &amp; the FinalS of b1 =  {  Q where Q is Element of b1 : Q meets the FinalS of A  }  &amp; 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 #) &amp; 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 (E ^omega)
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 #) &amp; 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 (E ^omega);
let A be non empty automaton over F;
cluster _bool A ->  non empty strict deterministic ;
coherence
 ( not _bool A is empty &amp; _bool A is deterministic )
proofend;
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
proofend;

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
proofend;
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)
proofend;
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 )
proofend;

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 &amp; q in the FinalS of A &amp; 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 &amp; q in the FinalS of A &amp; p,u ==>* q,A )  }  is Subset of (E ^omega)
proofend;
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 &amp; q in the FinalS of A &amp; 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 &amp; q in the FinalS of A &amp; p,w ==>* q,A ) )
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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 &amp; (R . (len R)) `2 = <%> E &amp; not (R . 2) `2 = <%e%> ^ u holds
(R . 2) `2 = u
proofend;

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 &amp; (R . (len R)) `2 = <%> E holds
len R > len u
proofend;

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 &amp; (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R &amp; (R . l) `2 = v )
proofend;

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 ) &amp; ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b1 being Element of E ^omega st b1 = u ) )
proofend;
uniqueness
 for b1, b2 being Element of E ^omega holds
( ( ex w being Element of E ^omega st w ^ v = u &amp; ( for w being Element of E ^omega st w ^ v = u holds
b1 = w ) &amp; ( for w being Element of E ^omega st w ^ v = u holds
b2 = w ) implies b1 = b2 ) &amp; ( ( for w being Element of E ^omega holds not w ^ v = u ) &amp; b1 = u &amp; b2 = u implies b1 = b2 ) )
proofend;
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 ) ) &amp; ( ( 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, w, v 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)] &amp; p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] &amp; q . (len q) = [y,v] )
proofend;

theorem Th26: :: FSM_3:26
for x, y being set
for E being non empty set
for u, w, v 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]
proofend;

theorem Th27: :: FSM_3:27
for x, y being set
for E being non empty set
for u, w, v 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
proofend;

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 &amp; r,v ==>* q,TS )
proofend;

theorem Th29: :: FSM_3:29
for X being set
for E being non empty set
for w, v 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)
proofend;

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)}
proofend;

theorem Th31: :: FSM_3:31
for X being set
for E being non empty set
for w, v 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))}
proofend;

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))}
proofend;

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 &amp; x in P holds
P in the FinalS of (_bool A)
proofend;

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
proofend;

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))}
proofend;

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))}
proofend;

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))}
proofend;

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)
proofend;

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
proofend;

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
proofend;