:: String Rewriting Systems
:: by Micha{\l} Trybulec
::
:: Received July 17, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: REWRITE2:1
for k being Nat
for p being FinSequence st not k in dom p & k + 1 in dom p holds
k = 0
proofend;

theorem Th2: :: REWRITE2:2
for k being Nat
for p, q being FinSequence st k > len p &amp; k <= len (p ^ q) holds
ex l being Nat st
( k = (len p) + l &amp; l >= 1 &amp; l <= len q )
proofend;

theorem Th3: :: REWRITE2:3
for k being Nat
for R being Relation
for p being RedSequence of R st k >= 1 holds
p | k is RedSequence of R
proofend;

theorem Th4: :: REWRITE2:4
for k being Nat
for R being Relation
for p being RedSequence of R st k in dom p holds
ex q being RedSequence of R st
( len q = k &amp; q . 1 = p . 1 &amp; q . (len q) = p . k )
proofend;

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;
attrf is XFinSequence-yielding  means :Def1: :: REWRITE2:def 1
 for x being set st x in dom f holds
f . x is XFinSequence;
end;

:: deftheorem Def1 defines XFinSequence-yielding REWRITE2:def_1_:_
 for f being Function holds
( f is XFinSequence-yielding iff for x being set st x in dom f holds
f . x is XFinSequence );

registration
cluster empty Relation-like Function-like  ->  XFinSequence-yielding for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is XFinSequence-yielding
proofend;
end;

registration
let f be XFinSequence;
cluster<*f*> ->  XFinSequence-yielding ;
coherence
 <*f*> is XFinSequence-yielding
proofend;
end;

registration
let p be XFinSequence-yielding Function;
let x be set ;
clusterp . x ->  Relation-like Function-like finite ;
coherence
 ( p . x is finite &amp; p . x is Function-like &amp; p . x is Relation-like )
proofend;
end;

registration
let p be XFinSequence-yielding Function;
let x be set ;
clusterp . x ->  T-Sequence-like ;
coherence
 p . x is T-Sequence-like
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding for set ;
existence
 ex b1 being FinSequence st b1 is XFinSequence-yielding
proofend;
end;

registration
let E be set ;
cluster  ->  XFinSequence-yielding for FinSequence of E ^omega ;
coherence
 for b1 being FinSequence of E ^omega holds b1 is XFinSequence-yielding
proofend;
end;

registration
let p, q be XFinSequence-yielding FinSequence;
clusterp ^ q ->  XFinSequence-yielding ;
coherence
 p ^ q is XFinSequence-yielding
proofend;
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;
funcs ^+ p ->  XFinSequence-yielding Function means :Def2: :: REWRITE2:def 2
( dom it = dom p &amp; ( for x being set st x in dom p holds
it . x = s ^ (p . x) ) );
existence
 ex b1 being XFinSequence-yielding Function st
( dom b1 = dom p &amp; ( for x being set st x in dom p holds
b1 . x = s ^ (p . x) ) )
proofend;
uniqueness
 for b1, b2 being XFinSequence-yielding Function st dom b1 = dom p &amp; ( for x being set st x in dom p holds
b1 . x = s ^ (p . x) ) &amp; dom b2 = dom p &amp; ( for x being set st x in dom p holds
b2 . x = s ^ (p . x) ) holds
b1 = b2
proofend;
funcp +^ s ->  XFinSequence-yielding Function means :Def3: :: REWRITE2:def 3
( dom it = dom p &amp; ( for x being set st x in dom p holds
it . x = (p . x) ^ s ) );
existence
 ex b1 being XFinSequence-yielding Function st
