:: Equivalence of Epsilon, Nondeterministic [Finite] Automata and Deterministic
:: [Finite] Automata
:: by Micha{\l} Trybulec
::
:: Received May 25, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, AFINSQ_1, NAT_1, REWRITE3, XXREAL_0,
ARYTM_3, CARD_1, FINSEQ_1, ORDINAL4, RELAT_1, FUNCT_1, FLANG_1, FSM_1,
STRUCT_0, ZFMISC_1, TARSKI, FINSET_1, REWRITE2, PRELAMB, FSM_2, LANG1,
REWRITE1, MCART_1, FSM_3;
notations CARD_1, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XCMPLX_0, ORDINAL1,
DOMAIN_1, FUNCT_1, RELSET_1, XXREAL_0, FINSET_1, AFINSQ_1, SUBSET_1,
REWRITE1, FLANG_1, STRUCT_0, NUMBERS, MCART_1, FINSEQ_1, REWRITE3;
constructors NAT_1, MEMBERED, REWRITE1, FLANG_1, XREAL_0, REWRITE3, RELSET_1,
XTUPLE_0;
registrations CARD_1, NAT_1, XREAL_0, XBOOLE_0, XXREAL_0, STRUCT_0, SUBSET_1,
REWRITE1, AFINSQ_1, RELAT_1, FINSET_1, FINSEQ_1, REWRITE3, FUNCT_1,
RELSET_1, ORDINAL1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions STRUCT_0;
expansions STRUCT_0;
theorems AFINSQ_1, CARD_1, FLANG_1, FUNCT_1, NAT_1, ORDINAL1, RELAT_1,
RELSET_1, REWRITE1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, ZFMISC_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, REWRITE3, XTUPLE_0;
schemes FINSEQ_1, FRAENKEL, NAT_1, RELSET_1;
begin
reserve x, y, X for set;
reserve E for non empty set;
reserve e for Element of E;
reserve u, u1, v, v1, v2, w, w9, w1, w2 for Element of E^omega;
reserve F for Subset of E^omega;
reserve i, k, l for Nat;
reserve TS for non empty transition-system over F;
reserve S, T for Subset of TS;
:: Preliminaries - Natural Numbers
theorem Th1:
i >= k + l implies i >= k
proof
assume i >= k + l;
then i + l >= k + l + 0 by XREAL_1:7;
hence thesis by XREAL_1:6;
end;
:: Preliminaries - Sequences
theorem
for a, b being FinSequence holds a ^ b = a or b ^ a = a implies b = {}
proof
let a, b be FinSequence such that
A1: a ^ b = a or b ^ a = a;
per cases by A1;
suppose
A2: a ^ b = a;
len(a ^ b) = len(a) + len(b) by FINSEQ_1:22;
hence thesis by A2;
end;
suppose
A3: b ^ a = a;
len(b ^ a) = len(b) + len(a) by FINSEQ_1:22;
hence thesis by A3;
end;
end;
theorem Th3:
for p, q being FinSequence st k in dom p & len p + 1 = len q
holds k + 1 in dom q
proof
let p, q be FinSequence such that
A1: k in dom p and
A2: len p + 1 = len q;
k <= len p by A1,FINSEQ_3:25;
then 1 + 0 <= k + 1 & k + 1 <= len p + 1 by XREAL_1:7;
hence thesis by A2,FINSEQ_3:25;
end;
:: Preliminaries - XFinSequences and Words in E^omega
theorem Th4:
len u = 1 implies ex e st <%e%> = u & e = u.0
proof
assume len u = 1;
then len u = 0 + 1;
then consider v, e such that
A1: len v = 0 and
A2: u = v^<%e%> by FLANG_1:7;
take e;
v = <%>E by A1;
then u = {}^<%e%> by A2;
then u = <%e%>;
hence thesis;
end;
theorem Th5:
k <> 0 & len u <= k + 1 implies ex v1, v2 st len v1 <= k & len v2
<= k & u = v1^v2
proof
assume that
A1: k <> 0 and
A2: len u <= k + 1;
per cases;
suppose
len u = k + 1;
then consider v1, e such that
A3: len v1 = k and
A4: u = v1 ^ <%e%> by FLANG_1:7;
reconsider v2 = <%e%> as Element of E^omega;
take v1, v2;
thus len v1 <= k by A3;
0 + 1 <= k by A1,NAT_1:13;
hence len v2 <= k by AFINSQ_1:34;
thus u = v1^v2 by A4;
end;
suppose
A5: len u <> k + 1;
reconsider v2 = <%>E as Element of E^omega;
take u, v2;
thus len u <= k by A2,A5,NAT_1:8;
thus len v2 <= k;
thus u = u^{}
.= u^v2;
end;
end;
theorem Th6:
for p, q being XFinSequence st <%x%>^p = <%y%>^q holds x = y & p = q
proof
let p, q be XFinSequence such that
A1: <%x%>^p = <%y%>^q;
(<%x%>^p).0 = x by AFINSQ_1:35;
then x = y by A1,AFINSQ_1:35;
hence thesis by A1,AFINSQ_1:28;
end;
theorem Th7:
len u > 0 implies ex e, u1 st u = <%e%>^u1
proof
assume len u > 0;
then consider k such that
A1: len u = k + 1 by NAT_1:6;
ex u1, e st len u1 = k & u = <%e%>^u1 by A1,FLANG_1:9;
hence thesis;
end;
:: Preliminaries - Lex
registration
let E;
cluster Lex(E) -> non empty;
coherence
proof
<%e%> in Lex(E) by FLANG_1:def 4;
hence thesis;
end;
end;
theorem Th8:
not <%>E in Lex(E)
proof
assume <%>E in Lex(E);
then ex e st e in E & <%>E = <%e%> by FLANG_1:def 4;
hence contradiction;
end;
theorem Th9:
u in Lex(E) iff len u = 1
proof
thus u in Lex(E) implies len u = 1
proof
assume u in Lex(E);
then ex e st e in E & u = <%e%> by FLANG_1:def 4;
hence thesis by AFINSQ_1:def 4;
end;
assume len u = 1;
then ex e st <%e%> = u & e = u.0 by Th4;
hence thesis by FLANG_1:def 4;
end;
theorem Th10:
u <> v & u in Lex(E) & v in Lex(E) implies not ex w st u^w = v or w^u = v
proof
assume that
A1: u <> v and
A2: u in Lex(E) and
A3: v in Lex(E);
A4: len u = 1 by A2,Th9;
given w such that
A5: u^w = v or w^u = v;
A6: len v = 1 by A3,Th9;
per cases by A5;
suppose
A7: u^w = v;
len (u^w) = 1 + len w by A4,AFINSQ_1:17;
then w = <%>E by A6,A7;
hence contradiction by A1,A7;
end;
suppose
A8: w^u = v;
len (w^u) = 1 + len w by A4,AFINSQ_1:17;
then w = <%>E by A6,A8;
hence contradiction by A1,A8;
end;
end;
:: Transition Systems over Lex(E)
theorem Th11:
for TS being transition-system over Lex E
holds the Tran of TS is Function implies TS is deterministic
proof
let TS be transition-system over Lex(E) such that
A1: (the Tran of TS) is Function;
A2: now
let p be Element of TS, u, v such that
A3: u <> v and
A4: [p, u] in dom (the Tran of TS) & [p, v] in dom (the Tran of TS);
u in Lex(E) & v in Lex(E) by A4,ZFMISC_1:87;
hence not ex w st u^w = v or v^w = u by A3,Th10;
end;
not <%>E in rng dom (the Tran of TS) by Th8;
hence thesis by A1,A2,REWRITE3:def 1;
end;
:: Powerset Construction for Transition Systems
:: This is a construction that limits new transitions to single character ones.
definition
let E, F, TS;
func _bool TS -> strict transition-system over Lex(E) means
:Def1:
the
carrier of it = bool (the carrier of TS) & for S, w, T holds [[S, w], T] in the
Tran of it iff len w = 1 & T = w-succ_of (S, TS);
existence
proof
set cTS = bool (the carrier of TS);
defpred P[set, set] means for c being Element of cTS, i being Element of E
^omega st $1 = [c, i] holds len i = 1 & $2 = i-succ_of (c, TS);
consider tTS being Relation of [: cTS, Lex(E) :], cTS such that
A1: for x being Element of [: cTS, Lex(E) :], y being Element of cTS
holds [x, y] in tTS iff P[x, y] from RELSET_1:sch 2;
set bTS = transition-system(# cTS, tTS #);
reconsider bTS as strict transition-system over Lex(E);
take bTS;
thus the carrier of bTS = bool (the carrier of TS);
let S, w, T;
thus [[S, w], T] in the Tran of bTS implies len w = 1 & T = w-succ_of (S,
TS)
proof
assume
A2: [[S, w], T] in the Tran of bTS;
then reconsider xc = [S, w] as Element of [: cTS, Lex(E) :] by
ZFMISC_1:87;
[xc, T] in tTS by A2;
hence thesis by A1;
end;
set x = [S, w];
assume that
A3: len w = 1 and
A4: T = w-succ_of (S, TS);
A5: now
let xc be Element of cTS, xi be Element of E^omega such that
A6: x = [xc, xi];
xc = S by A6,XTUPLE_0:1;
hence len xi = 1 & T = xi-succ_of (xc, TS) by A3,A4,A6,XTUPLE_0:1;
end;
w in Lex(E) by A3,Th9;
then reconsider x as Element of [: cTS, Lex(E) :] by ZFMISC_1:87;
[x, T] in tTS by A1,A5;
hence thesis;
end;
uniqueness
proof
set cTS = bool (the carrier of TS);
let bTS1, bTS2 be strict transition-system over Lex(E) such that
A7: the carrier of bTS1 = cTS and
A8: for S, w, T holds [[S, w], T] in the Tran of bTS1 iff len w = 1 &
T = w-succ_of (S, TS) and
A9: the carrier of bTS2 = cTS and
A10: for S, w, T holds [[S, w], T] in the Tran of bTS2 iff len w = 1 &
T = w-succ_of (S, TS);
A11: for x being object
holds x in the Tran of bTS2 implies x in the Tran of bTS1
proof let x be object;
assume
A12: x in the Tran of bTS2;
then consider xbi, xc being object such that
A13: x = [xbi, xc] and
A14: xbi in [: cTS, Lex(E) :] and
A15: xc in cTS by A9,RELSET_1:2;
reconsider xc as Element of cTS by A15;
[: cTS, Lex(E) :] c= [:cTS, Lex(E):];
then consider xb, xi being object such that
A16: xbi = [xb, xi] and
A17: xb in cTS and
A18: xi in Lex(E) by A14,RELSET_1:2;
reconsider xb as Element of cTS by A17;
reconsider xi as Element of Lex(E) by A18;
reconsider xe = xi as Element of E^omega;
A19: len xe = 1 by Th9;
xc = xi-succ_of (xb, TS) by A10,A12,A13,A16;
hence thesis by A8,A13,A16,A19;
end;
for x being object
holds x in the Tran of bTS1 implies x in the Tran of bTS2
proof let x be object;
assume
A20: x in the Tran of bTS1;
then consider xbi, xc being object such that
A21: x = [xbi, xc] and
A22: xbi in [: cTS, Lex(E) :] and
A23: xc in cTS by A7,RELSET_1:2;
reconsider xc as Element of cTS by A23;
[: cTS, Lex(E) :] c= [:cTS, Lex(E):];
then consider xb, xi being object such that
A24: xbi = [xb, xi] and
A25: xb in cTS and
A26: xi in Lex(E) by A22,RELSET_1:2;
reconsider xb as Element of cTS by A25;
reconsider xi as Element of Lex(E) by A26;
reconsider xe = xi as Element of E^omega;
A27: len xe = 1 by Th9;
xc = xi-succ_of (xb, TS) by A8,A20,A21,A24;
hence thesis by A10,A21,A24,A27;
end;
hence thesis by A7,A9,A11,TARSKI:2;
end;
end;
registration
let E, F, TS;
cluster _bool TS -> non empty deterministic;
coherence
proof
set bTS = _bool TS;
set wTS = the carrier of bTS;
set tTS = the Tran of bTS;
for x, y1, y2 being object st [x, y1] in tTS & [x, y2] in tTS
holds y1 = y2
proof
let x, y1, y2 be object such that
A1: [x, y1] in tTS and
A2: [x, y2] in tTS;
reconsider x as Element of [: wTS, Lex(E) :] by A1,ZFMISC_1:87;
reconsider y1, y2 as Element of wTS by A1,A2,ZFMISC_1:87;
the carrier of bTS = bool (the carrier of TS) by Def1;
then consider xc, xi being object such that
A3: xc in wTS and
A4: xi in Lex(E) and
A5: x = [xc, xi] by ZFMISC_1:def 2;
reconsider xc as Element of wTS by A3;
reconsider xi as Element of Lex(E) by A4;
reconsider xi as Element of E^omega;
reconsider xc, y1, y2 as Subset of TS by Def1;
y1 = xi-succ_of (xc, TS) & y2 = xi-succ_of (xc, TS) by A1,A2,A5,Def1;
hence thesis;
end;
then
A6: the Tran of bTS is Function by FUNCT_1:def 1;
the carrier of bTS = bool (the carrier of TS) by Def1;
hence thesis by A6,Th11;
end;
end;
registration
let E, F;
let TS be finite non empty transition-system over F;
cluster _bool TS -> finite;
coherence
proof
bool the carrier of TS is finite;
hence thesis by Def1;
end;
end;
theorem Th12:
x, <%e%> ==>* y, <%>E, _bool TS implies x, <%e%> ==>. y, <%>E, _bool TS
proof
not <%>E in rng dom (the Tran of _bool TS) by REWRITE3:def 1;
hence thesis by REWRITE3:92;
end;
theorem Th13:
len w = 1 implies (X = w-succ_of (S, TS) iff S, w ==>* X, _bool TS)
proof
assume
A1: len w = 1;
thus X = w-succ_of (S, TS) implies S, w ==>* X, _bool TS
proof
assume X = w-succ_of (S, TS);
then [[S, w], X] in the Tran of _bool TS by A1,Def1;
then S, w -->. X, _bool TS by REWRITE3:def 2;
then S, w ==>. X, <%>E, _bool TS by REWRITE3:23;
then S, w ==>* X, <%>E, _bool TS by REWRITE3:87;
hence thesis by REWRITE3:def 7;
end;
assume S, w ==>* X, _bool TS;
then
A2: S, w ==>* X, <%>E, _bool TS by REWRITE3:def 7;
ex e st w = <%e%> & w.0 = e by A1,Th4;
then S, w^{} ==>. X, <%>E, _bool TS by A2,Th12;
then
A3: S, w -->. X, _bool TS by REWRITE3:24;
then X in _bool TS by REWRITE3:15;
then X in the carrier of _bool TS;
then reconsider X9 = X as Subset of TS by Def1;
[[S, w], X9] in the Tran of _bool TS by A3,REWRITE3:def 2;
hence thesis by Def1;
end;
:: Semiautomata
definition
let E, F;
struct (transition-system over F) semiautomaton over F (# carrier -> set,
Tran -> Relation of [: the carrier, F :], the carrier, InitS -> Subset of the
carrier #);
end;
definition
let E, F;
let SA be semiautomaton over F;
attr SA is deterministic means
:Def2:
(the transition-system of SA) is deterministic & card (the InitS of SA) = 1;
end;
registration
let E, F;
cluster strict non empty finite deterministic for semiautomaton over F;
existence
proof
set X = the non empty finite set;
reconsider T = {} as Relation of [: X, F :], X by RELSET_1:12;
set x = the Element of X;
reconsider I = { x } as Subset of X;
take SA = semiautomaton (# X, T, I #);
thus SA is strict;
thus SA is non empty;
thus the carrier of SA is finite;
thus (the transition-system of SA) is deterministic by RELAT_1:38
,REWRITE3:14;
thus card (the InitS of SA) = 1 by CARD_1:30;
end;
end;
reserve SA for non empty semiautomaton over F;
registration
let E, F, SA;
cluster the transition-system of SA -> non empty;
coherence;
end;
definition
let E, F, SA;
func _bool SA -> strict semiautomaton over Lex(E) means
:Def3:
the
transition-system of it = _bool the transition-system of SA & the InitS of it =
{ <%>E-succ_of (the InitS of SA, SA) };
existence
proof
reconsider TS = the transition-system of SA as non empty transition-system
over F;
set cSA = the carrier of _bool TS;
reconsider iSA = { <%>E-succ_of (the InitS of SA, SA) } as Subset of cSA
by Def1;
reconsider tSA = (the Tran of _bool TS) as Relation of [: cSA, Lex(E) :],
cSA;
set bSA = semiautomaton(# cSA, tSA, iSA #);
card iSA = 1 by CARD_1:30;
then reconsider
bSA as strict non empty deterministic semiautomaton over Lex(E)
by Def2;
take bSA;
thus thesis;
end;
uniqueness;
end;
registration
let E, F, SA;
cluster _bool SA -> non empty deterministic;
coherence
proof
set TS = _bool SA;
the InitS of TS = { <%>E-succ_of (the InitS of SA, SA) } by Def3;
then
A1: card the InitS of TS = 1 by CARD_1:30;
the transition-system of TS = _bool the transition-system of SA by Def3;
hence thesis by A1;
end;
end;
theorem Th14:
the carrier of _bool SA = bool the carrier of SA
proof
the transition-system of _bool SA = _bool the transition-system of SA by Def3
;
hence thesis by Def1;
end;
registration
let E, F;
let SA be finite non empty semiautomaton over F;
cluster _bool SA -> finite;
coherence
proof
bool the carrier of SA is finite;
hence thesis by Th14;
end;
end;
:: Left-languages
definition
let E, F, SA;
let Q be Subset of SA;
func left-Lang(Q) -> Subset of E^omega equals
{ w : Q meets w-succ_of (the
InitS of SA, SA) };
coherence
proof
defpred P[Element of E^omega] means Q meets $1-succ_of (the InitS of SA,
SA);
{ w : P[w] } c= E^omega from FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem Th15:
for Q being Subset of SA holds w in left-Lang(Q) iff Q meets w
-succ_of (the InitS of SA, SA)
proof
let Q be Subset of SA;
thus w in left-Lang(Q) implies Q meets w-succ_of (the InitS of SA, SA)
proof
assume w in left-Lang(Q);
then ex w9 st w9 = w & Q meets w9-succ_of (the InitS of SA, SA);
hence thesis;
end;
thus thesis;
end;
:: Automata
definition
let E, F;
struct (semiautomaton over F) automaton over F (# carrier -> set, Tran ->
Relation of [: the carrier, F :], the carrier, InitS -> Subset of the carrier,
FinalS -> Subset of the carrier #);
end;
definition
let E, F;
let A be automaton over F;
attr A is deterministic means
:Def5:
(the semiautomaton of A) is deterministic;
end;
registration
let E, F;
cluster strict non empty finite deterministic for automaton over F;
existence
proof
set X = the non empty finite set;
reconsider T = {} as Relation of [: X, F :], X by RELSET_1:12;
set x = the Element of X;
reconsider I = { x } as Subset of X;
take A = automaton (# X, T, I, I #);
thus A is strict;
thus A is non empty;
thus the carrier of A is finite;
(the transition-system of A) is deterministic & card (the InitS of A)
= 1 by CARD_1:30,RELAT_1:38,REWRITE3:14;
then the semiautomaton of A is deterministic;
hence A is deterministic;
end;
end;
reserve A for non empty automaton over F;
reserve p, q for Element of A;
registration
let E, F, A;
cluster the transition-system of A -> non empty;
coherence;
cluster the semiautomaton of A -> non empty;
coherence;
end;
definition
let E, F, A;
func _bool A -> strict automaton over Lex(E) means
:Def6:
the semiautomaton
of it = _bool the semiautomaton of A & the FinalS of it = { Q where Q is
Element of it : Q meets (the FinalS of A) };
existence
proof
reconsider SA = the semiautomaton of A as non empty semiautomaton over F;
set cA = the carrier of _bool SA;
reconsider tA = (the Tran of _bool SA) as Relation of [: cA, Lex(E) :], cA;
set iA = the InitS of _bool SA;
{ Q where Q is Element of _bool SA : Q meets (the FinalS of A) } is
Subset of cA
proof
defpred P[set] means $1 meets (the FinalS of A);
{ Q where Q is Element of _bool SA : P[Q] } c= the
carrier of _bool SA from FRAENKEL:sch 10;
hence thesis;
end;
then reconsider
fA = { Q where Q is Element of _bool SA : Q meets (the FinalS
of A) } as Subset of cA;
set bA = automaton(# cA, tA, iA, fA #);
reconsider bA as strict non empty deterministic automaton over Lex(E) by
Def5;
take bA;
thus thesis;
end;
uniqueness;
end;
registration
let E, F, A;
cluster _bool A -> non empty deterministic;
coherence
proof
set XX = _bool A;
the semiautomaton of XX = _bool the semiautomaton of A by Def6;
hence thesis;
end;
end;
theorem Th16:
the carrier of _bool A = bool the carrier of A
proof
the semiautomaton of _bool A = _bool the semiautomaton of A by Def6;
hence thesis by Th14;
end;
registration
let E, F;
let A be finite non empty automaton over F;
cluster _bool A -> finite;
coherence
proof
bool the carrier of A is finite;
hence thesis by Th16;
end;
end;
:: Languages Accepted by Automata
definition
let E, F, A;
let Q be Subset of A;
func right-Lang(Q) -> Subset of E^omega equals
{ w : w-succ_of (Q, A) meets
(the FinalS of A) };
coherence
proof
defpred P[Element of E^omega] means $1-succ_of (Q, A) meets (the FinalS of
A);
{ w : P[w] } c= E^omega from FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem Th17:
for Q being Subset of A holds w in right-Lang(Q) iff w-succ_of (
Q, A) meets (the FinalS of A)
proof
let Q be Subset of A;
thus w in right-Lang(Q) implies w-succ_of (Q, A) meets (the FinalS of A)
proof
assume w in right-Lang(Q);
then ex w9 st w = w9 & w9-succ_of (Q, A) meets (the FinalS of A);
hence thesis;
end;
thus thesis;
end;
definition
let E, F, A;
func Lang(A) -> Subset of E^omega equals
{ u : ex p, q st p in the InitS of
A & q in the FinalS of A & p, u ==>* q, A };
coherence
proof
defpred P[Element of E^omega] means ex p, q st p in the InitS of A & q in
the FinalS of A & p, $1 ==>* q, A;
{ w : P[w] } c= E^omega from FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem Th18:
w in Lang(A) iff ex p, q st p in the InitS of A & q in the
FinalS of A & p, w ==>* q, A
proof
thus w in Lang(A) implies ex p, q st p in the InitS of A & q in the FinalS
of A & p, w ==>* q, A
proof
assume w in Lang(A);
then
ex u st w = u & ex p, q st p in the InitS of A & q in the FinalS of A
& p, u ==>* q, A;
hence thesis;
end;
thus thesis;
end;
theorem Th19:
w in Lang(A) iff w-succ_of (the InitS of A, A) meets (the FinalS of A)
proof
thus w in Lang(A) implies w-succ_of (the InitS of A, A) meets (the FinalS of
A)
proof
assume w in Lang(A);
then consider p, q such that
A1: p in the InitS of A and
A2: q in the FinalS of A and
A3: p, w ==>* q, A by Th18;
q in w-succ_of (the InitS of A, A) by A1,A3,REWRITE3:103;
hence thesis by A2,XBOOLE_0:3;
end;
assume w-succ_of (the InitS of A, A) meets (the FinalS of A);
then consider x being object such that
A4: x in w-succ_of (the InitS of A, A) and
A5: x in (the FinalS of A) by XBOOLE_0:3;
reconsider x as Element of A by A4;
ex p st p in the InitS of A & p, w ==>* x, A by A4,REWRITE3:103;
hence thesis by A5;
end;
theorem
Lang(A) = left-Lang(the FinalS of A)
proof
A1: w in Lang(A) implies w in left-Lang(the FinalS of A)
proof
assume w in Lang(A);
then w-succ_of (the InitS of A, A) meets (the FinalS of A) by Th19;
hence thesis;
end;
w in left-Lang(the FinalS of A) implies w in Lang(A)
proof
assume w in left-Lang(the FinalS of A);
then the FinalS of A meets w-succ_of (the InitS of A, A) by Th15;
hence thesis by Th19;
end;
hence thesis by A1,SUBSET_1:3;
end;
theorem
Lang(A) = right-Lang(the InitS of A)
proof
A1: w in Lang(A) implies w in right-Lang(the InitS of A)
proof
assume w in Lang(A);
then w-succ_of (the InitS of A, A) meets (the FinalS of A) by Th19;
hence thesis;
end;
w in right-Lang(the InitS of A) implies w in Lang(A)
proof
assume w in right-Lang(the InitS of A);
then w-succ_of (the InitS of A, A) meets (the FinalS of A) by Th17;
hence thesis by Th19;
end;
hence thesis by A1,SUBSET_1:3;
end;
:: Equivalence (with respect to the accepted languages)
:: of nondeterministic [finite] automata and deterministic [finite] automata.
reserve TS for non empty transition-system over Lex(E) \/ {<%>E};
theorem Th22:
for R being RedSequence of ==>.-relation(TS) st (R.1)`2 = <%e%>^
u & (R.len R)`2 = <%>E holds (R.2)`2 = <%e%>^u or (R.2)`2 = u
proof
let R be RedSequence of ==>.-relation(TS) such that
A1: (R.1)`2 = <%e%>^u and
A2: (R.len R)`2 = <%>E;
(R.1)`2 <> (R.len R)`2 by A1,A2,AFINSQ_1:30;
then len R >= 1 + 1 by NAT_1:8,25;
then rng R <> {} & 1 + 1 in dom R by FINSEQ_3:25;
then
A3: [R.1, R.2] in ==>.-relation(TS) by FINSEQ_3:32,REWRITE1:def 2;
then consider
p being Element of TS, v being Element of E^omega, q being Element
of TS, w such that
A4: R.1 = [p, v] and
A5: R.2 = [q, w] by REWRITE3:31;
p, v ==>. q, w, TS by A3,A4,A5,REWRITE3:def 4;
then consider u1 such that
A6: p, u1 -->. q, TS and
A7: v = u1^w by REWRITE3:22;
A8: u1 in Lex(E) \/ {<%>E} by A6,REWRITE3:15;
per cases by A8,XBOOLE_0:def 3;
suppose
u1 in Lex(E);
then len u1 = 1 by Th9;
then consider f being Element of E such that
A9: u1 = <%f%> and
u1.0 = f by Th4;
(R.1)`2 = <%f%>^w by A4,A7,A9;
then u = w by A1,Th6;
hence thesis by A5;
end;
suppose
u1 in {<%>E};
then
A10: u1 = <%>E by TARSKI:def 1;
v = (R.1)`2 & w = (R.2)`2 by A4,A5;
hence thesis by A1,A7,A10;
end;
end;
theorem Th23:
for R being RedSequence of ==>.-relation(TS) st (R.1)`2 = u & (R
.len R)`2 = <%>E holds len R > len u
proof
defpred P[Nat] means for R being RedSequence of ==>.-relation(TS), u st len
R = $1 & (R.1)`2 = u & (R.len R)`2 = <%>E holds len R > len u;
A1: now
let k;
assume
A2: P[k];
now
let R be RedSequence of ==>.-relation(TS), u such that
A3: len R = k + 1 and
A4: (R.1)`2 = u and
A5: (R.len R)`2 = <%>E;
per cases;
suppose
len u = 0;
hence len R > len u;
end;
suppose
A6: len u > 0;
then consider e, u1 such that
A7: u = <%e%>^u1 by Th7;
len R <> 1 by A4,A5,A6;
then consider R9 being RedSequence of ==>.-relation(TS) such that
A8: <*R.1*>^R9 = R and
A9: len R9 + 1 = len R by NAT_1:25,REWRITE3:5;
A10: len R9 + 0 < k + 1 by A3,A9,XREAL_1:6;
A11: len R9 >= 0 + 1 by NAT_1:8;
then len R9 in dom R9 by FINSEQ_3:25;
then
A12: (R9.len R9)`2 = <%>E by A5,A8,A9,FINSEQ_3:103;
1 in dom R9 by A11,FINSEQ_3:25;
then
A13: (<*R.1*>^R9).(1 + 1) = R9.1 by FINSEQ_3:103;
per cases by A4,A5,A7,Th22;
suppose
(R.2)`2 = <%e%>^u1;
hence len R > len u by A2,A3,A7,A8,A9,A10,A13,A12,XXREAL_0:2;
end;
suppose
(R.2)`2 = u1;
then len R9 > len u1 by A2,A3,A8,A9,A13,A12;
then len R > 1 + len u1 by A9,XREAL_1:6;
then len R > len <%e%> + len u1 by AFINSQ_1:def 4;
hence len R > len u by A7,AFINSQ_1:17;
end;
end;
end;
hence P[k + 1];
end;
A14: P[0];
for k holds P[k] from NAT_1:sch 2(A14, A1);
hence thesis;
end;
theorem Th24:
for R being RedSequence of ==>.-relation(TS) st (R.1)`2 = u^v &
(R.len R)`2 = <%>E ex l st l in dom R & (R.l)`2 = v
proof
defpred P[Nat] means for R being RedSequence of ==>.-relation(TS), u st len
R = $1 & (R.1)`2 = u^v & (R.len R)`2 = <%>E ex l st l in dom R & (R.l)`2 = v;
A1: now
let i;
assume
A2: P[i];
thus P[i + 1]
proof
let R be RedSequence of ==>.-relation(TS), u such that
A3: len R = i + 1 and
A4: (R.1)`2 = u^v and
A5: (R.len R)`2 = <%>E;
per cases;
suppose
A6: len u = 0;
set j = 1;
take j;
rng R <> {};
hence j in dom R by FINSEQ_3:32;
u = {} by A6;
hence (R.j)`2 = v by A4;
end;
suppose
A7: len u > 0;
then consider e, u1 such that
A8: u = <%e%>^u1 by Th7;
len u >= 0 + 1 by A7,NAT_1:13;
then len u + len v >= 1 + len v by XREAL_1:6;
then len(u^v) >= 1 + len v by AFINSQ_1:17;
then len(u^v) >= 1 by Th1;
then len R + len(u^v) > len(u^v) + 1 by A4,A5,Th23,XREAL_1:8;
then len R > 1 by XREAL_1:6;
then consider R9 being RedSequence of ==>.-relation(TS) such that
A9: len R9 + 1 = len R and
A10: for k st k in dom R9 holds R9.k = R.(k + 1) by REWRITE3:7;
A11: rng R9 <> {};
then
A12: (R9.1)`2 = (R.(1 + 1))`2 by A10,FINSEQ_3:32;
1 in dom R9 by A11,FINSEQ_3:32;
then 1 <= len R9 by FINSEQ_3:25;
then len R9 in dom R9 by FINSEQ_3:25;
then
A13: (R9.len R9)`2 = <%>E by A5,A9,A10;
A14: (R.1)`2 = <%e%>^(u1^v) by A4,A8,AFINSQ_1:27;
thus ex k st k in dom R & (R.k)`2 = v
proof
per cases by A4,A5,A14,Th22;
suppose
(R.2)`2 = u^v;
then consider l such that
A15: l in dom R9 and
A16: (R9.l)`2 = v by A2,A3,A9,A12,A13;
set k = l + 1;
take k;
thus k in dom R by A9,A15,Th3;
thus (R.k)`2 = v by A10,A15,A16;
end;
suppose
(R.2)`2 = u1^v;
then consider l such that
A17: l in dom R9 and
A18: (R9.l)`2 = v by A2,A3,A9,A12,A13;
set k = l + 1;
take k;
thus k in dom R by A9,A17,Th3;
thus (R.k)`2 = v by A10,A17,A18;
end;
end;
end;
end;
end;
A19: P[0];
for k holds P[k] from NAT_1:sch 2(A19, A1);
hence thesis;
end;
definition
let E, u, v;
func chop(u, v) -> Element of E^omega means
:Def9:
for w st w^v = u holds it = w if ex w st w^v = u otherwise it = u;
existence
proof
thus (ex w st w^v = u) implies ex w1 st for w st w^v = u holds w1 = w
proof
given w1 such that
A1: w1^v = u;
take w1;
let w;
assume w^v = u;
hence w1 = w by A1,AFINSQ_1:28;
end;
thus thesis;
end;
uniqueness
proof
let w1, w2;
hereby
given w such that
A2: w^v = u;
assume that
A3: for w st w^v = u holds w1 = w and
A4: for w st w^v = u holds w2 = w;
w1 = w by A2,A3;
hence w1 = w2 by A2,A4;
end;
thus thesis;
end;
consistency;
end;
theorem Th25:
for p being RedSequence of ==>.-relation(TS) st p.1 = [x, u^w] &
p.len p = [y, v^w] ex q being RedSequence of ==>.-relation(TS) st q.1 = [x, u]
& q.len q = [y, v]
proof
let p be RedSequence of ==>.-relation(TS) such that
A1: p.1 = [x, u^w] and
A2: p.len p = [y, v^w];
A3: len p >= 0 + 1 by NAT_1:13;
then 1 in dom p by FINSEQ_3:25;
then
A4: dim2(p.1, E) = (p.1)`2 by A1,REWRITE3:51
.= u^w by A1;
deffunc F(set) = [(p.$1)`1, chop(dim2(p.$1, E), w)];
consider q being FinSequence such that
A5: len q = len p and
A6: for k st k in dom q holds q.k = F(k) from FINSEQ_1:sch 2;
A7: for k being Nat st k in dom q & k + 1 in dom q holds [q.k, q.
(k + 1)] in ==>.-relation(TS)
proof
let k be Nat such that
A8: k in dom q and
A9: k + 1 in dom q;
1 <= k & k <= len q by A8,FINSEQ_3:25;
then
A10: k in dom p by A5,FINSEQ_3:25;
then consider v1 such that
A11: (p.k)`2 = v1^(v^w) by A2,REWRITE3:52;
1 <= k + 1 & k + 1 <= len q by A9,FINSEQ_3:25;
then
A12: k + 1 in dom p by A5,FINSEQ_3:25;
then consider v2 such that
A13: (p.(k + 1))`2 = v2^(v^w) by A2,REWRITE3:52;
A14: [p.k, p.(k + 1)] in ==>.-relation(TS) by A10,A12,REWRITE1:def 2;
then
[p.k, [(p.(k + 1))`1, v2^(v^w)]] in ==>.-relation(TS) by A10,A12,A13,
REWRITE3:48;
then
[[(p.k)`1, v1^(v^w)], [(p.(k + 1))`1, v2^(v^w)]] in ==>.-relation(TS)
by A10,A12,A11,REWRITE3:48;
then (p.k)`1, v1^(v^w) ==>. (p.(k + 1))`1, v2^(v^w), TS by REWRITE3:def 4;
then consider u1 such that
A15: (p.k)`1, u1 -->. (p.(k + 1))`1, TS and
A16: v1^(v^w) = u1^(v2^(v^w)) by REWRITE3:22;
A17: ex r1 being Element of TS, w1 being Element of E^omega, r2 being
Element of TS, w2 st p.k = [r1, w1] & p.(k + 1) = [r2, w2] by A14,REWRITE3:31;
then dim2(p.(k + 1), E) = v2^(v^w) by A13,REWRITE3:def 5;
then
A18: q.(k + 1) = [(p.(k + 1))`1, chop(v2^(v^w), w)] by A6,A9
.= [(p.(k + 1))`1, chop(v2^v^w, w)] by AFINSQ_1:27
.= [(p.(k + 1))`1, v2^v] by Def9;
v1^v^w = u1^(v2^(v^w)) by A16,AFINSQ_1:27
.= u1^v2^(v^w) by AFINSQ_1:27
.= u1^v2^v^w by AFINSQ_1:27;
then v1^v = u1^v2^v by AFINSQ_1:28
.= u1^(v2^v) by AFINSQ_1:27;
then
A19: (p.k)`1, v1^v ==>. (p.(k + 1))`1, v2^v, TS by A15,REWRITE3:def 3;
dim2(p.k, E) = v1^(v^w) by A11,A17,REWRITE3:def 5;
then q.k = [(p.k)`1, chop(v1^(v^w), w)] by A6,A8
.= [(p.k)`1, chop(v1^v^w, w)] by AFINSQ_1:27
.= [(p.k)`1, v1^v] by Def9;
hence thesis by A19,A18,REWRITE3:def 4;
end;
len p in dom p by A3,FINSEQ_3:25;
then
A20: dim2(p.len p, E) = (p.len p)`2 by A1,REWRITE3:51
.= v^w by A2;
reconsider q as RedSequence of ==>.-relation(TS) by A5,A7,REWRITE1:def 2;
1 in dom q by A5,A3,FINSEQ_3:25;
then
A21: q.1 = [(p.1)`1, chop(dim2(p.1, E), w)] by A6
.= [x, chop(u^w, w)] by A1,A4
.= [x, u] by Def9;
len p in dom q by A5,A3,FINSEQ_3:25;
then q.len q = [(p.len p)`1, chop(dim2(p.len p, E), w)] by A5,A6
.= [y, chop(v^w, w)] by A2,A20
.= [y, v] by Def9;
hence thesis by A21;
end;
theorem Th26:
==>.-relation(TS) reduces [x, u^w], [y, v^w] implies
==>.-relation(TS) reduces [x, u], [y, v]
proof
assume ==>.-relation(TS) reduces [x, u^w], [y, v^w];
then
ex p being RedSequence of ==>.-relation(TS) st p.1 = [x, u ^w] & p.len p
= [y, v^w] by REWRITE1:def 3;
then
ex q being RedSequence of ==>.-relation(TS) st q.1 = [x, u ] & q.len q =
[y, v] by Th25;
hence thesis by REWRITE1:def 3;
end;
theorem Th27:
x, u^w ==>* y, v^w, TS implies x, u ==>* y, v, TS
proof
assume x, u^w ==>* y, v^w, TS;
then ==>.-relation(TS) reduces [x, u^w], [y, v^w] by REWRITE3:def 6;
then ==>.-relation(TS) reduces [x, u], [y, v] by Th26;
hence thesis by REWRITE3:def 6;
end;
theorem Th28:
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
let p, q be Element of TS;
assume
A1: p, u^v ==>* q, TS;
then p, u^v ==>* q, <%>E, TS by REWRITE3:def 7;
then ==>.-relation(TS) reduces [p, u^v], [q, <%>E] by REWRITE3:def 6;
then consider R being RedSequence of ==>.-relation(TS) such that
A2: R.1 = [p, u^v] and
A3: R.len R = [q, <%>E] by REWRITE1:def 3;
A4: (R.len R)`2 = <%>E by A3;
(R.1)`2 = u^v by A2;
then consider l such that
A5: l in dom R and
A6: (R.l)`2 = v by A4,Th24;
per cases;
suppose
A7: l + 1 in dom R;
then (R.l)`1 in TS by A5,REWRITE3:49;
then reconsider r = (R.l)`1 as Element of TS;
A8: R.l = [r, v] by A5,A6,A7,REWRITE3:48;
A9: l <= len R by A5,FINSEQ_3:25;
take r;
A10: 1 in dom R & 1 <= l by A5,FINSEQ_3:25,FINSEQ_5:6;
reconsider l as Element of NAT by ORDINAL1:def 12;
==>.-relation(TS) reduces R.1, R.l by A5,A10,REWRITE1:17;
then p, u^v ==>* r, {}^v, TS by A2,A8,REWRITE3:def 6;
then p, u ==>* r, <%>E, TS by Th27;
hence p, u ==>* r, TS by REWRITE3:def 7;
0 + 1 <= len R by NAT_1:13;
then len R in dom R by FINSEQ_3:25;
then ==>.-relation(TS) reduces R.l, R.len R by A5,A9,REWRITE1:17;
then r, v ==>* q, <%>E, TS by A3,A8,REWRITE3:def 6;
hence r, v ==>* q, TS by REWRITE3:def 7;
end;
suppose
not l + 1 in dom R;
then
A11: v = <%>E by A4,A5,A6,REWRITE3:3;
thus thesis by A1,A11,REWRITE3:95;
end;
end;
theorem Th29:
w^v-succ_of (X, TS) = v-succ_of (w-succ_of (X, TS), TS)
proof
A1: now
let x be object;
assume
A2: x in v-succ_of (w-succ_of (X, TS), TS);
then reconsider r = x as Element of TS;
consider p being Element of TS such that
A3: p in w-succ_of (X, TS) and
A4: p, v ==>* r, TS by A2,REWRITE3:103;
consider q being Element of TS such that
A5: q in X and
A6: q, w ==>* p, TS by A3,REWRITE3:103;
q, w^v ==>* r, TS by A4,A6,REWRITE3:99;
hence x in w^v-succ_of (X, TS) by A5,REWRITE3:103;
end;
now
let x be object;
assume
A7: x in w^v-succ_of (X, TS);
then reconsider r = x as Element of TS;
consider q being Element of TS such that
A8: q in X and
A9: q, w^v ==>* r, TS by A7,REWRITE3:103;
consider p being Element of TS such that
A10: q, w ==>* p, TS and
A11: p, v ==>* r, TS by A9,Th28;
p in w-succ_of (X, TS) by A8,A10,REWRITE3:103;
hence x in v-succ_of (w-succ_of (X, TS), TS) by A11,REWRITE3:103;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th30:
_bool TS is non empty transition-system over Lex(E) \/ {<%>E}
proof
Lex(E) c= Lex(E) \/ {<%>E} by XBOOLE_1:7;
then dom the Tran of _bool TS c= [: the carrier of _bool TS, Lex(E) :] & [:
the carrier of _bool TS, Lex(E) :] c= [: the carrier of _bool TS, Lex(E) \/ {
<%>E} :] by ZFMISC_1:95;
hence thesis by RELSET_1:5,XBOOLE_1:1;
end;
theorem Th31:
w-succ_of ({ v-succ_of (X, TS) }, _bool TS) = { v^w-succ_of (X, TS) }
proof
defpred P[Nat] means len u <= $1 implies for v holds u-succ_of({ v-succ_of (
X, TS) }, _bool TS) = { v^u-succ_of (X, TS) };
A1: not <%>E in rng dom (the Tran of _bool TS) by Th8;
A2: P[0]
proof
let u;
assume len u <= 0;
then
A3: u = <%>E;
let v;
reconsider vso = { v-succ_of (X, TS) } as Subset of _bool TS by Def1;
u-succ_of (vso, _bool TS) = vso by A1,A3,REWRITE3:104;
hence u-succ_of({ v-succ_of ( X, TS) }, _bool TS)
= { v^{}-succ_of (X, TS) }
.= { v^{}-succ_of (X, TS) }
.= { v^u-succ_of (X, TS) } by A3;
end;
A4: now
let k;
assume
A5: P[k];
now
let u;
assume
A6: len u <= k + 1;
let v;
per cases;
suppose
A7: k = 0;
per cases by A6,A7,NAT_1:25;
suppose
len u = 0;
hence
u-succ_of ({ v-succ_of (X, TS) }, _bool TS) = { v^u-succ_of (X,
TS) } by A2;
end;
suppose
A8: len u = 1;
A9: now
let x be object;
assume
A10: x in { v^u-succ_of (X, TS) };
then reconsider P = x as Element of _bool TS by Def1;
x = v^u-succ_of (X, TS) by A10,TARSKI:def 1;
then x = u-succ_of (v-succ_of (X, TS), TS) by Th29;
then
A11: v-succ_of (X, TS), u ==>* x, _bool TS by A8,Th13;
v-succ_of (X, TS) is Element of _bool TS & v-succ_of (X, TS)
in { v-succ_of (X, TS) } by Def1,TARSKI:def 1;
then P in u-succ_of ( { v-succ_of (X, TS) }, _bool TS) by A11,
REWRITE3:103;
hence x in u-succ_of ( { v-succ_of (X, TS) }, _bool TS);
end;
now
let x be object;
assume
A12: x in u-succ_of ({ v-succ_of (X, TS) }, _bool TS);
then reconsider P = x as Element of _bool TS;
consider Q being Element of _bool TS such that
A13: Q in { v-succ_of (X, TS) } & Q, u ==>* P, _bool TS by A12,
REWRITE3:103;
Q = v-succ_of (X, TS) & P = u-succ_of (Q, TS) by A8,A13,Th13,
TARSKI:def 1;
then P = v^u-succ_of (X, TS) by Th29;
hence x in { v^u-succ_of (X, TS) } by TARSKI:def 1;
end;
hence
u-succ_of ({ v-succ_of (X, TS) }, _bool TS) = { v^u-succ_of (X,
TS) } by A9,TARSKI:2;
end;
end;
suppose
A14: k <> 0;
reconsider bTS = _bool TS as non empty transition-system over Lex(E)
\/ {<%>E} by Th30;
consider v1, v2 such that
A15: len v1 <= k and
A16: len v2 <= k and
A17: u = v1^v2 by A6,A14,Th5;
A18: v1-succ_of({ v-succ_of(X, TS) }, _bool TS) = { v^v1-succ_of (X,
TS) } by A5,A15;
A19: the Tran of bTS = the Tran of _bool TS;
then
v1^v2-succ_of ({ v-succ_of (X, TS) }, _bool TS) = v1^v2-succ_of (
{ v-succ_of (X, TS) }, bTS) by REWRITE3:105
.= v2-succ_of (v1-succ_of ({ v-succ_of (X, TS) }, bTS), bTS) by Th29
.= v2-succ_of (v1-succ_of ({ v-succ_of (X, TS) }, _bool TS), bTS)
by A19,REWRITE3:105
.= v2-succ_of(v1-succ_of({ v-succ_of (X, TS) }, _bool TS), _bool
TS) by A19,REWRITE3:105
.= { v^v1^v2-succ_of (X, TS) } by A5,A16,A18
.= { v^(v1^v2)-succ_of (X, TS) } by AFINSQ_1:27;
hence u-succ_of ({ v-succ_of (X, TS) }, _bool TS) = { v^u-succ_of (X,
TS) } by A17;
end;
end;
hence P[k + 1];
end;
for k holds P[k] from NAT_1:sch 2(A2, A4);
then len w <= len w implies w-succ_of ({ v-succ_of (X, TS) }, _bool TS) = {
v^w-succ_of (X, TS) };
hence thesis;
end;
reserve SA for non empty semiautomaton over Lex(E) \/ {<%>E};
theorem Th32:
w-succ_of ({ <%>E-succ_of (X, SA) }, _bool SA) = { w-succ_of (X, SA) }
proof
set TS = the transition-system of SA;
set Es = <%>E-succ_of (X, SA);
the transition-system of _bool SA = _bool TS by Def3;
hence w-succ_of ({ Es }, _bool SA) = w-succ_of ({ Es }, _bool TS) by
REWRITE3:105
.= w-succ_of ({ <%>E-succ_of (X, TS) }, _bool TS) by REWRITE3:105
.= { {}^w-succ_of (X, TS) } by Th31
.= { w-succ_of (X, TS) }
.= { w-succ_of (X, SA) } by REWRITE3:105;
end;
reserve A for non empty automaton over Lex(E) \/ {<%>E};
reserve P for Subset of A;
theorem Th33:
x in the FinalS of A & x in P implies P in the FinalS of _bool A
proof
assume x in the FinalS of A & x in P;
then
A1: P meets the FinalS of A by XBOOLE_0:3;
P is Element of _bool A by Th16;
then
P in { Q where Q is Element of _bool A : Q meets (the FinalS of A) } by A1;
hence thesis by Def6;
end;
theorem Th34:
X in the FinalS of _bool A implies X meets the FinalS of A
proof
assume
A1: X in the FinalS of _bool A;
the FinalS of _bool A = { Q where Q is Element of _bool A : Q meets (the
FinalS of A) } by Def6;
then
ex Q being Element of _bool A st X = Q & Q meets (the FinalS of A) by A1;
hence thesis;
end;
theorem Th35:
the InitS of _bool A = { <%>E-succ_of (the InitS of A, A) }
proof
the InitS of _bool A = the InitS of the semiautomaton of _bool A
.= the InitS of _bool the semiautomaton of A by Def6
.= { <%>E-succ_of (the InitS of the semiautomaton of A, the
semiautomaton of A) } by Def3;
hence thesis by REWRITE3:105;
end;
theorem Th36:
w-succ_of ({ <%>E-succ_of (X, A) }, _bool A) = { w-succ_of (X, A ) }
proof
set SA = the semiautomaton of A;
set Es = <%>E-succ_of (X, A);
the semiautomaton of _bool A = _bool SA by Def6;
hence w-succ_of ({ Es }, _bool A) = w-succ_of ({ Es }, _bool SA) by
REWRITE3:105
.= w-succ_of ({ <%>E-succ_of (X, SA) }, _bool SA) by REWRITE3:105
.= { w-succ_of (X, SA) } by Th32
.= { w-succ_of (X, A) } by REWRITE3:105;
end;
theorem Th37:
w-succ_of (the InitS of _bool A, _bool A) = { w-succ_of (the InitS of A, A) }
proof
set Es = <%>E-succ_of (the InitS of A, A);
the InitS of _bool A = { Es } by Th35;
hence thesis by Th36;
end;
theorem Th38:
Lang(A) = Lang(_bool A)
proof
set DA = _bool A;
A1: w in Lang(A) implies w in Lang(DA)
proof
assume w in Lang(A);
then w-succ_of (the InitS of A, A) meets the FinalS of A by Th19;
then ex x being object
st x in w-succ_of (the InitS of A, A) & x in the FinalS of A by
XBOOLE_0:3;
then
A2: w-succ_of (the InitS of A, A) in the FinalS of DA by Th33;
w-succ_of (the InitS of DA, DA) = { w-succ_of (the InitS of A, A) } by Th37
;
then w-succ_of (the InitS of A, A) in w-succ_of (the InitS of DA, DA) by
TARSKI:def 1;
then w-succ_of (the InitS of DA, DA) meets the FinalS of DA by A2,
XBOOLE_0:3;
hence thesis by Th19;
end;
w in Lang(DA) implies w in Lang(A)
proof
assume w in Lang(DA);
then w-succ_of (the InitS of DA, DA) meets the FinalS of DA by Th19;
then consider x being object such that
A3: x in w-succ_of (the InitS of DA, DA) and
A4: x in the FinalS of DA by XBOOLE_0:3;
w-succ_of (the InitS of _bool A, _bool A) = { w-succ_of (the InitS of
A, A) } by Th37;
then x = w-succ_of (the InitS of A, A) by A3,TARSKI:def 1;
then w-succ_of (the InitS of A, A) meets the FinalS of A by A4,Th34;
hence thesis by Th19;
end;
hence thesis by A1,SUBSET_1:3;
end;
theorem
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
let A be non empty automaton over Lex(E) \/ {<%>E};
set DA = _bool A;
take DA;
thus thesis by Th38;
end;
theorem
for FA being non empty finite automaton over Lex(E) \/ {<%>E} ex DFA
being non empty deterministic finite automaton over Lex(E) st Lang(FA) = Lang(
DFA)
proof
let FA be non empty finite automaton over Lex(E) \/ {<%>E};
set bNFA = _bool FA;
Lang(FA) = Lang(bNFA) by Th38;
hence thesis;
end;