Basing on the definitions from [1],
semi-Thue systems, Thue systems, and direct derivations are introduced.
Next, the standard reduction relation is defined that, in turn,
is used to introduce derivations using the theory from [2].
Finally, languages generated by rewriting systems are defined as all strings
reachable from an initial word. This is followed by the introduction
of the equivalence of semi-Thue systems with respect to the initial word.
Sections:
- Preliminaries
- XFinSequence Yielding Functions and Finite Sequences
- Concatenation of an XFinSequence with All Elements of an XFinSequence Yielding Function
- Semi-Thue Systems and Thue Systems
- Direct Derivations
- Reduction Relation
- Derivations
- Languages Generated by Semi-Thue Systems
- Equivalence of Semi-Thue Systems
Bibliography:
- [1] William M. Waite, Gerhard Goos: "Compiler Construction", Springer-Verlag New York Inc., 1984
- [2] Grzegorz Bancerek: "Reduction Relations", Formalized Mathematics, 1995
Mizar Mathematical Library identifier: REWRITE2.
Abstract in PDF: here.
Motorola Software Group, 2007.
Files:
:: String Rewriting Systems
:: by Micha{\l} Trybulec
::
:: Received July 17, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies FUNCT_1, BOOLE, FINSEQ_1, RELAT_1, AFINSQ_1, REWRITE2, RELAT_2,
FINSEQ_2, REWRITE1, FINSEQ_5, LANG1, CIRCTRM1, FUNCOP_1, ORDINAL2,
PRELAMB;
notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, RELAT_1, DOMAIN_1,
NAT_1, FINSEQ_5, FUNCT_1, RELSET_1, XXREAL_0, AFINSQ_1, CATALAN2,
RELAT_2, FINSEQ_1, REWRITE1, FINSEQ_2, FLANG_1, LANG1, OPOSET_1,
FUNCOP_1;
constructors POLYNOM1, XXREAL_0, NAT_1, FINSEQ_5, REWRITE1, FLANG_1, LANG1,
OPOSET_1, NUMBERS;
registrations SUBSET_1, RELSET_1, NAT_1, AFINSQ_1, REWRITE1, FINSEQ_1,
FUNCOP_1, ARYTM_3, XXREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0, RELAT_1,
FUNCT_1, XREAL_0, REAL_1, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries: finite sequences.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve x for set;
reserve k, l for Nat;
reserve p, q for FinSequence;
theorem :: REWRITE2:1
not k in dom p & k + 1 in dom p implies k = 0;
theorem :: REWRITE2:2
k > len p & k <= len (p^q) implies
ex l st k = len p + l & l >= 1 & l <= len q;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries: reduction sequences.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve R for Relation;
reserve p, q for RedSequence of R;
theorem :: REWRITE2:3
k >= 1 implies p | k is RedSequence of R;
theorem :: REWRITE2:4
k in dom p implies
ex q st len q = k & q.1 = p.1 & q.len q = p.k;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: XFinSequence yielding functions and finite sequences.
:: These definitions will be later used for introduction of
:: reduction sequences between words from E^omega (XFinSequences).
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let f be Function;
attr f is XFinSequence-yielding means
:: REWRITE2:def 1
x in dom f implies f.x is XFinSequence;
end;
registration
cluster {} -> XFinSequence-yielding;
end;
registration
let f be XFinSequence;
cluster <*f*> -> XFinSequence-yielding;
end;
registration
cluster XFinSequence-yielding Function;
end;
definition
let p be XFinSequence-yielding Function;
let x;
redefine func p.x -> XFinSequence;
end;
registration
cluster XFinSequence-yielding FinSequence;
end;
registration
let E be set;
cluster -> XFinSequence-yielding FinSequence of E^omega;
end;
registration
let p, q be XFinSequence-yielding FinSequence;
cluster p^q -> XFinSequence-yielding;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation (left-sided and right-sided ) of an XFinSequence
:: with all elements of a XFinSequence-yielding Function.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let s be XFinSequence;
let p be XFinSequence-yielding Function;
func s ^+ p -> XFinSequence-yielding Function means
:: REWRITE2:def 2
dom it = dom p & (for x st x in dom p holds it.x = s^(p.x));
func p +^ s -> XFinSequence-yielding Function means
:: REWRITE2:def 3
dom it = dom p & (for x st x in dom p holds it.x = (p.x)^s);
end;
registration
let s be XFinSequence;
let p be XFinSequence-yielding FinSequence;
cluster s ^+ p -> FinSequence-like;
cluster p +^ s -> FinSequence-like;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Properties of the left-sided and right-sided concatenation.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve E for set;
reserve s, t for XFinSequence;
reserve p, q for XFinSequence-yielding FinSequence;
theorem :: REWRITE2:5
len (s ^+ p) = len p & len(p +^ s) = len p;
theorem :: REWRITE2:6
<%>E ^+ p = p & p +^ <%>E = p;
theorem :: REWRITE2:7
s ^+ (t ^+ p) = (s^t) ^+ p & (p +^ t) +^ s = p +^ (t^s);
theorem :: REWRITE2:8
s ^+ (p +^ t) = (s ^+ p) +^ t;
theorem :: REWRITE2:9
s ^+ (p^q) = (s ^+ p)^(s ^+ q) & (p^q) +^ s = (p +^ s)^(q +^ s);
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Redefinitions for E^omega:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E be set;
let p be FinSequence of E^omega;
let k be Nat;
redefine func p.k -> Element of E^omega;
end;
definition
let E be set;
let k be Nat;
let s be Element of E^omega;
redefine func k |-> s -> FinSequence of E^omega;
end;
definition
let E be set;
let s be Element of E^omega;
let p be FinSequence of E^omega;
redefine func s ^+ p -> FinSequence of E^omega;
redefine func p +^ s -> FinSequence of E^omega;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Definitions of semi-Thue systems and Thue systems.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E be set;
mode semi-Thue-system of E is Relation of E^omega;
end;
reserve E for set;
reserve S, T, U for semi-Thue-system of E;
registration let S be Relation;
cluster S \/ S~-> symmetric;
end;
registration
let E;
cluster symmetric semi-Thue-system of E;
end;
definition
let E be set;
mode Thue-system of E is symmetric semi-Thue-system of E;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Direct derivations.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve s, t, s1, t1, u, v, u1, v1, w for Element of E^omega;
reserve p, q for FinSequence of E^omega;
definition
let E, S, s, t;
pred s -->. t, S means
:: REWRITE2:def 4
[s, t] in S;
end;
definition
let E, S, s, t;
pred s ==>. t, S means
:: REWRITE2:def 5
ex v, w, s1, t1 st s = v^s1^w & t = v^t1^w & s1 -->. t1, S;
end;
theorem :: REWRITE2:10
s -->. t, S implies s ==>. t, S;
theorem :: REWRITE2:11
s ==>. s, S implies
ex v, w, s1 st s = v^s1^w & s1 -->. s1, S;
theorem :: REWRITE2:12
s ==>. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S;
theorem :: REWRITE2:13
s ==>. t, S implies u^s^v ==>. u^t^v, S;
theorem :: REWRITE2:14
s -->. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S;
theorem :: REWRITE2:15
s -->. t, S implies u^s^v ==>. u^t^v, S;
theorem :: REWRITE2:16
S is Thue-system of E & s -->. t, S implies t -->. s, S;
theorem :: REWRITE2:17
S is Thue-system of E & s ==>. t, S implies t ==>. s, S;
theorem :: REWRITE2:18
S c= T & s -->. t, S implies s -->.t, T;
theorem :: REWRITE2:19
S c= T & s ==>. t, S implies s ==>.t, T;
theorem :: REWRITE2:20
not s ==>. t, {}(E^omega, E^omega);
theorem :: REWRITE2:21
s ==>. t, S \/ T implies s ==>. t, S or s ==>. t, T;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: ==>.-relation is introduced to define derivations
:: using concepts from REWRITE1.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E;
redefine func id E -> Relation of E;
end;
definition
let E, S;
func ==>.-relation(S) -> Relation of E^omega means
:: REWRITE2:def 6
[s, t] in it iff s ==>. t, S;
end;
theorem :: REWRITE2:22
S c= ==>.-relation(S);
theorem :: REWRITE2:23
p is RedSequence of ==>.-relation(S) implies
p +^ u is RedSequence of ==>.-relation(S) &
u ^+ p is RedSequence of ==>.-relation(S);
theorem :: REWRITE2:24
p is RedSequence of ==>.-relation(S) implies
t ^+ p +^ u is RedSequence of ==>.-relation(S);
theorem :: REWRITE2:25
S is Thue-system of E implies ==>.-relation(S) = (==>.-relation(S))~;
theorem :: REWRITE2:26
S c= T implies ==>.-relation(S) c= ==>.-relation(T);
theorem :: REWRITE2:27
==>.-relation(id (E^omega)) = id (E^omega);
theorem :: REWRITE2:28
==>.-relation(S \/ id (E^omega)) = ==>.-relation(S) \/ id (E^omega);
theorem :: REWRITE2:29
==>.-relation({}(E^omega, E^omega)) = {}(E^omega, E^omega);
theorem :: REWRITE2:30
s ==>. t, ==>.-relation(S) implies s ==>. t, S;
theorem :: REWRITE2:31
==>.-relation(==>.-relation(S)) = ==>.-relation(S);
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Derivations.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, S, s, t;
pred s ==>* t, S means
:: REWRITE2:def 7
==>.-relation(S) reduces s, t;
end;
theorem :: REWRITE2:32
s ==>* s, S;
theorem :: REWRITE2:33
s ==>. t, S implies s ==>* t, S;
theorem :: REWRITE2:34
s -->. t, S implies s ==>* t, S;
theorem :: REWRITE2:35
s ==>* t, S & t ==>* u, S implies s ==>* u, S;
theorem :: REWRITE2:36
s ==>* t, S implies s^u ==>* t^u, S & u^s ==>* u^t, S;
theorem :: REWRITE2:37
s ==>* t, S implies u^s^v ==>* u^t^v, S;
theorem :: REWRITE2:38
s ==>* t, S & u ==>* v, S implies s^u ==>* t^v, S & u^s ==>* v^t, S;
theorem :: REWRITE2:39
S is Thue-system of E & s ==>* t, S implies t ==>* s, S;
theorem :: REWRITE2:40
S c= T & s ==>* t, S implies s ==>* t, T;
theorem :: REWRITE2:41
s ==>* t, S iff s ==>* t, S \/ id (E^omega);
theorem :: REWRITE2:42
s ==>* t, {}(E^omega, E^omega) implies s = t;
theorem :: REWRITE2:43
s ==>* t, ==>.-relation(S) implies s ==>* t, S;
theorem :: REWRITE2:44
s ==>* t, S & u ==>. v, {[s, t]} implies u ==>* v, S;
theorem :: REWRITE2:45
s ==>* t, S & u ==>* v, S \/ {[s, t]} implies u ==>* v, S;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Languages generated by semi-Thue systems.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, S, w;
func Lang(w, S) -> Subset of E^omega equals
:: REWRITE2:def 8
{ s : w ==>* s, S };
end;
theorem :: REWRITE2:46
s in Lang(w, S) iff w ==>* s, S;
theorem :: REWRITE2:47
w in Lang(w, S);
registration
let E be non empty set;
let S be semi-Thue-system of E;
let w be Element of E^omega;
cluster Lang(w, S) -> non empty;
end;
theorem :: REWRITE2:48
S c= T implies Lang(w, S) c= Lang(w, T);
theorem :: REWRITE2:49
Lang(w, S) = Lang(w, S \/ id (E^omega));
theorem :: REWRITE2:50
Lang(w, {}(E^omega, E^omega)) = {w};
theorem :: REWRITE2:51
Lang(w, id (E^omega)) = {w};
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Equivalence of semi-Thue systems.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, S, T, w;
pred S, T are_equivalent_wrt w means
:: REWRITE2:def 9
Lang(w, S) = Lang(w, T);
end;
theorem :: REWRITE2:52
S, S are_equivalent_wrt w;
theorem :: REWRITE2:53
S, T are_equivalent_wrt w implies T, S are_equivalent_wrt w;
theorem :: REWRITE2:54
S, T are_equivalent_wrt w & T, U are_equivalent_wrt w implies
S, U are_equivalent_wrt w;
theorem :: REWRITE2:55
S, S \/ id (E^omega) are_equivalent_wrt w;
theorem :: REWRITE2:56
S, T are_equivalent_wrt w & S c= U & U c= T implies
S, U are_equivalent_wrt w & U, T are_equivalent_wrt w;
theorem :: REWRITE2:57
S, ==>.-relation(S) are_equivalent_wrt w;
theorem :: REWRITE2:58
S, T are_equivalent_wrt w &
==>.-relation(S \/ T) reduces w, s implies
==>.-relation(S) reduces w, s;
theorem :: REWRITE2:59
S, T are_equivalent_wrt w & w ==>* s, S \/ T implies w ==>* s, S;
theorem :: REWRITE2:60
S, T are_equivalent_wrt w implies S, S \/ T are_equivalent_wrt w;
theorem :: REWRITE2:61
s ==>. t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w;
theorem :: REWRITE2:62
s ==>* t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w;
Top
:: String Rewriting Systems
:: by Micha{\l} Trybulec
::
:: Received July 17, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies FUNCT_1, BOOLE, FINSEQ_1, RELAT_1, AFINSQ_1, REWRITE2, RELAT_2,
FINSEQ_2, REWRITE1, FINSEQ_5, LANG1, CIRCTRM1, FUNCOP_1, ORDINAL2,
PRELAMB;
notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, RELAT_1, DOMAIN_1,
NAT_1, FINSEQ_5, FUNCT_1, RELSET_1, XXREAL_0, AFINSQ_1, CATALAN2,
RELAT_2, FINSEQ_1, REWRITE1, FINSEQ_2, FLANG_1, LANG1, OPOSET_1,
FUNCOP_1;
constructors POLYNOM1, XXREAL_0, NAT_1, FINSEQ_5, REWRITE1, FLANG_1, LANG1,
OPOSET_1, NUMBERS;
registrations SUBSET_1, RELSET_1, NAT_1, AFINSQ_1, REWRITE1, FINSEQ_1,
FUNCOP_1, ARYTM_3, XXREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0, RELAT_1,
FUNCT_1, XREAL_0, REAL_1, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FINSEQ_1;
theorems AFINSQ_1, NAT_1, RELAT_1, RELAT_2, XREAL_1, ZFMISC_1, FINSEQ_1,
FINSEQ_2, FUNCT_1, REWRITE1, FINSEQ_3, FINSEQ_5, TARSKI, XBOOLE_0,
XBOOLE_1, ABCMIZ_0, RELSET_1, OPOSET_1, FUNCOP_1;
schemes FUNCT_1, NAT_1, RELSET_1;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries: finite sequences.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve x for set;
reserve k, l for Nat;
reserve p, q for FinSequence;
theorem ThSeq10:
not k in dom p & k + 1 in dom p implies k = 0
proof
assume
A: not k in dom p & k + 1 in dom p;
then
B: 1 <= k + 1 & k + 1 <= len p by FINSEQ_3:27;
per cases by A, FINSEQ_3:27;
suppose k < 1;
hence thesis by NAT_1:14;
end;
suppose k > len p;
hence thesis by B, NAT_1:13;
end;
end;
theorem ThSeq40:
k > len p & k <= len (p^q) implies
ex l st k = len p + l & l >= 1 & l <= len q
proof
assume
A: k > len p & k <= len (p^q);
then consider l such that
L: k = len p + l by NAT_1:10;
take l;
thus k = len p + l by L;
len p + l > len p + 0 by A, L;
then l > 0 & 0 + 1 = 1 by XREAL_1:8;
hence l >= 1 by NAT_1:13;
len p + l <= len p + len q by L, A, FINSEQ_1:35;
hence thesis by XREAL_1:8;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries: reduction sequences.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve R for Relation;
reserve p, q for RedSequence of R;
theorem ThRed9:
k >= 1 implies p | k is RedSequence of R
proof
assume
A: k >= 1;
per cases;
suppose k >= len p;
hence thesis by FINSEQ_1:79;
end;
suppose k < len p;
then
B: len (p | k) > 0 by A, FINSEQ_1:80;
now
let i be Element of NAT such that
C: i in dom (p | k) & i + 1 in dom (p | k);
D: dom (p | k) c= dom p by RELAT_1:89;
(p | k).i = p.i & (p | k).(i + 1) = p.(i + 1) by C, FUNCT_1:70;
hence [(p | k).i, (p | k).(i + 1)] in R by C, D, REWRITE1:def 2;
end;
hence thesis by B, REWRITE1:def 2;
end;
end;
theorem ThRed10:
k in dom p implies
ex q st len q = k & q.1 = p.1 & q.len q = p.k
proof
assume k in dom p;
then
B: 1 <= k & k <= len p by FINSEQ_3:27;
set q = p | k;
take q;
thus q is RedSequence of R by B, ThRed9;
thus len q = k by B, FINSEQ_1:80;
hence thesis by B, FINSEQ_3:121;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: XFinSequence yielding functions and finite sequences.
:: These definitions will be later used for introduction of
:: reduction sequences between words from E^omega (XFinSequences).
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let f be Function;
attr f is XFinSequence-yielding means :defXFin:
x in dom f implies f.x is XFinSequence;
end;
registration
cluster {} -> XFinSequence-yielding;
coherence
proof
let x;
thus thesis;
end;
end;
registration
let f be XFinSequence;
cluster <*f*> -> XFinSequence-yielding;
coherence
proof
let x be set;
assume x in dom <*f*>;
then x in {1} by FINSEQ_1:4,55;
then x = 1 by TARSKI:def 1;
hence thesis by FINSEQ_1:57;
end;
end;
registration
cluster XFinSequence-yielding Function;
existence
proof
consider f being XFinSequence, x being set;
A: dom (x --> f) = x by FUNCOP_1:19;
take F = x --> f;
let x;
assume x in dom F;
hence thesis by A, FUNCOP_1:13;
end;
end;
definition
let p be XFinSequence-yielding Function;
let x;
redefine func p.x -> XFinSequence;
coherence
proof
per cases;
suppose x in dom p;
hence thesis by defXFin;
end;
suppose not x in dom p;
hence thesis by FUNCT_1:def 4;
end;
end;
end;
registration
cluster XFinSequence-yielding FinSequence;
existence
proof
take {};
thus thesis;
end;
end;
registration
let E be set;
cluster -> XFinSequence-yielding FinSequence of E^omega;
coherence
proof
let f be FinSequence of E^omega;
let x;
assume x in dom f;
then f.x in E^omega by FINSEQ_2:13;
hence f.x is XFinSequence by AFINSQ_1:def 8;
end;
end;
registration
let p, q be XFinSequence-yielding FinSequence;
cluster p^q -> XFinSequence-yielding;
coherence
proof
now
let x;
assume
A: x in dom(p^q);
per cases by A, FINSEQ_1:38;
suppose x in dom p;
then p.x = (p^q).x by FINSEQ_1:def 7;
hence (p^q).x is XFinSequence;
end;
suppose ex l being Element of NAT st l in dom q & x = len p + l;
then consider l being Element of NAT such that
B: l in dom q & x = len p + l;
(p^q).(len p + l) = q.l by B, FINSEQ_1:def 7;
hence (p^q).x is XFinSequence by B;
end;
end;
hence thesis by defXFin;
end;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation (left-sided and right-sided ) of an XFinSequence
:: with all elements of a XFinSequence-yielding Function.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let s be XFinSequence;
let p be XFinSequence-yielding Function;
func s ^+ p -> XFinSequence-yielding Function means :defConcatL:
dom it = dom p & (for x st x in dom p holds it.x = s^(p.x));
existence
proof
defpred P[set, set] means
for x st x = $1 holds $2 = s^(p.x);
A1: for x, y1, y2 being set st x in dom p & P[x, y1] & P[x, y2] holds y1 = y2
proof
let x, y1, y2 be set;
assume x in dom p & P[x, y1] & P[x, y2];
then y1 = s^(p.x) & y2 = s^(p.x);
hence thesis;
end;
A2: for x st x in dom p ex y being set st P[x, y]
proof
let x;
assume x in dom p;
take s^(p.x);
thus thesis;
end;
consider f being Function such that
B: dom f = dom p & for x st x in dom p holds P[x, f.x]
from FUNCT_1:sch 2(A1, A2);
now
let x;
assume x in dom f;
then f.x = s^(p.x) by B;
hence f.x is XFinSequence;
end;
then reconsider g = f as XFinSequence-yielding Function by defXFin;
take g;
thus thesis by B;
end;
uniqueness
proof
let f, g be XFinSequence-yielding Function such that
A1: dom f = dom p & (for x st x in dom p holds f.x = s^(p.x)) and
A2: dom g = dom p & (for x st x in dom p holds g.x = s^(p.x));
now
let x;
assume x in dom f;
then f.x = s^(p.x) & g.x = s^(p.x) by A1, A2;
hence f.x = g.x;
end;
hence thesis by A1, A2, FUNCT_1:9;
end;
func p +^ s -> XFinSequence-yielding Function means :defConcatR:
dom it = dom p & (for x st x in dom p holds it.x = (p.x)^s);
existence
proof
defpred P[set, set] means
for x st x = $1 holds $2 = (p.x)^s;
A1: for x, y1, y2 being set st x in dom p & P[x, y1] & P[x, y2] holds y1 = y2
proof
let x, y1, y2 be set;
assume x in dom p & P[x, y1] & P[x, y2];
then y1 = (p.x)^s & y2 = (p.x)^s;
hence thesis;
end;
A2: for x st x in dom p ex y being set st P[x, y]
proof
let x;
assume x in dom p;
take (p.x)^s;
thus thesis;
end;
consider f being Function such that
B: dom f = dom p & for x st x in dom p holds P[x, f.x]
from FUNCT_1:sch 2(A1, A2);
now
let x;
assume x in dom f;
then f.x = (p.x)^s by B;
hence f.x is XFinSequence;
end;
then reconsider g = f as XFinSequence-yielding Function by defXFin;
take g;
thus thesis by B;
end;
uniqueness
proof
let f, g be XFinSequence-yielding Function such that
A1: dom f = dom p & (for x st x in dom p holds f.x = (p.x)^s) and
A2: dom g = dom p & (for x st x in dom p holds g.x = (p.x)^s);
now
let x;
assume x in dom f;
then f.x = (p.x)^s & g.x = (p.x)^s by A1, A2;
hence f.x = g.x;
end;
hence thesis by A1, A2, FUNCT_1:9;
end;
end;
registration
let s be XFinSequence;
let p be XFinSequence-yielding FinSequence;
cluster s ^+ p -> FinSequence-like;
coherence
proof
consider n being Element of NAT such that
A: dom p = Seg n by FINSEQ_1:def 2;
dom (s ^+ p) = Seg n by A, defConcatL;
hence thesis by FINSEQ_1:def 2;
end;
cluster p +^ s -> FinSequence-like;
coherence
proof
consider n being Element of NAT such that
A: dom p = Seg n by FINSEQ_1:def 2;
dom (p +^ s) = Seg n by A, defConcatR;
hence thesis by FINSEQ_1:def 2;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Properties of the left-sided and right-sided concatenation.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve E for set;
reserve s, t for XFinSequence;
reserve p, q for XFinSequence-yielding FinSequence;
theorem ThConcatLen:
len (s ^+ p) = len p & len(p +^ s) = len p
proof
dom (s ^+ p) = dom p & dom (p +^ s) = dom p by defConcatL, defConcatR;
hence thesis by FINSEQ_3:31;
end;
theorem
<%>E ^+ p = p & p +^ <%>E = p
proof
A:
dom (<%>E ^+ p) = dom p by defConcatL;
now
let k be Element of NAT;
assume
B: k in dom p;
thus (<%>E ^+ p).k = (<%>E)^(p.k) by B, defConcatL
.= p.k by AFINSQ_1:32;
end;
hence <%>E ^+ p = p by A, FINSEQ_1:17;
A:
dom (p +^ <%>E) = dom p by defConcatR;
now
let k be Element of NAT;
assume
B: k in dom p;
thus (p +^ <%>E).k = (p.k)^(<%>E) by B, defConcatR
.= p.k by AFINSQ_1:32;
end;
hence thesis by A, FINSEQ_1:17;
end;
theorem
s ^+ (t ^+ p) = (s^t) ^+ p & (p +^ t) +^ s = p +^ (t^s)
proof
A1:
dom (s ^+ (t ^+ p)) = dom (t ^+ p) by defConcatL
.= dom p by defConcatL
.= dom ((s^t) ^+ p) by defConcatL;
now
let k be Element of NAT;
assume
B2: k in dom (s ^+ (t ^+ p));
B1: k in dom (t ^+ p) by B2, defConcatL;
B: k in dom p by B1, defConcatL;
thus (s ^+ (t ^+ p)).k = s^((t ^+ p).k) by B1, defConcatL
.= s^(t^(p.k)) by B, defConcatL
.= s^t^(p.k) by AFINSQ_1:30
.= ((s^t) ^+ p).k by B, defConcatL;
end;
hence s ^+ (t ^+ p) = (s^t) ^+ p by A1, FINSEQ_1:17;
A1:
dom ((p +^ t) +^ s) = dom (p +^ t) by defConcatR
.= dom p by defConcatR
.= dom (p +^ (t^s)) by defConcatR;
now
let k be Element of NAT;
assume
B2: k in dom ((p +^ t) +^ s);
B1: k in dom (p +^ t) by B2, defConcatR;
B: k in dom p by B1, defConcatR;
thus ((p +^ t) +^ s).k = ((p +^ t).k)^s by B1, defConcatR
.= (p.k)^t^s by B, defConcatR
.= (p.k)^(t^s) by AFINSQ_1:30
.= (p +^ (t^s)).k by B, defConcatR;
end;
hence thesis by A1, FINSEQ_1:17;
end;
theorem
s ^+ (p +^ t) = (s ^+ p) +^ t
proof
A1:
dom (s ^+ (p +^ t)) = dom (p +^ t) by defConcatL
.= dom p by defConcatR
.= dom (s ^+ p) by defConcatL
.= dom ((s ^+ p) +^ t) by defConcatR;
now
let k be Element of NAT;
assume
B2: k in dom (s ^+ (p +^ t));
B1: k in dom (p +^ t) by B2, defConcatL;
B: k in dom p by B1, defConcatR;
B3: k in dom (s ^+ p) by B, defConcatL;
thus (s ^+ (p +^ t)).k = s^((p +^ t).k) by B1, defConcatL
.= s^((p.k)^t) by B, defConcatR
.= s^(p.k)^t by AFINSQ_1:30
.= ((s ^+ p).k)^t by B, defConcatL
.= ((s ^+ p) +^ t).k by B3, defConcatR;
end;
hence thesis by A1, FINSEQ_1:17;
end;
theorem
s ^+ (p^q) = (s ^+ p)^(s ^+ q) & (p^q) +^ s = (p +^ s)^(q +^ s)
proof
len (s ^+ (p^q)) = len (p^q) by ThConcatLen
.= len p + len q by FINSEQ_1:35
.= len (s ^+ p) + len q by ThConcatLen
.= len (s ^+ p) + len (s ^+ q) by ThConcatLen
.= len ((s ^+ p)^(s ^+ q)) by FINSEQ_1:35;
then
A: dom (s ^+ (p^q)) = dom ((s ^+ p)^(s ^+ q)) by FINSEQ_3:31;
now
let k be Element of NAT;
assume
B1: k in dom (s ^+ (p^q));
B2: k in dom (p^q) by B1, defConcatL;
now per cases;
suppose
C1: k in dom p;
C2: k in dom (s ^+ p) by C1, defConcatL;
thus (s ^+ (p^q)).k = s^((p^q).k) by B2, defConcatL
.= s^(p.k) by C1, FINSEQ_1:def 7
.= (s ^+ p).k by C1, defConcatL
.= ((s ^+ p)^(s ^+ q)).k by C2, FINSEQ_1:def 7;
end;
suppose
C': not k in dom p;
D1: k < 1 or k > len p by C', FINSEQ_3:27;
1 <= k & k <= len (p^q) by B2, FINSEQ_3:27;
then consider i being Nat such that
L: k = len p + i & i >= 1 & i <= len q by D1, ThSeq40;
L1: i in dom q by L, FINSEQ_3:27;
then
L2: i in dom (s ^+ q) by defConcatL;
C3: len (s ^+ p) = len p by ThConcatLen;
thus (s ^+ (p^q)).k
= s^((p^q).(len p + i)) by L, B2, defConcatL
.= s^(q.i) by L1, FINSEQ_1:def 7
.= (s ^+ q).i by L1, defConcatL
.= ((s ^+ p)^(s ^+ q)).k by L, L2, C3, FINSEQ_1:def 7;
end;
end;
hence (s ^+ (p^q)).k = ((s ^+ p)^(s ^+ q)).k;
end;
hence s ^+ (p^q) = (s ^+ p)^(s ^+ q) by A, FINSEQ_1:17;
len ((p^q) +^ s) = len (p^q) by ThConcatLen
.= len p + len q by FINSEQ_1:35
.= len (p +^ s) + len q by ThConcatLen
.= len (p +^ s) + len (q +^ s) by ThConcatLen
.= len ((p +^ s)^(q +^ s)) by FINSEQ_1:35;
then
A: dom ((p^q) +^ s) = dom ((p +^ s)^(q +^ s)) by FINSEQ_3:31;
now
let k be Element of NAT;
assume
B1: k in dom ((p^q) +^ s);
B2: k in dom (p^q) by B1, defConcatR;
now per cases;
suppose
C1: k in dom p;
C2: k in dom (p +^ s) by C1, defConcatR;
thus ((p^q) +^ s).k = ((p^q).k)^s by B2, defConcatR
.= (p.k)^s by C1, FINSEQ_1:def 7
.= (p +^ s).k by C1, defConcatR
.= ((p +^ s)^(q +^ s)).k by C2, FINSEQ_1:def 7;
end;
suppose
C': not k in dom p;
D1: k < 1 or k > len p by C', FINSEQ_3:27;
1 <= k & k <= len (p^q) by B2, FINSEQ_3:27;
then consider i being Nat such that
L: k = len p + i & i >= 1 & i <= len q by D1, ThSeq40;
L1: i in dom q by L, FINSEQ_3:27;
then
L2: i in dom (q +^ s) by defConcatR;
C3: len (p +^ s) = len p by ThConcatLen;
thus ((p^q) +^ s).k
= ((p^q).(len p + i))^s by L, B2, defConcatR
.= (q.i)^s by L1, FINSEQ_1:def 7
.= (q +^ s).i by L1, defConcatR
.= ((p +^ s)^(q +^ s)).k by L, L2, C3, FINSEQ_1:def 7;
end;
end;
hence ((p^q) +^ s).k = ((p +^ s)^(q +^ s)).k;
end;
hence thesis by A, FINSEQ_1:17;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Redefinitions for E^omega:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E be set;
let p be FinSequence of E^omega;
let k be Nat;
redefine func p.k -> Element of E^omega;
coherence
proof
per cases;
suppose k in dom p;
hence thesis by FINSEQ_2:13;
end;
suppose not k in dom p;
then p.k = {} by FUNCT_1:def 4;
then p.k is XFinSequence of E by AFINSQ_1:19;
hence thesis by AFINSQ_1:def 8;
end;
end;
end;
definition
let E be set;
let k be Nat;
let s be Element of E^omega;
redefine func k |-> s -> FinSequence of E^omega;
coherence by FINSEQ_2:77;
end;
definition
let E be set;
let s be Element of E^omega;
let p be FinSequence of E^omega;
redefine func s ^+ p -> FinSequence of E^omega;
coherence
proof
now
let i be Element of NAT such that
A: i in dom (s ^+ p);
i in dom p by A, defConcatL;
then (s ^+ p).i = s^(p.i) by defConcatL;
hence (s ^+ p).i in E^omega;
end;
hence s ^+ p is FinSequence of E^omega by FINSEQ_2:14;
end;
redefine func p +^ s -> FinSequence of E^omega;
coherence
proof
now
let i be Element of NAT such that
A: i in dom (p +^ s);
i in dom p by A, defConcatR;
then (p +^ s).i = (p.i)^s by defConcatR;
hence (p +^ s).i in E^omega;
end;
hence p +^ s is FinSequence of E^omega by FINSEQ_2:14;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Definitions of semi-Thue systems and Thue systems.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E be set;
mode semi-Thue-system of E is Relation of E^omega;
end;
reserve E for set;
reserve S, T, U for semi-Thue-system of E;
registration let S be Relation;
cluster S \/ S~-> symmetric;
coherence
proof
S \/ S~ = (S~~ \/ S~)~ by RELAT_1:40
.= (S \/ S~)~;
hence thesis by RELAT_2:30;
end;
end;
registration
let E;
cluster symmetric semi-Thue-system of E;
existence
proof
consider S;
take S \/ S~;
thus thesis;
end;
end;
definition
let E be set;
mode Thue-system of E is symmetric semi-Thue-system of E;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Direct derivations.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
reserve s, t, s1, t1, u, v, u1, v1, w for Element of E^omega;
reserve p, q for FinSequence of E^omega;
definition
let E, S, s, t;
pred s -->. t, S means :defProd:
[s, t] in S;
end;
definition
let E, S, s, t;
pred s ==>. t, S means :defDeriv1:
ex v, w, s1, t1 st s = v^s1^w & t = v^t1^w & s1 -->. t1, S;
end;
theorem ThProd10:
s -->. t, S implies s ==>. t, S
proof
assume
A: s -->. t, S;
take e = <%>E;
B: s = s^e by AFINSQ_1:32
.= e^s^e by AFINSQ_1:32;
t = t^e by AFINSQ_1:32
.= e^t^e by AFINSQ_1:32;
hence thesis by A, B;
end;
theorem
s ==>. s, S implies
ex v, w, s1 st s = v^s1^w & s1 -->. s1, S
proof
given v, w, s1, t1 such that
A: s = v^s1^w & s = v^t1^w & s1 -->. t1, S;
v^s1 = v^t1 by A, AFINSQ_1:31;
then s1 = t1 by AFINSQ_1:31;
hence thesis by A;
end;
theorem ThProd30:
s ==>. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S
proof
given v, w, s1, t1 such that
A: s = v^s1^w & t = v^t1^w & s1 -->. t1, S;
B1: u^s = u^(v^s1)^w by A, AFINSQ_1:30
.= u^v^s1^w by AFINSQ_1:30;
u^t = u^(v^t1)^w by A, AFINSQ_1:30
.= u^v^t1^w by AFINSQ_1:30;
hence u^s ==>. u^t, S by A, B1, defDeriv1;
B2:
s^u = v^s1^(w^u) by A, AFINSQ_1:30;
t^u = v^t1^(w^u) by A, AFINSQ_1:30;
hence thesis by A, B2, defDeriv1;
end;
theorem ThProd40:
s ==>. t, S implies u^s^v ==>. u^t^v, S
proof
assume s ==>. t, S;
then u^s ==>. u^t, S by ThProd30;
hence u^s^v ==>. u^t^v, S by ThProd30;
end;
theorem ThProd50:
s -->. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S
proof
assume s -->. t, S;
then s ==>. t, S by ThProd10;
hence thesis by ThProd30;
end;
theorem ThProd60:
s -->. t, S implies u^s^v ==>. u^t^v, S
proof
assume s -->. t, S;
then u^s ==>. u^t, S by ThProd50;
hence u^s^v ==>. u^t^v, S by ThProd30;
end;
theorem ThProd70:
S is Thue-system of E & s -->. t, S implies t -->. s, S
proof
assume
A: S is Thue-system of E & s -->. t, S;
then
B: S = S~ by RELAT_2:30;
[s, t] in S by A, defProd;
then [t, s] in S by B, RELAT_1:def 7;
hence thesis by defProd;
end;
theorem ThProd80:
S is Thue-system of E & s ==>. t, S implies t ==>. s, S
proof
assume
A: S is Thue-system of E & s ==>. t, S;
consider v, w, s1, t1 such that
C: s = v^s1^w & t = v^t1^w & s1 -->. t1, S by A, defDeriv1;
t1 -->. s1, S by A, C, ThProd70;
hence thesis by C, defDeriv1;
end;
theorem ThProd90:
S c= T & s -->. t, S implies s -->.t, T
proof
assume
A: S c= T & s -->. t, S;
then [s, t] in S by defProd;
hence thesis by A, defProd;
end;
theorem ThProd100:
S c= T & s ==>. t, S implies s ==>.t, T
proof
assume
A: S c= T & s ==>. t, S;
then consider v, w, s1, t1 such that
B: s = v^s1^w & t = v^t1^w & s1 -->. t1, S by defDeriv1;
s1 -->. t1, T by A, B, ThProd90;
hence thesis by B, defDeriv1;
end;
theorem ThProd110:
not s ==>. t, {}(E^omega, E^omega)
proof
assume s ==>. t, {}(E^omega, E^omega);
then consider v, w, s1, t1 such that
B: s = v^s1^w & t = v^t1^w & s1 -->. t1, {}(E^omega, E^omega) by defDeriv1;
[s1, t1] in {}(E^omega, E^omega) by B, defProd;
hence contradiction by OPOSET_1:def 1;
end;
theorem ThProd120:
s ==>. t, S \/ T implies s ==>. t, S or s ==>. t, T
proof
assume s ==>. t, S \/ T;
then consider v, w, s1, t1 such that
B: s = v^s1^w & t = v^t1^w & s1 -->. t1, S \/ T by defDeriv1;
C:
[s1, t1] in S \/ T by B, defProd;
per cases by C, XBOOLE_0:def 2;
suppose [s1, t1] in S;
then s1 -->. t1, S by defProd;
hence thesis by B, defDeriv1;
end;
suppose [s1, t1] in T;
then s1 -->. t1, T by defProd;
hence thesis by B, defDeriv1;
end;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: ==>.-relation is introduced to define derivations
:: using concepts from REWRITE1.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E;
redefine func id E -> Relation of E;
coherence by RELSET_1:29;
end;
definition
let E, S;
func ==>.-relation(S) -> Relation of E^omega means :defRed:
[s, t] in it iff s ==>. t, S;
existence
proof
defpred P[Element of E^omega, Element of E^omega] means
$1 ==>. $2, S;
consider R being Relation of E^omega such that
A: for s, t being Element of E^omega holds
[s, t] in R iff P[s, t] from RELSET_1:sch 2;
take R;
thus thesis by A;
end;
uniqueness
proof
let R1, R2 be Relation of E^omega such that
A1: for s, t being Element of E^omega holds
[s, t] in R1 iff s ==>. t, S
and
A2: for s, t being Element of E^omega holds
[s, t] in R2 iff s ==>. t, S;
now
let s, t be Element of E^omega;
[s, t] in R1 iff s ==>.t, S by A1;
hence [s, t] in R1 iff [s, t] in R2 by A2;
end;
hence thesis by RELSET_1:def 3;
end;
end;
theorem ThRedSeq5:
S c= ==>.-relation(S)
proof
thus x in S implies x in ==>.-relation(S)
proof
assume
A: x in S;
then consider a, b being set such that
B: a in E^omega & b in E^omega & x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by B;
a -->. b, S by A, B, defProd;
then a ==>.b, S by ThProd10;
hence thesis by B, defRed;
end;
end;
theorem ThRedSeq10:
p is RedSequence of ==>.-relation(S) implies
p +^ u is RedSequence of ==>.-relation(S) &
u ^+ p is RedSequence of ==>.-relation(S)
proof
assume
A: p is RedSequence of ==>.-relation(S);
len (p +^ u) = len p & len (u ^+ p) = len p by ThConcatLen;
then
B: len (p +^ u) > 0 & len (u ^+ p) > 0 by A, REWRITE1:def 2;
now
let i being Element of NAT such that
C: i in dom (p +^ u) & (i + 1) in dom (p +^ u);
D: i in dom p & (i + 1) in dom p by C, defConcatR;
then [p.i, p.(i + 1)] in ==>.-relation(S) by A, REWRITE1:def 2;
then
F: p.i ==>. p.(i + 1), S by defRed;
E: (p +^ u).i = (p.i)^u & (p +^ u).(i + 1) = (p.(i + 1))^u
by D, defConcatR;
(p.i)^u ==>. (p.(i + 1))^u, S by F, ThProd30;
hence [(p +^ u).i, (p +^ u).(i + 1)] in ==>.-relation(S) by E, defRed;
end;
hence p +^ u is RedSequence of ==>.-relation(S) by B, REWRITE1:def 2;
now
let i being Element of NAT such that
C: i in dom (u ^+ p) & (i + 1) in dom (u ^+ p);
D: i in dom p & (i + 1) in dom p by C, defConcatL;
then [p.i, p.(i + 1)] in ==>.-relation(S) by A, REWRITE1:def 2;
then
F: p.i ==>. p.(i + 1), S by defRed;
E: (u ^+ p).i = u^(p.i) & (u ^+ p).(i + 1) = u^(p.(i + 1))
by D, defConcatL;
u^(p.i) ==>. u^(p.(i + 1)), S by F, ThProd30;
hence [(u ^+ p).i, (u ^+ p).(i + 1)] in ==>.-relation(S) by E, defRed;
end;
hence thesis by B, REWRITE1:def 2;
end;
theorem
p is RedSequence of ==>.-relation(S) implies
t ^+ p +^ u is RedSequence of ==>.-relation(S)
proof
assume p is RedSequence of ==>.-relation(S);
then t ^+ p is RedSequence of ==>.-relation(S) by ThRedSeq10;
hence thesis by ThRedSeq10;
end;
theorem ThRedSeq30:
S is Thue-system of E implies ==>.-relation(S) = (==>.-relation(S))~
proof
assume
A: S is Thue-system of E;
now
let x;
thus x in ==>.-relation(S) implies x in (==>.-relation(S))~
proof
assume
B: x in ==>.-relation(S);
then consider a, b being set such that
C: a in E^omega & b in E^omega & x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by C;
a ==>. b, S by B, C, defRed;
then b ==>. a, S by A, ThProd80;
then [b, a] in ==>.-relation(S) by defRed;
hence thesis by C, RELAT_1:def 7;
end;
thus x in (==>.-relation(S))~ implies x in ==>.-relation(S)
proof
assume
B: x in (==>.-relation(S))~;
then consider a, b being set such that
C: a in E^omega & b in E^omega & x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by C;
[b, a] in ==>.-relation(S) by B, C, RELAT_1:def 7;
then b ==>. a, S by defRed;
then a ==>. b, S by A, ThProd80;
hence thesis by C, defRed;
end;
end;
hence thesis by TARSKI:2;
end;
theorem ThRedSeq40:
S c= T implies ==>.-relation(S) c= ==>.-relation(T)
proof
assume
A: S c= T;
thus x in ==>.-relation(S) implies x in ==>.-relation(T)
proof
assume
B: x in ==>.-relation(S);
consider s, t being set such that
C: x = [s, t] & s in E^omega & t in E^omega by B, RELSET_1:6;
reconsider s, t as Element of E^omega by C;
s ==>. t, S by C, B, defRed;
then s ==>. t, T by A, ThProd100;
hence thesis by C, defRed;
end;
end;
theorem ThRedSeq45:
==>.-relation(id (E^omega)) = id (E^omega)
proof
A:
id (E^omega) c= ==>.-relation(id (E^omega)) by ThRedSeq5;
==>.-relation(id (E^omega)) c= id (E^omega)
proof
let x;
assume
B: x in ==>.-relation(id (E^omega));
then consider a, b being set such that
C: a in E^omega & b in E^omega & x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by C;
a ==>. b, id (E^omega) by B, C, defRed;
then consider v, w, s1, t1 such that
D: a = v^s1^w & b = v^t1^w & s1 -->. t1, id (E^omega) by defDeriv1;
[s1, t1] in id (E^omega) by D, defProd;
then s1 = t1 by RELAT_1:def 10;
hence x in id (E^omega) by C, D, RELAT_1:def 10;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThRedSeq50:
==>.-relation(S \/ id (E^omega)) = ==>.-relation(S) \/ id (E^omega)
proof
A:
==>.-relation(S \/ id (E^omega)) c=
==>.-relation(S) \/ id (E^omega)
proof
let x;
assume
B: x in ==>.-relation(S \/ id (E^omega));
then consider a, b being set such that
C: a in E^omega & b in E^omega & x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by C;
a ==>. b, S \/ id (E^omega) by B, C, defRed;
then consider v, w, s1, t1 such that
D: a = v^s1^w & b = v^t1^w & s1 -->. t1, S \/ id (E^omega) by defDeriv1;
E: [s1, t1] in S \/ id (E^omega) by D, defProd;
per cases by E, XBOOLE_0:def 2;
suppose [s1, t1] in S;
then s1 -->. t1, S by defProd;
then v^s1^w ==>. v^t1^w, S by ThProd60;
then x in ==>.-relation(S) by C, D, defRed;
hence x in ==>.-relation(S) \/ id (E^omega) by XBOOLE_0:def 2;
end;
suppose [s1, t1] in id (E^omega);
then s1 = t1 by RELAT_1:def 10;
then x in id (E^omega) by C, D, RELAT_1:def 10;
hence x in ==>.-relation(S) \/ id (E^omega) by XBOOLE_0:def 2;
end;
end;
==>.-relation(S) \/ id (E^omega) c=
==>.-relation(S \/ id (E^omega))
proof
let x;
assume
B: x in ==>.-relation(S) \/ id (E^omega);
per cases by B, XBOOLE_0:def 2;
suppose
C: x in ==>.-relation(S);
S c= S \/ id (E^omega) by XBOOLE_1:7;
then ==>.-relation(S) c=
==>.-relation(S \/ id (E^omega)) by ThRedSeq40;
hence x in ==>.-relation(S \/ id (E^omega)) by C;
end;
suppose x in id (E^omega);
then
C: x in ==>.-relation(id (E^omega)) by ThRedSeq45;
id (E^omega) c= S \/ id (E^omega) by XBOOLE_1:7;
then ==>.-relation(id (E^omega)) c=
==>.-relation(S \/ id (E^omega)) by ThRedSeq40;
hence x in ==>.-relation(S \/ id (E^omega)) by C;
end;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThRedSeq60:
==>.-relation({}(E^omega, E^omega)) = {}(E^omega, E^omega)
proof
{}(E^omega, E^omega) = {} by OPOSET_1:def 1;
then
A: {}(E^omega, E^omega) c= ==>.-relation({}(E^omega, E^omega))
by XBOOLE_1:2;
==>.-relation({}(E^omega, E^omega)) c= {}(E^omega, E^omega)
proof
let x;
assume
B: x in ==>.-relation({}(E^omega, E^omega));
then consider a, b being set such that
C: a in E^omega & b in E^omega & x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by C;
a ==>. b, {}(E^omega, E^omega) by B, C, defRed;
hence thesis by ThProd110;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThRedSeq69:
s ==>. t, ==>.-relation(S) implies s ==>. t, S
proof
assume s ==>. t, ==>.-relation(S);
then consider v, w, s1, t1 such that
B: s = v^s1^w & t = v^t1^w & s1 -->. t1, ==>.-relation(S) by defDeriv1;
[s1, t1] in ==>.-relation(S) by B, defProd;
then s1 ==>. t1, S by defRed;
hence thesis by B, ThProd40;
end;
theorem ThRedSeq70:
==>.-relation(==>.-relation(S)) = ==>.-relation(S)
proof
A:
==>.-relation(S) c= ==>.-relation(==>.-relation(S))
by ThRedSeq5;
==>.-relation(==>.-relation(S)) c= ==>.-relation(S)
proof
let x;
assume
B: x in ==>.-relation(==>.-relation(S));
then consider a, b being set such that
C: a in E^omega & b in E^omega & x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by C;
a ==>. b, ==>.-relation(S) by B, C, defRed;
then a ==>. b, S by ThRedSeq69;
hence thesis by C, defRed;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Derivations.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, S, s, t;
pred s ==>* t, S means :defDerivN:
==>.-relation(S) reduces s, t;
end;
theorem ThDerivN10:
s ==>* s, S
proof
==>.-relation(S) reduces s, s by REWRITE1:13;
hence thesis by defDerivN;
end;
theorem ThDerivN20:
s ==>. t, S implies s ==>* t, S
proof
assume s ==>. t, S;
then [s, t] in ==>.-relation(S) by defRed;
then ==>.-relation(S) reduces s, t by REWRITE1:16;
hence thesis by defDerivN;
end;
theorem
s -->. t, S implies s ==>* t, S
proof
assume s -->. t, S;
then s ==>. t, S by ThProd10;
hence thesis by ThDerivN20;
end;
theorem ThDerivN40:
s ==>* t, S & t ==>* u, S implies s ==>* u, S
proof
assume s ==>* t, S & t ==>* u, S;
then ==>.-relation(S) reduces s, t &
==>.-relation(S) reduces t, u by defDerivN;
then ==>.-relation(S) reduces s, u by REWRITE1:17;
hence thesis by defDerivN;
end;
theorem ThDerivN50:
s ==>* t, S implies s^u ==>* t^u, S & u^s ==>* u^t, S
proof
assume s ==>* t, S;
then ==>.-relation(S) reduces s, t by defDerivN;
then consider p being RedSequence of ==>.-relation(S) such that
A: p.1 = s & p.(len p) = t by REWRITE1:def 3;
reconsider p as FinSequence of E^omega by A, ABCMIZ_0:74;
B1:
p +^ u is RedSequence of ==>.-relation(S) by ThRedSeq10;
(p +^ u).1 = s^u & (p +^ u).(len (p +^ u)) = t^u
proof
1 in dom p by FINSEQ_5:6;
hence (p +^ u).1 = s^u by A, defConcatR;
B2: len p = len (p +^ u) by ThConcatLen;
then len (p +^ u) in dom p by FINSEQ_5:6;
hence thesis by A, B2, defConcatR;
end;
then ==>.-relation(S) reduces s^u, t^u by B1, REWRITE1:def 3;
hence s^u ==>* t^u, S by defDerivN;
B1:
u ^+ p is RedSequence of ==>.-relation(S) by ThRedSeq10;
(u ^+ p).1 = u^s & (u ^+ p).(len (u ^+ p)) = u^t
proof
1 in dom p by FINSEQ_5:6;
hence (u ^+ p).1 = u^s by A, defConcatL;
B2: len p = len (u ^+ p) by ThConcatLen;
then len (u ^+ p) in dom p by FINSEQ_5:6;
hence thesis by A, B2, defConcatL;
end;
then ==>.-relation(S) reduces u^s, u^t by B1, REWRITE1:def 3;
hence u^s ==>* u^t, S by defDerivN;
end;
theorem ThDerivN60:
s ==>* t, S implies u^s^v ==>* u^t^v, S
proof
assume s ==>* t, S;
then u^s ==>* u^t, S by ThDerivN50;
hence thesis by ThDerivN50;
end;
theorem
s ==>* t, S & u ==>* v, S implies s^u ==>* t^v, S & u^s ==>* v^t, S
proof
assume
A: s ==>* t, S & u ==>* v, S;
B1:
s^u ==>* t^u, S by A, ThDerivN50;
t^u ==>* t^v, S by A, ThDerivN50;
hence s^u ==>* t^v, S by B1, ThDerivN40;
B2:
u^s ==>* u^t, S by A, ThDerivN50;
u^t ==>* v^t, S by A, ThDerivN50;
hence thesis by B2, ThDerivN40;
end;
theorem
S is Thue-system of E & s ==>* t, S implies t ==>* s, S
proof
assume
A: S is Thue-system of E & s ==>* t, S;
then ==>.-relation(S) reduces s, t by defDerivN;
then consider p being RedSequence of ==>.-relation(S) such that
B: p.1 = s & p.(len p) = t by REWRITE1:def 3;
set q = Rev p;
q is RedSequence of (==>.-relation(S))~ by REWRITE1:10;
then
C: q is RedSequence of ==>.-relation(S) by A, ThRedSeq30;
D:
q.1 = t by B, FINSEQ_5:65;
q.(len p) = s by B, FINSEQ_5:65;
then q.(len q) = s by FINSEQ_5:def 3;
then ==>.-relation(S) reduces t, s by C, D, REWRITE1:def 3;
hence thesis by defDerivN;
end;
theorem ThDerivN80:
S c= T & s ==>* t, S implies s ==>* t, T
proof
assume
A: S c= T & s ==>* t, S;
then
B: ==>.-relation(S) c= ==>.-relation(T) by ThRedSeq40;
==>.-relation(S) reduces s, t by A, defDerivN;
then ==>.-relation(T) reduces s, t by B, REWRITE1:23;
hence thesis by defDerivN;
end;
theorem ThDerivN90:
s ==>* t, S iff s ==>* t, S \/ id (E^omega)
proof
thus s ==>* t, S implies s ==>* t, S \/ id (E^omega)
proof
S c= S \/ id (E^omega) by XBOOLE_1:7;
hence thesis by ThDerivN80;
end;
assume s ==>* t, S \/ id (E^omega);
then ==>.-relation(S \/ id (E^omega)) reduces s, t by defDerivN;
then ==>.-relation(S) \/ id (E^omega) reduces s, t by ThRedSeq50;
then ==>.-relation(S) reduces s, t by REWRITE1:24;
hence thesis by defDerivN;
end;
theorem ThDerivN100:
s ==>* t, {}(E^omega, E^omega) implies s = t
proof
assume s ==>* t, {}(E^omega, E^omega);
then ==>.-relation({}(E^omega, E^omega)) reduces s, t by defDerivN;
then {}(E^omega, E^omega) reduces s, t by ThRedSeq60;
then {} reduces s, t by OPOSET_1:def 1;
hence thesis by REWRITE1:14;
end;
theorem ThDerivN110:
s ==>* t, ==>.-relation(S) implies s ==>* t, S
proof
assume s ==>* t, ==>.-relation(S);
then ==>.-relation(==>.-relation(S)) reduces s, t by defDerivN;
then ==>.-relation(S) reduces s, t by ThRedSeq70;
hence thesis by defDerivN;
end;
theorem ThDerivN119:
s ==>* t, S & u ==>. v, {[s, t]} implies u ==>* v, S
proof
assume that
A1: s ==>* t, S and
A2: u ==>. v, {[s, t]};
consider u1, v1, s1, t1 such that
B: u = u1^s1^v1 & v = u1^t1^v1 & s1 -->. t1, {[s, t]} by A2, defDeriv1;
[s1, t1] in {[s, t]} by B, defProd;
then [s1, t1] = [s, t] by TARSKI:def 1;
then s1 = s & t1 = t by ZFMISC_1:33;
hence thesis by A1, B, ThDerivN60;
end;
theorem ThDerivN120:
s ==>* t, S & u ==>* v, S \/ {[s, t]} implies u ==>* v, S
proof
assume that
A1: s ==>* t, S and
A2: u ==>* v, S \/ {[s, t]};
==>.-relation(S \/ {[s, t]}) reduces u, v by A2, defDerivN;
then consider p2
being RedSequence of ==>.-relation(S \/ {[s, t]}) such that
B2: p2.1 = u & p2.len p2 = v by REWRITE1:def 3;
defpred P[Nat] means
for p being RedSequence of ==>.-relation(S \/ {[s, t]}), s1, t1 st
len p = $1 & p.1 = s1 & p.len p = t1
ex q being RedSequence of ==>.-relation(S) st
q.1 = s1 & q.len q = t1;
C:
P[0] by REWRITE1:def 2;
D:
now
let k;
assume
D0: P[k];
thus P[k + 1]
proof
let p be RedSequence of ==>.-relation(S \/ {[s, t]}),
s1, t1 such that
D1: len p = k + 1 & p.1 = s1 & p.len p = t1;
per cases;
suppose not k in dom p & k + 1 in dom p;
then k = 0 by ThSeq10;
then p = <*s1*> by D1, FINSEQ_1:57;
then reconsider p as RedSequence of ==>.-relation(S)
by REWRITE1:7;
take p;
thus thesis by D1;
end;
suppose not k + 1 in dom p;
then 0 + 1 > k + 1 by D1, FINSEQ_3:27;
hence thesis by XREAL_1:8;
end;
suppose
D1a: k in dom p & k + 1 in dom p;
then
D1b: [p.k, p.(k + 1)] in ==>.-relation(S \/ {[s, t]})
by REWRITE1:def 2;
set w = p.k;
reconsider w as Element of E^omega by D1b, ZFMISC_1:106;
D1c: w ==>. t1, S \/ {[s, t]} by D1, D1b, defRed;
consider p1
being RedSequence of ==>.-relation(S \/ {[s, t]}) such that
D2: len p1 = k & p1.1 = s1 & p1.len p1 = w by D1, D1a, ThRed10;
consider q being RedSequence of ==>.-relation(S) such that
D3: q.1 = s1 & q.len q = w by D0, D2;
==>.-relation(S) reduces s1, w by D3, REWRITE1:def 3;
then
D3a: s1 ==>* w, S by defDerivN;
w ==>* t1, S
proof
per cases by D1c, ThProd120;
suppose w ==>. t1, S;
hence thesis by ThDerivN20;
end;
suppose w ==>. t1, {[s, t]};
hence thesis by A1, ThDerivN119;
end;
end;
then s1 ==>* t1, S by D3a, ThDerivN40;
then ==>.-relation(S) reduces s1, t1 by defDerivN;
hence thesis by REWRITE1:def 3;
end;
end;
end;
for k holds P[k] from NAT_1:sch 2(C, D);
then consider q being RedSequence of ==>.-relation(S) such that
E: q.1 = u & q.len q = v by B2;
==>.-relation(S) reduces u, v by E, REWRITE1:def 3;
hence thesis by defDerivN;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Languages generated by semi-Thue systems.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, S, w;
func Lang(w, S) -> Subset of E^omega equals
{ s : w ==>* s, S };
coherence
proof
set X = { s : w ==>* s, S };
X c= E^omega
proof
let x;
assume x in X;
then ex t st t = x & w ==>* t, S;
hence thesis;
end;
hence thesis;
end;
end;
theorem ThLang10:
s in Lang(w, S) iff w ==>* s, S
proof
thus s in Lang(w, S) implies w ==>* s, S
proof
assume s in Lang(w, S);
then ex t st t = s & w ==>* t, S;
hence thesis;
end;
thus thesis;
end;
theorem ThLang15:
w in Lang(w, S)
proof
w ==>* w, S by ThDerivN10;
hence thesis;
end;
registration
let E be non empty set;
let S be semi-Thue-system of E;
let w be Element of E^omega;
cluster Lang(w, S) -> non empty;
coherence by ThLang15;
end;
theorem ThLang20:
S c= T implies Lang(w, S) c= Lang(w, T)
proof
assume
A: S c= T;
thus x in Lang(w, S) implies x in Lang(w, T)
proof
assume
B: x in Lang(w, S);
reconsider y = x as Element of E^omega by B;
w ==>* y, S by B, ThLang10;
then w ==>* y, T by A, ThDerivN80;
hence x in Lang(w, T);
end;
end;
theorem ThLang25:
Lang(w, S) = Lang(w, S \/ id (E^omega))
proof
S c= S \/ id (E^omega) by XBOOLE_1:7;
then
A: Lang(w, S) c= Lang(w, S \/ id (E^omega)) by ThLang20;
Lang(w, S \/ id (E^omega)) c= Lang(w, S)
proof
let x;
assume
B: x in Lang(w, S \/ id (E^omega));
then reconsider s = x as Element of E^omega;
w ==>* s, S \/ id (E^omega) by B, ThLang10;
then w ==>* s, S by ThDerivN90;
hence x in Lang(w, S);
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThLang29:
Lang(w, {}(E^omega, E^omega)) = {w}
proof
now
let x;
assume that
B1: x <> w and
B2: x in Lang(w, {}(E^omega, E^omega));
reconsider t = x as Element of E^omega by B2;
w ==>* t, {}(E^omega, E^omega) by B2, ThLang10;
hence contradiction by B1, ThDerivN100;
end;
then x in Lang(w, {}(E^omega, E^omega)) iff x = w by ThLang15;
hence thesis by TARSKI:def 1;
end;
theorem
Lang(w, id (E^omega)) = {w}
proof
{}(E^omega, E^omega) \/ id (E^omega) = {} \/ id (E^omega) by OPOSET_1:def 1
.= id (E^omega);
hence Lang(w, id (E^omega)) = Lang(w, {}(E^omega, E^omega)) by ThLang25
.= {w} by ThLang29;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Equivalence of semi-Thue systems.
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, S, T, w;
pred S, T are_equivalent_wrt w means :defEq:
Lang(w, S) = Lang(w, T);
end;
theorem
S, S are_equivalent_wrt w
proof
thus Lang(w, S) = Lang(w, S);
end;
theorem
S, T are_equivalent_wrt w implies T, S are_equivalent_wrt w
proof
assume Lang(w, S) = Lang(w, T);
hence thesis by defEq;
end;
theorem
S, T are_equivalent_wrt w & T, U are_equivalent_wrt w implies
S, U are_equivalent_wrt w
proof
assume Lang(w, S) = Lang(w, T) & Lang(w, T) = Lang(w, U);
hence thesis by defEq;
end;
theorem
S, S \/ id (E^omega) are_equivalent_wrt w
proof
Lang(w, S) = Lang(w, S \/ id (E^omega)) by ThLang25;
hence thesis by defEq;
end;
theorem ThEq50:
S, T are_equivalent_wrt w & S c= U & U c= T implies
S, U are_equivalent_wrt w & U, T are_equivalent_wrt w
proof
assume that
A1: Lang(w, S) = Lang(w, T) and
A2: S c= U & U c= T;
Lang(w, S) c= Lang(w, U) & Lang(w, U) c= Lang(w, T) by A2, ThLang20;
hence Lang(w, S) = Lang(w, U) by A1, XBOOLE_0:def 10;
hence thesis by A1, defEq;
end;
theorem ThEq60:
S, ==>.-relation(S) are_equivalent_wrt w
proof
S c= ==>.-relation(S) by ThRedSeq5;
then
A: Lang(w, S) c= Lang(w, ==>.-relation(S)) by ThLang20;
Lang(w, ==>.-relation(S)) c= Lang(w, S)
proof
let x such that
C: x in Lang(w, ==>.-relation(S));
reconsider s = x as Element of E^omega by C;
w ==>* s, ==>.-relation(S) by C, ThLang10;
then w ==>* s, S by ThDerivN110;
hence thesis;
end;
hence Lang(w, S) = Lang(w, ==>.-relation(S)) by A, XBOOLE_0:def 10;
end;
theorem ThEq68:
S, T are_equivalent_wrt w &
==>.-relation(S \/ T) reduces w, s implies
==>.-relation(S) reduces w, s
proof
assume that
A1: Lang(w, S) = Lang(w, T) and
A2: ==>.-relation(S \/ T) reduces w, s;
consider p being RedSequence of ==>.-relation(S \/ T) such that
B: p.1 = w & p.len p = s by A2, REWRITE1:def 3;
defpred P[Nat] means
for p being RedSequence of ==>.-relation(S \/ T), t st
len p = $1 & p.1 = w & p.len p = t
ex q being RedSequence of ==>.-relation(S) st
q.1 = w & q.len q = t;
C:
P[0] by REWRITE1:def 2;
D:
now
let k;
assume
D0: P[k];
thus P[k + 1]
proof
let p be RedSequence of ==>.-relation(S \/ T), t such that
D1: len p = k + 1 & p.1 = w & p.len p = t;
per cases;
suppose not k in dom p & k + 1 in dom p;
then k = 0 by ThSeq10;
then p = <*w*> by D1, FINSEQ_1:57;
then reconsider p as RedSequence of ==>.-relation(S)
by REWRITE1:7;
take p;
thus thesis by D1;
end;
suppose not k + 1 in dom p;
then 0 + 1 > k + 1 by D1, FINSEQ_3:27;
hence thesis by XREAL_1:8;
end;
suppose
D1a: k in dom p & k + 1 in dom p;
then
D1b: [p.k, p.(k + 1)] in ==>.-relation(S \/ T) by REWRITE1:def 2;
set u = p.k;
reconsider u as Element of E^omega by D1b, ZFMISC_1:106;
D1c: u ==>. t, S \/ T by D1, D1b, defRed;
consider p1 being RedSequence of ==>.-relation(S \/ T) such that
D2: len p1 = k & p1.1 = w & p1.len p1 = u by D1, D1a, ThRed10;
consider q being RedSequence of ==>.-relation(S) such that
D3: q.1 = w & q.len q = u by D0, D2;
==>.-relation(S) reduces w, u by D3, REWRITE1:def 3;
then
D3a: w ==>* u, S by defDerivN;
per cases by D1c, ThProd120;
suppose u ==>. t, S;
then u ==>* t, S by ThDerivN20;
then w ==>* t, S by D3a, ThDerivN40;
then ==>.-relation(S) reduces w, t by defDerivN;
hence thesis by REWRITE1:def 3;
end;
suppose u ==>. t, T;
then
D5: u ==>* t, T by ThDerivN20;
u in Lang(w, S) by D3a;
then w ==>* u, T by A1, ThLang10;
then w ==>* t, T by D5, ThDerivN40;
then t in Lang(w, T);
then w ==>* t, S by A1, ThLang10;
then ==>.-relation(S) reduces w, t by defDerivN;
hence thesis by REWRITE1:def 3;
end;
end;
end;
end;
for k holds P[k] from NAT_1:sch 2(C, D);
then consider q being RedSequence of ==>.-relation(S) such that
E: q.1 = w & q.len q = s by B;
thus thesis by E, REWRITE1:def 3;
end;
theorem ThEq69:
S, T are_equivalent_wrt w & w ==>* s, S \/ T implies w ==>* s, S
proof
assume that
A1: S, T are_equivalent_wrt w and
A2: w ==>* s, S \/ T;
==>.-relation(S \/ T) reduces w, s by A2, defDerivN;
then ==>.-relation(S) reduces w, s by A1, ThEq68;
hence thesis by defDerivN;
end;
theorem ThEq70:
S, T are_equivalent_wrt w implies S, S \/ T are_equivalent_wrt w
proof
assume
A: S, T are_equivalent_wrt w;
thus Lang(w, S) = Lang(w, S \/ T)
proof
S c= S \/ T by XBOOLE_1:7;
then
B: Lang(w, S) c= Lang(w, S \/ T) by ThLang20;
Lang(w, S \/ T) c= Lang(w, S)
proof
let x such that
C: x in Lang(w, S \/ T);
reconsider s = x as Element of E^omega by C;
w ==>* s, S \/ T by C, ThLang10;
then w ==>* s, S by A, ThEq69;
hence x in Lang(w, S);
end;
hence thesis by B, XBOOLE_0:def 10;
end;
end;
theorem
s ==>. t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w
proof
assume
A: s ==>. t, S;
S, ==>.-relation(S) are_equivalent_wrt w by ThEq60;
then
B: S, S \/ ==>.-relation(S) are_equivalent_wrt w by ThEq70;
C:
S c= S \/ {[s, t]} by XBOOLE_1:7;
[s, t] in ==>.-relation(S) by A, defRed;
then {[s, t]} c= ==>.-relation(S) by ZFMISC_1:37;
then S \/ {[s, t]} c= S \/ ==>.-relation(S) by XBOOLE_1:9;
hence thesis by B, C, ThEq50;
end;
theorem
s ==>* t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w
proof
assume
A: s ==>* t, S;
S c= S \/ {[s, t]} by XBOOLE_1:7;
then
B: Lang(w, S) c= Lang(w, S \/ {[s, t]}) by ThLang20;
Lang(w, S \/ {[s, t]}) c= Lang(w, S)
proof
let x such that
C: x in Lang(w, S \/ {[s, t]});
reconsider u = x as Element of E^omega by C;
w ==>* u, S \/ {[s, t]} by C, ThLang10;
then w ==>* u, S by A, ThDerivN120;
hence thesis;
end;
hence Lang(w, S) = Lang(w, S \/ {[s, t]}) by B, XBOOLE_0:def 10;
end;
Top
|
Mizar