( dom b1 = dom p &amp; ( for x being set st x in dom p holds
b1 . x = (p . x) ^ s ) )
proofend;
uniqueness
 for b1, b2 being XFinSequence-yielding Function st dom b1 = dom p &amp; ( for x being set st x in dom p holds
b1 . x = (p . x) ^ s ) &amp; dom b2 = dom p &amp; ( for x being set st x in dom p holds
b2 . x = (p . x) ^ s ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ^+ REWRITE2:def_2_:_
 for s being XFinSequence
for p, b3 being XFinSequence-yielding Function holds
( b3 = s ^+ p iff ( dom b3 = dom p &amp; ( for x being set st x in dom p holds
b3 . x = s ^ (p . x) ) ) );

:: deftheorem Def3 defines +^ REWRITE2:def_3_:_
 for s being XFinSequence
for p, b3 being XFinSequence-yielding Function holds
( b3 = p +^ s iff ( dom b3 = dom p &amp; ( for x being set st x in dom p holds
b3 . x = (p . x) ^ s ) ) );

registration
let s be XFinSequence;
let p be XFinSequence-yielding FinSequence;
clusters ^+ p ->  FinSequence-like XFinSequence-yielding ;
coherence
 s ^+ p is FinSequence-like
proofend;
clusterp +^ s ->  FinSequence-like XFinSequence-yielding ;
coherence
 p +^ s is FinSequence-like
proofend;
end;

theorem Th5: :: REWRITE2:5
for s being XFinSequence
for p being XFinSequence-yielding FinSequence holds
( len (s ^+ p) = len p &amp; len (p +^ s) = len p )
proofend;

theorem :: REWRITE2:6
for E being set
for p being XFinSequence-yielding FinSequence holds
( (<%> E) ^+ p = p &amp; p +^ (<%> E) = p )
proofend;

theorem :: REWRITE2:7
for s, t being XFinSequence
for p being XFinSequence-yielding FinSequence holds
( s ^+ (t ^+ p) = (s ^ t) ^+ p &amp; (p +^ t) +^ s = p +^ (t ^ s) )
proofend;

theorem :: REWRITE2:8
for s, t being XFinSequence
for p being XFinSequence-yielding FinSequence holds s ^+ (p +^ t) = (s ^+ p) +^ t
proofend;

theorem :: REWRITE2:9
for s being XFinSequence
for p, q being XFinSequence-yielding FinSequence holds
( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) &amp; (p ^ q) +^ s = (p +^ s) ^ (q +^ s) )
proofend;

begin

:: Redefinitions for E^omega:
definition
let E be set ;
let p be FinSequence of E ^omega ;
let k be Nat;
:: original:.
redefine funcp . k ->  Element of E ^omega ;
coherence
 p . k is Element of E ^omega
proofend;
end;

definition
let E be set ;
let s be Element of E ^omega ;
let p be FinSequence of E ^omega ;
:: original:^+
redefine funcs ^+ p ->  FinSequence of E ^omega ;
coherence
 s ^+ p is FinSequence of E ^omega
proofend;
:: original:+^
redefine funcp +^ s ->  FinSequence of E ^omega ;
coherence
 p +^ s is FinSequence of E ^omega
proofend;
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;

registration
let S be Relation;
clusterS \/ (S ~) ->  symmetric ;
coherence
 S \/ (S ~) is symmetric
proofend;
end;

