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


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
proof end;

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

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
proof end;

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 & q . 1 = p . 1 & q . (len q) = p . k )
proof end;

:: 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: :: 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 Relation-like empty Function-like -> XFinSequence-yielding for set ;
coherence
for b1 being Function st b1 is empty holds
b1 is XFinSequence-yielding ;
end;

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

registration
let p be XFinSequence-yielding Function;
let x be object ;
cluster p . x -> Relation-like Function-like finite ;
coherence
( p . x is finite & p . x is Function-like & p . x is Relation-like )
proof end;
end;

registration
let p be XFinSequence-yielding Function;
let x be object ;
cluster p . x -> Sequence-like ;
coherence
p . x is Sequence-like
proof end;
end;

registration
cluster Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding for set ;
existence
ex b1 being FinSequence st b1 is XFinSequence-yielding
proof end;
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
proof end;
end;

registration
let p, q be XFinSequence-yielding FinSequence;
cluster p ^ q -> XFinSequence-yielding ;
coherence
p ^ q is XFinSequence-yielding
proof end;
end;

:: 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: :: REWRITE2:def 2
( dom it = dom p & ( 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 & ( for x being set st x in dom p holds
b1 . x = s ^ (p . x) ) )
proof end;
uniqueness
for b1, b2 being XFinSequence-yielding Function st dom b1 = dom p & ( for x being set st x in dom p holds
b1 . x = s ^ (p . x) ) & dom b2 = dom p & ( for x being set st x in dom p holds
b2 . x = s ^ (p . x) ) holds
b1 = b2
proof end;
func p +^ s -> XFinSequence-yielding Function means :Def3: :: REWRITE2:def 3
( dom it = dom p & ( 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 & ( for x being set st x in dom p holds
b1 . x = (p . x) ^ s ) )
proof end;
uniqueness
for b1, b2 being XFinSequence-yielding Function st dom b1 = dom p & ( for x being set st x in dom p holds
b1 . x = (p . x) ^ s ) & dom b2 = dom p & ( for x being set st x in dom p holds
b2 . x = (p . x) ^ s ) holds
b1 = b2
proof end;
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 & ( 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 & ( 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;
cluster s ^+ p -> FinSequence-like XFinSequence-yielding ;
coherence
s ^+ p is FinSequence-like
proof end;
cluster p +^ s -> FinSequence-like XFinSequence-yielding ;
coherence
p +^ s is FinSequence-like
proof end;
end;

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

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

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

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

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

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

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

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

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

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

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

:: deftheorem 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 ;
pred s ==>. t,S means :: REWRITE2:def 5
 ex v, w, s1, t1 being Element of E ^omega st
( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w & s1 -->. t1,S );
end;

:: deftheorem 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 & t = (v ^ t1) ^ w & 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
proof end;

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 & s1 -->. s1,S )
proof end;

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 & s ^ u ==>. t ^ u,S )
proof end;

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
proof end;

theorem :: 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 & s ^ u ==>. t ^ u,S )
proof end;

theorem :: 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 ;

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 & s -->. t,S holds
t -->. s,S
proof end;

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 & s ==>. t,S holds
t ==>. s,S by Th16;

theorem :: 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 & s -->. t,S holds
s -->. t,T ;

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 & s ==>. t,S holds
s ==>. t,T
proof end;

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

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 )
proof end;

:: ==>.-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 )
proof end;
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 ) ) & ( for s, t being Element of E ^omega holds
( [s,t] in b2 iff s ==>. t,S ) ) holds
b1 = b2
proof end;
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
proof end;

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 & u ^+ p is RedSequence of ==>.-relation S )
proof end;

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
proof end;

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) ~
proof end;

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
proof end;

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

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))
proof end;

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

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
proof end;

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

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

:: deftheorem 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 by REWRITE1:12;

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
proof end;

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 & t ==>* u,S holds
s ==>* u,S by REWRITE1:16;

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 & u ^ s ==>* u ^ t,S )
proof end;

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
proof end;

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 & u ==>* v,S holds
( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S )
proof end;

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 & s ==>* t,S holds
t ==>* s,S
proof end;

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 & s ==>* t,S holds
s ==>* t,T by Th26, REWRITE1:22;

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)) )
proof end;

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
proof end;

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 by Th31;

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 & u ==>. v,{[s,t]} holds
u ==>* v,S
proof end;

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 & u ==>* v,S \/ {[s,t]} holds
u ==>* v,S
proof end;

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)
proof end;
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 )
proof end;

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)
proof 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
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)
proof end;

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))))
proof end;

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

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

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

:: deftheorem 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 ;

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 ;

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 & T,U are_equivalent_wrt w holds
S,U are_equivalent_wrt w ;

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 by Th49;

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 & S c= U & U c= T holds
( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w )
proof end;

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
proof end;

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

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

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
proof end;

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
proof end;

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
proof end;