:: String Rewriting Systems
:: by Micha{\l} Trybulec
::
:: Received July 17, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, FINSEQ_1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0,
ORDINAL4, REWRITE1, TARSKI, SUBSET_1, FUNCT_1, AFINSQ_1, XBOOLE_0,
ORDINAL2, RELAT_2, PRELAMB, FINSEQ_5, LANG1, CIRCTRM1, REWRITE2,
ORDINAL1, FINSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSET_1, RELAT_1,
DOMAIN_1, XCMPLX_0, NAT_1, FINSEQ_5, FUNCT_1, RELSET_1, XXREAL_0,
AFINSQ_1, RELAT_2, FINSEQ_1, REWRITE1, FLANG_1, LANG1, PARTIT_2;
constructors NAT_1, FINSEQ_5, REWRITE1, FLANG_1, LANG1, XREAL_0, RELSET_1,
PARTIT_2;
registrations NAT_1, AFINSQ_1, REWRITE1, FINSEQ_1, XXREAL_0, XBOOLE_0,
RELAT_1, FUNCT_1, XREAL_0, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities FINSEQ_1;
expansions 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, PARTIT_2, XTUPLE_0;
schemes CLASSES1, NAT_1, RELSET_1;
begin :: Preliminaries: finite sequences.
reserve x for set;
reserve k, l for Nat;
reserve p, q for FinSequence;
theorem Th1:
not k in dom p & k + 1 in dom p implies k = 0
proof
assume that
A1: not k in dom p and
A2: k + 1 in dom p;
A3: k + 1 <= len p by A2,FINSEQ_3:25;
per cases by A1,FINSEQ_3:25;
suppose
k < 1;
hence thesis by NAT_1:14;
end;
suppose
k > len p;
hence thesis by A3,NAT_1:13;
end;
end;
theorem Th2:
k > len p & k <= len (p^q) implies ex l st k = len p + l & l >= 1
& l <= len q
proof
A1: 0 + 1 = 1;
assume that
A2: k > len p and
A3: k <= len (p^q);
consider l such that
A4: k = len p + l by A2,NAT_1:10;
take l;
thus k = len p + l by A4;
len p + l > len p + 0 by A2,A4;
then l > 0;
hence l >= 1 by A1,NAT_1:13;
len p + l <= len p + len q by A3,A4,FINSEQ_1:22;
hence thesis by XREAL_1:6;
end;
:: Preliminaries: reduction sequences.
reserve R for Relation;
reserve p, q for RedSequence of R;
theorem Th3:
k >= 1 implies p | k is RedSequence of R
proof
assume
A1: k >= 1;
per cases;
suppose
k >= len p;
hence thesis by FINSEQ_1:58;
end;
suppose
A2: k < len p;
A3: now
A4: dom (p | k) c= dom p by RELAT_1:60;
let i be Nat such that
A5: i in dom (p | k) & i + 1 in dom (p | k);
(p | k).i = p.i & (p | k).(i + 1) = p.(i + 1) by A5,FUNCT_1:47;
hence [(p | k).i, (p | k).(i + 1)] in R by A5,A4,REWRITE1:def 2;
end;
len (p | k) > 0 by A1,A2,FINSEQ_1:59;
hence thesis by A3,REWRITE1:def 2;
end;
end;
theorem Th4:
k in dom p implies ex q st len q = k & q.1 = p.1 & q.len q = p.k
proof
assume
A1: k in dom p;
set q = p | k;
take q;
A2: 1 <= k by A1,FINSEQ_3:25;
hence q is RedSequence of R by Th3;
k <= len p by A1,FINSEQ_3:25;
hence len q = k by FINSEQ_1:59;
hence thesis by A2,FINSEQ_3:112;
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
:Def1:
x in dom f implies f.x is XFinSequence;
end;
registration
cluster empty -> XFinSequence-yielding for Function;
coherence;
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:2,38;
then x = 1 by TARSKI:def 1;
hence thesis;
end;
end;
registration
let p be XFinSequence-yielding Function;
let x be object;
cluster p.x -> finite Function-like Relation-like;
coherence
proof
per cases;
suppose x in dom p;
hence thesis by Def1;
end;
suppose not x in dom p;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let p be XFinSequence-yielding Function;
let x be object;
cluster p.x -> Sequence-like;
coherence
proof
per cases;
suppose x in dom p;
hence thesis by Def1;
end;
suppose not x in dom p;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
cluster XFinSequence-yielding for FinSequence;
existence
proof
take {};
thus thesis;
end;
end;
registration
let E be set;
cluster -> XFinSequence-yielding for FinSequence of E^omega;
coherence
proof
let f be FinSequence of E^omega;
let x;
assume
A1: x in dom f;
then reconsider x as Nat;
f.x in E^omega by A1,FINSEQ_2:11;
hence thesis;
end;
end;
registration
let p, q be XFinSequence-yielding FinSequence;
cluster p^q -> XFinSequence-yielding;
coherence
proof
now
let x;
assume
A1: x in dom(p^q);
then reconsider x1=x as Nat;
per cases by A1,FINSEQ_1:25;
suppose
x1 in dom p;
then p.x1 = (p^q).x1 by FINSEQ_1:def 7;
hence (p^q).x is XFinSequence;
end;
suppose
ex l being Nat st l in dom q & x1 = len p + l;
then consider l being Nat such that
A2: l in dom q and
A3: x = len p + l;
(p^q).(len p + l) = q.l by A2,FINSEQ_1:def 7;
hence (p^q).x is XFinSequence by A3;
end;
end;
hence thesis;
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
:Def2:
dom it = dom p & for x st x in dom p holds it.x = s^(p.x);
existence
proof
defpred P[object,object] means for x st x = $1 holds $2 = s^(p.x);
A1: for x being object st x in dom p ex y being object st P[x, y]
proof
let x be object;
assume x in dom p;
take s^(p.x);
thus thesis;
end;
consider f being Function such that
A2: dom f = dom p &
for x being object st x in dom p holds P[x, f.x] from CLASSES1:
sch 1(A1);
now
let x;
assume x in dom f;
then f.x = s^(p.x) by A2;
hence f.x is XFinSequence;
end;
then reconsider g = f as XFinSequence-yielding Function by Def1;
take g;
thus thesis by A2;
end;
uniqueness
proof
let f, g be XFinSequence-yielding Function such that
A3: dom f = dom p and
A4: for x st x in dom p holds f.x = s^(p.x) and
A5: dom g = dom p and
A6: for x st x in dom p holds g.x = s^(p.x);
now
let x be object;
assume
A7: x in dom f;
then f.x = s^(p.x) by A3,A4;
hence f.x = g.x by A3,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:2;
end;
func p +^ s -> XFinSequence-yielding Function means
:Def3:
dom it = dom p & for x st x in dom p holds it.x = (p.x)^s;
existence
proof
defpred P[object,object] means for x st x = $1 holds $2 = (p.x)^s;
A8: for x being object st x in dom p ex y being object st P[x, y]
proof
let x be object;
assume x in dom p;
take (p.x)^s;
thus thesis;
end;
consider f being Function such that
A9: dom f = dom p &
for x being object st x in dom p holds P[x, f.x] from CLASSES1
:sch 1(A8);
now
let x;
assume x in dom f;
then f.x = (p.x)^s by A9;
hence f.x is XFinSequence;
end;
then reconsider g = f as XFinSequence-yielding Function by Def1;
take g;
thus thesis by A9;
end;
uniqueness
proof
let f, g be XFinSequence-yielding Function such that
A10: dom f = dom p and
A11: for x st x in dom p holds f.x = (p.x)^s and
A12: dom g = dom p and
A13: for x st x in dom p holds g.x = (p.x)^s;
now
let x be object;
assume
A14: x in dom f;
then f.x = (p.x)^s by A10,A11;
hence f.x = g.x by A10,A13,A14;
end;
hence thesis by A10,A12,FUNCT_1:2;
end;
end;
registration
let s be XFinSequence;
let p be XFinSequence-yielding FinSequence;
cluster s ^+ p -> FinSequence-like;
coherence
proof
consider n being Nat such that
A1: dom p = Seg n by FINSEQ_1:def 2;
dom (s ^+ p) = Seg n by A1,Def2;
hence thesis;
end;
cluster p +^ s -> FinSequence-like;
coherence
proof
consider n being Nat such that
A2: dom p = Seg n by FINSEQ_1:def 2;
dom (p +^ s) = Seg n by A2,Def3;
hence thesis;
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 Th5:
len (s ^+ p) = len p & len(p +^ s) = len p
proof
dom (s ^+ p) = dom p & dom (p +^ s) = dom p by Def2,Def3;
hence thesis by FINSEQ_3:29;
end;
theorem
<%>E ^+ p = p & p +^ <%>E = p
proof
A1: now
let k be Nat;
assume k in dom p;
hence (<%>E ^+ p).k = {}^(p.k) by Def2
.= p.k;
end;
dom (<%>E ^+ p) = dom p by Def2;
hence <%>E ^+ p = p by A1,FINSEQ_1:13;
A2: now
let k be Nat;
assume k in dom p;
hence (p +^ <%>E).k = (p.k)^{} by Def3
.= p.k;
end;
dom (p +^ <%>E) = dom p by Def3;
hence thesis by A2,FINSEQ_1:13;
end;
theorem
s ^+ (t ^+ p) = (s^t) ^+ p & (p +^ t) +^ s = p +^ (t^s)
proof
A1: now
let k be Nat;
assume k in dom (s ^+ (t ^+ p));
then
A2: k in dom (t ^+ p) by Def2;
then
A3: k in dom p by Def2;
thus (s ^+ (t ^+ p)).k = s^((t ^+ p).k) by A2,Def2
.= s^(t^(p.k)) by A3,Def2
.= s^t^(p.k) by AFINSQ_1:27
.= ((s^t) ^+ p).k by A3,Def2;
end;
dom (s ^+ (t ^+ p)) = dom (t ^+ p) by Def2
.= dom p by Def2
.= dom ((s^t) ^+ p) by Def2;
hence s ^+ (t ^+ p) = (s^t) ^+ p by A1,FINSEQ_1:13;
A4: now
let k be Nat;
assume k in dom ((p +^ t) +^ s);
then
A5: k in dom (p +^ t) by Def3;
then
A6: k in dom p by Def3;
thus ((p +^ t) +^ s).k = ((p +^ t).k)^s by A5,Def3
.= (p.k)^t^s by A6,Def3
.= (p.k)^(t^s) by AFINSQ_1:27
.= (p +^ (t^s)).k by A6,Def3;
end;
dom ((p +^ t) +^ s) = dom (p +^ t) by Def3
.= dom p by Def3
.= dom (p +^ (t^s)) by Def3;
hence thesis by A4,FINSEQ_1:13;
end;
theorem
s ^+ (p +^ t) = (s ^+ p) +^ t
proof
A1: now
let k be Nat;
assume k in dom (s ^+ (p +^ t));
then
A2: k in dom (p +^ t) by Def2;
then
A3: k in dom p by Def3;
then
A4: k in dom (s ^+ p) by Def2;
thus (s ^+ (p +^ t)).k = s^((p +^ t).k) by A2,Def2
.= s^((p.k)^t) by A3,Def3
.= s^(p.k)^t by AFINSQ_1:27
.= ((s ^+ p).k)^t by A3,Def2
.= ((s ^+ p) +^ t).k by A4,Def3;
end;
dom (s ^+ (p +^ t)) = dom (p +^ t) by Def2
.= dom p by Def3
.= dom (s ^+ p) by Def2
.= dom ((s ^+ p) +^ t) by Def3;
hence thesis by A1,FINSEQ_1:13;
end;
theorem
s ^+ (p^q) = (s ^+ p)^(s ^+ q) & (p^q) +^ s = (p +^ s)^(q +^ s)
proof
A1: now
let k be Nat;
assume
A2: k in dom (s ^+ (p^q));
then
A3: k in dom (p^q) by Def2;
now
per cases;
suppose
A4: k in dom p;
then
A5: k in dom (s ^+ p) by Def2;
thus (s ^+ (p^q)).k = s^((p^q).k) by A3,Def2
.= s^(p.k) by A4,FINSEQ_1:def 7
.= (s ^+ p).k by A4,Def2
.= ((s ^+ p)^(s ^+ q)).k by A5,FINSEQ_1:def 7;
end;
suppose
A6: not k in dom p;
A7: k <= len (p^q) by A3,FINSEQ_3:25;
k < 1 or k > len p by A6,FINSEQ_3:25;
then consider i being Nat such that
A8: k = len p + i and
A9: i >= 1 & i <= len q by A2,A7,Th2,FINSEQ_3:25;
A10: i in dom q by A9,FINSEQ_3:25;
then
A11: i in dom (s ^+ q) by Def2;
A12: len (s ^+ p) = len p by Th5;
thus (s ^+ (p^q)).k = s^((p^q).(len p + i)) by A3,A8,Def2
.= s^(q.i) by A10,FINSEQ_1:def 7
.= (s ^+ q).i by A10,Def2
.= ((s ^+ p)^(s ^+ q)).k by A8,A11,A12,FINSEQ_1:def 7;
end;
end;
hence (s ^+ (p^q)).k = ((s ^+ p)^(s ^+ q)).k;
end;
len (s ^+ (p^q)) = len (p^q) by Th5
.= len p + len q by FINSEQ_1:22
.= len (s ^+ p) + len q by Th5
.= len (s ^+ p) + len (s ^+ q) by Th5
.= len ((s ^+ p)^(s ^+ q)) by FINSEQ_1:22;
then dom (s ^+ (p^q)) = dom ((s ^+ p)^(s ^+ q)) by FINSEQ_3:29;
hence s ^+ (p^q) = (s ^+ p)^(s ^+ q) by A1,FINSEQ_1:13;
A13: now
let k be Nat;
assume
A14: k in dom ((p^q) +^ s);
then
A15: k in dom (p^q) by Def3;
now
per cases;
suppose
A16: k in dom p;
then
A17: k in dom (p +^ s) by Def3;
thus ((p^q) +^ s).k = ((p^q).k)^s by A15,Def3
.= (p.k)^s by A16,FINSEQ_1:def 7
.= (p +^ s).k by A16,Def3
.= ((p +^ s)^(q +^ s)).k by A17,FINSEQ_1:def 7;
end;
suppose
A18: not k in dom p;
A19: k <= len (p^q) by A15,FINSEQ_3:25;
k < 1 or k > len p by A18,FINSEQ_3:25;
then consider i being Nat such that
A20: k = len p + i and
A21: i >= 1 & i <= len q by A14,A19,Th2,FINSEQ_3:25;
A22: i in dom q by A21,FINSEQ_3:25;
then
A23: i in dom (q +^ s) by Def3;
A24: len (p +^ s) = len p by Th5;
thus ((p^q) +^ s).k = ((p^q).(len p + i))^s by A15,A20,Def3
.= (q.i)^s by A22,FINSEQ_1:def 7
.= (q +^ s).i by A22,Def3
.= ((p +^ s)^(q +^ s)).k by A20,A23,A24,FINSEQ_1:def 7;
end;
end;
hence ((p^q) +^ s).k = ((p +^ s)^(q +^ s)).k;
end;
len ((p^q) +^ s) = len (p^q) by Th5
.= len p + len q by FINSEQ_1:22
.= len (p +^ s) + len q by Th5
.= len (p +^ s) + len (q +^ s) by Th5
.= len ((p +^ s)^(q +^ s)) by FINSEQ_1:22;
then dom ((p^q) +^ s) = dom ((p +^ s)^(q +^ s)) by FINSEQ_3:29;
hence thesis by A13,FINSEQ_1:13;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
k in dom p;
hence thesis by FINSEQ_2:11;
end;
suppose
not k in dom p;
then p.k = {} by FUNCT_1:def 2;
then p.k is XFinSequence of E by AFINSQ_1:16;
hence thesis by AFINSQ_1:def 7;
end;
end;
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; :: redefines ^+ (REWRITE2, definition)
coherence
proof
now
let i be Nat;
assume i in dom (s ^+ p);
then i in dom p by Def2;
then (s ^+ p).i = s^(p.i) by Def2;
hence (s ^+ p).i in E^omega;
end;
hence thesis by FINSEQ_2:12;
end;
redefine func p +^ s -> FinSequence of E^omega; :: redefines +^ (REWRITE2, definition)
coherence
proof
now
let i be Nat;
assume i in dom (p +^ s);
then i in dom p by Def3;
then (p +^ s).i = (p.i)^s by Def3;
hence (p +^ s).i in E^omega;
end;
hence thesis by FINSEQ_2:12;
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:23
.= (S \/ S~)~;
hence thesis by RELAT_2:13;
end;
end;
registration
let E;
cluster symmetric for semi-Thue-system of E;
existence
proof
set S = the semi-Thue-system of E;
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 for FinSequence of E^omega;
definition
let E, S, s, t;
pred s -->. t, S means
[s, t] in S;
end;
definition
let E, S, s, t;
pred s ==>. t, S means
ex v, w, s1, t1 st s = v^s1^w & t = v^t1^w & s1 -->. t1, S;
end;
theorem Th10:
s -->. t, S implies s ==>. t, S
proof
assume
A1: s -->. t, S;
take e = <%>E;
A2: t = {}^t^{}
.= e^t^e;
s = {}^s^{}
.= e^s^e;
hence thesis by A1,A2;
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
A1: s = v^s1^w and
A2: s = v^t1^w and
A3: s1 -->. t1, S;
v^s1 = v^t1 by A1,A2,AFINSQ_1:28;
then s1 = t1 by AFINSQ_1:28;
hence thesis by A1,A3;
end;
theorem Th12:
s ==>. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S
proof
given v, w, s1, t1 such that
A1: s = v^s1^w and
A2: t = v^t1^w and
A3: s1 -->. t1, S;
A4: u^t = u^(v^t1)^w by A2,AFINSQ_1:27
.= u^v^t1^w by AFINSQ_1:27;
u^s = u^(v^s1)^w by A1,AFINSQ_1:27
.= u^v^s1^w by AFINSQ_1:27;
hence u^s ==>. u^t, S by A3,A4;
s^u = v^s1^(w^u) & t^u = v^t1^(w^u) by A1,A2,AFINSQ_1:27;
hence thesis by A3;
end;
theorem Th13:
s ==>. t, S implies u^s^v ==>. u^t^v, S
proof
assume s ==>. t, S;
then u^s ==>. u^t, S by Th12;
hence thesis by Th12;
end;
theorem
s -->. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S
proof
assume s -->. t, S;
then s ==>. t, S by Th10;
hence thesis by Th12;
end;
theorem
s -->. t, S implies u^s^v ==>. u^t^v, S;
theorem Th16:
S is Thue-system of E & s -->. t, S implies t -->. s, S
proof
assume S is Thue-system of E & s -->. t, S;
then S = S~ & [s, t] in S by RELAT_2:13;
then [t, s] in S by RELAT_1:def 7;
hence thesis;
end;
theorem Th17:
S is Thue-system of E & s ==>. t, S implies t ==>. s, S
by Th16;
theorem
S c= T & s -->. t, S implies s -->.t, T;
theorem Th19:
S c= T & s ==>. t, S implies s ==>.t, T
proof
assume that
A1: S c= T and
A2: s ==>. t, S;
consider v, w, s1, t1 such that
A3: s = v^s1^w & t = v^t1^w and
A4: s1 -->. t1, S by A2;
s1 -->. t1, T by A1,A4;
hence thesis by A3;
end;
theorem Th20:
not s ==>. t, {}(E^omega, E^omega)
proof
assume s ==>. t, {}(E^omega, E^omega);
then consider v, w, s1, t1 such that
s = v^s1^w and
t = v^t1^w and
A1: s1 -->. t1, {}(E^omega, E^omega);
[s1, t1] in {}(E^omega, E^omega) by A1;
hence contradiction by PARTIT_2:def 1;
end;
theorem Th21:
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
A1: s = v^s1^w & t = v^t1^w and
A2: s1 -->. t1, S \/ T;
A3: [s1, t1] in S \/ T by A2;
per cases by A3,XBOOLE_0:def 3;
suppose
[s1, t1] in S;
then s1 -->. t1, S;
hence thesis by A1;
end;
suppose
[s1, t1] in T;
then s1 -->. t1, T;
hence thesis by A1;
end;
end;
begin
:: ==>.-relation is introduced to define derivations
:: using concepts from REWRITE1.
definition
let E;
redefine func id E -> Relation of E; :: redefines id (RELAT_1, definition)
coherence by RELSET_1:14;
end;
definition
let E, S;
func ==>.-relation(S) -> Relation of E^omega means
:Def6:
[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
A1: 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 A1;
end;
uniqueness
proof
let R1, R2 be Relation of E^omega such that
A2: for s, t being Element of E^omega holds [s, t] in R1 iff s ==>. t, S and
A3: for s, t being Element of E^omega holds [s, t] in R2 iff s ==>. t, S;
for s,t being Element of E^omega holds [s, t] in R1 iff [s, t] in R2
by A2,A3;
hence thesis by RELSET_1:def 2;
end;
end;
theorem Th22:
S c= ==>.-relation(S)
proof
let x be object;
assume
A1: x in S;
then consider a, b being object such that
A2: a in E^omega & b in E^omega and
A3: x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by A2;
a -->. b, S by A1,A3;
then a ==>.b, S by Th10;
hence thesis by A3,Def6;
end;
theorem Th23:
p is RedSequence of ==>.-relation(S) implies p +^ u is
RedSequence of ==>.-relation(S) & u ^+ p is RedSequence of ==>.-relation(S)
proof
assume
A1: p is RedSequence of ==>.-relation(S);
A2: now
let i being Nat such that
A3: i in dom (p +^ u) and
A4: (i + 1) in dom (p +^ u);
A5: (i + 1) in dom p by A4,Def3;
then
A6: (p +^ u).(i + 1) = (p.(i + 1))^u by Def3;
A7: i in dom p by A3,Def3;
then [p.i, p.(i + 1)] in ==>.-relation(S) by A1,A5,REWRITE1:def 2;
then p.i ==>. p.(i + 1), S by Def6;
then
A8: (p.i)^u ==>. (p.(i + 1))^u, S by Th12;
(p +^ u).i = (p.i)^u by A7,Def3;
hence [(p +^ u).i, (p +^ u).(i + 1)] in ==>.-relation(S) by A6,A8,Def6;
end;
A9: now
let i being Nat such that
A10: i in dom (u ^+ p) and
A11: (i + 1) in dom (u ^+ p);
A12: (i + 1) in dom p by A11,Def2;
then
A13: (u ^+ p).(i + 1) = u^(p.(i + 1)) by Def2;
A14: i in dom p by A10,Def2;
then [p.i, p.(i + 1)] in ==>.-relation(S) by A1,A12,REWRITE1:def 2;
then p.i ==>. p.(i + 1), S by Def6;
then
A15: u^(p.i) ==>. u^(p.(i + 1)), S by Th12;
(u ^+ p).i = u^(p.i) by A14,Def2;
hence [(u ^+ p).i, (u ^+ p).(i + 1)] in ==>.-relation(S) by A13,A15,Def6;
end;
len (p +^ u) = len p by Th5;
hence p +^ u is RedSequence of ==>.-relation(S) by A1,A2,REWRITE1:def 2;
len (u ^+ p) = len p by Th5;
hence thesis by A1,A9,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 Th23;
hence thesis by Th23;
end;
theorem Th25:
S is Thue-system of E implies ==>.-relation(S) = (==>.-relation( S))~
proof
assume
A1: S is Thue-system of E;
now
let x be object;
thus x in ==>.-relation(S) implies x in (==>.-relation(S))~
proof
assume
A2: x in ==>.-relation(S);
then consider a, b being object such that
A3: a in E^omega & b in E^omega and
A4: x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by A3;
a ==>. b, S by A2,A4,Def6;
then b ==>. a, S by A1,Th17;
then [b, a] in ==>.-relation(S) by Def6;
hence thesis by A4,RELAT_1:def 7;
end;
thus x in (==>.-relation(S))~ implies x in ==>.-relation(S)
proof
assume
A5: x in (==>.-relation(S))~;
then consider a, b being object such that
A6: a in E^omega & b in E^omega and
A7: x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by A6;
[b, a] in ==>.-relation(S) by A5,A7,RELAT_1:def 7;
then b ==>. a, S by Def6;
then a ==>. b, S by A1,Th17;
hence thesis by A7,Def6;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th26:
S c= T implies ==>.-relation(S) c= ==>.-relation(T)
proof
assume
A1: S c= T;
let x be object;
assume
A2: x in ==>.-relation(S);
then consider s, t being object such that
A3: x = [s, t] and
A4: s in E^omega & t in E^omega by RELSET_1:2;
reconsider s, t as Element of E^omega by A4;
s ==>. t, S by A2,A3,Def6;
then s ==>. t, T by A1,Th19;
hence thesis by A3,Def6;
end;
theorem Th27:
==>.-relation(id (E^omega)) = id (E^omega)
proof
A1: ==>.-relation(id (E^omega)) c= id (E^omega)
proof
let x be object;
assume
A2: x in ==>.-relation(id (E^omega));
then consider a, b being object such that
A3: a in E^omega & b in E^omega and
A4: x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by A3;
a ==>. b, id (E^omega) by A2,A4,Def6;
then consider v, w, s1, t1 such that
A5: a = v^s1^w & b = v^t1^w and
A6: s1 -->. t1, id (E^omega);
[s1, t1] in id (E^omega) by A6;
then s1 = t1 by RELAT_1:def 10;
hence thesis by A4,A5,RELAT_1:def 10;
end;
id (E^omega) c= ==>.-relation(id (E^omega)) by Th22;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th28:
==>.-relation(S \/ id (E^omega)) = ==>.-relation(S) \/ id (E ^omega)
proof
A1: ==>.-relation(S \/ id (E^omega)) c= ==>.-relation(S) \/ id (E^omega)
proof
let x be object;
assume
A2: x in ==>.-relation(S \/ id (E^omega));
then consider a, b being object such that
A3: a in E^omega & b in E^omega and
A4: x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by A3;
a ==>. b, S \/ id (E^omega) by A2,A4,Def6;
then consider v, w, s1, t1 such that
A5: a = v^s1^w & b = v^t1^w and
A6: s1 -->. t1, S \/ id (E^omega);
A7: [s1, t1] in S \/ id (E^omega) by A6;
per cases by A7,XBOOLE_0:def 3;
suppose
[s1, t1] in S;
then s1 -->. t1, S;
then v^s1^w ==>. v^t1^w, S;
then x in ==>.-relation(S) by A4,A5,Def6;
hence thesis by XBOOLE_0:def 3;
end;
suppose
[s1, t1] in id (E^omega);
then s1 = t1 by RELAT_1:def 10;
then x in id (E^omega) by A4,A5,RELAT_1:def 10;
hence thesis by XBOOLE_0:def 3;
end;
end;
==>.-relation(S) \/ id (E^omega) c= ==>.-relation(S \/ id (E^omega))
proof
let x be object;
assume
A8: x in ==>.-relation(S) \/ id (E^omega);
per cases by A8,XBOOLE_0:def 3;
suppose
A9: x in ==>.-relation(S);
==>.-relation(S) c= ==>.-relation(S \/ id (E^omega)) by Th26,XBOOLE_1:7;
hence thesis by A9;
end;
suppose
A10: x in id (E^omega);
A11: ==>.-relation(id (E^omega)) c= ==>.-relation(S \/ id (E^omega)) by Th26,
XBOOLE_1:7;
x in ==>.-relation(id (E^omega)) by A10,Th27;
hence thesis by A11;
end;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th29:
==>.-relation({}(E^omega, E^omega)) = {}(E^omega, E^omega)
proof
A1: ==>.-relation({}(E^omega, E^omega)) c= {}(E^omega, E^omega)
proof
let x be object;
assume
A2: x in ==>.-relation({}(E^omega, E^omega));
then consider a, b being object such that
A3: a in E^omega & b in E^omega and
A4: x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by A3;
a ==>. b, {}(E^omega, E^omega) by A2,A4,Def6;
hence thesis by Th20;
end;
{}(E^omega, E^omega) = {} by PARTIT_2:def 1;
then {}(E^omega, E^omega) c= ==>.-relation({}(E^omega, E^omega));
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th30:
s ==>. t, ==>.-relation(S) implies s ==>. t, S
proof
assume s ==>. t, ==>.-relation(S);
then consider v, w, s1, t1 such that
A1: s = v^s1^w & t = v^t1^w and
A2: s1 -->. t1, ==>.-relation(S);
[s1, t1] in ==>.-relation(S) by A2;
then s1 ==>. t1, S by Def6;
hence thesis by A1,Th13;
end;
theorem Th31:
==>.-relation(==>.-relation(S)) = ==>.-relation(S)
proof
A1: ==>.-relation(==>.-relation(S)) c= ==>.-relation(S)
proof
let x be object;
assume
A2: x in ==>.-relation(==>.-relation(S));
then consider a, b being object such that
A3: a in E^omega & b in E^omega and
A4: x = [a, b] by ZFMISC_1:def 2;
reconsider a, b as Element of E^omega by A3;
a ==>. b, ==>.-relation(S) by A2,A4,Def6;
then a ==>. b, S by Th30;
hence thesis by A4,Def6;
end;
==>.-relation(S) c= ==>.-relation(==>.-relation(S)) by Th22;
hence thesis by A1,XBOOLE_0:def 10;
end;
begin :: Derivations.
definition
let E, S, s, t;
pred s ==>* t, S means
==>.-relation(S) reduces s, t;
end;
theorem Th32:
s ==>* s, S
by REWRITE1:12;
theorem Th33:
s ==>. t, S implies s ==>* t, S
proof
assume s ==>. t, S;
then [s, t] in ==>.-relation(S) by Def6;
then ==>.-relation(S) reduces s, t by REWRITE1:15;
hence thesis;
end;
theorem
s -->. t, S implies s ==>* t, S by Th10,Th33;
theorem Th35:
s ==>* t, S & t ==>* u, S implies s ==>* u, S
by REWRITE1:16;
theorem Th36:
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;
then consider p being RedSequence of ==>.-relation(S) such that
A1: p.1 = s and
A2: p.(len p) = t by REWRITE1:def 3;
reconsider p as FinSequence of E^omega by A1,ABCMIZ_0:73;
1 in dom p by FINSEQ_5:6;
then
A3: (p +^ u).1 = s^u by A1,Def3;
A4: len p = len (p +^ u) by Th5;
then len (p +^ u) in dom p by FINSEQ_5:6;
then
A5: (p +^ u).(len (p +^ u)) = t^u by A2,A4,Def3;
p +^ u is RedSequence of ==>.-relation(S) by Th23;
then ==>.-relation(S) reduces s^u, t^u by A3,A5,REWRITE1:def 3;
hence s^u ==>* t^u, S;
1 in dom p by FINSEQ_5:6;
then
A6: (u ^+ p).1 = u^s by A1,Def2;
A7: len p = len (u ^+ p) by Th5;
then len (u ^+ p) in dom p by FINSEQ_5:6;
then
A8: (u ^+ p).(len (u ^+ p)) = u^t by A2,A7,Def2;
u ^+ p is RedSequence of ==>.-relation(S) by Th23;
then ==>.-relation(S) reduces u^s, u^t by A6,A8,REWRITE1:def 3;
hence thesis;
end;
theorem Th37:
s ==>* t, S implies u^s^v ==>* u^t^v, S
proof
assume s ==>* t, S;
then u^s ==>* u^t, S by Th36;
hence thesis by Th36;
end;
theorem
s ==>* t, S & u ==>* v, S implies s^u ==>* t^v, S & u^s ==>* v^t, S
proof
assume
A1: s ==>* t, S & u ==>* v, S;
then s^u ==>* t^u, S & t^u ==>* t^v, S by Th36;
hence s^u ==>* t^v, S by Th35;
u^s ==>* u^t, S & u^t ==>* v^t, S by A1,Th36;
hence thesis by Th35;
end;
theorem
S is Thue-system of E & s ==>* t, S implies t ==>* s, S
proof
assume that
A1: S is Thue-system of E and
A2: s ==>* t, S;
==>.-relation(S) reduces s, t by A2;
then consider p being RedSequence of ==>.-relation(S) such that
A3: p.1 = s and
A4: p.(len p) = t by REWRITE1:def 3;
set q = Rev p;
q.(len p) = s by A3,FINSEQ_5:62;
then
A5: q.(len q) = s by FINSEQ_5:def 3;
q is RedSequence of (==>.-relation(S))~ by REWRITE1:9;
then
A6: q is RedSequence of ==>.-relation(S) by A1,Th25;
q.1 = t by A4,FINSEQ_5:62;
then ==>.-relation(S) reduces t, s by A6,A5,REWRITE1:def 3;
hence thesis;
end;
theorem Th40:
S c= T & s ==>* t, S implies s ==>* t, T
by Th26,REWRITE1:22;
theorem Th41:
s ==>* t, S iff s ==>* t, S \/ id (E^omega)
proof
thus s ==>* t, S implies s ==>* t, S \/ id (E^omega) by Th40,XBOOLE_1:7;
assume s ==>* t, S \/ id (E^omega);
then ==>.-relation(S \/ id (E^omega)) reduces s, t;
then ==>.-relation(S) \/ id (E^omega) reduces s, t by Th28;
then ==>.-relation(S) reduces s, t by REWRITE1:23;
hence thesis;
end;
theorem Th42:
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;
then {}(E^omega, E^omega) reduces s, t by Th29;
then {} reduces s, t by PARTIT_2:def 1;
hence thesis by REWRITE1:13;
end;
theorem Th43:
s ==>* t, ==>.-relation(S) implies s ==>* t, S
by Th31;
theorem Th44:
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
A3: u = u1^s1^v1 & v = u1^t1^v1 and
A4: s1 -->. t1, {[s, t]} by A2;
[s1, t1] in {[s, t]} by A4;
then [s1, t1] = [s, t] by TARSKI:def 1;
then s1 = s & t1 = t by XTUPLE_0:1;
hence thesis by A1,A3,Th37;
end;
theorem Th45:
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;
then
A3: ex p2 being RedSequence of ==>.-relation(S \/ {[s, t]}) st 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;
A4: now
let k;
assume
A5: P[k];
thus P[k + 1]
proof
let p be RedSequence of ==>.-relation(S \/ {[s, t]}), s1, t1 such that
A6: len p = k + 1 and
A7: p.1 = s1 and
A8: p.len p = t1;
per cases;
suppose
not k in dom p & k + 1 in dom p;
then k = 0 by Th1;
then p = <*s1*> by A6,A7,FINSEQ_1:40;
then reconsider p as RedSequence of ==>.-relation(S) by REWRITE1:6;
take p;
thus thesis by A7,A8;
end;
suppose
not k + 1 in dom p;
then 0 + 1 > k + 1 by A6,FINSEQ_3:25;
hence thesis by XREAL_1:6;
end;
suppose
A9: k in dom p & k + 1 in dom p;
set w = p.k;
A10: [p.k, p.(k + 1)] in ==>.-relation(S \/ {[s, t]}) by A9,REWRITE1:def 2;
then reconsider w as Element of E^omega by ZFMISC_1:87;
A11: w ==>. t1, S \/ {[s, t]} by A6,A8,A10,Def6;
A12: w ==>* t1, S
proof
per cases by A11,Th21;
suppose
w ==>. t1, S;
hence thesis by Th33;
end;
suppose
w ==>. t1, {[s, t]};
hence thesis by A1,Th44;
end;
end;
ex p1 being RedSequence of ==>.-relation(S \/ {[s, t]}) st len p1
= k & p1.1 = s1 & p1.len p1 = w by A7,A9,Th4;
then
ex q being RedSequence of ==>.-relation(S) st q.1 = s1 & q.len q =
w by A5;
then ==>.-relation(S) reduces s1, w by REWRITE1:def 3;
then s1 ==>* w, S;
then s1 ==>* t1, S by A12,Th35;
then ==>.-relation(S) reduces s1, t1;
hence thesis by REWRITE1:def 3;
end;
end;
end;
A13: P[0] by REWRITE1:def 2;
for k holds P[k] from NAT_1:sch 2(A13, A4);
then ex q being RedSequence of ==>.-relation(S) st q.1 = u & q.len q = v by
A3;
then ==>.-relation(S) reduces u, v by REWRITE1:def 3;
hence thesis;
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 be object;
assume x in X;
then ex t st t = x & w ==>* t, S;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th46:
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 Th47:
w in Lang(w, S)
proof
w ==>* w, S by Th32;
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 Th47;
end;
theorem Th48:
S c= T implies Lang(w, S) c= Lang(w, T)
proof
assume
A1: S c= T;
let x be object;
assume
A2: x in Lang(w, S);
then reconsider y = x as Element of E^omega;
w ==>* y, S by A2,Th46;
then w ==>* y, T by A1,Th40;
hence thesis;
end;
theorem Th49:
Lang(w, S) = Lang(w, S \/ id (E^omega))
proof
A1: Lang(w, S \/ id (E^omega)) c= Lang(w, S)
proof
let x be object;
assume
A2: x in Lang(w, S \/ id (E^omega));
then reconsider s = x as Element of E^omega;
w ==>* s, S \/ id (E^omega) by A2,Th46;
then w ==>* s, S by Th41;
hence thesis;
end;
Lang(w, S) c= Lang(w, S \/ id (E^omega)) by Th48,XBOOLE_1:7;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th50:
Lang(w, {}(E^omega, E^omega)) = {w}
proof
for x holds not(x <> w & x in Lang(w, {}(E^omega, E^omega))) by Th46,Th42;
then for x be object holds x in Lang(w, {}(E^omega, E^omega)) iff x = w
by Th47;
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 PARTIT_2:def 1
.= id (E^omega);
hence Lang(w, id (E^omega)) = Lang(w, {}(E^omega, E^omega)) by Th49
.= {w} by Th50;
end;
begin :: Equivalence of semi-Thue systems.
definition
let E, S, T, w;
pred S, T are_equivalent_wrt w means
Lang(w, S) = Lang(w, T);
end;
theorem
S, S are_equivalent_wrt w;
theorem
S, T are_equivalent_wrt w implies T, S are_equivalent_wrt w;
theorem
S, T are_equivalent_wrt w & T, U are_equivalent_wrt w implies S, U
are_equivalent_wrt w;
theorem
S, S \/ id (E^omega) are_equivalent_wrt w
by Th49;
theorem Th56:
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,Th48;
hence Lang(w, S) = Lang(w, U) by A1,XBOOLE_0:def 10;
hence thesis by A1;
end;
theorem Th57:
S, ==>.-relation(S) are_equivalent_wrt w
proof
A1: Lang(w, ==>.-relation(S)) c= Lang(w, S)
proof
let x be object such that
A2: x in Lang(w, ==>.-relation(S));
reconsider s = x as Element of E^omega by A2;
w ==>* s, ==>.-relation(S) by A2,Th46;
then w ==>* s, S by Th43;
hence thesis;
end;
Lang(w, S) c= Lang(w, ==>.-relation(S)) by Th22,Th48;
hence Lang(w, S) = Lang(w, ==>.-relation(S)) by A1,XBOOLE_0:def 10;
end;
theorem Th58:
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;
A3: ex p being RedSequence of ==>.-relation(S \/ T) st 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;
A4: now
let k;
assume
A5: P[k];
thus P[k + 1]
proof
let p be RedSequence of ==>.-relation(S \/ T), t such that
A6: len p = k + 1 and
A7: p.1 = w and
A8: p.len p = t;
per cases;
suppose
not k in dom p & k + 1 in dom p;
then k = 0 by Th1;
then p = <*w*> by A6,A7,FINSEQ_1:40;
then reconsider p as RedSequence of ==>.-relation(S) by REWRITE1:6;
take p;
thus thesis by A7,A8;
end;
suppose
not k + 1 in dom p;
then 0 + 1 > k + 1 by A6,FINSEQ_3:25;
hence thesis by XREAL_1:6;
end;
suppose
A9: k in dom p & k + 1 in dom p;
set u = p.k;
A10: [p.k, p.(k + 1)] in ==>.-relation(S \/ T) by A9,REWRITE1:def 2;
then reconsider u as Element of E^omega by ZFMISC_1:87;
A11: u ==>. t, S \/ T by A6,A8,A10,Def6;
ex p1 being RedSequence of ==>.-relation(S \/ T) st len p1 = k &
p1.1 = w & p1.len p1 = u by A7,A9,Th4;
then ex q being RedSequence of ==>.-relation(S) st q.1 = w & q.len q =
u by A5;
then ==>.-relation(S) reduces w, u by REWRITE1:def 3;
then
A12: w ==>* u, S;
per cases by A11,Th21;
suppose
u ==>. t, S;
then u ==>* t, S by Th33;
then w ==>* t, S by A12,Th35;
then ==>.-relation(S) reduces w, t;
hence thesis by REWRITE1:def 3;
end;
suppose
A13: u ==>. t, T;
u in Lang(w, S) by A12;
then
A14: w ==>* u, T by A1,Th46;
u ==>* t, T by A13,Th33;
then w ==>* t, T by A14,Th35;
then t in Lang(w, T);
then w ==>* t, S by A1,Th46;
then ==>.-relation(S) reduces w, t;
hence thesis by REWRITE1:def 3;
end;
end;
end;
end;
A15: P[0] by REWRITE1:def 2;
for k holds P[k] from NAT_1:sch 2(A15, A4);
then ex q being RedSequence of ==>.-relation(S) st q.1 = w & q.len q = s by
A3;
hence thesis by REWRITE1:def 3;
end;
theorem Th59:
S, T are_equivalent_wrt w & w ==>* s, S \/ T implies w ==>* s, S
by Th58;
theorem Th60:
S, T are_equivalent_wrt w implies S, S \/ T are_equivalent_wrt w
proof
assume
A1: S, T are_equivalent_wrt w;
A2: Lang(w, S \/ T) c= Lang(w, S)
proof
let x be object such that
A3: x in Lang(w, S \/ T);
reconsider s = x as Element of E^omega by A3;
w ==>* s, S \/ T by A3,Th46;
then w ==>* s, S by A1,Th59;
hence thesis;
end;
Lang(w, S) c= Lang(w, S \/ T) by Th48,XBOOLE_1:7;
hence Lang(w, S) = Lang(w, S \/ T) by A2,XBOOLE_0:def 10;
end;
theorem
s ==>. t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w
proof
assume s ==>. t, S;
then [s, t] in ==>.-relation(S) by Def6;
then {[s, t]} c= ==>.-relation(S) by ZFMISC_1:31;
then
A1: S \/ {[s, t]} c= S \/ ==>.-relation(S) by XBOOLE_1:9;
S, S \/ ==>.-relation(S) are_equivalent_wrt w & S c= S \/ {[s, t]} by Th57
,Th60,XBOOLE_1:7;
hence thesis by A1,Th56;
end;
theorem
s ==>* t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w
proof
assume
A1: s ==>* t, S;
A2: Lang(w, S \/ {[s, t]}) c= Lang(w, S)
proof
let x be object such that
A3: x in Lang(w, S \/ {[s, t]});
reconsider u = x as Element of E^omega by A3;
w ==>* u, S \/ {[s, t]} by A3,Th46;
then w ==>* u, S by A1,Th45;
hence thesis;
end;
Lang(w, S) c= Lang(w, S \/ {[s, t]}) by Th48,XBOOLE_1:7;
hence Lang(w, S) = Lang(w, S \/ {[s, t]}) by A2,XBOOLE_0:def 10;
end;