registration
let E be set ;
cluster Relation-like symmetric for Element of K6(([#] ((E ^omega),(E ^omega))));
existence
 ex b1 being semi-Thue-system of E st b1 is symmetric
proofend;
end;

definition
let E be set ;
mode Thue-system of E is symmetric semi-Thue-system of E;
end;

begin

definition
let E be set ;
let S be semi-Thue-system of E;
let s, t be Element of E ^omega ;
preds -->. t,S means :Def4: :: REWRITE2:def 4
[s,t] in S;
end;

:: deftheorem Def4 defines -->. REWRITE2:def_4_:_
 for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega holds
( s -->. t,S iff [s,t] in S );

definition
let E be set ;
let S be semi-Thue-system of E;
let s, t be Element of E ^omega ;
preds ==>. t,S means :Def5: :: REWRITE2:def 5
 ex v, w, s1, t1 being Element of E ^omega st
( s = (v ^ s1) ^ w &amp; t = (v ^ t1) ^ w &amp; s1 -->. t1,S );
end;

:: deftheorem Def5 defines ==>. REWRITE2:def_5_:_
 for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega holds
( s ==>. t,S iff ex v, w, s1, t1 being Element of E ^omega st
( s = (v ^ s1) ^ w &amp; t = (v ^ t1) ^ w &amp; s1 -->. t1,S ) );

theorem Th10: :: REWRITE2:10
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st s -->. t,S holds
s ==>. t,S
proofend;

theorem :: REWRITE2:11
for E being set
for S being semi-Thue-system of E
for s being Element of E ^omega st s ==>. s,S holds
ex v, w, s1 being Element of E ^omega st
( s = (v ^ s1) ^ w &amp; s1 -->. s1,S )
proofend;

theorem Th12: :: REWRITE2:12
for E being set
for S being semi-Thue-system of E
for s, t, u being Element of E ^omega st s ==>. t,S holds
( u ^ s ==>. u ^ t,S &amp; s ^ u ==>. t ^ u,S )
proofend;

theorem Th13: :: REWRITE2:13
for E being set
for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>. t,S holds
(u ^ s) ^ v ==>. (u ^ t) ^ v,S
proofend;

theorem Th14: :: REWRITE2:14
for E being set
for S being semi-Thue-system of E
for s, t, u being Element of E ^omega st s -->. t,S holds
( u ^ s ==>. u ^ t,S &amp; s ^ u ==>. t ^ u,S )
proofend;

theorem Th15: :: REWRITE2:15
for E being set
for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s -->. t,S holds
(u ^ s) ^ v ==>. (u ^ t) ^ v,S
proofend;

theorem Th16: :: REWRITE2:16
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st S is Thue-system of E &amp; s -->. t,S holds
t -->. s,S
proofend;

theorem Th17: :: REWRITE2:17
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st S is Thue-system of E &amp; s ==>. t,S holds
t ==>. s,S
proofend;

theorem Th18: :: REWRITE2:18
for E being set
for S, T being semi-Thue-system of E
for s, t being Element of E ^omega st S c= T &amp; s -->. t,S holds
s -->. t,T
proofend;

theorem Th19: :: REWRITE2:19
for E being set
for S, T being semi-Thue-system of E
for s, t being Element of E ^omega st S c= T &amp; s ==>. t,S holds
s ==>. t,T
proofend;

theorem Th20: :: REWRITE2:20
for E being set
for s, t being Element of E ^omega holds not s ==>. t, {} ((E ^omega),(E ^omega))
proofend;

theorem Th21: :: REWRITE2:21
for E being set
for S, T being semi-Thue-system of E
for s, t being Element of E ^omega holds
( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )
proofend;

begin

:: ==>.-relation is introduced to define derivations
:: using concepts from REWRITE1.
definition
let E be set ;
:: original:id
redefine func id E ->  Relation of E;
coherence
 id E is Relation of E by RELSET_1:14;
end;

definition
let E be set ;
let S be semi-Thue-system of E;
func ==>.-relation S ->  Relation of (E ^omega) means :Def6: :: REWRITE2:def 6
 for s, t being Element of E ^omega holds
( [s,t] in it iff s ==>. t,S );
existence
 ex b1 being Relation of (E ^omega) st
for s, t being Element of E ^omega holds
( [s,t] in b1 iff s ==>. t,S )
proofend;
uniqueness
 for b1, b2 being Relation of (E ^omega) st ( for s, t being Element of E ^omega holds
( [s,t] in b1 iff s ==>. t,S ) ) &amp; ( for s, t being Element of E ^omega holds
( [s,t] in b2 iff s ==>. t,S ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines ==>.-relation REWRITE2:def_6_:_
 for E being set
for S being semi-Thue-system of E
for b3 being Relation of (E ^omega) holds
( b3 = ==>.-relation S iff for s, t being Element of E ^omega holds
( [s,t] in b3 iff s ==>. t,S ) );

theorem Th22: :: REWRITE2:22
for E being set
for S being semi-Thue-system of E holds S c= ==>.-relation S
proofend;

theorem Th23: :: REWRITE2:23
for E being set
for S being semi-Thue-system of E
for u being Element of E ^omega
for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds
( p +^ u is RedSequence of ==>.-relation S &amp; u ^+ p is RedSequence of ==>.-relation S )
proofend;

theorem :: REWRITE2:24
for E being set
for S being semi-Thue-system of E
for t, u being Element of E ^omega
for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds
(t ^+ p) +^ u is RedSequence of ==>.-relation S
proofend;

theorem Th25: :: REWRITE2:25
for E being set
for S being semi-Thue-system of E st S is Thue-system of E holds
==>.-relation S = (==>.-relation S) ~
proofend;

theorem Th26: :: REWRITE2:26
for E being set
for S, T being semi-Thue-system of E st S c= T holds
==>.-relation S c= ==>.-relation T
proofend;

theorem Th27: :: REWRITE2:27
for E being set holds ==>.-relation (id (E ^omega)) = id (E ^omega)
proofend;

theorem Th28: :: REWRITE2:28
for E being set
for S being semi-Thue-system of E holds ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega))
proofend;

theorem Th29: :: REWRITE2:29
for E being set holds ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega))
proofend;

theorem Th30: :: REWRITE2:30
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st s ==>. t, ==>.-relation S holds
s ==>. t,S
proofend;

theorem Th31: :: REWRITE2:31
for E being set
for S being semi-Thue-system of E holds ==>.-relation (==>.-relation S) = ==>.-relation S
proofend;

begin

definition
let E be set ;
let S be semi-Thue-system of E;
let s, t be Element of E ^omega ;
preds ==>* t,S means :Def7: :: REWRITE2:def 7
 ==>.-relation S reduces s,t;
end;

:: deftheorem Def7 defines ==>* REWRITE2:def_7_:_
 for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega holds
( s ==>* t,S iff ==>.-relation S reduces s,t );

theorem Th32: :: REWRITE2:32
for E being set
for S being semi-Thue-system of E
for s being Element of E ^omega holds s ==>* s,S
proofend;

theorem Th33: :: REWRITE2:33
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st s ==>. t,S holds
s ==>* t,S
proofend;

theorem :: REWRITE2:34
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st s -->. t,S holds
s ==>* t,S by Th10, Th33;

theorem Th35: :: REWRITE2:35
for E being set
for S being semi-Thue-system of E
for s, t, u being Element of E ^omega st s ==>* t,S &amp; t ==>* u,S holds
s ==>* u,S
proofend;

theorem Th36: :: REWRITE2:36
for E being set
for S being semi-Thue-system of E
for s, t, u being Element of E ^omega st s ==>* t,S holds
( s ^ u ==>* t ^ u,S &amp; u ^ s ==>* u ^ t,S )
proofend;

theorem Th37: :: REWRITE2:37
for E being set
for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>* t,S holds
(u ^ s) ^ v ==>* (u ^ t) ^ v,S
proofend;

theorem :: REWRITE2:38
for E being set
for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>* t,S &amp; u ==>* v,S holds
( s ^ u ==>* t ^ v,S &amp; u ^ s ==>* v ^ t,S )
proofend;

theorem :: REWRITE2:39
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st S is Thue-system of E &amp; s ==>* t,S holds
t ==>* s,S
proofend;

theorem Th40: :: REWRITE2:40
for E being set
for S, T being semi-Thue-system of E
for s, t being Element of E ^omega st S c= T &amp; s ==>* t,S holds
s ==>* t,T
proofend;

theorem Th41: :: REWRITE2:41
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega holds
( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) )
proofend;

