:: Equivalence of Epsilon, Nondeterministic [Finite] Automata and Deterministic
:: [Finite] Automata
:: by Micha{\l} Trybulec
::
:: Received May 25, 2009
:: Copyright (c) 2009 Association of Mizar Users
environ
vocabularies BOOLE, FUNCT_1, FINSEQ_1, RELAT_1, ALGSEQ_1, AFINSQ_1, LANG1,
FSM_1, FSM_2, FINSET_1, PRELAMB, REWRITE1, REWRITE2, FLANG_1, CARD_1,
ARYTM, MCART_1, REWRITE3, FSM_3;
notations REWRITE2, CARD_1, TARSKI, XBOOLE_0, ZFMISC_1, XCMPLX_0, NAT_1,
DOMAIN_1, FUNCT_1, RELSET_1, FUNCT_2, XXREAL_0, FINSET_1, RELAT_1,
CARD_FIN, AFINSQ_1, SUBSET_1, REWRITE1, CATALAN2, FLANG_1, STRUCT_0,
NUMBERS, ORDINAL1, XREAL_0, REAL_1, MCART_1, FINSEQ_1, REWRITE3;
constructors CARD_1, XXREAL_0, NAT_1, FSM_1, MEMBERED, CARD_FIN, SUBSET_1,
REWRITE2, REWRITE1, RELAT_1, FUNCT_1, FLANG_1, NUMBERS, XCMPLX_0,
XREAL_0, WELLORD2, MCART_1, FINSEQ_1, REWRITE3, RELSET_1;
registrations CARD_1, RELSET_1, NAT_1, XREAL_0, XBOOLE_0, MEMBERED, XXREAL_0,
REWRITE2, STRUCT_0, SUBSET_1, REWRITE1, AFINSQ_1, RELAT_1, FUNCT_1,
ORDINAL1, NUMBERS, REAL_1, FINSET_1, FINSEQ_1, REWRITE3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, STRUCT_0;
theorems AFINSQ_1, CARD_1, FLANG_1, FUNCT_1, NAT_1, ORDINAL1, RELAT_1,
RELSET_1, REWRITE1, STRUCT_0, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1,
XREAL_1, XXREAL_0, ZFMISC_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, MCART_1,
REWRITE3;
schemes FINSEQ_1, FRAENKEL, NAT_1, RELSET_1;
begin
reserve x, x1, x2, y, y1, y2, z, z1, z2, X, X1, X2, Y, Z for set;
reserve E for non empty set;
reserve e for Element of E;
reserve u, u', u1, u2, v, v1, v2, w, w', w1, w2 for Element of E^omega;
reserve F, F1, F2 for Subset of E^omega;
reserve i, j, k, l, n for Nat;
reserve TS for non empty transition-system over F;
reserve s, s', s1, s2, t, t', t1, t2 for Element of TS;
reserve S, T for Subset of TS;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Natural Numbers
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem LmNat1:
i >= k + l implies i >= k
proof
assume i >= k + l;
then i + l >= k + l + 0 by XREAL_1:9;
hence thesis by XREAL_1:8;
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 a ^ b = a;
then len(a ^ b) = len(a) + len(b) & len(a ^ b) = len(a) by FINSEQ_1:35;
hence thesis;
end;
suppose b ^ a = a;
then len(b ^ a) = len(b) + len(a) & len(b ^ a) = len(a) by FINSEQ_1:35;
hence thesis;
end;
end;
theorem ThTS3i:
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
A: k in dom p & len p + 1 = len q;
1 <= k & k <= len p by A, FINSEQ_3:27;
then 1 + 0 <= k + 1 & k + 1 <= len p + 1 by XREAL_1:9;
hence thesis by A, FINSEQ_3:27;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - XFinSequences and Words in E^omega
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem LmXSeq10:
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
B: len v = 0 & u = v^<%e%> by FLANG_1:7;
take e;
v = <%>E by B;
then u = <%e%> by B, AFINSQ_1:32;
hence thesis by AFINSQ_1:38;
end;
theorem LmXSeq20:
k <> 0 & len u <= k + 1 implies
ex v1, v2 st len v1 <= k & len v2 <= k & u = v1^v2
proof
assume
A: k <> 0 & len u <= k + 1;
per cases;
suppose len u = k + 1;
then consider v1, e such that
B: len v1 = k & u = v1 ^ <%e%> by FLANG_1:7;
reconsider v2 = <%e%> as Element of E^omega;
take v1, v2;
thus len v1 <= k by B;
thus len v2 <= k
proof
0 + 1 <= k by A, NAT_1:13;
hence thesis by AFINSQ_1:38;
end;
thus u = v1^v2 by B;
end;
suppose
B: len u <> k + 1;
reconsider v2 = <%>E as Element of E^omega;
take u, v2;
thus len u <= k by A, B, NAT_1:8;
thus len v2 <= k;
thus u = u^v2 by AFINSQ_1:32;
end;
end;
theorem LmSeq30:
for p, q being XFinSequence st <%x%>^p = <%y%>^q holds x = y & p = q
proof
let p, q be XFinSequence such that
A: <%x%>^p = <%y%>^q;
(<%x%>^p).0 = x by AFINSQ_1:39;
then x = y by A, AFINSQ_1:39;
hence thesis by A, AFINSQ_1:31;
end;
theorem ThTS3j:
len u > 0 implies ex e, u1 st u = <%e%>^u1
proof
assume len u > 0;
then consider k such that
B: len u = k + 1 by NAT_1:6;
ex u1, e st len u1 = k & u = <%e%>^u1 by B, 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 ThLex10:
not <%>E in Lex(E)
proof
assume <%>E in Lex(E);
then consider e such that
A: e in E & <%>E = <%e%> by FLANG_1:def 4;
thus contradiction by A;
end;
theorem ThLex20:
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 consider e such that
A: e in E & u = <%e%> by FLANG_1:def 4;
thus thesis by A, AFINSQ_1:def 5;
end;
assume len u = 1;
then consider e such that
B: <%e%> = u & e = u.0 by LmXSeq10;
thus thesis by B, FLANG_1:def 4;
end;
theorem ThLex30:
u <> v & u in Lex(E) & v in Lex(E) implies
not ex w st u^w = v or w^u = v
proof
assume
A: u <> v & u in Lex(E) & v in Lex(E);
A1: len u = 1 & len v = 1 by A, ThLex20;
given w such that
B: u^w = v or w^u = v;
per cases by B;
suppose
C: u^w = v;
len (u^w) = 1 + len w by A1, AFINSQ_1:20;
then w = <%>E by A1, C;
hence contradiction by A, C, AFINSQ_1:32;
end;
suppose
C: w^u = v;
len (w^u) = 1 + len w by A1, AFINSQ_1:20;
then w = <%>E by A1, C;
hence contradiction by A, C, AFINSQ_1:32;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Transition Systems over Lex(E)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThTS10:
for TS being transition-system over Lex(E) holds
not <%>E in rng dom (the Tran of TS)
proof
let TS be transition-system over Lex(E);
dom (the Tran of TS) c= [: the carrier of TS, Lex(E) :]
by RELAT_1:def 18;
then rng dom the Tran of TS c= Lex(E) by RELAT_1:def 19;
hence thesis by ThLex10;
end;
theorem ThDet20:
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
A: (the Tran of TS) is Function;
E: dom (the Tran of TS) c= [: the carrier of TS, Lex(E) :]
by RELAT_1:def 18;
B: not <%>E in rng dom (the Tran of TS) by ThTS10;
now
let p be Element of TS, u, v such that
C1: u <> v and
C2: [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 C2, E, ZFMISC_1:106;
hence not ex w st u^w = v or v^w = u by C1, ThLex30;
end;
hence thesis by A, B, 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
:DefBool:
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
A: 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
D: [[S, w], T] in the Tran of bTS;
then reconsider xc = [S, w] as Element of [: cTS, Lex(E) :]
by ZFMISC_1:106;
[xc, T] in tTS by D;
hence thesis by A;
end;
assume
B: len w = 1 & T = w-succ_of (S, TS);
set x = [S, w];
D: now
let xc be Element of cTS,
xi be Element of E^omega such that
C: x = [xc, xi];
xc = S & xi = w by C, ZFMISC_1:33;
hence len xi = 1 & T = xi-succ_of (xc, TS) by B;
end;
w in Lex(E) by B, ThLex20;
then reconsider x as Element of [: cTS, Lex(E) :] by ZFMISC_1:106;
[x, T] in tTS by A, D;
hence thesis;
end;
uniqueness
proof
set cTS = bool (the carrier of TS);
let bTS1, bTS2 be strict transition-system over Lex(E) such that
A1: the carrier of bTS1 = cTS &
for S, w, T holds
[[S, w], T] in the Tran of bTS1 iff len w = 1 & T = w-succ_of (S, TS)
and
A2: the carrier of bTS2 = cTS &
for S, w, T holds
[[S, w], T] in the Tran of bTS2 iff len w = 1 & T = w-succ_of (S, TS);
C: x in the Tran of bTS1 implies x in the Tran of bTS2
proof
assume
D: x in the Tran of bTS1;
consider xbi, xc being set such that
E: x = [xbi, xc] & xbi in [: cTS, Lex(E) :] & xc in cTS
by A1, D, RELSET_1:6;
[: cTS, Lex(E) :] c= [:cTS, Lex(E):]; then
consider xb, xi being set such that
F: xbi = [xb, xi] & xb in cTS & xi in Lex(E) by E, RELSET_1:6;
reconsider xi as Element of Lex(E) by F;
reconsider xe = xi as Element of E^omega;
reconsider xb as Element of cTS by F;
reconsider xc as Element of cTS by E;
G: xc = xi-succ_of (xb, TS) by F, E, D, A1;
len xe = 1 by ThLex20;
hence thesis by A2, E, F, G;
end;
x in the Tran of bTS2 implies x in the Tran of bTS1
proof
assume
D: x in the Tran of bTS2;
consider xbi, xc being set such that
E: x = [xbi, xc] & xbi in [: cTS, Lex(E) :] & xc in cTS
by A2, D, RELSET_1:6;
[: cTS, Lex(E) :] c= [:cTS, Lex(E):]; then
consider xb, xi being set such that
F: xbi = [xb, xi] & xb in cTS & xi in Lex(E) by E, RELSET_1:6;
reconsider xi as Element of Lex(E) by F;
reconsider xe = xi as Element of E^omega;
reconsider xb as Element of cTS by F;
reconsider xc as Element of cTS by E;
G: xc = xi-succ_of (xb, TS) by F, E, D, A2;
len xe = 1 by ThLex20;
hence thesis by A1, E, F, G;
end;
hence thesis by A1, A2, C, TARSKI:2;
end;
end;
registration
let E, F, TS;
cluster _bool TS -> non empty deterministic;
coherence
proof
set bTS = _bool TS;
set cTS = bool (the carrier of TS);
set wTS = the carrier of bTS;
set tTS = the Tran of bTS;
X: bTS is deterministic
proof
for x, y1, y2 being set st [x, y1] in tTS & [x, y2] in tTS holds y1 = y2
proof
let x, y1, y2 be set such that
B: [x, y1] in tTS & [x, y2] in tTS;
U: the carrier of bTS = bool (the carrier of TS) by DefBool;
reconsider x as Element of [: wTS, Lex(E) :] by B, ZFMISC_1:106;
reconsider y1, y2 as Element of wTS by B, ZFMISC_1:106;
consider xc, xi being set such that
C: xc in wTS & xi in Lex(E) & x = [xc, xi] by U, ZFMISC_1:def 2;
reconsider xi as Element of Lex(E) by C;
reconsider xc as Element of wTS by C;
reconsider xi as Element of E^omega;
reconsider xc, y1, y2 as Subset of TS by DefBool;
y1 = xi-succ_of (xc, TS) & y2 = xi-succ_of (xc, TS)
by B, C, DefBool;
hence thesis;
end;
then the Tran of bTS is Function by FUNCT_1:def 1;
hence thesis by ThDet20;
end;
the carrier of bTS = bool (the carrier of TS) by DefBool;
hence thesis by X;
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 DefBool;
end;
end;
theorem ThBool5:
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 ThBool10:
len w = 1 implies (X = w-succ_of (S, TS) iff S, w ==>* X, _bool TS)
proof
assume
A: len w = 1;
then consider e such that
B: w = <%e%> & w.0 = e by LmXSeq10;
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 A, DefBool;
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 S, w ==>* X, <%>E, _bool TS by REWRITE3:def 7;
then S, w ==>. X, <%>E, _bool TS by B, ThBool5;
then S, w^<%>E ==>. X, <%>E, _bool TS by AFINSQ_1:32;
then
C: S, w -->. X, _bool TS by REWRITE3:24;
then X in _bool TS by REWRITE3:15;
then X in the carrier of _bool TS by STRUCT_0:def 5;
then reconsider X' = X as Subset of TS by DefBool;
[[S, w], X'] in the Tran of _bool TS by C, REWRITE3:def 2;
hence thesis by DefBool;
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
:defDetSA:
(the transition-system of SA) is deterministic &
card (the InitS of SA) = 1;
end;
registration
let E, F;
cluster strict non empty finite deterministic semiautomaton over F;
existence
proof
consider X being non empty finite set;
reconsider T = {} as Relation of [: X, F :], X by RELSET_1:25;
consider x being 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:60, REWRITE3:14;
thus card (the InitS of SA) = 1 by CARD_1:50;
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 :DefBoolSA:
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 tSA = (the Tran of _bool TS) as
Relation of [: cSA, Lex(E) :], cSA;
reconsider iSA = { <%>E-succ_of (the InitS of SA, SA) } as Subset of cSA
by DefBool;
set bSA = semiautomaton(# cSA, tSA, iSA #);
card iSA = 1 by CARD_1:50;
then reconsider bSA as
strict non empty deterministic semiautomaton over Lex(E) by defDetSA;
take bSA;
thus thesis;
end;
uniqueness;
end;
registration
let E, F, SA;
cluster _bool SA -> non empty deterministic;
coherence
proof
set TS = _bool SA;
X: the transition-system of TS = _bool the transition-system of SA
by DefBoolSA;
the InitS of TS = { <%>E-succ_of (the InitS of SA, SA) } by DefBoolSA;
then card the InitS of TS = 1 by CARD_1:50;
hence thesis by defDetSA, X;
end;
end;
theorem ThSA10:
the carrier of _bool SA = bool the carrier of SA
proof
the transition-system of _bool SA = _bool the transition-system of SA
by DefBoolSA;
hence thesis by DefBool;
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 ThSA10;
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 ThLeft10:
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 w' st w' = w & Q meets w'-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 :defDetA:
(the semiautomaton of A) is deterministic;
end;
registration
let E, F;
cluster strict non empty finite deterministic automaton over F;
existence
proof
consider X being non empty finite set;
reconsider T = {} as Relation of [: X, F :], X by RELSET_1:25;
consider x being 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;
B: (the transition-system of A) is deterministic by RELAT_1:60, REWRITE3:14;
card (the InitS of A) = 1 by CARD_1:50;
then the semiautomaton of A is deterministic by B, defDetSA;
hence A is deterministic by defDetA;
end;
end;
reserve A for non empty automaton over F;
reserve p, q for Element of A;
reserve P, Q for Subset 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 :defBoolA:
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 the carrier 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 defDetA;
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 defBoolA;
hence thesis by defDetA;
end;
end;
theorem ThA10:
the carrier of _bool A = bool the carrier of A
proof
the semiautomaton of _bool A = _bool the semiautomaton of A
by defBoolA;
hence thesis by ThSA10;
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 ThA10;
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 ThRight10:
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 w' st w = w' & w'-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 ThLang5:
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 ThLang10:
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 ThLang5;
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 such that
A1: x in w-succ_of (the InitS of A, A) and
A2: x in (the FinalS of A) by XBOOLE_0:3;
reconsider x as Element of A by A1;
consider p such that
B: p in the InitS of A & p, w ==>* x, A by A1, REWRITE3:103;
thus thesis by A2, B;
end;
theorem
Lang(A) = left-Lang(the FinalS of A)
proof
A: 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 ThLang10;
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 ThLeft10;
hence thesis by ThLang10;
end;
hence thesis by A, SUBSET_1:8;
end;
theorem
Lang(A) = right-Lang(the InitS of A)
proof
A: 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 ThLang10;
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 ThRight10;
hence thesis by ThLang10;
end;
hence thesis by A, SUBSET_1:8;
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 ThTS3h:
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
A: (R.1)`2 = <%e%>^u & (R.len R)`2 = <%>E;
A1: rng R <> {};
(R.1)`2 <> (R.len R)`2 by A, AFINSQ_1:33;
then len R >= 1 + 1 & 2 >= 1 by NAT_1:8, 26;
then 1 + 1 in dom R by FINSEQ_3:27;
then
B: [R.1, R.2] in ==>.-relation(TS) by A1, FINSEQ_3:34, REWRITE1:def 2;
consider p being Element of TS, v being Element of E^omega,
q being Element of TS, w such that
C1: R.1 = [p, v] and
C2: R.2 = [q, w] by B, REWRITE3:31;
p, v ==>. q, w, TS by B, C1, C2, REWRITE3:def 4;
then consider u1 such that
D: p, u1 -->. q, TS & v = u1^w by REWRITE3:22;
E: u1 in Lex(E) \/ {<%>E} by D, REWRITE3:15;
per cases by E, XBOOLE_0:def 3;
suppose u1 in Lex(E);
then len u1 = 1 by ThLex20;
then consider f being Element of E such that
F: u1 = <%f%> & u1.0 = f by LmXSeq10;
(R.1)`2 = <%f%>^w by C1, D, F, MCART_1:7;
then e = f & u = w by A, LmSeq30;
hence thesis by C2, MCART_1:7;
end;
suppose u1 in {<%>E};
then
F: u1 = <%>E by TARSKI:def 1;
v = (R.1)`2 & w = (R.2)`2 by C1, C2, MCART_1:7;
hence thesis by A, D, F, AFINSQ_1:32;
end;
end;
theorem ThTS3g:
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;
A: P[0];
B: now
let k;
assume
B1: P[k];
now
let R be RedSequence of ==>.-relation(TS), u such that
C: len R = k + 1 & (R.1)`2 = u & (R.len R)`2 = <%>E;
per cases;
suppose len u = 0;
hence len R > len u;
end;
suppose
D2: len u > 0;
then consider e, u1 such that
D: u = <%e%>^u1 by ThTS3j;
len R <> 1 by C, D2;
then consider R' being RedSequence of ==>.-relation(TS) such that
E: <*R.1*>^R' = R & len R' + 1 = len R by REWRITE3:5, NAT_1:26;
I: len R' + 0 < k + 1 by C, E, XREAL_1:8;
rng R' <> {} & len R' >= 0 + 1 by NAT_1:8;
then
K: 1 in dom R' & len R' in dom R' by FINSEQ_3:27;
then
F: (<*R.1*>^R').(1 + 1) = R'.1 by REWRITE3:1;
H: (R'.len R')`2 = <%>E by C, E, K, REWRITE3:1;
per cases by C, D, ThTS3h;
suppose (R.2)`2 = <%e%>^u1;
hence len R > len u by C, D, E, F, H, B1, I, XXREAL_0:2;
end;
suppose (R.2)`2 = u1;
then len R' > len u1 by C, E, F, H, B1;
then len R > 1 + len u1 by E, XREAL_1:8;
then len R > len <%e%> + len u1 by AFINSQ_1:def 5;
hence len R > len u by D, AFINSQ_1:20;
end;
end;
end;
hence P[k + 1];
end;
for k holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThTS3e:
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;
A: P[0];
B: now
let i;
assume
C: P[i];
thus P[i + 1]
proof
let R be RedSequence of ==>.-relation(TS), u such that
D: len R = i + 1 & (R.1)`2 = u^v & (R.len R)`2 = <%>E;
per cases;
suppose len u = 0;
then
E: u = {};
set j = 1;
take j;
rng R <> {};
hence j in dom R by FINSEQ_3:34;
thus (R.j)`2 = v by D, E, AFINSQ_1:32;
end;
suppose
D3: len u > 0;
then len u >= 0 + 1 by NAT_1:13;
then len u + len v >= 1 + len v by XREAL_1:8;
then len(u^v) >= 1 + len v by AFINSQ_1:20;
then len(u^v) >= 1 by LmNat1;
then len R + len(u^v) > len(u^v) + 1 by D, ThTS3g, XREAL_1:10;
then len R > 1 by XREAL_1:8;
then consider R' being RedSequence of ==>.-relation(TS) such that
F: len R' + 1 = len R &
for k st k in dom R' holds R'.k = R.(k + 1) by REWRITE3:7;
G0: rng R' <> {};
then
G1: 1 in dom R' by FINSEQ_3:34;
H: (R'.1)`2 = (R.(1 + 1))`2 by F, G0, FINSEQ_3:34;
1 <= len R' by G1, FINSEQ_3:27;
then len R' in dom R' by FINSEQ_3:27;
then
H': (R'.len R')`2 = <%>E by D, F;
consider e, u1 such that
H2: u = <%e%>^u1 by D3, ThTS3j;
Z: (R.1)`2 = <%e%>^(u1^v) by D, H2, AFINSQ_1:30;
thus ex k st k in dom R & (R.k)`2 = v
proof
per cases by D, ThTS3h, Z;
suppose (R.2)`2 = u^v;
then consider l such that
I: l in dom R' & (R'.l)`2 = v by C, D, F, H, H';
set k = l + 1;
take k;
thus k in dom R by I, F, ThTS3i;
thus (R.k)`2 = v by F, I;
end;
suppose (R.2)`2 = u1^v;
then consider l such that
I: l in dom R' & (R'.l)`2 = v by C, D, F, H, H';
set k = l + 1;
take k;
thus k in dom R by I, F, ThTS3i;
thus (R.k)`2 = v by F, I;
end;
end;
end;
end;
end;
for k holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
definition
let E, u, v;
func chop(u, v) -> Element of E^omega means
:defCut:
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
A: w1^v = u;
take w1;
let w such that
B: w^v = u;
thus w1 = w by A, B, AFINSQ_1:31;
end;
thus thesis;
end;
uniqueness
proof
let w1, w2;
hereby
given w such that
A: w^v = u;
assume that
B1: for w st w^v = u holds w1 = w and
B2: for w st w^v = u holds w2 = w;
w1 = w & w2 = w by A, B1, B2;
hence w1 = w2;
end;
thus thesis;
end;
consistency;
end;
theorem ThTS3k'b:
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
A: p.1 = [x, u^w] & p.len p = [y, v^w];
deffunc F(set) = [(p.$1)`1, chop(dim2(p.$1, E), w)];
consider q being FinSequence such that
B1: len q = len p and
B2: for k st k in dom q holds q.k = F(k) from FINSEQ_1:sch 2;
for k being Element of NAT st k in dom q & k + 1 in dom q holds
[q.k, q.(k + 1)] in ==>.-relation(TS)
proof
let k be Element of NAT such that
C1: k in dom q & k + 1 in dom q;
1 <= k & k <= len q & 1 <= k + 1 & k + 1 <= len q by C1, FINSEQ_3:27;
then
C2: k in dom p & k + 1 in dom p by B1, FINSEQ_3:27;
consider v1 such that
D1: (p.k)`2 = v1^(v^w) by A, C2, REWRITE3:52;
consider v2 such that
D2: (p.(k + 1))`2 = v2^(v^w) by A, C2, REWRITE3:52;
D3: [p.k, p.(k + 1)] in ==>.-relation(TS) by C2, REWRITE1:def 2;
then
D4: 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 REWRITE3:31;
D5: dim2(p.k, E) = v1^(v^w) by D1, D4, REWRITE3:def 5;
D6: dim2(p.(k + 1), E) = v2^(v^w) by D2, D4, REWRITE3:def 5;
[p.k, [(p.(k + 1))`1, v2^(v^w)]] in ==>.-relation(TS)
by C2, D2, D3, REWRITE3:48;
then [[(p.k)`1, v1^(v^w)], [(p.(k + 1))`1, v2^(v^w)]]
in ==>.-relation(TS)
by C2, D1, 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
E: (p.k)`1, u1 -->. (p.(k + 1))`1, TS & v1^(v^w) = u1^(v2^(v^w))
by REWRITE3:22;
v1^v^w = u1^(v2^(v^w)) by E, AFINSQ_1:30
.= u1^v2^(v^w) by AFINSQ_1:30
.= u1^v2^v^w by AFINSQ_1:30;
then v1^v = u1^v2^v by AFINSQ_1:31
.= u1^(v2^v) by AFINSQ_1:30;
then
F: (p.k)`1, v1^v ==>. (p.(k + 1))`1, v2^v, TS by E, REWRITE3:def 3;
G1: q.k = [(p.k)`1, chop(v1^(v^w), w)] by B2, C1, D5
.= [(p.k)`1, chop(v1^v^w, w)] by AFINSQ_1:30
.= [(p.k)`1, v1^v] by defCut;
q.(k + 1) = [(p.(k + 1))`1, chop(v2^(v^w), w)] by B2, C1, D6
.= [(p.(k + 1))`1, chop(v2^v^w, w)] by AFINSQ_1:30
.= [(p.(k + 1))`1, v2^v] by defCut;
hence thesis by F, G1, REWRITE3:def 4;
end;
then reconsider q as RedSequence of ==>.-relation(TS)
by B1, REWRITE1:def 2;
H3: len p >= 0 + 1 by NAT_1:13;
then
H4: 1 in dom p & len p in dom p by FINSEQ_3:27;
H0: 1 in dom q & len p in dom q by B1, H3, FINSEQ_3:27;
H1: dim2(p.1, E) = (p.1)`2 by A, H4, REWRITE3:51
.= u^w by A, MCART_1:7;
H2: dim2(p.len p, E) = (p.len p)`2 by A, H4, REWRITE3:51
.= v^w by A, MCART_1:7;
I1: q.1 = [(p.1)`1, chop(dim2(p.1, E), w)] by B2, H0
.= [x, chop(u^w, w)] by A, H1, MCART_1:7
.= [x, u] by defCut;
q.len q = [(p.len p)`1, chop(dim2(p.len p, E), w)] by B1, B2, H0
.= [y, chop(v^w, w)] by A, H2, MCART_1:7
.= [y, v] by defCut;
hence thesis by I1;
end;
theorem ThTS3k'a:
==>.-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 consider p being RedSequence of ==>.-relation(TS) such that
A: p.1 = [x, u^w] & p.len p = [y, v^w] by REWRITE1:def 3;
consider q being RedSequence of ==>.-relation(TS) such that
B: q.1 = [x, u] & q.len q = [y, v] by A, ThTS3k'b;
thus thesis by B, REWRITE1:def 3;
end;
theorem ThTS3k:
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 ThTS3k'a;
hence thesis by REWRITE3:def 6;
end;
theorem ThTS3:
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
A: 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
B: R.1 = [p, u^v] & R.len R = [q, <%>E] by REWRITE1:def 3;
C: (R.1)`2 = u^v & (R.len R)`2 = <%>E by B, MCART_1:7;
consider l such that
D1: l in dom R and
D2: (R.l)`2 = v by C, ThTS3e;
per cases;
suppose
E2: l + 1 in dom R;
then (R.l)`1 in TS by D1, REWRITE3:49;
then reconsider r = (R.l)`1 as Element of TS by STRUCT_0:def 5;
D3: R.l = [r, v] by D1, D2, E2, REWRITE3:48;
D4: 1 in dom R by FINSEQ_5:6;
D5: 1 <= l by D1, FINSEQ_3:27;
0 + 1 <= len R by NAT_1:13;
then
D6: len R in dom R by FINSEQ_3:27;
D7: l <= len R by D1, FINSEQ_3:27;
reconsider l as Element of NAT by ORDINAL1:def 13;
take r;
thus p, u ==>* r, TS
proof
==>.-relation(TS) reduces R.1, R.l by D5, D4, D1, REWRITE1:18;
then p, u^v ==>* r, v, TS by B, D3, REWRITE3:def 6;
then p, u^v ==>* r, <%>E^v, TS by AFINSQ_1:32;
then p, u ==>* r, <%>E, TS by ThTS3k;
hence thesis by REWRITE3:def 7;
end;
thus r, v ==>* q, TS
proof
==>.-relation(TS) reduces R.l, R.len R by D7, D6, D1, REWRITE1:18;
then r, v ==>* q, <%>E, TS by B, D3, REWRITE3:def 6;
hence thesis by REWRITE3:def 7;
end;
end;
suppose not l + 1 in dom R;
then v = <%>E by C, D1, D2, REWRITE3:3;
then p, u ==>* q, TS & q, v ==>* q, TS by A, REWRITE3:95, AFINSQ_1:32;
hence thesis;
end;
end;
theorem ThSucc19:
w^v-succ_of (X, TS) = v-succ_of (w-succ_of (X, TS), TS)
proof
C1: now
let x;
assume
D0: 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
D1: p in w-succ_of (X, TS) & p, v ==>* r, TS by D0, REWRITE3:103;
consider q being Element of TS such that
D2: q in X & q, w ==>* p, TS by D1, REWRITE3:103;
q, w^v ==>* r, TS by D1, D2, REWRITE3:99;
hence x in w^v-succ_of (X, TS) by D2, REWRITE3:103;
end;
now
let x;
assume
D0: x in w^v-succ_of (X, TS);
then reconsider r = x as Element of TS;
consider q being Element of TS such that
D1: q in X & q, w^v ==>* r, TS by D0, REWRITE3:103;
consider p being Element of TS such that
D2: q, w ==>* p, TS & p, v ==>* r, TS by D1, ThTS3;
p in w-succ_of (X, TS) & p, v ==>* r, TS by D1, D2, REWRITE3:103;
hence x in v-succ_of (w-succ_of (X, TS), TS) by REWRITE3:103;
end;
hence thesis by C1, TARSKI:2;
end;
theorem ThTS38:
_bool TS is non empty transition-system over Lex(E) \/ {<%>E}
proof
A: dom the Tran of _bool TS c= [: the carrier of _bool TS, Lex(E) :]
by RELAT_1:def 18;
Lex(E) c= Lex(E) \/ {<%>E} by XBOOLE_1:7;
then [: the carrier of _bool TS, Lex(E) :] c=
[: the carrier of _bool TS, Lex(E) \/ {<%>E} :] by ZFMISC_1:118;
hence thesis by A, RELSET_1:13, XBOOLE_1:1;
end;
theorem ThTS39:
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) };
Z: not <%>E in rng dom (the Tran of _bool TS) by ThTS10;
A: P[0]
proof
let u;
assume len u <= 0;
then
A1: u = <%>E;
let v;
reconsider vso = { v-succ_of (X, TS) } as Subset of _bool TS
by DefBool;
u-succ_of (vso, _bool TS) = vso by Z, A1, REWRITE3:104;
hence thesis by A1, AFINSQ_1:32;
end;
B: now
let k;
assume
B1: P[k];
now
let u;
assume
Y: len u <= k + 1;
let v;
per cases;
suppose
Y1: k = 0;
per cases by Y, Y1, NAT_1:26;
suppose len u = 0;
hence u-succ_of ({ v-succ_of (X, TS) }, _bool TS) =
{ v^u-succ_of (X, TS) } by A;
end;
suppose
Y2: len u = 1;
C1: now
let x;
assume
D1: x in u-succ_of ({ v-succ_of (X, TS) }, _bool TS);
reconsider P = x as Element of _bool TS by D1;
consider Q being Element of _bool TS such that
D2: Q in { v-succ_of (X, TS) } & Q, u ==>* P, _bool TS
by D1, REWRITE3:103;
D3: Q = v-succ_of (X, TS) by D2, TARSKI:def 1;
P = u-succ_of (Q, TS) by D2, Y2, ThBool10;
then P = v^u-succ_of (X, TS) by D3, ThSucc19;
hence x in { v^u-succ_of (X, TS) } by TARSKI:def 1;
end;
now
let x;
assume
D: x in { v^u-succ_of (X, TS) };
then
D0: x = v^u-succ_of (X, TS) by TARSKI:def 1;
reconsider P = x as Element of _bool TS by D, DefBool;
x = u-succ_of (v-succ_of (X, TS), TS) by D0, ThSucc19;
then
D1: v-succ_of (X, TS), u ==>* x, _bool TS by Y2, ThBool10;
D2: v-succ_of (X, TS) is Element of _bool TS by DefBool;
v-succ_of (X, TS) in { v-succ_of (X, TS) } by TARSKI:def 1;
then P in u-succ_of ( { v-succ_of (X, TS) }, _bool TS)
by D1, D2, REWRITE3:103;
hence x in u-succ_of ( { v-succ_of (X, TS) }, _bool TS);
end;
hence u-succ_of ({ v-succ_of (X, TS) }, _bool TS) =
{ v^u-succ_of (X, TS) } by C1, TARSKI:2;
end;
end;
suppose k <> 0;
then consider v1, v2 such that
B2: len v1 <= k & len v2 <= k & u = v1^v2 by LmXSeq20, Y;
C1: v1-succ_of({ v-succ_of(X, TS) }, _bool TS) = { v^v1-succ_of (X, TS) }
by B1, B2;
reconsider bTS = _bool TS as
non empty transition-system over Lex(E) \/ {<%>E} by ThTS38;
C2: the carrier of bTS = the carrier of _bool TS &
the Tran of bTS = the Tran of _bool TS;
v1^v2-succ_of ({ v-succ_of (X, TS) }, _bool TS)
= v1^v2-succ_of ({ v-succ_of (X, TS) }, bTS) by C2, REWRITE3:105
.= v2-succ_of (v1-succ_of ({ v-succ_of (X, TS) }, bTS), bTS)
by ThSucc19
.= v2-succ_of (v1-succ_of ({ v-succ_of (X, TS) }, _bool TS), bTS)
by C2, REWRITE3:105
.= v2-succ_of(v1-succ_of({ v-succ_of (X, TS) }, _bool TS), _bool TS)
by C2, REWRITE3:105
.= { v^v1^v2-succ_of (X, TS) } by C1, B1, B2
.= { v^(v1^v2)-succ_of (X, TS) } by AFINSQ_1:30;
hence u-succ_of ({ v-succ_of (X, TS) }, _bool TS) =
{ v^u-succ_of (X, TS) } by B2;
end;
end;
hence P[k + 1];
end;
for k holds P[k] from NAT_1:sch 2(A, B);
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 ThSA39:
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 DefBoolSA;
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
.= { <%>E^w-succ_of (X, TS) } by ThTS39
.= { w-succ_of (X, TS) } by AFINSQ_1:32
.= { 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 ThA20:
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
A: P meets the FinalS of A by XBOOLE_0:3;
P is Element of _bool A by ThA10;
then P in { Q where Q is Element of _bool A : Q meets (the FinalS of A) }
by A;
hence thesis by defBoolA;
end;
theorem ThA30:
X in the FinalS of _bool A implies X meets the FinalS of A
proof
assume
A: 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 defBoolA;
then consider Q being Element of _bool A such that
B: X = Q & Q meets (the FinalS of A) by A;
thus thesis by B;
end;
theorem ThA38:
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 defBoolA
.= { <%>E-succ_of (the InitS of the semiautomaton of A,
the semiautomaton of A) } by DefBoolSA;
hence thesis by REWRITE3:105;
end;
theorem ThA39:
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 defBoolA;
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 ThSA39
.= { w-succ_of (X, A) } by REWRITE3:105;
end;
theorem ThA40:
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 ThA38;
hence thesis by ThA39;
end;
theorem ThLang20:
Lang(A) = Lang(_bool A)
proof
set DA = _bool A;
A: 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 ThLang10;
then consider x such that
B: x in w-succ_of (the InitS of A, A) & x in the FinalS of A
by XBOOLE_0:3;
C: w-succ_of (the InitS of A, A) in the FinalS of DA by B, ThA20;
w-succ_of (the InitS of DA, DA) = { w-succ_of (the InitS of A, A) }
by ThA40;
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 C, XBOOLE_0:3;
hence thesis by ThLang10;
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 ThLang10;
then consider x such that
B: x in w-succ_of (the InitS of DA, DA) & 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 ThA40;
then x = w-succ_of (the InitS of A, A) by B, TARSKI:def 1;
then w-succ_of (the InitS of A, A) meets the FinalS of A by B, ThA30;
hence thesis by ThLang10;
end;
hence thesis by A, SUBSET_1:8;
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 ThLang20;
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 ThLang20;
hence thesis;
end;