Bazując na pojęciach wprowadzonych w [3],
wprowadzone zostały semiautomaty, lewe języki, automaty oraz prawe języki.
Zdefiniowane zostały także języki akceptowane przez automaty.
Następnie, została przedstawiona determinizacja systemów tranzycyjnych,
semiautomatów oraz automatów. Na końcu pokazana jest
równoważność automatów deterministycznych i epsilon niedeterministycznych.
Sekcje:
 Pojęcia wstępne
 Systemy tranzycyjne nad Lex(E)
 Determinizacja systemów tranzycyjnych
 Semiautomaty
 Lewe języki
 Automaty
 Prawe języki
 Języki akceptowane przez automaty
 Równoważność automatów deterministycznych i epsilon niedeterministycznych
Bibliografia:
 [1] John E. Hopcroft, Jeffrey D. Ullman: "Wprowadzenie do teorii automatów, języków i obliczeń", AddisonWesley Publishing Company, 1979
 [2] William M. Waite, Gerhard Goos: "Konstrukcja kompilatorów", SpringerVerlag New York Inc., 1984
 [3] Michał Trybulec: "Labelled State Transition Systems", Formalized Mathematics, 2009
Identyfikator Mizar Mathematical Library: FSM_3.
Abstrakt w wersji PDF: tutaj.
YAC Software, 2009.
Pliki:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Equivalence of Deterministic and Epsilon Nondeterministic Automata
:: Micha{\l} Trybulec
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
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;
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 transitionsystem 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 :: FSM_3:1
i >= k + l implies i >= k;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries  Sequences
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FSM_3:2
for a, b being FinSequence holds
a ^ b = a or b ^ a = a implies b = {};
theorem :: FSM_3:3
for p, q being FinSequence st
k in dom p & len p + 1 = len q holds k + 1 in dom q;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries  XFinSequences and Words in E^omega
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FSM_3:4
len u = 1 implies ex e st <%e%> = u & e = u.0;
theorem :: FSM_3:5
k <> 0 & len u <= k + 1 implies
ex v1, v2 st len v1 <= k & len v2 <= k & u = v1^v2;
theorem :: FSM_3:6
for p, q being XFinSequence st <%x%>^p = <%y%>^q holds x = y & p = q;
theorem :: FSM_3:7
len u > 0 implies ex e, u1 st u = <%e%>^u1;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries  Lex
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
registration
let E;
cluster Lex(E) > non empty Subset of E^omega;
end;
theorem :: FSM_3:8
not <%>E in Lex(E);
theorem :: FSM_3:9
u in Lex(E) iff len u = 1;
theorem :: FSM_3:10
u <> v & u in Lex(E) & v in Lex(E) implies
not ex w st u^w = v or w^u = v;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Transition Systems over Lex(E)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FSM_3:11
for TS being transitionsystem over Lex(E) holds
not <%>E in rng dom (the Tran of TS);
theorem :: FSM_3:12
for TS being transitionsystem over Lex(E) holds
(the Tran of TS) is Function implies TS is deterministic;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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 non empty deterministic transitionsystem over Lex(E)
means
:: FSM_3:def 1
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 = wsucc_of (S, TS);
end;
definition
let E, F;
let TS be finite non empty transitionsystem over F;
redefine func _bool TS >
strict finite non empty deterministic transitionsystem over Lex(E);
end;
theorem :: FSM_3:13
x, <%e%> ==>* y, <%>E, _bool TS implies x, <%e%> ==>. y, <%>E, _bool TS;
theorem :: FSM_3:14
len w = 1 implies (X = wsucc_of (S, TS) iff S, w ==>* X, _bool TS);
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Semiautomata
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, F;
struct (transitionsystem 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
:: FSM_3:def 2
(the transitionsystem of SA) is deterministic &
Card (the InitS of SA) = 1;
end;
registration
let E, F;
cluster strict non empty finite deterministic semiautomaton over F;
end;
reserve SA for non empty semiautomaton over F;
registration
let E, F, SA;
cluster the transitionsystem of SA > non empty;
end;
definition
let E, F, SA;
func _bool SA > strict non empty deterministic semiautomaton over Lex(E)
means
:: FSM_3:def 3
the transitionsystem of it = _bool the transitionsystem of SA &
the InitS of it = { <%>Esucc_of (the InitS of SA, SA) };
end;
theorem :: FSM_3:15
the carrier of _bool SA = bool the carrier of SA;
definition
let E, F;
let SA be finite non empty semiautomaton over F;
redefine func _bool SA >
strict finite non empty deterministic semiautomaton over Lex(E);
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Leftlanguages
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, F, SA;
let Q be Subset of SA;
func leftLang(Q) > Subset of E^omega equals
:: FSM_3:def 4
{ w : Q meets wsucc_of (the InitS of SA, SA) };
end;
theorem :: FSM_3:16
for Q being Subset of SA holds
w in leftLang(Q) iff Q meets wsucc_of (the InitS of SA, SA);
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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
:: FSM_3:def 5
(the semiautomaton of A) is deterministic;
end;
registration
let E, F;
cluster strict non empty finite deterministic automaton over F;
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 transitionsystem of A > non empty;
cluster the semiautomaton of A > non empty;
end;
definition
let E, F, A;
func _bool A > strict non empty deterministic automaton over Lex(E)
means
:: FSM_3:def 6
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) };
end;
theorem :: FSM_3:17
the carrier of _bool A = bool the carrier of A;
definition
let E, F;
let A be finite non empty automaton over F;
redefine func _bool A >
strict finite non empty deterministic automaton over Lex(E);
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Languages Accepted by Automata
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, F, A;
let Q be Subset of A;
func rightLang(Q) > Subset of E^omega equals
:: FSM_3:def 7
{ w : wsucc_of (Q, A) meets (the FinalS of A) };
end;
theorem :: FSM_3:18
for Q being Subset of A holds
w in rightLang(Q) iff wsucc_of (Q, A) meets (the FinalS of A);
definition
let E, F, A;
func Lang(A) > Subset of E^omega equals
:: FSM_3:def 8
{ u : ex p, q st
p in the InitS of A & q in the FinalS of A & p, u ==>* q, A };
end;
theorem :: FSM_3:19
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;
theorem :: FSM_3:20
w in Lang(A) iff wsucc_of (the InitS of A, A) meets (the FinalS of A);
theorem :: FSM_3:21
Lang(A) = leftLang(the FinalS of A);
theorem :: FSM_3:22
Lang(A) = rightLang(the InitS of A);
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Equivalence (with respect to the accepted languages)
:: of nondeterministic [finite] automata and deterministic [finite] automata.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve TS for non empty transitionsystem over Lex(E) \/ {<%>E};
theorem :: FSM_3:23
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;
theorem :: FSM_3:24
for R being RedSequence of ==>.relation(TS) st
(R.1)`2 = u & (R.len R)`2 = <%>E holds len R > len u;
theorem :: FSM_3:25
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;
definition
let E, u, v;
func chop(u, v) > Element of E^omega means
:: FSM_3:def 9
for w st w^v = u holds it = w if ex w st w^v = u otherwise it = u;
end;
theorem :: FSM_3:26
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];
theorem :: FSM_3:27
==>.relation(TS) reduces [x, u^w], [y, v^w] implies
==>.relation(TS) reduces [x, u], [y, v];
theorem :: FSM_3:28
x, u^w ==>* y, v^w, TS implies x, u ==>* y, v, TS;
theorem :: FSM_3:29
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;
theorem :: FSM_3:30
w^vsucc_of (X, TS) = vsucc_of (wsucc_of (X, TS), TS);
theorem :: FSM_3:31
_bool TS is non empty transitionsystem over Lex(E) \/ {<%>E};
theorem :: FSM_3:32
wsucc_of ({ vsucc_of (X, TS) }, _bool TS) = { v^wsucc_of (X, TS) };
reserve SA for non empty semiautomaton over Lex(E) \/ {<%>E};
theorem :: FSM_3:33
wsucc_of ({ <%>Esucc_of (X, SA) }, _bool SA) = { wsucc_of (X, SA) };
reserve A for non empty automaton over Lex(E) \/ {<%>E};
reserve P for Subset of A;
theorem :: FSM_3:34
x in the FinalS of A & x in P implies P in the FinalS of _bool A;
theorem :: FSM_3:35
X in the FinalS of _bool A implies X meets the FinalS of A;
theorem :: FSM_3:36
the InitS of _bool A = { <%>Esucc_of (the InitS of A, A) };
theorem :: FSM_3:37
wsucc_of ({ <%>Esucc_of (X, A) }, _bool A) = { wsucc_of (X, A) };
theorem :: FSM_3:38
wsucc_of (the InitS of _bool A, _bool A) = { wsucc_of (the InitS of A, A) }
;
theorem :: FSM_3:39
Lang(A) = Lang(_bool A);
theorem :: FSM_3:40
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);
theorem :: FSM_3:41
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);
Góra
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Equivalence of Deterministic and Epsilon Nondeterministic Automata
:: Micha{\l} Trybulec
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
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;
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 transitionsystem 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;
take 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;
take 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;
consider u1, e such that
C: len u1 = k & u = <%e%>^u1 by B, FLANG_1:9;
thus thesis by C;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries  Lex
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
registration
let E;
cluster Lex(E) > non empty Subset of E^omega;
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 transitionsystem over Lex(E) holds
not <%>E in rng dom (the Tran of TS)
proof
let TS be transitionsystem over Lex(E);
dom (the Tran of TS) c= [: the carrier of TS, Lex(E) :] by RELSET_1:12;
then dom (the Tran of TS) is Relation of the carrier of TS, Lex(E)
by RELSET_1:def 1;
then rng dom the Tran of TS c= Lex(E) by RELSET_1:12;
hence thesis by ThLex10;
end;
theorem ThDet20:
for TS being transitionsystem over Lex(E) holds
(the Tran of TS) is Function implies TS is deterministic
proof
let TS be transitionsystem 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 RELSET_1:12;
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 non empty deterministic transitionsystem 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 = wsucc_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 = isucc_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 = transitionsystem(# cTS, tTS #);
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;
reconsider x as Element of [: cTS, Lex(E) :] by B, ZFMISC_1:106;
reconsider y1, y2 as Element of cTS by B, ZFMISC_1:106;
[: cTS, Lex(E) :] is Relation of cTS, Lex(E) by RELSET_1:def 1;
then consider xc, xi being set such that
C: x = [xc, xi] & xc in cTS & xi in Lex(E) by RELSET_1:6;
reconsider xi as Element of Lex(E) by C;
reconsider xc as Element of cTS by C;
y1 = xisucc_of (xc, TS) & y2 = xisucc_of (xc, TS) by A, B, C;
hence thesis;
end;
then the Tran of bTS is Function by FUNCT_1:def 1;
hence thesis by ThDet20;
end;
then reconsider bTS as
strict non empty deterministic transitionsystem 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 = wsucc_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 = wsucc_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 = xisucc_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 non empty deterministic transitionsystem 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 = wsucc_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 = wsucc_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) :] is Relation of cTS, Lex(E) by RELSET_1:def 1;
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 = xisucc_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) :] is Relation of cTS, Lex(E) by RELSET_1:def 1;
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 = xisucc_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;
definition
let E, F;
let TS be finite non empty transitionsystem over F;
redefine func _bool TS >
strict finite non empty deterministic transitionsystem over Lex(E);
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 = wsucc_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 = wsucc_of (S, TS) implies S, w ==>* X, _bool TS
proof
assume X = wsucc_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 (transitionsystem 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 transitionsystem 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 transitionsystem 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 transitionsystem of SA > non empty;
coherence;
end;
definition
let E, F, SA;
func _bool SA > strict non empty deterministic semiautomaton over Lex(E)
means
:DefBoolSA:
the transitionsystem of it = _bool the transitionsystem of SA &
the InitS of it = { <%>Esucc_of (the InitS of SA, SA) };
existence
proof
reconsider TS = the transitionsystem of SA as
non empty transitionsystem 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 = { <%>Esucc_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;
theorem ThSA10:
the carrier of _bool SA = bool the carrier of SA
proof
the transitionsystem of _bool SA = _bool the transitionsystem of SA
by DefBoolSA;
hence thesis by DefBool;
end;
definition
let E, F;
let SA be finite non empty semiautomaton over F;
redefine func _bool SA >
strict finite non empty deterministic semiautomaton over Lex(E);
coherence
proof
bool the carrier of SA is finite;
hence thesis by ThSA10;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Leftlanguages
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, F, SA;
let Q be Subset of SA;
func leftLang(Q) > Subset of E^omega equals
{ w : Q meets wsucc_of (the InitS of SA, SA) };
coherence
proof
defpred P[Element of E^omega] means
Q meets $1succ_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 leftLang(Q) iff Q meets wsucc_of (the InitS of SA, SA)
proof
let Q be Subset of SA;
thus w in leftLang(Q) implies Q meets wsucc_of (the InitS of SA, SA)
proof
assume w in leftLang(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 transitionsystem 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 transitionsystem of A > non empty;
coherence;
cluster the semiautomaton of A > non empty;
coherence;
end;
definition
let E, F, A;
func _bool A > strict non empty deterministic 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;
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;
definition
let E, F;
let A be finite non empty automaton over F;
redefine func _bool A >
strict finite non empty deterministic automaton over Lex(E);
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 rightLang(Q) > Subset of E^omega equals
{ w : wsucc_of (Q, A) meets (the FinalS of A) };
coherence
proof
defpred P[Element of E^omega] means
$1succ_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 rightLang(Q) iff wsucc_of (Q, A) meets (the FinalS of A)
proof
let Q be Subset of A;
thus w in rightLang(Q) implies wsucc_of (Q, A) meets (the FinalS of A)
proof
assume w in rightLang(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 wsucc_of (the InitS of A, A) meets (the FinalS of A)
proof
thus w in Lang(A) implies
wsucc_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 wsucc_of (the InitS of A, A) by A1, A3, REWRITE3:103;
hence thesis by A2, XBOOLE_0:3;
end;
assume wsucc_of (the InitS of A, A) meets (the FinalS of A);
then consider x such that
A1: x in wsucc_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) = leftLang(the FinalS of A)
proof
A: w in Lang(A) implies w in leftLang(the FinalS of A)
proof
assume w in Lang(A);
then wsucc_of (the InitS of A, A) meets (the FinalS of A) by ThLang10;
hence thesis;
end;
w in leftLang(the FinalS of A) implies w in Lang(A)
proof
assume w in leftLang(the FinalS of A);
then the FinalS of A meets wsucc_of (the InitS of A, A) by ThLeft10;
hence thesis by ThLang10;
end;
hence thesis by A, SUBSET_1:8;
end;
theorem
Lang(A) = rightLang(the InitS of A)
proof
A: w in Lang(A) implies w in rightLang(the InitS of A)
proof
assume w in Lang(A);
then wsucc_of (the InitS of A, A) meets (the FinalS of A) by ThLang10;
hence thesis;
end;
w in rightLang(the InitS of A) implies w in Lang(A)
proof
assume w in rightLang(the InitS of A);
then wsucc_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 transitionsystem 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 2;
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;
G2: 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;
thus thesis by F, G1, G2, 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;
I2: 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;
thus thesis by I1, I2;
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^vsucc_of (X, TS) = vsucc_of (wsucc_of (X, TS), TS)
proof
C1: now
let x;
assume
D0: x in vsucc_of (wsucc_of (X, TS), TS);
then reconsider r = x as Element of TS;
consider p being Element of TS such that
D1: p in wsucc_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^vsucc_of (X, TS) by D2, REWRITE3:103;
end;
now
let x;
assume
D0: x in w^vsucc_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 wsucc_of (X, TS) & p, v ==>* r, TS by D1, D2, REWRITE3:103;
hence x in vsucc_of (wsucc_of (X, TS), TS) by REWRITE3:103;
end;
hence thesis by C1, TARSKI:2;
end;
theorem ThTS38:
_bool TS is non empty transitionsystem over Lex(E) \/ {<%>E}
proof
A: dom the Tran of _bool TS c= [: the carrier of _bool TS, Lex(E) :]
by RELSET_1:12;
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:
wsucc_of ({ vsucc_of (X, TS) }, _bool TS) = { v^wsucc_of (X, TS) }
proof
defpred P[Nat] means
len u <= $1 implies
for v holds
usucc_of({ vsucc_of (X, TS) }, _bool TS) = { v^usucc_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 = { vsucc_of (X, TS) } as Subset of _bool TS
by DefBool;
usucc_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 usucc_of ({ vsucc_of (X, TS) }, _bool TS) =
{ v^usucc_of (X, TS) } by A;
end;
suppose
Y2: len u = 1;
C1: now
let x;
assume
D1: x in usucc_of ({ vsucc_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 { vsucc_of (X, TS) } & Q, u ==>* P, _bool TS
by D1, REWRITE3:103;
D3: Q = vsucc_of (X, TS) by D2, TARSKI:def 1;
P = usucc_of (Q, TS) by D2, Y2, ThBool10;
then P = v^usucc_of (X, TS) by D3, ThSucc19;
hence x in { v^usucc_of (X, TS) } by TARSKI:def 1;
end;
now
let x;
assume
D: x in { v^usucc_of (X, TS) };
then
D0: x = v^usucc_of (X, TS) by TARSKI:def 1;
reconsider P = x as Element of _bool TS by D, DefBool;
x = usucc_of (vsucc_of (X, TS), TS) by D0, ThSucc19;
then
D1: vsucc_of (X, TS), u ==>* x, _bool TS by Y2, ThBool10;
D2: vsucc_of (X, TS) is Element of _bool TS by DefBool;
vsucc_of (X, TS) in { vsucc_of (X, TS) } by TARSKI:def 1;
then P in usucc_of ( { vsucc_of (X, TS) }, _bool TS)
by D1, D2, REWRITE3:103;
hence x in usucc_of ( { vsucc_of (X, TS) }, _bool TS);
end;
hence usucc_of ({ vsucc_of (X, TS) }, _bool TS) =
{ v^usucc_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: v1succ_of({ vsucc_of(X, TS) }, _bool TS) = { v^v1succ_of (X, TS) }
by B1, B2;
reconsider bTS = _bool TS as
non empty transitionsystem 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^v2succ_of ({ vsucc_of (X, TS) }, _bool TS)
= v1^v2succ_of ({ vsucc_of (X, TS) }, bTS) by C2, REWRITE3:105
.= v2succ_of (v1succ_of ({ vsucc_of (X, TS) }, bTS), bTS)
by ThSucc19
.= v2succ_of (v1succ_of ({ vsucc_of (X, TS) }, _bool TS), bTS)
by C2, REWRITE3:105
.= v2succ_of(v1succ_of({ vsucc_of (X, TS) }, _bool TS), _bool TS)
by C2, REWRITE3:105
.= { v^v1^v2succ_of (X, TS) } by C1, B1, B2
.= { v^(v1^v2)succ_of (X, TS) } by AFINSQ_1:30;
hence usucc_of ({ vsucc_of (X, TS) }, _bool TS) =
{ v^usucc_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
wsucc_of ({ vsucc_of (X, TS) }, _bool TS) = { v^wsucc_of (X, TS) };
hence thesis;
end;
reserve SA for non empty semiautomaton over Lex(E) \/ {<%>E};
theorem ThSA39:
wsucc_of ({ <%>Esucc_of (X, SA) }, _bool SA) = { wsucc_of (X, SA) }
proof
set TS = the transitionsystem of SA;
set Es = <%>Esucc_of (X, SA);
the transitionsystem of _bool SA = _bool TS by DefBoolSA;
hence wsucc_of ({ Es }, _bool SA)
= wsucc_of ({ Es }, _bool TS) by REWRITE3:105
.= wsucc_of ({ <%>Esucc_of (X, TS) }, _bool TS) by REWRITE3:105
.= { <%>E^wsucc_of (X, TS) } by ThTS39
.= { wsucc_of (X, TS) } by AFINSQ_1:32
.= { wsucc_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 = { <%>Esucc_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
.= { <%>Esucc_of (the InitS of the semiautomaton of A,
the semiautomaton of A) } by DefBoolSA;
hence thesis by REWRITE3:105;
end;
theorem ThA39:
wsucc_of ({ <%>Esucc_of (X, A) }, _bool A) = { wsucc_of (X, A) }
proof
set SA = the semiautomaton of A;
set Es = <%>Esucc_of (X, A);
the semiautomaton of _bool A = _bool SA by defBoolA;
hence wsucc_of ({ Es }, _bool A)
= wsucc_of ({ Es }, _bool SA) by REWRITE3:105
.= wsucc_of ({ <%>Esucc_of (X, SA) }, _bool SA) by REWRITE3:105
.= { wsucc_of (X, SA) } by ThSA39
.= { wsucc_of (X, A) } by REWRITE3:105;
end;
theorem ThA40:
wsucc_of (the InitS of _bool A, _bool A) = { wsucc_of (the InitS of A, A) }
proof
set Es = <%>Esucc_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 wsucc_of (the InitS of A, A) meets the FinalS of A by ThLang10;
then consider x such that
B: x in wsucc_of (the InitS of A, A) & x in the FinalS of A
by XBOOLE_0:3;
C: wsucc_of (the InitS of A, A) in the FinalS of DA by B, ThA20;
wsucc_of (the InitS of DA, DA) = { wsucc_of (the InitS of A, A) }
by ThA40;
then wsucc_of (the InitS of A, A) in wsucc_of (the InitS of DA, DA)
by TARSKI:def 1;
then wsucc_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 wsucc_of (the InitS of DA, DA) meets the FinalS of DA by ThLang10;
then consider x such that
B: x in wsucc_of (the InitS of DA, DA) & x in the FinalS of DA
by XBOOLE_0:3;
wsucc_of (the InitS of _bool A, _bool A) =
{ wsucc_of (the InitS of A, A) } by ThA40;
then x = wsucc_of (the InitS of A, A) by B, TARSKI:def 1;
then wsucc_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;
Góra