theorem Th42: :: REWRITE2:42
for E being set
for s, t being Element of E ^omega st s ==>* t, {} ((E ^omega),(E ^omega)) holds
s = t
proofend;

theorem Th43: :: REWRITE2:43
for E being set
for S being semi-Thue-system of E
for s, t being Element of E ^omega st s ==>* t, ==>.-relation S holds
s ==>* t,S
proofend;

theorem Th44: :: REWRITE2:44
for E being set
for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>* t,S &amp; u ==>. v,{[s,t]} holds
u ==>* v,S
proofend;

theorem Th45: :: REWRITE2:45
for E being set
for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>* t,S &amp; u ==>* v,S \/ {[s,t]} holds
u ==>* v,S
proofend;

begin

definition
let E be set ;
let S be semi-Thue-system of E;
let w be Element of E ^omega ;
func Lang (w,S) ->  Subset of (E ^omega) equals :: REWRITE2:def 8
 {  s where s is Element of E ^omega : w ==>* s,S  }  ;
coherence
  {  s where s is Element of E ^omega : w ==>* s,S  }  is Subset of (E ^omega)
proofend;
end;

:: deftheorem  defines Lang REWRITE2:def_8_:_
 for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds Lang (w,S) =  {  s where s is Element of E ^omega : w ==>* s,S  }  ;

