:: by Micha{\l} Trybulec

::

:: Received July 17, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

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 )

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

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 )

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;

definition

let f be Function;

end;
attr f is XFinSequence-yielding means :Def1: :: REWRITE2:def 1

for x being set st x in dom f holds

f . x is XFinSequence;

for x being set st x in dom f holds

f . x is XFinSequence;

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

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

registration

let p be XFinSequence-yielding Function;

let x be object ;

coherence

( p . x is finite & p . x is Function-like & p . x is Relation-like )

end;
let x be object ;

coherence

( p . x is finite & p . x is Function-like & p . x is Relation-like )

proof end;

registration

let p be XFinSequence-yielding Function;

let x be object ;

coherence

p . x is Sequence-like

end;
let x be object ;

coherence

p . x is Sequence-like

proof end;

registration

ex b_{1} being FinSequence st b_{1} is XFinSequence-yielding
end;

cluster Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding for set ;

existence ex b

proof end;

registration

let E be set ;

coherence

for b_{1} being FinSequence of E ^omega holds b_{1} is XFinSequence-yielding

end;
coherence

for b

proof end;

registration
end;

:: Concatenation (left-sided and right-sided ) of an XFinSequence

:: with all elements of a XFinSequence-yielding Function.

:: with all elements of a XFinSequence-yielding Function.

definition

let s be XFinSequence;

let p be XFinSequence-yielding Function;

ex b_{1} being XFinSequence-yielding Function st

( dom b_{1} = dom p & ( for x being set st x in dom p holds

b_{1} . x = s ^ (p . x) ) )

for b_{1}, b_{2} being XFinSequence-yielding Function st dom b_{1} = dom p & ( for x being set st x in dom p holds

b_{1} . x = s ^ (p . x) ) & dom b_{2} = dom p & ( for x being set st x in dom p holds

b_{2} . x = s ^ (p . x) ) holds

b_{1} = b_{2}

ex b_{1} being XFinSequence-yielding Function st

( dom b_{1} = dom p & ( for x being set st x in dom p holds

b_{1} . x = (p . x) ^ s ) )

for b_{1}, b_{2} being XFinSequence-yielding Function st dom b_{1} = dom p & ( for x being set st x in dom p holds

b_{1} . x = (p . x) ^ s ) & dom b_{2} = dom p & ( for x being set st x in dom p holds

b_{2} . x = (p . x) ^ s ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom p & ( for x being set st x in dom p holds

it . x = s ^ (p . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

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 ( dom it = dom p & ( for x being set st x in dom p holds

it . x = (p . x) ^ s ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines ^+ REWRITE2:def 2 :

for s being XFinSequence

for p, b_{3} being XFinSequence-yielding Function holds

( b_{3} = s ^+ p iff ( dom b_{3} = dom p & ( for x being set st x in dom p holds

b_{3} . x = s ^ (p . x) ) ) );

for s being XFinSequence

for p, b

( b

b

:: deftheorem Def3 defines +^ REWRITE2:def 3 :

for s being XFinSequence

for p, b_{3} being XFinSequence-yielding Function holds

( b_{3} = p +^ s iff ( dom b_{3} = dom p & ( for x being set st x in dom p holds

b_{3} . x = (p . x) ^ s ) ) );

for s being XFinSequence

for p, b

( b

b

registration

let s be XFinSequence;

let p be XFinSequence-yielding FinSequence;

coherence

s ^+ p is FinSequence-like

p +^ s is FinSequence-like

end;
let p be XFinSequence-yielding FinSequence;

coherence

s ^+ p is FinSequence-like

proof end;

coherence p +^ s is FinSequence-like

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

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 )

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) )

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

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) )

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

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

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

redefine func p +^ s -> FinSequence of E ^omega ;

coherence

p +^ s is FinSequence of E ^omega

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

:: Definitions of semi-Thue systems and Thue systems.

registration
end;

registration
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 );

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

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

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

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 )

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 )

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

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 )

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

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

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;

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

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

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 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 )

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.

:: 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;
:: original: id

redefine func id E -> Relation of E;

coherence

id E is Relation of E by RELSET_1:14;

definition

let E be set ;

let S be semi-Thue-system of E;

ex b_{1} being Relation of (E ^omega) st

for s, t being Element of E ^omega holds

( [s,t] in b_{1} iff s ==>. t,S )

for b_{1}, b_{2} being Relation of (E ^omega) st ( for s, t being Element of E ^omega holds

( [s,t] in b_{1} iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds

( [s,t] in b_{2} iff s ==>. t,S ) ) holds

b_{1} = b_{2}

end;
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 for s, t being Element of E ^omega holds

( [s,t] in it iff s ==>. t,S );

ex b

for s, t being Element of E ^omega holds

( [s,t] in b

proof end;

uniqueness for b

( [s,t] in b

( [s,t] in b

b

proof end;

:: deftheorem Def6 defines ==>.-relation REWRITE2:def 6 :

for E being set

for S being semi-Thue-system of E

for b_{3} being Relation of (E ^omega) holds

( b_{3} = ==>.-relation S iff for s, t being Element of E ^omega holds

( [s,t] in b_{3} iff s ==>. t,S ) );

for E being set

for S being semi-Thue-system of E

for b

( b

( [s,t] in b

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 )

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

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) ~

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

for S, T being semi-Thue-system of E st S c= T holds

==>.-relation S c= ==>.-relation T

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))

for S being semi-Thue-system of E holds ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (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

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

for S being semi-Thue-system of E holds ==>.-relation (==>.-relation S) = ==>.-relation S

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

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;

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

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

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;

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 )

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

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 )

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

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;

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)) )

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

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;

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

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

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 ;

{ s where s is Element of E ^omega : w ==>* s,S } is Subset of (E ^omega)

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

{ s where s is Element of E ^omega : w ==>* s,S } is Subset of (E ^omega)

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

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 )

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)

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 ;

coherence

not Lang (w,S) is empty by Th47;

end;
let S be semi-Thue-system of E;

let w be Element of E ^omega ;

coherence

not Lang (w,S) is empty by Th47;

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)

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))))

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;

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

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 ;

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 ;

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 ;

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;

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 )

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

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

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;

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

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

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

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;

:: These definitions will be later used for introduction of

:: reduction sequences between words from E^omega (XFinSequences).