:: 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 b₁ being Function st b₁ is empty holds
b₁ 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 b₁ being FinSequence st b₁ is XFinSequence-yielding

proof end;

end;

registration

let E be set ;

cluster -> XFinSequence-yielding for FinSequence of E ^omega ;

coherence
for b₁ being FinSequence of E ^omega holds b₁ 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 b₁ being XFinSequence-yielding Function st
( dom b₁ = dom p & ( for x being set st x in dom p holds
b₁ . x = s ^ (p . x) ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence-yielding Function st dom b₁ = dom p & ( for x being set st x in dom p holds
b₁ . x = s ^ (p . x) ) & dom b₂ = dom p & ( for x being set st x in dom p holds
b₂ . x = s ^ (p . x) ) holds
b₁ = b₂

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 b₁ being XFinSequence-yielding Function st
( dom b₁ = dom p & ( for x being set st x in dom p holds
b₁ . x = (p . x) ^ s ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence-yielding Function st dom b₁ = dom p & ( for x being set st x in dom p holds
b₁ . x = (p . x) ^ s ) & dom b₂ = dom p & ( for x being set st x in dom p holds
b₂ . x = (p . x) ^ s ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ^+ REWRITE2:def 2 :
for s being XFinSequence
for p, b₃ being XFinSequence-yielding Function holds
( b₃ = s ^+ p iff ( dom b₃ = dom p & ( for x being set st x in dom p holds
b₃ . x = s ^ (p . x) ) ) );

:: deftheorem Def3 defines +^ REWRITE2:def 3 :
for s being XFinSequence
for p, b₃ being XFinSequence-yielding Function holds
( b₃ = p +^ s iff ( dom b₃ = dom p & ( for x being set st x in dom p holds
b₃ . 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 b₁ being semi-Thue-system of E st b₁ 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 b₁ being Relation of (E ^omega) st
for s, t being Element of E ^omega holds
( [s,t] in b₁ iff s ==>. t,S )

proof end;

uniqueness
for b₁, b₂ being Relation of (E ^omega) st ( for s, t being Element of E ^omega holds
( [s,t] in b₁ iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds
( [s,t] in b₂ iff s ==>. t,S ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ==>.-relation REWRITE2:def 6 :
for E being set
for S being semi-Thue-system of E
for b₃ being Relation of (E ^omega) holds
( b₃ = ==>.-relation S iff for s, t being Element of E ^omega holds
( [s,t] in b₃ 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;