theorem Th46: :: REWRITE2:46
for E being set
for S being semi-Thue-system of E
for s, w being Element of E ^omega holds
( s in Lang (w,S) iff w ==>* s,S )
proofend;

theorem Th47: :: REWRITE2:47
for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds w in Lang (w,S)
proofend;

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
 not Lang (w,S) is empty by Th47;
end;

theorem Th48: :: REWRITE2:48
for E being set
for S, T being semi-Thue-system of E
for w being Element of E ^omega st S c= T holds
Lang (w,S) c= Lang (w,T)
proofend;

theorem Th49: :: REWRITE2:49
for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds Lang (w,S) = Lang (w,(S \/ (id (E ^omega))))
proofend;

theorem Th50: :: REWRITE2:50
for E being set
for w being Element of E ^omega holds Lang (w,({} ((E ^omega),(E ^omega)))) = {w}
proofend;

theorem :: REWRITE2:51
for E being set
for w being Element of E ^omega holds Lang (w,(id (E ^omega))) = {w}
proofend;

begin

definition
let E be set ;
let S, T be semi-Thue-system of E;
let w be Element of E ^omega ;
predS,T are_equivalent_wrt w means :Def9: :: REWRITE2:def 9
 Lang (w,S) = Lang (w,T);
end;

:: deftheorem Def9 defines are_equivalent_wrt REWRITE2:def_9_:_
 for E being set
for S, T being semi-Thue-system of E
for w being Element of E ^omega holds
( S,T are_equivalent_wrt w iff Lang (w,S) = Lang (w,T) );

theorem :: REWRITE2:52
for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds S,S are_equivalent_wrt w
proofend;

theorem :: REWRITE2:53
for E being set
for S, T being semi-Thue-system of E
for w being Element of E ^omega st S,T are_equivalent_wrt w holds
T,S are_equivalent_wrt w
proofend;

theorem :: REWRITE2:54
for E being set
for S, T, U being semi-Thue-system of E
for w being Element of E ^omega st S,T are_equivalent_wrt w &amp; T,U are_equivalent_wrt w holds
S,U are_equivalent_wrt w
proofend;

theorem :: REWRITE2:55
for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds S,S \/ (id (E ^omega)) are_equivalent_wrt w
proofend;

theorem Th56: :: REWRITE2:56
for E being set
for S, T, U being semi-Thue-system of E
for w being Element of E ^omega st S,T are_equivalent_wrt w &amp; S c= U &amp; U c= T holds
( S,U are_equivalent_wrt w &amp; U,T are_equivalent_wrt w )
proofend;

theorem Th57: :: REWRITE2:57
for E being set
for S being semi-Thue-system of E
for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w
proofend;

theorem Th58: :: REWRITE2:58
for E being set
for S, T being semi-Thue-system of E
for w, s being Element of E ^omega st S,T are_equivalent_wrt w &amp; ==>.-relation (S \/ T) reduces w,s holds
==>.-relation S reduces w,s
proofend;

theorem Th59: :: REWRITE2:59
for E being set
for S, T being semi-Thue-system of E
for w, s being Element of E ^omega st S,T are_equivalent_wrt w &amp; w ==>* s,S \/ T holds
w ==>* s,S
proofend;

theorem Th60: :: REWRITE2:60
for E being set
for S, T being semi-Thue-system of E
for w being Element of E ^omega st S,T are_equivalent_wrt w holds
S,S \/ T are_equivalent_wrt w
proofend;

theorem :: REWRITE2:61
for E being set
for S being semi-Thue-system of E
for s, t, w being Element of E ^omega st s ==>. t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
proofend;

theorem :: REWRITE2:62
for E being set
for S being semi-Thue-system of E
for s, t, w being Element of E ^omega st s ==>* t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
proofend;