:: REWRITE2 semantic presentation
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
proof
let k be Nat; ::_thesis: for p being FinSequence st not k in dom p & k + 1 in dom p holds
k = 0
let p be FinSequence; ::_thesis: ( not k in dom p & k + 1 in dom p implies k = 0 )
assume that
A1: not k in dom p and
A2: k + 1 in dom p ; ::_thesis: k = 0
A3: k + 1 <= len p by A2, FINSEQ_3:25;
percases ( k < 1 or k > len p ) by A1, FINSEQ_3:25;
suppose k < 1 ; ::_thesis: k = 0
hence k = 0 by NAT_1:14; ::_thesis: verum
end;
suppose k > len p ; ::_thesis: k = 0
hence k = 0 by A3, NAT_1:13; ::_thesis: verum
end;
end;
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
let k be Nat; ::_thesis: 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 )
let p, q be FinSequence; ::_thesis: ( k > len p & k <= len (p ^ q) implies ex l being Nat st
( k = (len p) + l & l >= 1 & l <= len q ) )
A1: 0 + 1 = 1 ;
assume that
A2: k > len p and
A3: k <= len (p ^ q) ; ::_thesis: ex l being Nat st
( k = (len p) + l & l >= 1 & l <= len q )
consider l being Nat such that
A4: k = (len p) + l by A2, NAT_1:10;
take l ; ::_thesis: ( k = (len p) + l & l >= 1 & l <= len q )
thus k = (len p) + l by A4; ::_thesis: ( l >= 1 & l <= len q )
(len p) + l > (len p) + 0 by A2, A4;
then l > 0 ;
hence l >= 1 by A1, NAT_1:13; ::_thesis: l <= len q
(len p) + l <= (len p) + (len q) by A3, A4, FINSEQ_1:22;
hence l <= len q by XREAL_1:6; ::_thesis: verum
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
let k be Nat; ::_thesis: for R being Relation
for p being RedSequence of R st k >= 1 holds
p | k is RedSequence of R
let R be Relation; ::_thesis: for p being RedSequence of R st k >= 1 holds
p | k is RedSequence of R
let p be RedSequence of R; ::_thesis: ( k >= 1 implies p | k is RedSequence of R )
assume A1: k >= 1 ; ::_thesis: p | k is RedSequence of R
percases ( k >= len p or k < len p ) ;
suppose k >= len p ; ::_thesis: p | k is RedSequence of R
hence p | k is RedSequence of R by FINSEQ_1:58; ::_thesis: verum
end;
supposeA2: k < len p ; ::_thesis: p | k is RedSequence of R
A3: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(p_|_k)_&_i_+_1_in_dom_(p_|_k)_holds_
[((p_|_k)_._i),((p_|_k)_._(i_+_1))]_in_R
A4: dom (p | k) c= dom p by RELAT_1:60;
let i be Element of NAT ; ::_thesis: ( i in dom (p | k) & i + 1 in dom (p | k) implies [((p | k) . i),((p | k) . (i + 1))] in R )
assume A5: ( i in dom (p | k) & i + 1 in dom (p | k) ) ; ::_thesis: [((p | k) . i),((p | k) . (i + 1))] in R
( (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; ::_thesis: verum
end;
len (p | k) > 0 by A1, A2, FINSEQ_1:59;
hence p | k is RedSequence of R by A3, REWRITE1:def_2; ::_thesis: verum
end;
end;
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
let k be Nat; ::_thesis: 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 )
let R be Relation; ::_thesis: 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 )
let p be RedSequence of R; ::_thesis: ( k in dom p implies ex q being RedSequence of R st
( len q = k & q . 1 = p . 1 & q . (len q) = p . k ) )
assume A1: k in dom p ; ::_thesis: ex q being RedSequence of R st
( len q = k & q . 1 = p . 1 & q . (len q) = p . k )
set q = p | k;
take p | k ; ::_thesis: ( p | k is RedSequence of R & len (p | k) = k & (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k )
A2: 1 <= k by A1, FINSEQ_3:25;
hence p | k is RedSequence of R by Th3; ::_thesis: ( len (p | k) = k & (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k )
k <= len p by A1, FINSEQ_3:25;
hence len (p | k) = k by FINSEQ_1:59; ::_thesis: ( (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k )
hence ( (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k ) by A2, FINSEQ_3:112; ::_thesis: verum
end;
begin
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
proof
let X be Function; ::_thesis: ( X is empty implies X is XFinSequence-yielding )
assume A1: X is empty ; ::_thesis: X is XFinSequence-yielding
let x be set ; :: according to REWRITE2:def_1 ::_thesis: ( x in dom X implies X . x is XFinSequence )
thus ( x in dom X implies X . x is XFinSequence ) by A1; ::_thesis: verum
end;
end;
registration
let f be XFinSequence;
cluster<*f*> -> XFinSequence-yielding ;
coherence
<*f*> is XFinSequence-yielding
proof
let x be set ; :: according to REWRITE2:def_1 ::_thesis: ( x in dom <*f*> implies <*f*> . x is XFinSequence )
assume x in dom <*f*> ; ::_thesis: <*f*> . x is XFinSequence
then x in {1} by FINSEQ_1:2, FINSEQ_1:38;
then x = 1 by TARSKI:def_1;
hence <*f*> . x is XFinSequence by FINSEQ_1:40; ::_thesis: verum
end;
end;
registration
let p be XFinSequence-yielding Function;
let x be set ;
clusterp . x -> Relation-like Function-like finite ;
coherence
( p . x is finite & p . x is Function-like & p . x is Relation-like )
proof
percases ( x in dom p or not x in dom p ) ;
suppose x in dom p ; ::_thesis: ( p . x is finite & p . x is Function-like & p . x is Relation-like )
hence ( p . x is finite & p . x is Function-like & p . x is Relation-like ) by Def1; ::_thesis: verum
end;
suppose not x in dom p ; ::_thesis: ( p . x is finite & p . x is Function-like & p . x is Relation-like )
hence ( p . x is finite & p . x is Function-like & p . x is Relation-like ) by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
end;
registration
let p be XFinSequence-yielding Function;
let x be set ;
clusterp . x -> T-Sequence-like ;
coherence
p . x is T-Sequence-like
proof
percases ( x in dom p or not x in dom p ) ;
suppose x in dom p ; ::_thesis: p . x is T-Sequence-like
hence p . x is T-Sequence-like by Def1; ::_thesis: verum
end;
suppose not x in dom p ; ::_thesis: p . x is T-Sequence-like
hence p . x is T-Sequence-like by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
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
proof
take {} ; ::_thesis: {} is XFinSequence-yielding
thus {} is XFinSequence-yielding ; ::_thesis: verum
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
let f be FinSequence of E ^omega ; ::_thesis: f is XFinSequence-yielding
let x be set ; :: according to REWRITE2:def_1 ::_thesis: ( x in dom f implies f . x is XFinSequence )
assume A1: x in dom f ; ::_thesis: f . x is XFinSequence
then reconsider x = x as Element of NAT ;
f . x in E ^omega by A1, FINSEQ_2:11;
hence f . x is XFinSequence ; ::_thesis: verum
end;
end;
registration
let p, q be XFinSequence-yielding FinSequence;
clusterp ^ q -> XFinSequence-yielding ;
coherence
p ^ q is XFinSequence-yielding
proof
now__::_thesis:_for_x_being_set_st_x_in_dom_(p_^_q)_holds_
(p_^_q)_._x_is_XFinSequence
let x be set ; ::_thesis: ( x in dom (p ^ q) implies (p ^ q) . b1 is XFinSequence )
assume A1: x in dom (p ^ q) ; ::_thesis: (p ^ q) . b1 is XFinSequence
then reconsider x1 = x as Element of NAT ;
percases ( x1 in dom p or ex l being Nat st
( l in dom q & x1 = (len p) + l ) ) by A1, FINSEQ_1:25;
suppose x1 in dom p ; ::_thesis: (p ^ q) . b1 is XFinSequence
then p . x1 = (p ^ q) . x1 by FINSEQ_1:def_7;
hence (p ^ q) . x is XFinSequence ; ::_thesis: verum
end;
suppose ex l being Nat st
( l in dom q & x1 = (len p) + l ) ; ::_thesis: (p ^ q) . b1 is XFinSequence
then consider l being Element of 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; ::_thesis: verum
end;
end;
end;
hence p ^ q is XFinSequence-yielding by Def1; ::_thesis: verum
end;
end;
begin
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 & ( 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
defpred S1[ set , set ] means for x being set st x = $1 holds
$2 = s ^ (p . x);
A1: for x being set st x in dom p holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in dom p implies ex y being set st S1[x,y] )
assume x in dom p ; ::_thesis: ex y being set st S1[x,y]
take s ^ (p . x) ; ::_thesis: S1[x,s ^ (p . x)]
thus S1[x,s ^ (p . x)] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = dom p & ( for x being set st x in dom p holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_is_XFinSequence
let x be set ; ::_thesis: ( x in dom f implies f . x is XFinSequence )
assume x in dom f ; ::_thesis: f . x is XFinSequence
then f . x = s ^ (p . x) by A2;
hence f . x is XFinSequence ; ::_thesis: verum
end;
then reconsider g = f as XFinSequence-yielding Function by Def1;
take g ; ::_thesis: ( dom g = dom p & ( for x being set st x in dom p holds
g . x = s ^ (p . x) ) )
thus ( dom g = dom p & ( for x being set st x in dom p holds
g . x = s ^ (p . x) ) ) by A2; ::_thesis: verum
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
let f, g be XFinSequence-yielding Function; ::_thesis: ( dom f = dom p & ( for x being set st x in dom p holds
f . x = s ^ (p . x) ) & dom g = dom p & ( for x being set st x in dom p holds
g . x = s ^ (p . x) ) implies f = g )
assume that
A3: dom f = dom p and
A4: for x being set st x in dom p holds
f . x = s ^ (p . x) and
A5: dom g = dom p and
A6: for x being set st x in dom p holds
g . x = s ^ (p . x) ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A7: x in dom f ; ::_thesis: f . x = g . x
then f . x = s ^ (p . x) by A3, A4;
hence f . x = g . x by A3, A6, A7; ::_thesis: verum
end;
hence f = g by A3, A5, FUNCT_1:2; ::_thesis: verum
end;
funcp +^ 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
defpred S1[ set , set ] means for x being set st x = $1 holds
$2 = (p . x) ^ s;
A8: for x being set st x in dom p holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in dom p implies ex y being set st S1[x,y] )
assume x in dom p ; ::_thesis: ex y being set st S1[x,y]
take (p . x) ^ s ; ::_thesis: S1[x,(p . x) ^ s]
thus S1[x,(p . x) ^ s] ; ::_thesis: verum
end;
consider f being Function such that
A9: ( dom f = dom p & ( for x being set st x in dom p holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A8);
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_is_XFinSequence
let x be set ; ::_thesis: ( x in dom f implies f . x is XFinSequence )
assume x in dom f ; ::_thesis: f . x is XFinSequence
then f . x = (p . x) ^ s by A9;
hence f . x is XFinSequence ; ::_thesis: verum
end;
then reconsider g = f as XFinSequence-yielding Function by Def1;
take g ; ::_thesis: ( dom g = dom p & ( for x being set st x in dom p holds
g . x = (p . x) ^ s ) )
thus ( dom g = dom p & ( for x being set st x in dom p holds
g . x = (p . x) ^ s ) ) by A9; ::_thesis: verum
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
let f, g be XFinSequence-yielding Function; ::_thesis: ( dom f = dom p & ( for x being set st x in dom p holds
f . x = (p . x) ^ s ) & dom g = dom p & ( for x being set st x in dom p holds
g . x = (p . x) ^ s ) implies f = g )
assume that
A10: dom f = dom p and
A11: for x being set st x in dom p holds
f . x = (p . x) ^ s and
A12: dom g = dom p and
A13: for x being set st x in dom p holds
g . x = (p . x) ^ s ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A14: x in dom f ; ::_thesis: f . x = g . x
then f . x = (p . x) ^ s by A10, A11;
hence f . x = g . x by A10, A13, A14; ::_thesis: verum
end;
hence f = g by A10, A12, FUNCT_1:2; ::_thesis: verum
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;
clusters ^+ p -> FinSequence-like XFinSequence-yielding ;
coherence
s ^+ p is FinSequence-like
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 s ^+ p is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
clusterp +^ s -> FinSequence-like XFinSequence-yielding ;
coherence
p +^ s is FinSequence-like
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 p +^ s is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
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
let s be XFinSequence; ::_thesis: for p being XFinSequence-yielding FinSequence holds
( len (s ^+ p) = len p & len (p +^ s) = len p )
let p be XFinSequence-yielding FinSequence; ::_thesis: ( len (s ^+ p) = len p & len (p +^ s) = len p )
( dom (s ^+ p) = dom p & dom (p +^ s) = dom p ) by Def2, Def3;
hence ( len (s ^+ p) = len p & len (p +^ s) = len p ) by FINSEQ_3:29; ::_thesis: verum
end;
theorem :: REWRITE2:6
for E being set
for p being XFinSequence-yielding FinSequence holds
( (<%> E) ^+ p = p & p +^ (<%> E) = p )
proof
let E be set ; ::_thesis: for p being XFinSequence-yielding FinSequence holds
( (<%> E) ^+ p = p & p +^ (<%> E) = p )
let p be XFinSequence-yielding FinSequence; ::_thesis: ( (<%> E) ^+ p = p & p +^ (<%> E) = p )
A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
((<%>_E)_^+_p)_._k_=_p_._k
let k be Nat; ::_thesis: ( k in dom p implies ((<%> E) ^+ p) . k = p . k )
assume k in dom p ; ::_thesis: ((<%> E) ^+ p) . k = p . k
hence ((<%> E) ^+ p) . k = {} ^ (p . k) by Def2
.= p . k ;
::_thesis: verum
end;
dom ((<%> E) ^+ p) = dom p by Def2;
hence (<%> E) ^+ p = p by A1, FINSEQ_1:13; ::_thesis: p +^ (<%> E) = p
A2: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
(p_+^_(<%>_E))_._k_=_p_._k
let k be Nat; ::_thesis: ( k in dom p implies (p +^ (<%> E)) . k = p . k )
assume k in dom p ; ::_thesis: (p +^ (<%> E)) . k = p . k
hence (p +^ (<%> E)) . k = (p . k) ^ {} by Def3
.= p . k ;
::_thesis: verum
end;
dom (p +^ (<%> E)) = dom p by Def3;
hence p +^ (<%> E) = p by A2, FINSEQ_1:13; ::_thesis: verum
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
let s, t be XFinSequence; ::_thesis: for p being XFinSequence-yielding FinSequence holds
( s ^+ (t ^+ p) = (s ^ t) ^+ p & (p +^ t) +^ s = p +^ (t ^ s) )
let p be XFinSequence-yielding FinSequence; ::_thesis: ( s ^+ (t ^+ p) = (s ^ t) ^+ p & (p +^ t) +^ s = p +^ (t ^ s) )
A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(s_^+_(t_^+_p))_holds_
(s_^+_(t_^+_p))_._k_=_((s_^_t)_^+_p)_._k
let k be Nat; ::_thesis: ( k in dom (s ^+ (t ^+ p)) implies (s ^+ (t ^+ p)) . k = ((s ^ t) ^+ p) . k )
assume k in dom (s ^+ (t ^+ p)) ; ::_thesis: (s ^+ (t ^+ p)) . k = ((s ^ t) ^+ p) . k
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 ; ::_thesis: verum
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; ::_thesis: (p +^ t) +^ s = p +^ (t ^ s)
A4: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((p_+^_t)_+^_s)_holds_
((p_+^_t)_+^_s)_._k_=_(p_+^_(t_^_s))_._k
let k be Nat; ::_thesis: ( k in dom ((p +^ t) +^ s) implies ((p +^ t) +^ s) . k = (p +^ (t ^ s)) . k )
assume k in dom ((p +^ t) +^ s) ; ::_thesis: ((p +^ t) +^ s) . k = (p +^ (t ^ s)) . k
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 ; ::_thesis: verum
end;
dom ((p +^ t) +^ s) = dom (p +^ t) by Def3
.= dom p by Def3
.= dom (p +^ (t ^ s)) by Def3 ;
hence (p +^ t) +^ s = p +^ (t ^ s) by A4, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: REWRITE2:8
for s, t being XFinSequence
for p being XFinSequence-yielding FinSequence holds s ^+ (p +^ t) = (s ^+ p) +^ t
proof
let s, t be XFinSequence; ::_thesis: for p being XFinSequence-yielding FinSequence holds s ^+ (p +^ t) = (s ^+ p) +^ t
let p be XFinSequence-yielding FinSequence; ::_thesis: s ^+ (p +^ t) = (s ^+ p) +^ t
A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(s_^+_(p_+^_t))_holds_
(s_^+_(p_+^_t))_._k_=_((s_^+_p)_+^_t)_._k
let k be Nat; ::_thesis: ( k in dom (s ^+ (p +^ t)) implies (s ^+ (p +^ t)) . k = ((s ^+ p) +^ t) . k )
assume k in dom (s ^+ (p +^ t)) ; ::_thesis: (s ^+ (p +^ t)) . k = ((s ^+ p) +^ t) . k
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 ; ::_thesis: verum
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 s ^+ (p +^ t) = (s ^+ p) +^ t by A1, FINSEQ_1:13; ::_thesis: verum
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
let s be XFinSequence; ::_thesis: for p, q being XFinSequence-yielding FinSequence holds
( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) )
let p, q be XFinSequence-yielding FinSequence; ::_thesis: ( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) )
A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(s_^+_(p_^_q))_holds_
(s_^+_(p_^_q))_._k_=_((s_^+_p)_^_(s_^+_q))_._k
let k be Nat; ::_thesis: ( k in dom (s ^+ (p ^ q)) implies (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k )
assume A2: k in dom (s ^+ (p ^ q)) ; ::_thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
then A3: k in dom (p ^ q) by Def2;
now__::_thesis:_(s_^+_(p_^_q))_._k_=_((s_^+_p)_^_(s_^+_q))_._k
percases ( k in dom p or not k in dom p ) ;
supposeA4: k in dom p ; ::_thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
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 ; ::_thesis: verum
end;
supposeA6: not k in dom p ; ::_thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
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 ; ::_thesis: verum
end;
end;
end;
hence (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k ; ::_thesis: verum
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; ::_thesis: (p ^ q) +^ s = (p +^ s) ^ (q +^ s)
A13: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((p_^_q)_+^_s)_holds_
((p_^_q)_+^_s)_._k_=_((p_+^_s)_^_(q_+^_s))_._k
let k be Nat; ::_thesis: ( k in dom ((p ^ q) +^ s) implies ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k )
assume A14: k in dom ((p ^ q) +^ s) ; ::_thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
then A15: k in dom (p ^ q) by Def3;
now__::_thesis:_((p_^_q)_+^_s)_._k_=_((p_+^_s)_^_(q_+^_s))_._k
percases ( k in dom p or not k in dom p ) ;
supposeA16: k in dom p ; ::_thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
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 ; ::_thesis: verum
end;
supposeA18: not k in dom p ; ::_thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
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 ; ::_thesis: verum
end;
end;
end;
hence ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k ; ::_thesis: verum
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 (p ^ q) +^ s = (p +^ s) ^ (q +^ s) by A13, FINSEQ_1:13; ::_thesis: verum
end;
begin
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
proof
percases ( k in dom p or not k in dom p ) ;
suppose k in dom p ; ::_thesis: p . k is Element of E ^omega
hence p . k is Element of E ^omega by FINSEQ_2:11; ::_thesis: verum
end;
suppose not k in dom p ; ::_thesis: p . k is Element of E ^omega
then p . k = {} by FUNCT_1:def_2;
then p . k is XFinSequence of by AFINSQ_1:16;
hence p . k is Element of E ^omega by AFINSQ_1:def_7; ::_thesis: verum
end;
end;
end;
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
proof
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(s_^+_p)_holds_
(s_^+_p)_._i_in_E_^omega
let i be Nat; ::_thesis: ( i in dom (s ^+ p) implies (s ^+ p) . i in E ^omega )
assume i in dom (s ^+ p) ; ::_thesis: (s ^+ p) . i in E ^omega
then i in dom p by Def2;
then (s ^+ p) . i = s ^ (p . i) by Def2;
hence (s ^+ p) . i in E ^omega ; ::_thesis: verum
end;
hence s ^+ p is FinSequence of E ^omega by FINSEQ_2:12; ::_thesis: verum
end;
:: original: +^
redefine funcp +^ s -> FinSequence of E ^omega ;
coherence
p +^ s is FinSequence of E ^omega
proof
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(p_+^_s)_holds_
(p_+^_s)_._i_in_E_^omega
let i be Nat; ::_thesis: ( i in dom (p +^ s) implies (p +^ s) . i in E ^omega )
assume i in dom (p +^ s) ; ::_thesis: (p +^ s) . i in E ^omega
then i in dom p by Def3;
then (p +^ s) . i = (p . i) ^ s by Def3;
hence (p +^ s) . i in E ^omega ; ::_thesis: verum
end;
hence p +^ s is FinSequence of E ^omega by FINSEQ_2:12; ::_thesis: verum
end;
end;
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
proof
S \/ (S ~) = (((S ~) ~) \/ (S ~)) ~ by RELAT_1:23
.= (S \/ (S ~)) ~ ;
hence S \/ (S ~) is symmetric by RELAT_2:13; ::_thesis: verum
end;
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
proof
set S = the semi-Thue-system of E;
take the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) ; ::_thesis: the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) is symmetric
thus the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) is symmetric ; ::_thesis: verum
end;
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 & t = (v ^ t1) ^ w & 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 & 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
let E be set ; ::_thesis: for S being semi-Thue-system of E
for s, t being Element of E ^omega st s -->. t,S holds
s ==>. t,S
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s -->. t,S holds
s ==>. t,S
let s, t be Element of E ^omega ; ::_thesis: ( s -->. t,S implies s ==>. t,S )
assume A1: s -->. t,S ; ::_thesis: s ==>. t,S
take e = <%> E; :: according to REWRITE2:def_5 ::_thesis: ex w, s1, t1 being Element of E ^omega st
( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S )
A2: t = ({} ^ t) ^ {}
.= (e ^ t) ^ e ;
s = ({} ^ s) ^ {}
.= (e ^ s) ^ e ;
hence ex w, s1, t1 being Element of E ^omega st
( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S ) by A1, A2; ::_thesis: verum
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
let E be set ; ::_thesis: 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 )
let S be semi-Thue-system of E; ::_thesis: 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 )
let s be Element of E ^omega ; ::_thesis: ( s ==>. s,S implies ex v, w, s1 being Element of E ^omega st
( s = (v ^ s1) ^ w & s1 -->. s1,S ) )
given v, w, s1, t1 being Element of E ^omega such that A1: s = (v ^ s1) ^ w and
A2: s = (v ^ t1) ^ w and
A3: s1 -->. t1,S ; :: according to REWRITE2:def_5 ::_thesis: ex v, w, s1 being Element of E ^omega st
( s = (v ^ s1) ^ w & s1 -->. s1,S )
v ^ s1 = v ^ t1 by A1, A2, AFINSQ_1:28;
then s1 = t1 by AFINSQ_1:28;
hence ex v, w, s1 being Element of E ^omega st
( s = (v ^ s1) ^ w & s1 -->. s1,S ) by A1, A3; ::_thesis: verum
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
let E be set ; ::_thesis: 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 )
let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s ==>. t,S holds
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
let s, t, u be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) )
given v, w, s1, t1 being Element of E ^omega such that A1: s = (v ^ s1) ^ w and
A2: t = (v ^ t1) ^ w and
A3: s1 -->. t1,S ; :: according to REWRITE2:def_5 ::_thesis: ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,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, Def5; ::_thesis: s ^ u ==>. t ^ u,S
( s ^ u = (v ^ s1) ^ (w ^ u) & t ^ u = (v ^ t1) ^ (w ^ u) ) by A1, A2, AFINSQ_1:27;
hence s ^ u ==>. t ^ u,S by A3, Def5; ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>. t,S holds
(u ^ s) ^ v ==>. (u ^ t) ^ v,S
let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies (u ^ s) ^ v ==>. (u ^ t) ^ v,S )
assume s ==>. t,S ; ::_thesis: (u ^ s) ^ v ==>. (u ^ t) ^ v,S
then u ^ s ==>. u ^ t,S by Th12;
hence (u ^ s) ^ v ==>. (u ^ t) ^ v,S by Th12; ::_thesis: verum
end;
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 & s ^ u ==>. t ^ u,S )
proof
let E be set ; ::_thesis: 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 )
let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s -->. t,S holds
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
let s, t, u be Element of E ^omega ; ::_thesis: ( s -->. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) )
assume s -->. t,S ; ::_thesis: ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
then s ==>. t,S by Th10;
hence ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) by Th12; ::_thesis: verum
end;
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
proof
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s -->. t,S holds
(u ^ s) ^ v ==>. (u ^ t) ^ v,S
let s, t, u, v be Element of E ^omega ; ::_thesis: ( s -->. t,S implies (u ^ s) ^ v ==>. (u ^ t) ^ v,S )
assume s -->. t,S ; ::_thesis: (u ^ s) ^ v ==>. (u ^ t) ^ v,S
then u ^ s ==>. u ^ t,S by Th14;
hence (u ^ s) ^ v ==>. (u ^ t) ^ v,S by Th12; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S is Thue-system of E & s -->. t,S holds
t -->. s,S
let s, t be Element of E ^omega ; ::_thesis: ( S is Thue-system of E & s -->. t,S implies t -->. s,S )
assume ( S is Thue-system of E & s -->. t,S ) ; ::_thesis: t -->. s,S
then ( S = S ~ & [s,t] in S ) by Def4, RELAT_2:13;
then [t,s] in S by RELAT_1:def_7;
hence t -->. s,S by Def4; ::_thesis: verum
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
proof
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S is Thue-system of E & s ==>. t,S holds
t ==>. s,S
let s, t be Element of E ^omega ; ::_thesis: ( S is Thue-system of E & s ==>. t,S implies t ==>. s,S )
assume that
A1: S is Thue-system of E and
A2: s ==>. t,S ; ::_thesis: t ==>. s,S
consider v, w, s1, t1 being Element of E ^omega such that
A3: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and
A4: s1 -->. t1,S by A2, Def5;
t1 -->. s1,S by A1, A4, Th16;
hence t ==>. s,S by A3, Def5; ::_thesis: verum
end;
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 & s -->. t,S holds
s -->. t,T
proof
let E be set ; ::_thesis: 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
let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S c= T & s -->. t,S holds
s -->. t,T
let s, t be Element of E ^omega ; ::_thesis: ( S c= T & s -->. t,S implies s -->. t,T )
assume that
A1: S c= T and
A2: s -->. t,S ; ::_thesis: s -->. t,T
[s,t] in S by A2, Def4;
hence s -->. t,T by A1, Def4; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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
let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S c= T & s ==>. t,S holds
s ==>. t,T
let s, t be Element of E ^omega ; ::_thesis: ( S c= T & s ==>. t,S implies s ==>. t,T )
assume that
A1: S c= T and
A2: s ==>. t,S ; ::_thesis: s ==>. t,T
consider v, w, s1, t1 being Element of E ^omega such that
A3: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and
A4: s1 -->. t1,S by A2, Def5;
s1 -->. t1,T by A1, A4, Th18;
hence s ==>. t,T by A3, Def5; ::_thesis: verum
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
let E be set ; ::_thesis: for s, t being Element of E ^omega holds not s ==>. t, {} ((E ^omega),(E ^omega))
let s, t be Element of E ^omega ; ::_thesis: not s ==>. t, {} ((E ^omega),(E ^omega))
assume s ==>. t, {} ((E ^omega),(E ^omega)) ; ::_thesis: contradiction
then consider v, w, s1, t1 being Element of E ^omega such that
s = (v ^ s1) ^ w and
t = (v ^ t1) ^ w and
A1: s1 -->. t1, {} ((E ^omega),(E ^omega)) by Def5;
[s1,t1] in {} ((E ^omega),(E ^omega)) by A1, Def4;
hence contradiction by PARTIT_2:def_1; ::_thesis: verum
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
let E be set ; ::_thesis: 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 )
let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega holds
( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )
let s, t be Element of E ^omega ; ::_thesis: ( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )
assume s ==>. t,S \/ T ; ::_thesis: ( s ==>. t,S or s ==>. t,T )
then consider v, w, s1, t1 being Element of E ^omega such that
A1: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and
A2: s1 -->. t1,S \/ T by Def5;
A3: [s1,t1] in S \/ T by A2, Def4;
percases ( [s1,t1] in S or [s1,t1] in T ) by A3, XBOOLE_0:def_3;
suppose [s1,t1] in S ; ::_thesis: ( s ==>. t,S or s ==>. t,T )
then s1 -->. t1,S by Def4;
hence ( s ==>. t,S or s ==>. t,T ) by A1, Def5; ::_thesis: verum
end;
suppose [s1,t1] in T ; ::_thesis: ( s ==>. t,S or s ==>. t,T )
then s1 -->. t1,T by Def4;
hence ( s ==>. t,S or s ==>. t,T ) by A1, Def5; ::_thesis: verum
end;
end;
end;
begin
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
defpred S1[ 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 S1[s,t] ) from RELSET_1:sch_2();
take R ; ::_thesis: for s, t being Element of E ^omega holds
( [s,t] in R iff s ==>. t,S )
thus for s, t being Element of E ^omega holds
( [s,t] in R iff s ==>. t,S ) by A1; ::_thesis: verum
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
let R1, R2 be Relation of (E ^omega); ::_thesis: ( ( for s, t being Element of E ^omega holds
( [s,t] in R1 iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds
( [s,t] in R2 iff s ==>. t,S ) ) implies R1 = R2 )
assume 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 ) ; ::_thesis: R1 = R2
now__::_thesis:_for_s,_t_being_Element_of_E_^omega_holds_
(_[s,t]_in_R1_iff_[s,t]_in_R2_)
let s, t be Element of E ^omega ; ::_thesis: ( [s,t] in R1 iff [s,t] in R2 )
( [s,t] in R1 iff s ==>. t,S ) by A2;
hence ( [s,t] in R1 iff [s,t] in R2 ) by A3; ::_thesis: verum
end;
hence R1 = R2 by RELSET_1:def_2; ::_thesis: verum
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
let E be set ; ::_thesis: for S being semi-Thue-system of E holds S c= ==>.-relation S
let S be semi-Thue-system of E; ::_thesis: S c= ==>.-relation S
thus for x being set st x in S holds
x in ==>.-relation S :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in S implies x in ==>.-relation S )
assume A1: x in S ; ::_thesis: x in ==>.-relation S
then consider a, b being set such that
A2: ( a in E ^omega & b in E ^omega ) and
A3: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = b as Element of E ^omega by A2;
a -->. b,S by A1, A3, Def4;
then a ==>. b,S by Th10;
hence x in ==>.-relation S by A3, Def6; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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 )
let S be semi-Thue-system of E; ::_thesis: 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 )
let u be Element of E ^omega ; ::_thesis: 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 )
let p be FinSequence of E ^omega ; ::_thesis: ( p is RedSequence of ==>.-relation S implies ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) )
assume A1: p is RedSequence of ==>.-relation S ; ::_thesis: ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S )
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(p_+^_u)_&_i_+_1_in_dom_(p_+^_u)_holds_
[((p_+^_u)_._i),((p_+^_u)_._(i_+_1))]_in_==>.-relation_S
let i be Element of NAT ; ::_thesis: ( i in dom (p +^ u) & i + 1 in dom (p +^ u) implies [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S )
assume that
A3: i in dom (p +^ u) and
A4: i + 1 in dom (p +^ u) ; ::_thesis: [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S
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; ::_thesis: verum
end;
A9: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(u_^+_p)_&_i_+_1_in_dom_(u_^+_p)_holds_
[((u_^+_p)_._i),((u_^+_p)_._(i_+_1))]_in_==>.-relation_S
let i be Element of NAT ; ::_thesis: ( i in dom (u ^+ p) & i + 1 in dom (u ^+ p) implies [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S )
assume that
A10: i in dom (u ^+ p) and
A11: i + 1 in dom (u ^+ p) ; ::_thesis: [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S
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; ::_thesis: verum
end;
len (p +^ u) = len p by Th5;
hence p +^ u is RedSequence of ==>.-relation S by A1, A2, REWRITE1:def_2; ::_thesis: u ^+ p is RedSequence of ==>.-relation S
len (u ^+ p) = len p by Th5;
hence u ^+ p is RedSequence of ==>.-relation S by A1, A9, REWRITE1:def_2; ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: 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
let t, u be Element of E ^omega ; ::_thesis: for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds
(t ^+ p) +^ u is RedSequence of ==>.-relation S
let p be FinSequence of E ^omega ; ::_thesis: ( p is RedSequence of ==>.-relation S implies (t ^+ p) +^ u is RedSequence of ==>.-relation S )
assume p is RedSequence of ==>.-relation S ; ::_thesis: (t ^+ p) +^ u is RedSequence of ==>.-relation S
then t ^+ p is RedSequence of ==>.-relation S by Th23;
hence (t ^+ p) +^ u is RedSequence of ==>.-relation S by Th23; ::_thesis: verum
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
let E be set ; ::_thesis: for S being semi-Thue-system of E st S is Thue-system of E holds
==>.-relation S = (==>.-relation S) ~
let S be semi-Thue-system of E; ::_thesis: ( S is Thue-system of E implies ==>.-relation S = (==>.-relation S) ~ )
assume A1: S is Thue-system of E ; ::_thesis: ==>.-relation S = (==>.-relation S) ~
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_==>.-relation_S_implies_x_in_(==>.-relation_S)_~_)_&_(_x_in_(==>.-relation_S)_~_implies_x_in_==>.-relation_S_)_)
let x be set ; ::_thesis: ( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) )
thus ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) ::_thesis: ( x in (==>.-relation S) ~ implies x in ==>.-relation S )
proof
assume A2: x in ==>.-relation S ; ::_thesis: x in (==>.-relation S) ~
then consider a, b being set such that
A3: ( a in E ^omega & b in E ^omega ) and
A4: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = 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 x in (==>.-relation S) ~ by A4, RELAT_1:def_7; ::_thesis: verum
end;
thus ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) ::_thesis: verum
proof
assume A5: x in (==>.-relation S) ~ ; ::_thesis: x in ==>.-relation S
then consider a, b being set such that
A6: ( a in E ^omega & b in E ^omega ) and
A7: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = 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 x in ==>.-relation S by A7, Def6; ::_thesis: verum
end;
end;
hence ==>.-relation S = (==>.-relation S) ~ by TARSKI:1; ::_thesis: verum
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
let E be set ; ::_thesis: for S, T being semi-Thue-system of E st S c= T holds
==>.-relation S c= ==>.-relation T
let S, T be semi-Thue-system of E; ::_thesis: ( S c= T implies ==>.-relation S c= ==>.-relation T )
assume A1: S c= T ; ::_thesis: ==>.-relation S c= ==>.-relation T
thus for x being set st x in ==>.-relation S holds
x in ==>.-relation T :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in ==>.-relation S implies x in ==>.-relation T )
assume A2: x in ==>.-relation S ; ::_thesis: x in ==>.-relation T
then consider s, t being set such that
A3: x = [s,t] and
A4: ( s in E ^omega & t in E ^omega ) by RELSET_1:2;
reconsider s = s, t = t as Element of E ^omega by A4;
s ==>. t,S by A2, A3, Def6;
then s ==>. t,T by A1, Th19;
hence x in ==>.-relation T by A3, Def6; ::_thesis: verum
end;
end;
theorem Th27: :: REWRITE2:27
for E being set holds ==>.-relation (id (E ^omega)) = id (E ^omega)
proof
let E be set ; ::_thesis: ==>.-relation (id (E ^omega)) = id (E ^omega)
A1: ==>.-relation (id (E ^omega)) c= id (E ^omega)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation (id (E ^omega)) or x in id (E ^omega) )
assume A2: x in ==>.-relation (id (E ^omega)) ; ::_thesis: x in id (E ^omega)
then consider a, b being set such that
A3: ( a in E ^omega & b in E ^omega ) and
A4: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = b as Element of E ^omega by A3;
a ==>. b, id (E ^omega) by A2, A4, Def6;
then consider v, w, s1, t1 being Element of E ^omega such that
A5: ( a = (v ^ s1) ^ w & b = (v ^ t1) ^ w ) and
A6: s1 -->. t1, id (E ^omega) by Def5;
[s1,t1] in id (E ^omega) by A6, Def4;
then s1 = t1 by RELAT_1:def_10;
hence x in id (E ^omega) by A4, A5, RELAT_1:def_10; ::_thesis: verum
end;
id (E ^omega) c= ==>.-relation (id (E ^omega)) by Th22;
hence ==>.-relation (id (E ^omega)) = id (E ^omega) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let E be set ; ::_thesis: for S being semi-Thue-system of E holds ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega))
let S be semi-Thue-system of E; ::_thesis: ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega))
A1: ==>.-relation (S \/ (id (E ^omega))) c= (==>.-relation S) \/ (id (E ^omega))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation (S \/ (id (E ^omega))) or x in (==>.-relation S) \/ (id (E ^omega)) )
assume A2: x in ==>.-relation (S \/ (id (E ^omega))) ; ::_thesis: x in (==>.-relation S) \/ (id (E ^omega))
then consider a, b being set such that
A3: ( a in E ^omega & b in E ^omega ) and
A4: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = b as Element of E ^omega by A3;
a ==>. b,S \/ (id (E ^omega)) by A2, A4, Def6;
then consider v, w, s1, t1 being Element of E ^omega such that
A5: ( a = (v ^ s1) ^ w & b = (v ^ t1) ^ w ) and
A6: s1 -->. t1,S \/ (id (E ^omega)) by Def5;
A7: [s1,t1] in S \/ (id (E ^omega)) by A6, Def4;
percases ( [s1,t1] in S or [s1,t1] in id (E ^omega) ) by A7, XBOOLE_0:def_3;
suppose [s1,t1] in S ; ::_thesis: x in (==>.-relation S) \/ (id (E ^omega))
then s1 -->. t1,S by Def4;
then (v ^ s1) ^ w ==>. (v ^ t1) ^ w,S by Th15;
then x in ==>.-relation S by A4, A5, Def6;
hence x in (==>.-relation S) \/ (id (E ^omega)) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose [s1,t1] in id (E ^omega) ; ::_thesis: x in (==>.-relation S) \/ (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 x in (==>.-relation S) \/ (id (E ^omega)) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
(==>.-relation S) \/ (id (E ^omega)) c= ==>.-relation (S \/ (id (E ^omega)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (==>.-relation S) \/ (id (E ^omega)) or x in ==>.-relation (S \/ (id (E ^omega))) )
assume A8: x in (==>.-relation S) \/ (id (E ^omega)) ; ::_thesis: x in ==>.-relation (S \/ (id (E ^omega)))
percases ( x in ==>.-relation S or x in id (E ^omega) ) by A8, XBOOLE_0:def_3;
supposeA9: x in ==>.-relation S ; ::_thesis: x in ==>.-relation (S \/ (id (E ^omega)))
==>.-relation S c= ==>.-relation (S \/ (id (E ^omega))) by Th26, XBOOLE_1:7;
hence x in ==>.-relation (S \/ (id (E ^omega))) by A9; ::_thesis: verum
end;
supposeA10: x in id (E ^omega) ; ::_thesis: x in ==>.-relation (S \/ (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 x in ==>.-relation (S \/ (id (E ^omega))) by A11; ::_thesis: verum
end;
end;
end;
hence ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th29: :: REWRITE2:29
for E being set holds ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega))
proof
let E be set ; ::_thesis: ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega))
A1: ==>.-relation ({} ((E ^omega),(E ^omega))) c= {} ((E ^omega),(E ^omega))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation ({} ((E ^omega),(E ^omega))) or x in {} ((E ^omega),(E ^omega)) )
assume A2: x in ==>.-relation ({} ((E ^omega),(E ^omega))) ; ::_thesis: x in {} ((E ^omega),(E ^omega))
then consider a, b being set such that
A3: ( a in E ^omega & b in E ^omega ) and
A4: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = b as Element of E ^omega by A3;
a ==>. b, {} ((E ^omega),(E ^omega)) by A2, A4, Def6;
hence x in {} ((E ^omega),(E ^omega)) by Th20; ::_thesis: verum
end;
{} ((E ^omega),(E ^omega)) = {} by PARTIT_2:def_1;
then {} ((E ^omega),(E ^omega)) c= ==>.-relation ({} ((E ^omega),(E ^omega))) by XBOOLE_1:2;
hence ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega)) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s ==>. t, ==>.-relation S holds
s ==>. t,S
let s, t be Element of E ^omega ; ::_thesis: ( s ==>. t, ==>.-relation S implies s ==>. t,S )
assume s ==>. t, ==>.-relation S ; ::_thesis: s ==>. t,S
then consider v, w, s1, t1 being Element of E ^omega such that
A1: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and
A2: s1 -->. t1, ==>.-relation S by Def5;
[s1,t1] in ==>.-relation S by A2, Def4;
then s1 ==>. t1,S by Def6;
hence s ==>. t,S by A1, Th13; ::_thesis: verum
end;
theorem Th31: :: REWRITE2:31
for E being set
for S being semi-Thue-system of E holds ==>.-relation (==>.-relation S) = ==>.-relation S
proof
let E be set ; ::_thesis: for S being semi-Thue-system of E holds ==>.-relation (==>.-relation S) = ==>.-relation S
let S be semi-Thue-system of E; ::_thesis: ==>.-relation (==>.-relation S) = ==>.-relation S
A1: ==>.-relation (==>.-relation S) c= ==>.-relation S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation (==>.-relation S) or x in ==>.-relation S )
assume A2: x in ==>.-relation (==>.-relation S) ; ::_thesis: x in ==>.-relation S
then consider a, b being set such that
A3: ( a in E ^omega & b in E ^omega ) and
A4: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = b as Element of E ^omega by A3;
a ==>. b, ==>.-relation S by A2, A4, Def6;
then a ==>. b,S by Th30;
hence x in ==>.-relation S by A4, Def6; ::_thesis: verum
end;
==>.-relation S c= ==>.-relation (==>.-relation S) by Th22;
hence ==>.-relation (==>.-relation S) = ==>.-relation S by A1, XBOOLE_0:def_10; ::_thesis: verum
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 :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
proof
let E be set ; ::_thesis: for S being semi-Thue-system of E
for s being Element of E ^omega holds s ==>* s,S
let S be semi-Thue-system of E; ::_thesis: for s being Element of E ^omega holds s ==>* s,S
let s be Element of E ^omega ; ::_thesis: s ==>* s,S
==>.-relation S reduces s,s by REWRITE1:12;
hence s ==>* s,S by Def7; ::_thesis: verum
end;
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
let E be set ; ::_thesis: for S being semi-Thue-system of E
for s, t being Element of E ^omega st s ==>. t,S holds
s ==>* t,S
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s ==>. t,S holds
s ==>* t,S
let s, t be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies s ==>* t,S )
assume s ==>. t,S ; ::_thesis: s ==>* t,S
then [s,t] in ==>.-relation S by Def6;
then ==>.-relation S reduces s,t by REWRITE1:15;
hence s ==>* t,S by Def7; ::_thesis: verum
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
proof
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s ==>* t,S & t ==>* u,S holds
s ==>* u,S
let s, t, u be Element of E ^omega ; ::_thesis: ( s ==>* t,S & t ==>* u,S implies s ==>* u,S )
assume ( s ==>* t,S & t ==>* u,S ) ; ::_thesis: s ==>* u,S
then ( ==>.-relation S reduces s,t & ==>.-relation S reduces t,u ) by Def7;
then ==>.-relation S reduces s,u by REWRITE1:16;
hence s ==>* u,S by Def7; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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 )
let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s ==>* t,S holds
( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )
let s, t, u be Element of E ^omega ; ::_thesis: ( s ==>* t,S implies ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) )
assume s ==>* t,S ; ::_thesis: ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )
then ==>.-relation S reduces s,t by Def7;
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 = 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 by Def7; ::_thesis: u ^ s ==>* u ^ t,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 u ^ s ==>* u ^ t,S by Def7; ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S holds
(u ^ s) ^ v ==>* (u ^ t) ^ v,S
let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S implies (u ^ s) ^ v ==>* (u ^ t) ^ v,S )
assume s ==>* t,S ; ::_thesis: (u ^ s) ^ v ==>* (u ^ t) ^ v,S
then u ^ s ==>* u ^ t,S by Th36;
hence (u ^ s) ^ v ==>* (u ^ t) ^ v,S by Th36; ::_thesis: verum
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
let E be set ; ::_thesis: 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 )
let S be semi-Thue-system of E; ::_thesis: 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 )
let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S & u ==>* v,S implies ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S ) )
assume A1: ( s ==>* t,S & u ==>* v,S ) ; ::_thesis: ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S )
then ( s ^ u ==>* t ^ u,S & t ^ u ==>* t ^ v,S ) by Th36;
hence s ^ u ==>* t ^ v,S by Th35; ::_thesis: u ^ s ==>* v ^ t,S
( u ^ s ==>* u ^ t,S & u ^ t ==>* v ^ t,S ) by A1, Th36;
hence u ^ s ==>* v ^ t,S by Th35; ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S is Thue-system of E & s ==>* t,S holds
t ==>* s,S
let s, t be Element of E ^omega ; ::_thesis: ( S is Thue-system of E & s ==>* t,S implies t ==>* s,S )
assume that
A1: S is Thue-system of E and
A2: s ==>* t,S ; ::_thesis: t ==>* s,S
==>.-relation S reduces s,t by A2, Def7;
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;
(Rev p) . (len p) = s by A3, FINSEQ_5:62;
then A5: (Rev p) . (len (Rev p)) = s by FINSEQ_5:def_3;
Rev p is RedSequence of (==>.-relation S) ~ by REWRITE1:9;
then A6: Rev p is RedSequence of ==>.-relation S by A1, Th25;
(Rev p) . 1 = t by A4, FINSEQ_5:62;
then ==>.-relation S reduces t,s by A6, A5, REWRITE1:def_3;
hence t ==>* s,S by Def7; ::_thesis: verum
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
proof
let E be set ; ::_thesis: 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
let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S c= T & s ==>* t,S holds
s ==>* t,T
let s, t be Element of E ^omega ; ::_thesis: ( S c= T & s ==>* t,S implies s ==>* t,T )
assume that
A1: S c= T and
A2: s ==>* t,S ; ::_thesis: s ==>* t,T
==>.-relation S reduces s,t by A2, Def7;
then ==>.-relation T reduces s,t by A1, Th26, REWRITE1:22;
hence s ==>* t,T by Def7; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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)) )
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega holds
( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) )
let s, t be Element of E ^omega ; ::_thesis: ( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) )
thus ( s ==>* t,S implies s ==>* t,S \/ (id (E ^omega)) ) by Th40, XBOOLE_1:7; ::_thesis: ( s ==>* t,S \/ (id (E ^omega)) implies s ==>* t,S )
assume s ==>* t,S \/ (id (E ^omega)) ; ::_thesis: s ==>* t,S
then ==>.-relation (S \/ (id (E ^omega))) reduces s,t by Def7;
then (==>.-relation S) \/ (id (E ^omega)) reduces s,t by Th28;
then ==>.-relation S reduces s,t by REWRITE1:23;
hence s ==>* t,S by Def7; ::_thesis: verum
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
let E be set ; ::_thesis: for s, t being Element of E ^omega st s ==>* t, {} ((E ^omega),(E ^omega)) holds
s = t
let s, t be Element of E ^omega ; ::_thesis: ( s ==>* t, {} ((E ^omega),(E ^omega)) implies s = t )
assume s ==>* t, {} ((E ^omega),(E ^omega)) ; ::_thesis: s = t
then ==>.-relation ({} ((E ^omega),(E ^omega))) reduces s,t by Def7;
then {} ((E ^omega),(E ^omega)) reduces s,t by Th29;
then {} reduces s,t by PARTIT_2:def_1;
hence s = t by REWRITE1:13; ::_thesis: verum
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
proof
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s ==>* t, ==>.-relation S holds
s ==>* t,S
let s, t be Element of E ^omega ; ::_thesis: ( s ==>* t, ==>.-relation S implies s ==>* t,S )
assume s ==>* t, ==>.-relation S ; ::_thesis: s ==>* t,S
then ==>.-relation (==>.-relation S) reduces s,t by Def7;
then ==>.-relation S reduces s,t by Th31;
hence s ==>* t,S by Def7; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>. v,{[s,t]} holds
u ==>* v,S
let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S & u ==>. v,{[s,t]} implies u ==>* v,S )
assume that
A1: s ==>* t,S and
A2: u ==>. v,{[s,t]} ; ::_thesis: u ==>* v,S
consider u1, v1, s1, t1 being Element of E ^omega such that
A3: ( u = (u1 ^ s1) ^ v1 & v = (u1 ^ t1) ^ v1 ) and
A4: s1 -->. t1,{[s,t]} by A2, Def5;
[s1,t1] in {[s,t]} by A4, Def4;
then [s1,t1] = [s,t] by TARSKI:def_1;
then ( s1 = s & t1 = t ) by XTUPLE_0:1;
hence u ==>* v,S by A1, A3, Th37; ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds
u ==>* v,S
let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S & u ==>* v,S \/ {[s,t]} implies u ==>* v,S )
assume that
A1: s ==>* t,S and
A2: u ==>* v,S \/ {[s,t]} ; ::_thesis: u ==>* v,S
==>.-relation (S \/ {[s,t]}) reduces u,v by A2, Def7;
then A3: ex p2 being RedSequence of ==>.-relation (S \/ {[s,t]}) st
( p2 . 1 = u & p2 . (len p2) = v ) by REWRITE1:def_3;
defpred S1[ Nat] means for p being RedSequence of ==>.-relation (S \/ {[s,t]})
for s1, t1 being Element of E ^omega st len p = $1 & p . 1 = s1 & p . (len p) = t1 holds
ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 );
A4: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let p be RedSequence of ==>.-relation (S \/ {[s,t]}); ::_thesis: for s1, t1 being Element of E ^omega st len p = k + 1 & p . 1 = s1 & p . (len p) = t1 holds
ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 )
let s1, t1 be Element of E ^omega ; ::_thesis: ( len p = k + 1 & p . 1 = s1 & p . (len p) = t1 implies ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 ) )
assume that
A6: len p = k + 1 and
A7: p . 1 = s1 and
A8: p . (len p) = t1 ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 )
percases ( ( not k in dom p & k + 1 in dom p ) or not k + 1 in dom p or ( k in dom p & k + 1 in dom p ) ) ;
suppose ( not k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 )
then k = 0 by Th1;
then p = <*s1*> by A6, A7, FINSEQ_1:40;
then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:6;
take p ; ::_thesis: ( p . 1 = s1 & p . (len p) = t1 )
thus ( p . 1 = s1 & p . (len p) = t1 ) by A7, A8; ::_thesis: verum
end;
suppose not k + 1 in dom p ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 )
then 0 + 1 > k + 1 by A6, FINSEQ_3:25;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 ) by XREAL_1:6; ::_thesis: verum
end;
supposeA9: ( k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 )
set w = p . k;
A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ {[s,t]}) by A9, REWRITE1:def_2;
then reconsider w = p . k 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
percases ( w ==>. t1,S or w ==>. t1,{[s,t]} ) by A11, Th21;
suppose w ==>. t1,S ; ::_thesis: w ==>* t1,S
hence w ==>* t1,S by Th33; ::_thesis: verum
end;
suppose w ==>. t1,{[s,t]} ; ::_thesis: w ==>* t1,S
hence w ==>* t1,S by A1, Th44; ::_thesis: verum
end;
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 by Def7;
then s1 ==>* t1,S by A12, Th35;
then ==>.-relation S reduces s1,t1 by Def7;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 ) by REWRITE1:def_3; ::_thesis: verum
end;
end;
end;
end;
A13: S1[ 0 ] by REWRITE1:def_2;
for k being Nat holds S1[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 u ==>* v,S by Def7; ::_thesis: verum
end;
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)
proof
set X = { s where s is Element of E ^omega : w ==>* s,S } ;
{ s where s is Element of E ^omega : w ==>* s,S } c= E ^omega
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { s where s is Element of E ^omega : w ==>* s,S } or x in E ^omega )
assume x in { s where s is Element of E ^omega : w ==>* s,S } ; ::_thesis: x in E ^omega
then ex t being Element of E ^omega st
( t = x & w ==>* t,S ) ;
hence x in E ^omega ; ::_thesis: verum
end;
hence { s where s is Element of E ^omega : w ==>* s,S } is Subset of (E ^omega) ; ::_thesis: verum
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
let E be set ; ::_thesis: 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 )
let S be semi-Thue-system of E; ::_thesis: for s, w being Element of E ^omega holds
( s in Lang (w,S) iff w ==>* s,S )
let s, w be Element of E ^omega ; ::_thesis: ( s in Lang (w,S) iff w ==>* s,S )
thus ( s in Lang (w,S) implies w ==>* s,S ) ::_thesis: ( w ==>* s,S implies s in Lang (w,S) )
proof
assume s in Lang (w,S) ; ::_thesis: w ==>* s,S
then ex t being Element of E ^omega st
( t = s & w ==>* t,S ) ;
hence w ==>* s,S ; ::_thesis: verum
end;
thus ( w ==>* s,S implies s in Lang (w,S) ) ; ::_thesis: verum
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
let E be set ; ::_thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds w in Lang (w,S)
let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds w in Lang (w,S)
let w be Element of E ^omega ; ::_thesis: w in Lang (w,S)
w ==>* w,S by Th32;
hence w in Lang (w,S) ; ::_thesis: verum
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
let E be set ; ::_thesis: 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)
let S, T be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S c= T holds
Lang (w,S) c= Lang (w,T)
let w be Element of E ^omega ; ::_thesis: ( S c= T implies Lang (w,S) c= Lang (w,T) )
assume A1: S c= T ; ::_thesis: Lang (w,S) c= Lang (w,T)
thus for x being set st x in Lang (w,S) holds
x in Lang (w,T) :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in Lang (w,S) implies x in Lang (w,T) )
assume A2: x in Lang (w,S) ; ::_thesis: x in Lang (w,T)
then reconsider y = x as Element of E ^omega ;
w ==>* y,S by A2, Th46;
then w ==>* y,T by A1, Th40;
hence x in Lang (w,T) ; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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))))
let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds Lang (w,S) = Lang (w,(S \/ (id (E ^omega))))
let w be Element of E ^omega ; ::_thesis: Lang (w,S) = Lang (w,(S \/ (id (E ^omega))))
A1: Lang (w,(S \/ (id (E ^omega)))) c= Lang (w,S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(S \/ (id (E ^omega)))) or x in Lang (w,S) )
assume A2: x in Lang (w,(S \/ (id (E ^omega)))) ; ::_thesis: x in Lang (w,S)
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 x in Lang (w,S) ; ::_thesis: verum
end;
Lang (w,S) c= Lang (w,(S \/ (id (E ^omega)))) by Th48, XBOOLE_1:7;
hence Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) by A1, XBOOLE_0:def_10; ::_thesis: verum
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
let E be set ; ::_thesis: for w being Element of E ^omega holds Lang (w,({} ((E ^omega),(E ^omega)))) = {w}
let w be Element of E ^omega ; ::_thesis: Lang (w,({} ((E ^omega),(E ^omega)))) = {w}
now__::_thesis:_for_x_being_set_st_x_<>_w_holds_
not_x_in_Lang_(w,({}_((E_^omega),(E_^omega))))
let x be set ; ::_thesis: ( x <> w implies not x in Lang (w,({} ((E ^omega),(E ^omega)))) )
assume that
A1: x <> w and
A2: x in Lang (w,({} ((E ^omega),(E ^omega)))) ; ::_thesis: contradiction
reconsider t = x as Element of E ^omega by A2;
w ==>* t, {} ((E ^omega),(E ^omega)) by A2, Th46;
hence contradiction by A1, Th42; ::_thesis: verum
end;
then for x being set holds
( x in Lang (w,({} ((E ^omega),(E ^omega)))) iff x = w ) by Th47;
hence Lang (w,({} ((E ^omega),(E ^omega)))) = {w} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: REWRITE2:51
for E being set
for w being Element of E ^omega holds Lang (w,(id (E ^omega))) = {w}
proof
let E be set ; ::_thesis: for w being Element of E ^omega holds Lang (w,(id (E ^omega))) = {w}
let w be Element of E ^omega ; ::_thesis: Lang (w,(id (E ^omega))) = {w}
({} ((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 ;
::_thesis: verum
end;
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
proof
let E be set ; ::_thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds S,S are_equivalent_wrt w
let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds S,S are_equivalent_wrt w
let w be Element of E ^omega ; ::_thesis: S,S are_equivalent_wrt w
thus Lang (w,S) = Lang (w,S) ; :: according to REWRITE2:def_9 ::_thesis: verum
end;
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
proof
let E be set ; ::_thesis: 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
let S, T be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w holds
T,S are_equivalent_wrt w
let w be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w implies T,S are_equivalent_wrt w )
assume Lang (w,S) = Lang (w,T) ; :: according to REWRITE2:def_9 ::_thesis: T,S are_equivalent_wrt w
hence T,S are_equivalent_wrt w by Def9; ::_thesis: verum
end;
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
proof
let E be set ; ::_thesis: 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
let S, T, U be semi-Thue-system of E; ::_thesis: 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
let w be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w & T,U are_equivalent_wrt w implies S,U are_equivalent_wrt w )
assume ( Lang (w,S) = Lang (w,T) & Lang (w,T) = Lang (w,U) ) ; :: according to REWRITE2:def_9 ::_thesis: S,U are_equivalent_wrt w
hence S,U are_equivalent_wrt w by Def9; ::_thesis: verum
end;
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
proof
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds S,S \/ (id (E ^omega)) are_equivalent_wrt w
let w be Element of E ^omega ; ::_thesis: S,S \/ (id (E ^omega)) are_equivalent_wrt w
Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) by Th49;
hence S,S \/ (id (E ^omega)) are_equivalent_wrt w by Def9; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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 )
let S, T, U be semi-Thue-system of E; ::_thesis: 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 )
let w be Element of E ^omega ; ::_thesis: ( 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 ) )
assume that
A1: Lang (w,S) = Lang (w,T) and
A2: ( S c= U & U c= T ) ; :: according to REWRITE2:def_9 ::_thesis: ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w )
( 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; :: according to REWRITE2:def_9 ::_thesis: U,T are_equivalent_wrt w
hence U,T are_equivalent_wrt w by A1, Def9; ::_thesis: verum
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
let E be set ; ::_thesis: for S being semi-Thue-system of E
for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w
let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w
let w be Element of E ^omega ; ::_thesis: S, ==>.-relation S are_equivalent_wrt w
A1: Lang (w,(==>.-relation S)) c= Lang (w,S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(==>.-relation S)) or x in Lang (w,S) )
assume A2: x in Lang (w,(==>.-relation S)) ; ::_thesis: x in Lang (w,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 x in Lang (w,S) ; ::_thesis: verum
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; :: according to REWRITE2:def_9 ::_thesis: verum
end;
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 & ==>.-relation (S \/ T) reduces w,s holds
==>.-relation S reduces w,s
proof
let E be set ; ::_thesis: for S, T being semi-Thue-system of E
for w, s being Element of E ^omega st S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s holds
==>.-relation S reduces w,s
let S, T be semi-Thue-system of E; ::_thesis: for w, s being Element of E ^omega st S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s holds
==>.-relation S reduces w,s
let w, s be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s implies ==>.-relation S reduces w,s )
assume that
A1: Lang (w,S) = Lang (w,T) and
A2: ==>.-relation (S \/ T) reduces w,s ; :: according to REWRITE2:def_9 ::_thesis: ==>.-relation S 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 S1[ Nat] means for p being RedSequence of ==>.-relation (S \/ T)
for t being Element of E ^omega st len p = $1 & p . 1 = w & p . (len p) = t holds
ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t );
A4: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let p be RedSequence of ==>.-relation (S \/ T); ::_thesis: for t being Element of E ^omega st len p = k + 1 & p . 1 = w & p . (len p) = t holds
ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )
let t be Element of E ^omega ; ::_thesis: ( len p = k + 1 & p . 1 = w & p . (len p) = t implies ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) )
assume that
A6: len p = k + 1 and
A7: p . 1 = w and
A8: p . (len p) = t ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )
percases ( ( not k in dom p & k + 1 in dom p ) or not k + 1 in dom p or ( k in dom p & k + 1 in dom p ) ) ;
suppose ( not k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )
then k = 0 by Th1;
then p = <*w*> by A6, A7, FINSEQ_1:40;
then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:6;
take p ; ::_thesis: ( p . 1 = w & p . (len p) = t )
thus ( p . 1 = w & p . (len p) = t ) by A7, A8; ::_thesis: verum
end;
suppose not k + 1 in dom p ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )
then 0 + 1 > k + 1 by A6, FINSEQ_3:25;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) by XREAL_1:6; ::_thesis: verum
end;
supposeA9: ( k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )
set u = p . k;
A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ T) by A9, REWRITE1:def_2;
then reconsider u = p . k 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 by Def7;
percases ( u ==>. t,S or u ==>. t,T ) by A11, Th21;
suppose u ==>. t,S ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )
then u ==>* t,S by Th33;
then w ==>* t,S by A12, Th35;
then ==>.-relation S reduces w,t by Def7;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) by REWRITE1:def_3; ::_thesis: verum
end;
supposeA13: u ==>. t,T ; ::_thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = 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 by Def7;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) by REWRITE1:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
A15: S1[ 0 ] by REWRITE1:def_2;
for k being Nat holds S1[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 ==>.-relation S reduces w,s by REWRITE1:def_3; ::_thesis: verum
end;
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 & w ==>* s,S \/ T holds
w ==>* s,S
proof
let E be set ; ::_thesis: for S, T being semi-Thue-system of E
for w, s being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds
w ==>* s,S
let S, T be semi-Thue-system of E; ::_thesis: for w, s being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds
w ==>* s,S
let w, s be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w & w ==>* s,S \/ T implies w ==>* s,S )
assume that
A1: S,T are_equivalent_wrt w and
A2: w ==>* s,S \/ T ; ::_thesis: w ==>* s,S
==>.-relation (S \/ T) reduces w,s by A2, Def7;
then ==>.-relation S reduces w,s by A1, Th58;
hence w ==>* s,S by Def7; ::_thesis: verum
end;
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
let E be set ; ::_thesis: 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
let S, T be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w holds
S,S \/ T are_equivalent_wrt w
let w be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w implies S,S \/ T are_equivalent_wrt w )
assume A1: S,T are_equivalent_wrt w ; ::_thesis: S,S \/ T are_equivalent_wrt w
A2: Lang (w,(S \/ T)) c= Lang (w,S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(S \/ T)) or x in Lang (w,S) )
assume A3: x in Lang (w,(S \/ T)) ; ::_thesis: x in Lang (w,S)
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 x in Lang (w,S) ; ::_thesis: verum
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; :: according to REWRITE2:def_9 ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, w being Element of E ^omega st s ==>. t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
let s, t, w be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies S,S \/ {[s,t]} are_equivalent_wrt w )
assume s ==>. t,S ; ::_thesis: S,S \/ {[s,t]} are_equivalent_wrt w
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 S,S \/ {[s,t]} are_equivalent_wrt w by A1, Th56; ::_thesis: verum
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
let E be set ; ::_thesis: 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
let S be semi-Thue-system of E; ::_thesis: for s, t, w being Element of E ^omega st s ==>* t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
let s, t, w be Element of E ^omega ; ::_thesis: ( s ==>* t,S implies S,S \/ {[s,t]} are_equivalent_wrt w )
assume A1: s ==>* t,S ; ::_thesis: S,S \/ {[s,t]} are_equivalent_wrt w
A2: Lang (w,(S \/ {[s,t]})) c= Lang (w,S)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(S \/ {[s,t]})) or x in Lang (w,S) )
assume A3: x in Lang (w,(S \/ {[s,t]})) ; ::_thesis: x in Lang (w,S)
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 x in Lang (w,S) ; ::_thesis: verum
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; :: according to REWRITE2:def_9 ::_thesis: verum
end;