:: REWRITE1 semantic presentation
begin
definition
let p, q be FinSequence;
funcp $^ q -> FinSequence means :Def1: :: REWRITE1:def 1
it = p ^ q if ( p = {} or q = {} )
otherwise ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & it = r ^ q );
existence
( ( ( p = {} or q = {} ) implies ex b1 being FinSequence st b1 = p ^ q ) & ( p = {} or q = {} or ex b1 being FinSequence ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b1 = r ^ q ) ) )
proof
thus ( ( p = {} or q = {} ) implies ex r being FinSequence st r = p ^ q ) ; ::_thesis: ( p = {} or q = {} or ex b1 being FinSequence ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b1 = r ^ q ) )
assume that
A1: p <> {} and
q <> {} ; ::_thesis: ex b1 being FinSequence ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b1 = r ^ q )
len p >= 0 + 1 by A1, NAT_1:13;
then consider i being Nat such that
A2: len p = 1 + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
reconsider r = p | (Seg i) as FinSequence by FINSEQ_1:15;
take r ^ q ; ::_thesis: ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q )
take i ; ::_thesis: ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q )
take r ; ::_thesis: ( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q )
thus ( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence holds
( ( ( p = {} or q = {} ) & b1 = p ^ q & b2 = p ^ q implies b1 = b2 ) & ( p = {} or q = {} or for i being Element of NAT
for r being FinSequence holds
( not len p = i + 1 or not r = p | (Seg i) or not b1 = r ^ q ) or for i being Element of NAT
for r being FinSequence holds
( not len p = i + 1 or not r = p | (Seg i) or not b2 = r ^ q ) or b1 = b2 ) ) ;
consistency
for b1 being FinSequence holds verum ;
end;
:: deftheorem Def1 defines $^ REWRITE1:def_1_:_
for p, q, b3 being FinSequence holds
( ( ( p = {} or q = {} ) implies ( b3 = p $^ q iff b3 = p ^ q ) ) & ( p = {} or q = {} or ( b3 = p $^ q iff ex i being Element of NAT ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b3 = r ^ q ) ) ) );
Lm1: now__::_thesis:_for_p_being_FinSequence
for_x_being_Nat_st_x_in_dom_p_holds_
(_x_<=_len_p_&_x_>=_0_+_1_&_x_>_0_)
let p be FinSequence; ::_thesis: for x being Nat st x in dom p holds
( x <= len p & x >= 0 + 1 & x > 0 )
let x be Nat; ::_thesis: ( x in dom p implies ( x <= len p & x >= 0 + 1 & x > 0 ) )
assume x in dom p ; ::_thesis: ( x <= len p & x >= 0 + 1 & x > 0 )
then A1: x in Seg (len p) by FINSEQ_1:def_3;
hence ( x <= len p & x >= 0 + 1 ) by FINSEQ_1:1; ::_thesis: x > 0
thus x > 0 by A1, FINSEQ_1:1; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_p_being_FinSequence
for_x_being_Nat_st_x_+_1_in_dom_p_holds_
x_<_len_p
let p be FinSequence; ::_thesis: for x being Nat st x + 1 in dom p holds
x < len p
let x be Nat; ::_thesis: ( x + 1 in dom p implies x < len p )
assume x + 1 in dom p ; ::_thesis: x < len p
then x + 1 <= len p by Lm1;
hence x < len p by NAT_1:13; ::_thesis: verum
end;
Lm3: now__::_thesis:_for_p_being_FinSequence
for_x_being_Nat_st_(_x_<=_len_p_or_x_<_len_p_)_&_(_x_>=_1_or_x_>_0_)_holds_
x_in_dom_p
let p be FinSequence; ::_thesis: for x being Nat st ( x <= len p or x < len p ) & ( x >= 1 or x > 0 ) holds
x in dom p
let x be Nat; ::_thesis: ( ( x <= len p or x < len p ) & ( x >= 1 or x > 0 ) implies x in dom p )
assume that
A1: ( x <= len p or x < len p ) and
A2: ( x >= 1 or x > 0 ) ; ::_thesis: x in dom p
x >= 0 + 1 by A2, NAT_1:13;
then x in Seg (len p) by A1, FINSEQ_1:1;
hence x in dom p by FINSEQ_1:def_3; ::_thesis: verum
end;
Lm4: now__::_thesis:_for_p_being_FinSequence
for_x_being_Nat_st_x_<_len_p_holds_
x_+_1_in_dom_p
let p be FinSequence; ::_thesis: for x being Nat st x < len p holds
x + 1 in dom p
let x be Nat; ::_thesis: ( x < len p implies x + 1 in dom p )
assume x < len p ; ::_thesis: x + 1 in dom p
then x + 1 <= len p by NAT_1:13;
hence x + 1 in dom p by Lm3; ::_thesis: verum
end;
theorem :: REWRITE1:1
for p being FinSequence holds
( {} $^ p = p & p $^ {} = p )
proof
let p be FinSequence; ::_thesis: ( {} $^ p = p & p $^ {} = p )
( {} ^ p = p & p ^ {} = p ) by FINSEQ_1:34;
hence ( {} $^ p = p & p $^ {} = p ) by Def1; ::_thesis: verum
end;
theorem Th2: :: REWRITE1:2
for q, p being FinSequence
for x being set st q <> {} holds
(p ^ <*x*>) $^ q = p ^ q
proof
let q, p be FinSequence; ::_thesis: for x being set st q <> {} holds
(p ^ <*x*>) $^ q = p ^ q
let x be set ; ::_thesis: ( q <> {} implies (p ^ <*x*>) $^ q = p ^ q )
len <*x*> = 1 by FINSEQ_1:40;
then A1: len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:22;
assume q <> {} ; ::_thesis: (p ^ <*x*>) $^ q = p ^ q
then consider i being Element of NAT , r being FinSequence such that
A2: len (p ^ <*x*>) = i + 1 and
A3: r = (p ^ <*x*>) | (Seg i) and
A4: (p ^ <*x*>) $^ q = r ^ q by Def1;
i <= i + 1 by NAT_1:11;
then A5: len r = i by A2, A3, FINSEQ_1:17;
ex s being FinSequence st p ^ <*x*> = r ^ s by A3, FINSEQ_1:80;
then consider t being FinSequence such that
A6: p ^ t = r by A2, A1, A5, FINSEQ_1:47;
(len r) + 0 = (len p) + (len t) by A6, FINSEQ_1:22;
then t = {} by A2, A1, A5;
hence (p ^ <*x*>) $^ q = p ^ q by A4, A6, FINSEQ_1:34; ::_thesis: verum
end;
theorem :: REWRITE1:3
for p, q being FinSequence
for x, y being set holds (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q
proof
let p, q be FinSequence; ::_thesis: for x, y being set holds (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q
let x, y be set ; ::_thesis: (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q
(p ^ <*y*>) ^ q = p ^ (<*y*> ^ q) by FINSEQ_1:32;
hence (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q by Th2; ::_thesis: verum
end;
theorem :: REWRITE1:4
for q being FinSequence
for x being set st q <> {} holds
<*x*> $^ q = q
proof
let q be FinSequence; ::_thesis: for x being set st q <> {} holds
<*x*> $^ q = q
let x be set ; ::_thesis: ( q <> {} implies <*x*> $^ q = q )
( {} ^ <*x*> = <*x*> & {} ^ q = q ) by FINSEQ_1:34;
hence ( q <> {} implies <*x*> $^ q = q ) by Th2; ::_thesis: verum
end;
theorem :: REWRITE1:5
for p being FinSequence st p <> {} holds
ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 )
proof
let p be FinSequence; ::_thesis: ( p <> {} implies ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) )
defpred S1[ Element of NAT ] means for p being FinSequence st p <> {} & len p = $1 holds
ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 );
assume A1: p <> {} ; ::_thesis: ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 )
now__::_thesis:_for_i_being_Element_of_NAT_st_(_for_p_being_FinSequence_st_p_<>_{}_&_len_p_=_i_holds_
ex_x_being_set_ex_q_being_FinSequence_st_
(_p_=_<*x*>_^_q_&_len_p_=_(len_q)_+_1_)_)_holds_
for_p_being_FinSequence_st_p_<>_{}_&_len_p_=_i_+_1_holds_
ex_x_being_set_ex_q_being_FinSequence_st_
(_p_=_<*x*>_^_q_&_len_p_=_(len_q)_+_1_)
let i be Element of NAT ; ::_thesis: ( ( for p being FinSequence st p <> {} & len p = i holds
ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) ) implies for p being FinSequence st p <> {} & len p = i + 1 holds
ex x being set ex q being FinSequence st
( q = <*b4*> ^ b5 & len q = (len b5) + 1 ) )
assume A2: for p being FinSequence st p <> {} & len p = i holds
ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) ; ::_thesis: for p being FinSequence st p <> {} & len p = i + 1 holds
ex x being set ex q being FinSequence st
( q = <*b4*> ^ b5 & len q = (len b5) + 1 )
let p be FinSequence; ::_thesis: ( p <> {} & len p = i + 1 implies ex x being set ex q being FinSequence st
( q = <*b3*> ^ b4 & len q = (len b4) + 1 ) )
assume that
A3: p <> {} and
A4: len p = i + 1 ; ::_thesis: ex x being set ex q being FinSequence st
( q = <*b3*> ^ b4 & len q = (len b4) + 1 )
consider q being FinSequence, y being set such that
A5: p = q ^ <*y*> by A3, FINSEQ_1:46;
A6: len p = (len q) + (len <*y*>) by A5, FINSEQ_1:22;
A7: len <*y*> = 1 by FINSEQ_1:39;
percases ( q = {} or q <> {} ) ;
supposeA8: q = {} ; ::_thesis: ex x being set ex q being FinSequence st
( q = <*b3*> ^ b4 & len q = (len b4) + 1 )
then p = <*y*> by A5, FINSEQ_1:34
.= <*y*> ^ {} by FINSEQ_1:34 ;
hence ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A7, A6, A8; ::_thesis: verum
end;
suppose q <> {} ; ::_thesis: ex x being set ex q being FinSequence st
( q = <*b3*> ^ b4 & len q = (len b4) + 1 )
then consider x being set , r being FinSequence such that
A9: q = <*x*> ^ r and
A10: len q = (len r) + 1 by A2, A4, A7, A6;
A11: len (r ^ <*y*>) = (len r) + 1 by A7, FINSEQ_1:22;
p = <*x*> ^ (r ^ <*y*>) by A5, A9, FINSEQ_1:32;
hence ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A7, A6, A10, A11; ::_thesis: verum
end;
end;
end;
then A12: for i being Element of NAT st S1[i] holds
S1[i + 1] ;
A13: S1[ 0 ] ;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A13, A12);
hence ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A1; ::_thesis: verum
end;
scheme :: REWRITE1:sch 1
PathCatenation{ P1[ set , set ], F1() -> FinSequence, F2() -> FinSequence } :
for i being Element of NAT st i in dom (F1() $^ F2()) & i + 1 in dom (F1() $^ F2()) holds
for x, y being set st x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) holds
P1[x,y]
provided
A1: for i being Element of NAT st i in dom F1() & i + 1 in dom F1() holds
P1[F1() . i,F1() . (i + 1)] and
A2: for i being Element of NAT st i in dom F2() & i + 1 in dom F2() holds
P1[F2() . i,F2() . (i + 1)] and
A3: ( len F1() > 0 & len F2() > 0 & F1() . (len F1()) = F2() . 1 )
proof
F1() <> {} by A3;
then consider r being FinSequence, a being set such that
A4: F1() = r ^ <*a*> by FINSEQ_1:46;
F2() <> {} by A3;
then A5: F1() $^ F2() = r ^ F2() by A4, Th2;
0 + 1 <= len F2() by A3, NAT_1:13;
then A6: 1 in Seg (len F2()) by FINSEQ_1:1;
A7: Seg (len F2()) = dom F2() by FINSEQ_1:def_3;
let i be Element of NAT ; ::_thesis: ( i in dom (F1() $^ F2()) & i + 1 in dom (F1() $^ F2()) implies for x, y being set st x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) holds
P1[x,y] )
assume that
A8: i in dom (F1() $^ F2()) and
A9: i + 1 in dom (F1() $^ F2()) ; ::_thesis: for x, y being set st x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) holds
P1[x,y]
A10: i >= 0 + 1 by A8, Lm1;
let x, y be set ; ::_thesis: ( x = (F1() $^ F2()) . i & y = (F1() $^ F2()) . (i + 1) implies P1[x,y] )
A11: i + 1 >= 1 by NAT_1:11;
A12: len F1() = (len r) + (len <*a*>) by A4, FINSEQ_1:22
.= (len r) + 1 by FINSEQ_1:40 ;
assume that
A13: x = (F1() $^ F2()) . i and
A14: y = (F1() $^ F2()) . (i + 1) ; ::_thesis: P1[x,y]
percases ( i < len F1() or i >= len F1() ) ;
supposeA15: i < len F1() ; ::_thesis: P1[x,y]
then ( i in dom F1() & i + 1 in dom F1() ) by A10, Lm3, Lm4;
then A16: P1[F1() . i,F1() . (i + 1)] by A1;
A17: now__::_thesis:_(_i_+_1_<=_len_r_implies_(_y_=_r_._(i_+_1)_&_r_._(i_+_1)_=_F1()_._(i_+_1)_)_)
assume i + 1 <= len r ; ::_thesis: ( y = r . (i + 1) & r . (i + 1) = F1() . (i + 1) )
then i + 1 in Seg (len r) by A11, FINSEQ_1:1;
then i + 1 in dom r by FINSEQ_1:def_3;
hence ( y = r . (i + 1) & r . (i + 1) = F1() . (i + 1) ) by A14, A4, A5, FINSEQ_1:def_7; ::_thesis: verum
end;
A18: i <= len r by A12, A15, NAT_1:13;
then i in Seg (len r) by A10, FINSEQ_1:1;
then i in dom r by FINSEQ_1:def_3;
then A19: ( x = r . i & r . i = F1() . i ) by A13, A4, A5, FINSEQ_1:def_7;
( i = len r or i < len r ) by A18, XXREAL_0:1;
hence P1[x,y] by A3, A6, A7, A14, A5, A12, A16, A19, A17, FINSEQ_1:def_7, NAT_1:13; ::_thesis: verum
end;
suppose i >= len F1() ; ::_thesis: P1[x,y]
then consider k being Nat such that
A20: i = (len F1()) + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A21: i = (len r) + (1 + k) by A12, A20;
len (F1() $^ F2()) = (len r) + (len F2()) by A5, FINSEQ_1:22;
then A22: k + 1 < len F2() by A9, A21, Lm2, XREAL_1:7;
then A23: (k + 1) + 1 in dom F2() by Lm4;
A24: k + 1 in dom F2() by A22, Lm3;
then A25: x = F2() . (k + 1) by A13, A5, A21, FINSEQ_1:def_7;
((len r) + (1 + k)) + 1 = (len r) + ((k + 1) + 1) ;
then y = F2() . ((k + 1) + 1) by A14, A5, A12, A20, A23, FINSEQ_1:def_7;
hence P1[x,y] by A2, A24, A23, A25; ::_thesis: verum
end;
end;
end;
definition
let R be Relation;
mode RedSequence of R -> FinSequence means :Def2: :: REWRITE1:def 2
( len it > 0 & ( for i being Element of NAT st i in dom it & i + 1 in dom it holds
[(it . i),(it . (i + 1))] in R ) );
existence
ex b1 being FinSequence st
( len b1 > 0 & ( for i being Element of NAT st i in dom b1 & i + 1 in dom b1 holds
[(b1 . i),(b1 . (i + 1))] in R ) )
proof
take p = <*{}*>; ::_thesis: ( len p > 0 & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) )
thus len p > 0 ; ::_thesis: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R
let i be Element of NAT ; ::_thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in R )
assume that
A1: i in dom p and
A2: i + 1 in dom p ; ::_thesis: [(p . i),(p . (i + 1))] in R
A3: dom p = {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by A1, TARSKI:def_1;
hence [(p . i),(p . (i + 1))] in R by A3, A2, TARSKI:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines RedSequence REWRITE1:def_2_:_
for R being Relation
for b2 being FinSequence holds
( b2 is RedSequence of R iff ( len b2 > 0 & ( for i being Element of NAT st i in dom b2 & i + 1 in dom b2 holds
[(b2 . i),(b2 . (i + 1))] in R ) ) );
registration
let R be Relation;
cluster -> non empty for RedSequence of R;
coherence
for b1 being RedSequence of R holds not b1 is empty by Def2, CARD_1:27;
end;
theorem Th6: :: REWRITE1:6
for R being Relation
for a being set holds <*a*> is RedSequence of R
proof
let R be Relation; ::_thesis: for a being set holds <*a*> is RedSequence of R
let a be set ; ::_thesis: <*a*> is RedSequence of R
set p = <*a*>;
thus len <*a*> > 0 ; :: according to REWRITE1:def_2 ::_thesis: for i being Element of NAT st i in dom <*a*> & i + 1 in dom <*a*> holds
[(<*a*> . i),(<*a*> . (i + 1))] in R
let i be Element of NAT ; ::_thesis: ( i in dom <*a*> & i + 1 in dom <*a*> implies [(<*a*> . i),(<*a*> . (i + 1))] in R )
assume that
A1: i in dom <*a*> and
A2: i + 1 in dom <*a*> ; ::_thesis: [(<*a*> . i),(<*a*> . (i + 1))] in R
A3: dom <*a*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by A1, TARSKI:def_1;
hence [(<*a*> . i),(<*a*> . (i + 1))] in R by A3, A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th7: :: REWRITE1:7
for R being Relation
for a, b being set st [a,b] in R holds
<*a,b*> is RedSequence of R
proof
let R be Relation; ::_thesis: for a, b being set st [a,b] in R holds
<*a,b*> is RedSequence of R
let a, b be set ; ::_thesis: ( [a,b] in R implies <*a,b*> is RedSequence of R )
assume A1: [a,b] in R ; ::_thesis: <*a,b*> is RedSequence of R
set p = <*a,b*>;
thus len <*a,b*> > 0 ; :: according to REWRITE1:def_2 ::_thesis: for i being Element of NAT st i in dom <*a,b*> & i + 1 in dom <*a,b*> holds
[(<*a,b*> . i),(<*a,b*> . (i + 1))] in R
let i be Element of NAT ; ::_thesis: ( i in dom <*a,b*> & i + 1 in dom <*a,b*> implies [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R )
assume that
A2: i in dom <*a,b*> and
A3: i + 1 in dom <*a,b*> ; ::_thesis: [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R
len <*a,b*> = 1 + 1 by FINSEQ_1:44;
then i + 1 <= 1 + 1 by A3, Lm1;
then A4: i <= 1 by XREAL_1:6;
i >= 1 by A2, Lm1;
then ( <*a,b*> . 1 = a & i = 1 ) by A4, FINSEQ_1:44, XXREAL_0:1;
hence [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R by A1, FINSEQ_1:44; ::_thesis: verum
end;
theorem Th8: :: REWRITE1:8
for R being Relation
for p, q being RedSequence of R st p . (len p) = q . 1 holds
p $^ q is RedSequence of R
proof
let R be Relation; ::_thesis: for p, q being RedSequence of R st p . (len p) = q . 1 holds
p $^ q is RedSequence of R
let p, q be RedSequence of R; ::_thesis: ( p . (len p) = q . 1 implies p $^ q is RedSequence of R )
defpred S1[ set , set ] means [$1,$2] in R;
set r = p $^ q;
consider p1 being FinSequence, x being set such that
A1: p = p1 ^ <*x*> by FINSEQ_1:46;
assume p . (len p) = q . 1 ; ::_thesis: p $^ q is RedSequence of R
then A2: ( len p > 0 & len q > 0 & p . (len p) = q . 1 ) ;
p $^ q = p1 ^ q by A1, Th2;
hence len (p $^ q) > 0 ; :: according to REWRITE1:def_2 ::_thesis: for i being Element of NAT st i in dom (p $^ q) & i + 1 in dom (p $^ q) holds
[((p $^ q) . i),((p $^ q) . (i + 1))] in R
A3: for i being Element of NAT st i in dom q & i + 1 in dom q holds
S1[q . i,q . (i + 1)] by Def2;
A4: for i being Element of NAT st i in dom p & i + 1 in dom p holds
S1[p . i,p . (i + 1)] by Def2;
for i being Element of NAT st i in dom (p $^ q) & i + 1 in dom (p $^ q) holds
for x, y being set st x = (p $^ q) . i & y = (p $^ q) . (i + 1) holds
S1[x,y] from REWRITE1:sch_1(A4, A3, A2);
hence for i being Element of NAT st i in dom (p $^ q) & i + 1 in dom (p $^ q) holds
[((p $^ q) . i),((p $^ q) . (i + 1))] in R ; ::_thesis: verum
end;
theorem Th9: :: REWRITE1:9
for R being Relation
for p being RedSequence of R holds Rev p is RedSequence of R ~
proof
let R be Relation; ::_thesis: for p being RedSequence of R holds Rev p is RedSequence of R ~
let p be RedSequence of R; ::_thesis: Rev p is RedSequence of R ~
len p > 0 ;
hence len (Rev p) > 0 by FINSEQ_5:def_3; :: according to REWRITE1:def_2 ::_thesis: for i being Element of NAT st i in dom (Rev p) & i + 1 in dom (Rev p) holds
[((Rev p) . i),((Rev p) . (i + 1))] in R ~
let i be Element of NAT ; ::_thesis: ( i in dom (Rev p) & i + 1 in dom (Rev p) implies [((Rev p) . i),((Rev p) . (i + 1))] in R ~ )
assume that
A1: i in dom (Rev p) and
A2: i + 1 in dom (Rev p) ; ::_thesis: [((Rev p) . i),((Rev p) . (i + 1))] in R ~
A3: len (Rev p) = len p by FINSEQ_5:def_3;
then A4: dom (Rev p) = Seg (len p) by FINSEQ_1:def_3;
i + 1 <= len p by A3, A2, Lm1;
then reconsider k = ((len p) - (i + 1)) + 1 as Element of NAT by FINSEQ_5:1;
A5: dom p = Seg (len p) by FINSEQ_1:def_3;
then A6: k in dom p by A4, A2, FINSEQ_5:2;
k = (len p) - i ;
then k + 1 in dom p by A4, A5, A1, FINSEQ_5:2;
then A7: [(p . k),(p . (k + 1))] in R by A6, Def2;
( (Rev p) . i = p . (((len p) - i) + 1) & (Rev p) . (i + 1) = p . (((len p) - (i + 1)) + 1) ) by A1, A2, FINSEQ_5:def_3;
hence [((Rev p) . i),((Rev p) . (i + 1))] in R ~ by A7, RELAT_1:def_7; ::_thesis: verum
end;
theorem Th10: :: REWRITE1:10
for R, Q being Relation st R c= Q holds
for p being RedSequence of R holds p is RedSequence of Q
proof
let R, Q be Relation; ::_thesis: ( R c= Q implies for p being RedSequence of R holds p is RedSequence of Q )
assume A1: R c= Q ; ::_thesis: for p being RedSequence of R holds p is RedSequence of Q
let p be RedSequence of R; ::_thesis: p is RedSequence of Q
thus len p > 0 ; :: according to REWRITE1:def_2 ::_thesis: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in Q
let i be Element of NAT ; ::_thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in Q )
assume ( i in dom p & i + 1 in dom p ) ; ::_thesis: [(p . i),(p . (i + 1))] in Q
then [(p . i),(p . (i + 1))] in R by Def2;
hence [(p . i),(p . (i + 1))] in Q by A1; ::_thesis: verum
end;
begin
definition
let R be Relation;
let a, b be set ;
predR reduces a,b means :Def3: :: REWRITE1:def 3
ex p being RedSequence of R st
( p . 1 = a & p . (len p) = b );
end;
:: deftheorem Def3 defines reduces REWRITE1:def_3_:_
for R being Relation
for a, b being set holds
( R reduces a,b iff ex p being RedSequence of R st
( p . 1 = a & p . (len p) = b ) );
definition
let R be Relation;
let a, b be set ;
preda,b are_convertible_wrt R means :Def4: :: REWRITE1:def 4
R \/ (R ~) reduces a,b;
end;
:: deftheorem Def4 defines are_convertible_wrt REWRITE1:def_4_:_
for R being Relation
for a, b being set holds
( a,b are_convertible_wrt R iff R \/ (R ~) reduces a,b );
theorem Th11: :: REWRITE1:11
for R being Relation
for a, b being set holds
( R reduces a,b iff ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) )
proof
let R be Relation; ::_thesis: for a, b being set holds
( R reduces a,b iff ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) )
let a, b be set ; ::_thesis: ( R reduces a,b iff ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) )
thus ( R reduces a,b implies ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) ) ::_thesis: ( ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) implies R reduces a,b )
proof
given p being RedSequence of R such that A1: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def_3 ::_thesis: ex p being FinSequence st
( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) )
take p ; ::_thesis: ( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) )
thus ( len p > 0 & p . 1 = a & p . (len p) = b & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) ) by A1, Def2; ::_thesis: verum
end;
given p being FinSequence such that A2: len p > 0 and
A3: ( p . 1 = a & p . (len p) = b ) and
A4: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ; ::_thesis: R reduces a,b
reconsider p = p as RedSequence of R by A2, A4, Def2;
take p ; :: according to REWRITE1:def_3 ::_thesis: ( p . 1 = a & p . (len p) = b )
thus ( p . 1 = a & p . (len p) = b ) by A3; ::_thesis: verum
end;
theorem Th12: :: REWRITE1:12
for R being Relation
for a being set holds R reduces a,a
proof
let R be Relation; ::_thesis: for a being set holds R reduces a,a
let a be set ; ::_thesis: R reduces a,a
reconsider p = <*a*> as RedSequence of R by Th6;
take p ; :: according to REWRITE1:def_3 ::_thesis: ( p . 1 = a & p . (len p) = a )
len p = 1 by FINSEQ_1:40;
hence ( p . 1 = a & p . (len p) = a ) by FINSEQ_1:40; ::_thesis: verum
end;
theorem Th13: :: REWRITE1:13
for a, b being set st {} reduces a,b holds
a = b
proof
let a, b be set ; ::_thesis: ( {} reduces a,b implies a = b )
given p being RedSequence of {} such that A1: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def_3 ::_thesis: a = b
A2: now__::_thesis:_not_len_p_>_1
assume len p > 1 ; ::_thesis: contradiction
then ( 1 in dom p & 1 + 1 in dom p ) by Lm3, Lm4;
hence contradiction by Def2; ::_thesis: verum
end;
len p >= 0 + 1 by NAT_1:13;
hence a = b by A1, A2, XXREAL_0:1; ::_thesis: verum
end;
theorem Th14: :: REWRITE1:14
for R being Relation
for a, b being set st R reduces a,b & not a in field R holds
a = b
proof
let R be Relation; ::_thesis: for a, b being set st R reduces a,b & not a in field R holds
a = b
let a, b be set ; ::_thesis: ( R reduces a,b & not a in field R implies a = b )
given p being RedSequence of R such that A1: p . 1 = a and
A2: p . (len p) = b ; :: according to REWRITE1:def_3 ::_thesis: ( a in field R or a = b )
assume A3: not a in field R ; ::_thesis: a = b
A4: now__::_thesis:_not_len_p_>_1
assume len p > 1 ; ::_thesis: contradiction
then ( 1 in dom p & 1 + 1 in dom p ) by Lm3, Lm4;
then [(p . 1),(p . (1 + 1))] in R by Def2;
hence contradiction by A1, A3, RELAT_1:15; ::_thesis: verum
end;
len p >= 0 + 1 by NAT_1:13;
hence a = b by A1, A2, A4, XXREAL_0:1; ::_thesis: verum
end;
theorem Th15: :: REWRITE1:15
for R being Relation
for a, b being set st [a,b] in R holds
R reduces a,b
proof
let R be Relation; ::_thesis: for a, b being set st [a,b] in R holds
R reduces a,b
let a, b be set ; ::_thesis: ( [a,b] in R implies R reduces a,b )
assume [a,b] in R ; ::_thesis: R reduces a,b
then reconsider p = <*a,b*> as RedSequence of R by Th7;
take p ; :: according to REWRITE1:def_3 ::_thesis: ( p . 1 = a & p . (len p) = b )
len p = 2 by FINSEQ_1:44;
hence ( p . 1 = a & p . (len p) = b ) by FINSEQ_1:44; ::_thesis: verum
end;
theorem Th16: :: REWRITE1:16
for R being Relation
for a, b, c being set st R reduces a,b & R reduces b,c holds
R reduces a,c
proof
let R be Relation; ::_thesis: for a, b, c being set st R reduces a,b & R reduces b,c holds
R reduces a,c
let a, b, c be set ; ::_thesis: ( R reduces a,b & R reduces b,c implies R reduces a,c )
given p being RedSequence of R such that A1: p . 1 = a and
A2: p . (len p) = b ; :: according to REWRITE1:def_3 ::_thesis: ( not R reduces b,c or R reduces a,c )
given q being RedSequence of R such that A3: q . 1 = b and
A4: q . (len q) = c ; :: according to REWRITE1:def_3 ::_thesis: R reduces a,c
reconsider r = p $^ q as RedSequence of R by A2, A3, Th8;
take r ; :: according to REWRITE1:def_3 ::_thesis: ( r . 1 = a & r . (len r) = c )
consider p1 being FinSequence, x being set such that
A5: p = p1 ^ <*x*> by FINSEQ_1:46;
0 + 1 <= len q by NAT_1:13;
then len q in Seg (len q) by FINSEQ_1:1;
then A6: len q in dom q by FINSEQ_1:def_3;
A7: r = p1 ^ q by A5, Th2;
( p1 = {} or len p1 >= 0 + 1 ) by NAT_1:13;
then ( ( r = q & p = <*x*> ) or 1 in Seg (len p1) ) by A5, A7, FINSEQ_1:1, FINSEQ_1:34;
then ( 1 in dom p1 or ( len p = 1 & r = q ) ) by FINSEQ_1:40, FINSEQ_1:def_3;
then ( ( r . 1 = p1 . 1 & p1 . 1 = a ) or ( r . 1 = b & b = a ) ) by A1, A2, A3, A5, A7, FINSEQ_1:def_7;
hence r . 1 = a ; ::_thesis: r . (len r) = c
len r = (len p1) + (len q) by A7, FINSEQ_1:22;
hence r . (len r) = c by A4, A7, A6, FINSEQ_1:def_7; ::_thesis: verum
end;
theorem Th17: :: REWRITE1:17
for R being Relation
for p being RedSequence of R
for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
R reduces p . i,p . j
proof
let R be Relation; ::_thesis: for p being RedSequence of R
for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
R reduces p . i,p . j
let p be RedSequence of R; ::_thesis: for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
R reduces p . i,p . j
let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & i <= j implies R reduces p . i,p . j )
defpred S1[ Element of NAT ] means ( i + $1 in dom p implies R reduces p . i,p . (i + $1) );
assume that
A1: i in dom p and
A2: j in dom p and
A3: i <= j ; ::_thesis: R reduces p . i,p . j
consider k being Nat such that
A4: j = i + k by A3, NAT_1:10;
now__::_thesis:_for_j_being_Element_of_NAT_st_(_i_+_j_in_dom_p_implies_R_reduces_p_._i,p_._(i_+_j)_)_&_i_+_(j_+_1)_in_dom_p_holds_
R_reduces_p_._i,p_._(i_+_(j_+_1))
A5: i >= 1 by A1, Lm1;
let j be Element of NAT ; ::_thesis: ( ( i + j in dom p implies R reduces p . i,p . (i + j) ) & i + (j + 1) in dom p implies R reduces p . i,p . (i + (j + 1)) )
assume that
A6: ( i + j in dom p implies R reduces p . i,p . (i + j) ) and
A7: i + (j + 1) in dom p ; ::_thesis: R reduces p . i,p . (i + (j + 1))
A8: i + (j + 1) = (i + j) + 1 ;
then A9: i + j < len p by A7, Lm2;
then i + j in dom p by A5, Lm3;
then [(p . (i + j)),(p . (i + (j + 1)))] in R by A7, A8, Def2;
then R reduces p . (i + j),p . (i + (j + 1)) by Th15;
hence R reduces p . i,p . (i + (j + 1)) by A6, A5, A9, Lm3, Th16; ::_thesis: verum
end;
then A10: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A11: S1[ 0 ] by Th12;
A12: for j being Element of NAT holds S1[j] from NAT_1:sch_1(A11, A10);
k in NAT by ORDINAL1:def_12;
hence R reduces p . i,p . j by A2, A12, A4; ::_thesis: verum
end;
theorem Th18: :: REWRITE1:18
for R being Relation
for a, b being set st R reduces a,b & a <> b holds
( a in field R & b in field R )
proof
let R be Relation; ::_thesis: for a, b being set st R reduces a,b & a <> b holds
( a in field R & b in field R )
let a, b be set ; ::_thesis: ( R reduces a,b & a <> b implies ( a in field R & b in field R ) )
given p being RedSequence of R such that A1: a = p . 1 and
A2: b = p . (len p) ; :: according to REWRITE1:def_3 ::_thesis: ( not a <> b or ( a in field R & b in field R ) )
A3: len p >= 0 + 1 by NAT_1:13;
assume a <> b ; ::_thesis: ( a in field R & b in field R )
then len p > 1 by A1, A2, A3, XXREAL_0:1;
then A4: 1 + 1 in dom p by Lm4;
1 in dom p by A3, Lm3;
then A5: [a,(p . 2)] in R by A1, A4, Def2;
hence a in field R by RELAT_1:15; ::_thesis: b in field R
defpred S1[ Element of NAT ] means ( $1 in dom p implies p . $1 in field R );
A6: len p in dom p by FINSEQ_5:6;
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_p_._i_in_field_R_)_&_i_+_1_in_dom_p_holds_
p_._(i_+_1)_in_field_R
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies p . i in field R ) & i + 1 in dom p implies p . (b1 + 1) in field R )
assume that
( i in dom p implies p . i in field R ) and
A7: i + 1 in dom p ; ::_thesis: p . (b1 + 1) in field R
A8: i < len p by A7, Lm2;
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: p . (b1 + 1) in field R
hence p . (i + 1) in field R by A1, A5, RELAT_1:15; ::_thesis: verum
end;
suppose i > 0 ; ::_thesis: p . (b1 + 1) in field R
then i in dom p by A8, Lm3;
then [(p . i),(p . (i + 1))] in R by A7, Def2;
hence p . (i + 1) in field R by RELAT_1:15; ::_thesis: verum
end;
end;
end;
then A9: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A10: S1[ 0 ] by Lm1;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A10, A9);
hence b in field R by A2, A6; ::_thesis: verum
end;
theorem :: REWRITE1:19
for R being Relation
for a, b being set st R reduces a,b holds
( a in field R iff b in field R ) by Th18;
theorem Th20: :: REWRITE1:20
for R being Relation
for a, b being set holds
( R reduces a,b iff ( a = b or [a,b] in R [*] ) )
proof
let R be Relation; ::_thesis: for a, b being set holds
( R reduces a,b iff ( a = b or [a,b] in R [*] ) )
let a, b be set ; ::_thesis: ( R reduces a,b iff ( a = b or [a,b] in R [*] ) )
hereby ::_thesis: ( ( a = b or [a,b] in R [*] ) implies R reduces a,b )
assume A1: R reduces a,b ; ::_thesis: ( a <> b implies [a,b] in R [*] )
then consider p being RedSequence of R such that
A2: ( a = p . 1 & b = p . (len p) ) by Def3;
A3: now__::_thesis:_for_i_being_Nat_st_i_>=_1_&_i_<_len_p_holds_
[(p_._i),(p_._(i_+_1))]_in_R
let i be Nat; ::_thesis: ( i >= 1 & i < len p implies [(p . i),(p . (i + 1))] in R )
assume ( i >= 1 & i < len p ) ; ::_thesis: [(p . i),(p . (i + 1))] in R
then ( i in dom p & i + 1 in dom p ) by Lm3, Lm4;
hence [(p . i),(p . (i + 1))] in R by Def2; ::_thesis: verum
end;
assume a <> b ; ::_thesis: [a,b] in R [*]
then A4: ( a in field R & b in field R ) by A1, Th18;
len p >= 0 + 1 by NAT_1:13;
hence [a,b] in R [*] by A2, A4, A3, FINSEQ_1:def_16; ::_thesis: verum
end;
assume that
A5: ( a = b or [a,b] in R [*] ) and
A6: not R reduces a,b ; ::_thesis: contradiction
consider p being FinSequence such that
A7: len p >= 1 and
A8: ( p . 1 = a & p . (len p) = b ) and
A9: for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R by A5, A6, Th12, FINSEQ_1:def_16;
p is RedSequence of R
proof
thus len p > 0 by A7; :: according to REWRITE1:def_2 ::_thesis: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R
let i be Element of NAT ; ::_thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in R )
assume that
A10: i in dom p and
A11: i + 1 in dom p ; ::_thesis: [(p . i),(p . (i + 1))] in R
i >= 1 by A10, Lm1;
hence [(p . i),(p . (i + 1))] in R by A9, A11, Lm2; ::_thesis: verum
end;
hence contradiction by A6, A8, Def3; ::_thesis: verum
end;
theorem Th21: :: REWRITE1:21
for R being Relation
for a, b being set holds
( R reduces a,b iff R [*] reduces a,b )
proof
let R be Relation; ::_thesis: for a, b being set holds
( R reduces a,b iff R [*] reduces a,b )
let a, b be set ; ::_thesis: ( R reduces a,b iff R [*] reduces a,b )
( R reduces a,b iff ( a = b or [a,b] in R [*] ) ) by Th20;
hence ( R reduces a,b implies R [*] reduces a,b ) by Th12, Th15; ::_thesis: ( R [*] reduces a,b implies R reduces a,b )
given p being RedSequence of R [*] such that A1: a = p . 1 and
A2: b = p . (len p) ; :: according to REWRITE1:def_3 ::_thesis: R reduces a,b
defpred S1[ Element of NAT ] means ( $1 in dom p implies R reduces a,p . $1 );
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_R_reduces_a,p_._i_)_&_i_+_1_in_dom_p_holds_
R_reduces_a,p_._(i_+_1)
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies R reduces a,p . i ) & i + 1 in dom p implies R reduces a,p . (b1 + 1) )
assume that
A3: ( i in dom p implies R reduces a,p . i ) and
A4: i + 1 in dom p ; ::_thesis: R reduces a,p . (b1 + 1)
A5: i < len p by A4, Lm2;
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: R reduces a,p . (b1 + 1)
hence R reduces a,p . (i + 1) by A1, Th12; ::_thesis: verum
end;
supposeA6: i > 0 ; ::_thesis: R reduces a,p . (b1 + 1)
then i in dom p by A5, Lm3;
then [(p . i),(p . (i + 1))] in R [*] by A4, Def2;
then R reduces p . i,p . (i + 1) by Th20;
hence R reduces a,p . (i + 1) by A3, A5, A6, Lm3, Th16; ::_thesis: verum
end;
end;
end;
then A7: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A8: len p in dom p by FINSEQ_5:6;
A9: S1[ 0 ] by Lm1;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A9, A7);
hence R reduces a,b by A2, A8; ::_thesis: verum
end;
theorem Th22: :: REWRITE1:22
for R, Q being Relation st R c= Q holds
for a, b being set st R reduces a,b holds
Q reduces a,b
proof
let R, Q be Relation; ::_thesis: ( R c= Q implies for a, b being set st R reduces a,b holds
Q reduces a,b )
assume A1: R c= Q ; ::_thesis: for a, b being set st R reduces a,b holds
Q reduces a,b
let a, b be set ; ::_thesis: ( R reduces a,b implies Q reduces a,b )
given p being RedSequence of R such that A2: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def_3 ::_thesis: Q reduces a,b
p is RedSequence of Q by A1, Th10;
hence ex p being RedSequence of Q st
( p . 1 = a & p . (len p) = b ) by A2; :: according to REWRITE1:def_3 ::_thesis: verum
end;
theorem :: REWRITE1:23
for R being Relation
for X, a, b being set holds
( R reduces a,b iff R \/ (id X) reduces a,b )
proof
let R be Relation; ::_thesis: for X, a, b being set holds
( R reduces a,b iff R \/ (id X) reduces a,b )
let X be set ; ::_thesis: for a, b being set holds
( R reduces a,b iff R \/ (id X) reduces a,b )
let a, b be set ; ::_thesis: ( R reduces a,b iff R \/ (id X) reduces a,b )
thus ( R reduces a,b implies R \/ (id X) reduces a,b ) by Th22, XBOOLE_1:7; ::_thesis: ( R \/ (id X) reduces a,b implies R reduces a,b )
given p being RedSequence of R \/ (id X) such that A1: p . 1 = a and
A2: p . (len p) = b ; :: according to REWRITE1:def_3 ::_thesis: R reduces a,b
defpred S1[ Element of NAT ] means ( $1 in dom p implies R reduces a,p . $1 );
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_R_reduces_a,p_._i_)_&_i_+_1_in_dom_p_holds_
R_reduces_a,p_._(i_+_1)
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies R reduces a,p . i ) & i + 1 in dom p implies R reduces a,p . (b1 + 1) )
assume A3: ( i in dom p implies R reduces a,p . i ) ; ::_thesis: ( i + 1 in dom p implies R reduces a,p . (b1 + 1) )
assume A4: i + 1 in dom p ; ::_thesis: R reduces a,p . (b1 + 1)
percases ( i in dom p or not i in dom p ) ;
supposeA5: i in dom p ; ::_thesis: R reduces a,p . (b1 + 1)
then [(p . i),(p . (i + 1))] in R \/ (id X) by A4, Def2;
then ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in id X ) by XBOOLE_0:def_3;
then ( R reduces p . i,p . (i + 1) or p . i = p . (i + 1) ) by Th15, RELAT_1:def_10;
hence R reduces a,p . (i + 1) by A3, A5, Th16; ::_thesis: verum
end;
suppose not i in dom p ; ::_thesis: R reduces a,p . (b1 + 1)
then ( i < 0 + 1 or ( i > len p & i + 1 <= len p ) ) by A4, Lm1, Lm3;
then i = 0 by NAT_1:13;
hence R reduces a,p . (i + 1) by A1, Th12; ::_thesis: verum
end;
end;
end;
then A6: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A7: len p in dom p by Lm3;
A8: S1[ 0 ] by Lm1;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A8, A6);
hence R reduces a,b by A2, A7; ::_thesis: verum
end;
theorem Th24: :: REWRITE1:24
for R being Relation
for a, b being set st R reduces a,b holds
R ~ reduces b,a
proof
let R be Relation; ::_thesis: for a, b being set st R reduces a,b holds
R ~ reduces b,a
let a, b be set ; ::_thesis: ( R reduces a,b implies R ~ reduces b,a )
given p being RedSequence of R such that A1: p . 1 = a and
A2: p . (len p) = b ; :: according to REWRITE1:def_3 ::_thesis: R ~ reduces b,a
reconsider q = Rev p as RedSequence of R ~ by Th9;
take q ; :: according to REWRITE1:def_3 ::_thesis: ( q . 1 = b & q . (len q) = a )
1 in dom q by FINSEQ_5:6;
hence q . 1 = p . (((len p) - 1) + 1) by FINSEQ_5:def_3
.= b by A2 ;
::_thesis: q . (len q) = a
( len q in dom q & len q = len p ) by FINSEQ_5:6, FINSEQ_5:def_3;
hence q . (len q) = p . (((len p) - (len p)) + 1) by FINSEQ_5:def_3
.= a by A1 ;
::_thesis: verum
end;
Lm5: for R being Relation
for a, b being set st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt R implies b,a are_convertible_wrt R )
assume R \/ (R ~) reduces a,b ; :: according to REWRITE1:def_4 ::_thesis: b,a are_convertible_wrt R
then (R \/ (R ~)) ~ reduces b,a by Th24;
then (R ~) \/ ((R ~) ~) reduces b,a by RELAT_1:23;
hence R \/ (R ~) reduces b,a ; :: according to REWRITE1:def_4 ::_thesis: verum
end;
theorem Th25: :: REWRITE1:25
for R being Relation
for a, b being set st R reduces a,b holds
( a,b are_convertible_wrt R & b,a are_convertible_wrt R )
proof
let R be Relation; ::_thesis: for a, b being set st R reduces a,b holds
( a,b are_convertible_wrt R & b,a are_convertible_wrt R )
let a, b be set ; ::_thesis: ( R reduces a,b implies ( a,b are_convertible_wrt R & b,a are_convertible_wrt R ) )
given p being RedSequence of R such that A1: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def_3 ::_thesis: ( a,b are_convertible_wrt R & b,a are_convertible_wrt R )
p is RedSequence of R \/ (R ~)
proof
thus len p > 0 ; :: according to REWRITE1:def_2 ::_thesis: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R \/ (R ~)
let i be Element of NAT ; ::_thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in R \/ (R ~) )
assume ( i in dom p & i + 1 in dom p ) ; ::_thesis: [(p . i),(p . (i + 1))] in R \/ (R ~)
then [(p . i),(p . (i + 1))] in R by Def2;
hence [(p . i),(p . (i + 1))] in R \/ (R ~) by XBOOLE_0:def_3; ::_thesis: verum
end;
then R \/ (R ~) reduces a,b by A1, Def3;
hence a,b are_convertible_wrt R by Def4; ::_thesis: b,a are_convertible_wrt R
hence b,a are_convertible_wrt R by Lm5; ::_thesis: verum
end;
theorem Th26: :: REWRITE1:26
for R being Relation
for a being set holds a,a are_convertible_wrt R
proof
let R be Relation; ::_thesis: for a being set holds a,a are_convertible_wrt R
let a be set ; ::_thesis: a,a are_convertible_wrt R
R reduces a,a by Th12;
hence a,a are_convertible_wrt R by Th25; ::_thesis: verum
end;
theorem Th27: :: REWRITE1:27
for a, b being set st a,b are_convertible_wrt {} holds
a = b
proof
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt {} implies a = b )
assume a,b are_convertible_wrt {} ; ::_thesis: a = b
then {} \/ ({} ~) reduces a,b by Def4;
hence a = b by Th13; ::_thesis: verum
end;
theorem :: REWRITE1:28
for R being Relation
for a, b being set st a,b are_convertible_wrt R & not a in field R holds
a = b
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_convertible_wrt R & not a in field R holds
a = b
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt R & not a in field R implies a = b )
A1: ( field R = field (R ~) & field (R \/ (R ~)) = (field R) \/ (field (R ~)) ) by RELAT_1:18, RELAT_1:21;
assume R \/ (R ~) reduces a,b ; :: according to REWRITE1:def_4 ::_thesis: ( a in field R or a = b )
hence ( a in field R or a = b ) by A1, Th14; ::_thesis: verum
end;
theorem Th29: :: REWRITE1:29
for R being Relation
for a, b being set st [a,b] in R holds
a,b are_convertible_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st [a,b] in R holds
a,b are_convertible_wrt R
let a, b be set ; ::_thesis: ( [a,b] in R implies a,b are_convertible_wrt R )
assume [a,b] in R ; ::_thesis: a,b are_convertible_wrt R
then R reduces a,b by Th15;
hence a,b are_convertible_wrt R by Th25; ::_thesis: verum
end;
theorem Th30: :: REWRITE1:30
for R being Relation
for a, b, c being set st a,b are_convertible_wrt R & b,c are_convertible_wrt R holds
a,c are_convertible_wrt R
proof
let R be Relation; ::_thesis: for a, b, c being set st a,b are_convertible_wrt R & b,c are_convertible_wrt R holds
a,c are_convertible_wrt R
let a, b, c be set ; ::_thesis: ( a,b are_convertible_wrt R & b,c are_convertible_wrt R implies a,c are_convertible_wrt R )
assume ( R \/ (R ~) reduces a,b & R \/ (R ~) reduces b,c ) ; :: according to REWRITE1:def_4 ::_thesis: a,c are_convertible_wrt R
hence R \/ (R ~) reduces a,c by Th16; :: according to REWRITE1:def_4 ::_thesis: verum
end;
theorem :: REWRITE1:31
for R being Relation
for a, b being set st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R by Lm5;
theorem Th32: :: REWRITE1:32
for R being Relation
for a, b being set st a,b are_convertible_wrt R & a <> b holds
( a in field R & b in field R )
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_convertible_wrt R & a <> b holds
( a in field R & b in field R )
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt R & a <> b implies ( a in field R & b in field R ) )
A1: field (R \/ (R ~)) = (field R) \/ (field (R ~)) by RELAT_1:18
.= (field R) \/ (field R) by RELAT_1:21
.= field R ;
assume R \/ (R ~) reduces a,b ; :: according to REWRITE1:def_4 ::_thesis: ( not a <> b or ( a in field R & b in field R ) )
hence ( not a <> b or ( a in field R & b in field R ) ) by A1, Th18; ::_thesis: verum
end;
definition
let R be Relation;
let a be set ;
preda is_a_normal_form_wrt R means :: REWRITE1:def 5
for b being set holds not [a,b] in R;
end;
:: deftheorem defines is_a_normal_form_wrt REWRITE1:def_5_:_
for R being Relation
for a being set holds
( a is_a_normal_form_wrt R iff for b being set holds not [a,b] in R );
theorem Th33: :: REWRITE1:33
for R being Relation
for a, b being set st a is_a_normal_form_wrt R & R reduces a,b holds
a = b
proof
let R be Relation; ::_thesis: for a, b being set st a is_a_normal_form_wrt R & R reduces a,b holds
a = b
let a, b be set ; ::_thesis: ( a is_a_normal_form_wrt R & R reduces a,b implies a = b )
assume A1: for b being set holds not [a,b] in R ; :: according to REWRITE1:def_5 ::_thesis: ( not R reduces a,b or a = b )
assume R reduces a,b ; ::_thesis: a = b
then consider p being FinSequence such that
A2: len p > 0 and
A3: p . 1 = a and
A4: p . (len p) = b and
A5: for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R by Th11;
A6: now__::_thesis:_not_len_p_>_1
assume len p > 1 ; ::_thesis: contradiction
then ( 1 in dom p & 1 + 1 in dom p ) by Lm3, Lm4;
then [a,(p . (1 + 1))] in R by A3, A5;
hence contradiction by A1; ::_thesis: verum
end;
len p >= 0 + 1 by A2, NAT_1:13;
hence a = b by A3, A4, A6, XXREAL_0:1; ::_thesis: verum
end;
theorem Th34: :: REWRITE1:34
for R being Relation
for a being set st not a in field R holds
a is_a_normal_form_wrt R
proof
let R be Relation; ::_thesis: for a being set st not a in field R holds
a is_a_normal_form_wrt R
let a be set ; ::_thesis: ( not a in field R implies a is_a_normal_form_wrt R )
assume A1: not a in field R ; ::_thesis: a is_a_normal_form_wrt R
assume ex b being set st [a,b] in R ; :: according to REWRITE1:def_5 ::_thesis: contradiction
hence contradiction by A1, RELAT_1:15; ::_thesis: verum
end;
definition
let R be Relation;
let a, b be set ;
predb is_a_normal_form_of a,R means :Def6: :: REWRITE1:def 6
( b is_a_normal_form_wrt R & R reduces a,b );
preda,b are_convergent_wrt R means :Def7: :: REWRITE1:def 7
ex c being set st
( R reduces a,c & R reduces b,c );
preda,b are_divergent_wrt R means :Def8: :: REWRITE1:def 8
ex c being set st
( R reduces c,a & R reduces c,b );
preda,b are_convergent<=1_wrt R means :Def9: :: REWRITE1:def 9
ex c being set st
( ( [a,c] in R or a = c ) & ( [b,c] in R or b = c ) );
preda,b are_divergent<=1_wrt R means :Def10: :: REWRITE1:def 10
ex c being set st
( ( [c,a] in R or a = c ) & ( [c,b] in R or b = c ) );
end;
:: deftheorem Def6 defines is_a_normal_form_of REWRITE1:def_6_:_
for R being Relation
for a, b being set holds
( b is_a_normal_form_of a,R iff ( b is_a_normal_form_wrt R & R reduces a,b ) );
:: deftheorem Def7 defines are_convergent_wrt REWRITE1:def_7_:_
for R being Relation
for a, b being set holds
( a,b are_convergent_wrt R iff ex c being set st
( R reduces a,c & R reduces b,c ) );
:: deftheorem Def8 defines are_divergent_wrt REWRITE1:def_8_:_
for R being Relation
for a, b being set holds
( a,b are_divergent_wrt R iff ex c being set st
( R reduces c,a & R reduces c,b ) );
:: deftheorem Def9 defines are_convergent<=1_wrt REWRITE1:def_9_:_
for R being Relation
for a, b being set holds
( a,b are_convergent<=1_wrt R iff ex c being set st
( ( [a,c] in R or a = c ) & ( [b,c] in R or b = c ) ) );
:: deftheorem Def10 defines are_divergent<=1_wrt REWRITE1:def_10_:_
for R being Relation
for a, b being set holds
( a,b are_divergent<=1_wrt R iff ex c being set st
( ( [c,a] in R or a = c ) & ( [c,b] in R or b = c ) ) );
theorem Th35: :: REWRITE1:35
for R being Relation
for a being set st not a in field R holds
a is_a_normal_form_of a,R
proof
let R be Relation; ::_thesis: for a being set st not a in field R holds
a is_a_normal_form_of a,R
let a be set ; ::_thesis: ( not a in field R implies a is_a_normal_form_of a,R )
assume not a in field R ; ::_thesis: a is_a_normal_form_of a,R
hence ( a is_a_normal_form_wrt R & R reduces a,a ) by Th12, Th34; :: according to REWRITE1:def_6 ::_thesis: verum
end;
theorem Th36: :: REWRITE1:36
for R being Relation
for a, b being set st R reduces a,b holds
( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R )
proof
let R be Relation; ::_thesis: for a, b being set st R reduces a,b holds
( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R )
let a, b be set ; ::_thesis: ( R reduces a,b implies ( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R ) )
( R reduces a,a & R reduces b,b ) by Th12;
hence ( R reduces a,b implies ( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R ) ) by Def7, Def8; ::_thesis: verum
end;
theorem Th37: :: REWRITE1:37
for R being Relation
for a, b being set st ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) holds
a,b are_convertible_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) holds
a,b are_convertible_wrt R
let a, b be set ; ::_thesis: ( ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) implies a,b are_convertible_wrt R )
assume A1: ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) ; ::_thesis: a,b are_convertible_wrt R
percases ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) by A1;
suppose a,b are_convergent_wrt R ; ::_thesis: a,b are_convertible_wrt R
then consider c being set such that
A2: ( R reduces a,c & R reduces b,c ) by Def7;
( a,c are_convertible_wrt R & c,b are_convertible_wrt R ) by A2, Th25;
hence a,b are_convertible_wrt R by Th30; ::_thesis: verum
end;
suppose a,b are_divergent_wrt R ; ::_thesis: a,b are_convertible_wrt R
then consider c being set such that
A3: ( R reduces c,a & R reduces c,b ) by Def8;
( c,b are_convertible_wrt R & a,c are_convertible_wrt R ) by A3, Th25;
hence a,b are_convertible_wrt R by Th30; ::_thesis: verum
end;
end;
end;
theorem Th38: :: REWRITE1:38
for R being Relation
for a being set holds
( a,a are_convergent_wrt R & a,a are_divergent_wrt R )
proof
let R be Relation; ::_thesis: for a being set holds
( a,a are_convergent_wrt R & a,a are_divergent_wrt R )
let a be set ; ::_thesis: ( a,a are_convergent_wrt R & a,a are_divergent_wrt R )
thus ( ex b being set st
( R reduces a,b & R reduces a,b ) & ex b being set st
( R reduces b,a & R reduces b,a ) ) by Th12; :: according to REWRITE1:def_7,REWRITE1:def_8 ::_thesis: verum
end;
theorem Th39: :: REWRITE1:39
for a, b being set st ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) holds
a = b
proof
let a, b be set ; ::_thesis: ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )
A1: now__::_thesis:_(_a,b_are_convergent_wrt_{}_&_(_a,b_are_convergent_wrt_{}_or_a,b_are_divergent_wrt_{}_)_implies_a_=_b_)
assume a,b are_convergent_wrt {} ; ::_thesis: ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )
then consider c being set such that
A2: {} reduces a,c and
A3: {} reduces b,c by Def7;
a = c by A2, Th13;
hence ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b ) by A3, Th13; ::_thesis: verum
end;
A4: now__::_thesis:_(_a,b_are_divergent_wrt_{}_&_(_a,b_are_convergent_wrt_{}_or_a,b_are_divergent_wrt_{}_)_implies_a_=_b_)
assume a,b are_divergent_wrt {} ; ::_thesis: ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b )
then consider c being set such that
A5: {} reduces c,a and
A6: {} reduces c,b by Def8;
a = c by A5, Th13;
hence ( ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) implies a = b ) by A6, Th13; ::_thesis: verum
end;
assume ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) ; ::_thesis: a = b
hence a = b by A1, A4; ::_thesis: verum
end;
theorem :: REWRITE1:40
for R being Relation
for a, b being set st a,b are_convergent_wrt R holds
b,a are_convergent_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_convergent_wrt R holds
b,a are_convergent_wrt R
let a, b be set ; ::_thesis: ( a,b are_convergent_wrt R implies b,a are_convergent_wrt R )
assume ex c being set st
( R reduces a,c & R reduces b,c ) ; :: according to REWRITE1:def_7 ::_thesis: b,a are_convergent_wrt R
hence ex c being set st
( R reduces b,c & R reduces a,c ) ; :: according to REWRITE1:def_7 ::_thesis: verum
end;
theorem :: REWRITE1:41
for R being Relation
for a, b being set st a,b are_divergent_wrt R holds
b,a are_divergent_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_divergent_wrt R holds
b,a are_divergent_wrt R
let a, b be set ; ::_thesis: ( a,b are_divergent_wrt R implies b,a are_divergent_wrt R )
assume ex c being set st
( R reduces c,a & R reduces c,b ) ; :: according to REWRITE1:def_8 ::_thesis: b,a are_divergent_wrt R
hence ex c being set st
( R reduces c,b & R reduces c,a ) ; :: according to REWRITE1:def_8 ::_thesis: verum
end;
theorem Th42: :: REWRITE1:42
for R being Relation
for a, b, c being set st ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) holds
a,c are_convergent_wrt R
proof
let R be Relation; ::_thesis: for a, b, c being set st ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) holds
a,c are_convergent_wrt R
let a, b, c be set ; ::_thesis: ( ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) implies a,c are_convergent_wrt R )
assume A1: ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) ; ::_thesis: a,c are_convergent_wrt R
percases ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) by A1;
supposeA2: ( R reduces a,b & b,c are_convergent_wrt R ) ; ::_thesis: a,c are_convergent_wrt R
then consider d being set such that
A3: R reduces b,d and
A4: R reduces c,d by Def7;
R reduces a,d by A2, A3, Th16;
hence a,c are_convergent_wrt R by A4, Def7; ::_thesis: verum
end;
supposeA5: ( a,b are_convergent_wrt R & R reduces c,b ) ; ::_thesis: a,c are_convergent_wrt R
then consider d being set such that
A6: R reduces a,d and
A7: R reduces b,d by Def7;
R reduces c,d by A5, A7, Th16;
hence a,c are_convergent_wrt R by A6, Def7; ::_thesis: verum
end;
end;
end;
theorem :: REWRITE1:43
for R being Relation
for a, b, c being set st ( ( R reduces b,a & b,c are_divergent_wrt R ) or ( a,b are_divergent_wrt R & R reduces b,c ) ) holds
a,c are_divergent_wrt R
proof
let R be Relation; ::_thesis: for a, b, c being set st ( ( R reduces b,a & b,c are_divergent_wrt R ) or ( a,b are_divergent_wrt R & R reduces b,c ) ) holds
a,c are_divergent_wrt R
let a, b, c be set ; ::_thesis: ( ( ( R reduces b,a & b,c are_divergent_wrt R ) or ( a,b are_divergent_wrt R & R reduces b,c ) ) implies a,c are_divergent_wrt R )
assume A1: ( ( R reduces b,a & b,c are_divergent_wrt R ) or ( a,b are_divergent_wrt R & R reduces b,c ) ) ; ::_thesis: a,c are_divergent_wrt R
percases ( ( R reduces b,a & b,c are_divergent_wrt R ) or ( a,b are_divergent_wrt R & R reduces b,c ) ) by A1;
supposeA2: ( R reduces b,a & b,c are_divergent_wrt R ) ; ::_thesis: a,c are_divergent_wrt R
then consider d being set such that
A3: R reduces d,b and
A4: R reduces d,c by Def8;
R reduces d,a by A2, A3, Th16;
hence a,c are_divergent_wrt R by A4, Def8; ::_thesis: verum
end;
supposeA5: ( a,b are_divergent_wrt R & R reduces b,c ) ; ::_thesis: a,c are_divergent_wrt R
then consider d being set such that
A6: R reduces d,a and
A7: R reduces d,b by Def8;
R reduces d,c by A5, A7, Th16;
hence a,c are_divergent_wrt R by A6, Def8; ::_thesis: verum
end;
end;
end;
theorem Th44: :: REWRITE1:44
for R being Relation
for a, b being set st a,b are_convergent<=1_wrt R holds
a,b are_convergent_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_convergent<=1_wrt R holds
a,b are_convergent_wrt R
let a, b be set ; ::_thesis: ( a,b are_convergent<=1_wrt R implies a,b are_convergent_wrt R )
given c being set such that A1: ( ( [a,c] in R or a = c ) & ( [b,c] in R or b = c ) ) ; :: according to REWRITE1:def_9 ::_thesis: a,b are_convergent_wrt R
take c ; :: according to REWRITE1:def_7 ::_thesis: ( R reduces a,c & R reduces b,c )
thus ( R reduces a,c & R reduces b,c ) by A1, Th12, Th15; ::_thesis: verum
end;
theorem Th45: :: REWRITE1:45
for R being Relation
for a, b being set st a,b are_divergent<=1_wrt R holds
a,b are_divergent_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_divergent<=1_wrt R holds
a,b are_divergent_wrt R
let a, b be set ; ::_thesis: ( a,b are_divergent<=1_wrt R implies a,b are_divergent_wrt R )
given c being set such that A1: ( ( [c,a] in R or a = c ) & ( [c,b] in R or b = c ) ) ; :: according to REWRITE1:def_10 ::_thesis: a,b are_divergent_wrt R
take c ; :: according to REWRITE1:def_8 ::_thesis: ( R reduces c,a & R reduces c,b )
thus ( R reduces c,a & R reduces c,b ) by A1, Th12, Th15; ::_thesis: verum
end;
definition
let R be Relation;
let a be set ;
preda has_a_normal_form_wrt R means :Def11: :: REWRITE1:def 11
ex b being set st b is_a_normal_form_of a,R;
end;
:: deftheorem Def11 defines has_a_normal_form_wrt REWRITE1:def_11_:_
for R being Relation
for a being set holds
( a has_a_normal_form_wrt R iff ex b being set st b is_a_normal_form_of a,R );
theorem Th46: :: REWRITE1:46
for R being Relation
for a being set st not a in field R holds
a has_a_normal_form_wrt R
proof
let R be Relation; ::_thesis: for a being set st not a in field R holds
a has_a_normal_form_wrt R
let a be set ; ::_thesis: ( not a in field R implies a has_a_normal_form_wrt R )
assume not a in field R ; ::_thesis: a has_a_normal_form_wrt R
hence ex b being set st b is_a_normal_form_of a,R by Th35; :: according to REWRITE1:def_11 ::_thesis: verum
end;
definition
let R be Relation;
let a be set ;
assume that
A1: a has_a_normal_form_wrt R and
A2: for b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c ;
func nf (a,R) -> set means :Def12: :: REWRITE1:def 12
it is_a_normal_form_of a,R;
existence
ex b1 being set st b1 is_a_normal_form_of a,R by A1, Def11;
uniqueness
for b1, b2 being set st b1 is_a_normal_form_of a,R & b2 is_a_normal_form_of a,R holds
b1 = b2 by A2;
end;
:: deftheorem Def12 defines nf REWRITE1:def_12_:_
for R being Relation
for a being set st a has_a_normal_form_wrt R & ( for b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c ) holds
for b3 being set holds
( b3 = nf (a,R) iff b3 is_a_normal_form_of a,R );
begin
definition
let R be Relation;
attrR is co-well_founded means :Def13: :: REWRITE1:def 13
R ~ is well_founded ;
attrR is weakly-normalizing means :Def14: :: REWRITE1:def 14
for a being set st a in field R holds
a has_a_normal_form_wrt R;
attrR is strongly-normalizing means :: REWRITE1:def 15
for f being ManySortedSet of NAT holds
not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R;
end;
:: deftheorem Def13 defines co-well_founded REWRITE1:def_13_:_
for R being Relation holds
( R is co-well_founded iff R ~ is well_founded );
:: deftheorem Def14 defines weakly-normalizing REWRITE1:def_14_:_
for R being Relation holds
( R is weakly-normalizing iff for a being set st a in field R holds
a has_a_normal_form_wrt R );
:: deftheorem defines strongly-normalizing REWRITE1:def_15_:_
for R being Relation holds
( R is strongly-normalizing iff for f being ManySortedSet of NAT holds
not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R );
definition
let R be Relation;
redefine attr R is co-well_founded means :Def16: :: REWRITE1:def 16
for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) );
compatibility
( R is co-well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
proof
A1: field R = field (R ~) by RELAT_1:21;
hereby ::_thesis: ( ( for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) ) implies R is co-well_founded )
assume R is co-well_founded ; ::_thesis: for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
then A2: R ~ is well_founded by Def13;
let Y be set ; ::_thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
assume ( Y c= field R & Y <> {} ) ; ::_thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
then consider a being set such that
A3: a in Y and
A4: (R ~) -Seg a misses Y by A1, A2, WELLORD1:def_2;
take a = a; ::_thesis: ( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
thus a in Y by A3; ::_thesis: for b being set st b in Y & a <> b holds
not [a,b] in R
let b be set ; ::_thesis: ( b in Y & a <> b implies not [a,b] in R )
assume b in Y ; ::_thesis: ( a <> b implies not [a,b] in R )
then not b in (R ~) -Seg a by A4, XBOOLE_0:3;
then ( a = b or not [b,a] in R ~ ) by WELLORD1:1;
hence ( a <> b implies not [a,b] in R ) by RELAT_1:def_7; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A5: for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) ; ::_thesis: R is co-well_founded
R ~ is well_founded
proof
let Y be set ; :: according to WELLORD1:def_2 ::_thesis: ( not Y c= field (R ~) or Y = {} or ex b1 being set st
( b1 in Y & (R ~) -Seg b1 misses Y ) )
assume ( Y c= field (R ~) & Y <> {} ) ; ::_thesis: ex b1 being set st
( b1 in Y & (R ~) -Seg b1 misses Y )
then consider a being set such that
A6: a in Y and
A7: for b being set st b in Y & a <> b holds
not [a,b] in R by A1, A5;
take a ; ::_thesis: ( a in Y & (R ~) -Seg a misses Y )
thus a in Y by A6; ::_thesis: (R ~) -Seg a misses Y
now__::_thesis:_((R_~)_-Seg_a)_/\_Y_is_empty
assume not ((R ~) -Seg a) /\ Y is empty ; ::_thesis: contradiction
then reconsider A = ((R ~) -Seg a) /\ Y as non empty set ;
set x = the Element of A;
A8: the Element of A in (R ~) -Seg a by XBOOLE_0:def_4;
then ( the Element of A in Y & the Element of A <> a ) by WELLORD1:1, XBOOLE_0:def_4;
then A9: not [a, the Element of A] in R by A7;
[ the Element of A,a] in R ~ by A8, WELLORD1:1;
hence contradiction by A9, RELAT_1:def_7; ::_thesis: verum
end;
hence (R ~) -Seg a misses Y by XBOOLE_0:def_7; ::_thesis: verum
end;
hence R is co-well_founded by Def13; ::_thesis: verum
end;
end;
end;
:: deftheorem Def16 defines co-well_founded REWRITE1:def_16_:_
for R being Relation holds
( R is co-well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) );
scheme :: REWRITE1:sch 2
coNoetherianInduction{ F1() -> Relation, P1[ set ] } :
for a being set st a in field F1() holds
P1[a]
provided
A1: F1() is co-well_founded and
A2: for a being set st ( for b being set st [a,b] in F1() & a <> b holds
P1[b] ) holds
P1[a]
proof
given a being set such that A3: a in field F1() and
A4: P1[a] ; ::_thesis: contradiction
reconsider X = field F1() as non empty set by A3;
reconsider a = a as Element of X by A3;
set Y = { x where x is Element of X : P1[x] } ;
A5: a in { x where x is Element of X : P1[x] } by A4;
{ x where x is Element of X : P1[x] } c= field F1()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of X : P1[x] } or y in field F1() )
assume y in { x where x is Element of X : P1[x] } ; ::_thesis: y in field F1()
then ex x being Element of X st
( y = x & P1[x] ) ;
hence y in field F1() ; ::_thesis: verum
end;
then consider a being set such that
A6: a in { x where x is Element of X : P1[x] } and
A7: for b being set st b in { x where x is Element of X : P1[x] } & a <> b holds
not [a,b] in F1() by A1, A5, Def16;
A8: now__::_thesis:_for_b_being_set_st_[a,b]_in_F1()_&_a_<>_b_holds_
P1[b]
let b be set ; ::_thesis: ( [a,b] in F1() & a <> b implies P1[b] )
assume that
A9: ( [a,b] in F1() & a <> b ) and
A10: P1[b] ; ::_thesis: contradiction
( not b in { x where x is Element of X : P1[x] } & b in X ) by A7, A9, RELAT_1:15;
hence contradiction by A10; ::_thesis: verum
end;
ex x being Element of X st
( a = x & P1[x] ) by A6;
hence contradiction by A2, A8; ::_thesis: verum
end;
registration
cluster Relation-like strongly-normalizing -> irreflexive co-well_founded for set ;
coherence
for b1 being Relation st b1 is strongly-normalizing holds
( b1 is irreflexive & b1 is co-well_founded )
proof
defpred S1[ set ] means verum;
let R be Relation; ::_thesis: ( R is strongly-normalizing implies ( R is irreflexive & R is co-well_founded ) )
assume A1: for f being ManySortedSet of NAT holds
not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R ; :: according to REWRITE1:def_15 ::_thesis: ( R is irreflexive & R is co-well_founded )
thus R is irreflexive ::_thesis: R is co-well_founded
proof
given x being set such that x in field R and
A2: [x,x] in R ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: contradiction
dom (NAT --> x) = NAT by FUNCOP_1:13;
then reconsider f = NAT --> x as ManySortedSet of NAT by PARTFUN1:def_2, RELAT_1:def_18;
consider i being Element of NAT such that
A3: not [(f . i),(f . (i + 1))] in R by A1;
f . i = x by FUNCOP_1:7;
hence contradiction by A2, A3, FUNCOP_1:7; ::_thesis: verum
end;
defpred S2[ set , set ] means [c1,c2] in R;
let Y be set ; :: according to REWRITE1:def_16 ::_thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
assume that
Y c= field R and
A4: Y <> {} and
A5: for a being set st a in Y holds
ex b being set st
( b in Y & a <> b & [a,b] in R ) ; ::_thesis: contradiction
reconsider Y = Y as non empty set by A4;
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
ex_y_being_set_st_
(_y_in_Y_&_[x,y]_in_R_)
let x be set ; ::_thesis: ( x in Y implies ex y being set st
( y in Y & [x,y] in R ) )
assume x in Y ; ::_thesis: ex y being set st
( y in Y & [x,y] in R )
then ex b being set st
( b in Y & x <> b & [x,b] in R ) by A5;
hence ex y being set st
( y in Y & [x,y] in R ) ; ::_thesis: verum
end;
then A6: for x being set st x in Y & S1[x] holds
ex y being set st
( y in Y & S2[x,y] & S1[y] ) ;
set y = the Element of Y;
A7: ( the Element of Y in Y & S1[ the Element of Y] ) ;
consider f being Function such that
A8: ( dom f = NAT & rng f c= Y & f . 0 = the Element of Y ) and
A9: for k being Element of NAT holds
( S2[f . k,f . (k + 1)] & S1[f . k] ) from TREES_2:sch_5(A7, A6);
f is ManySortedSet of NAT by A8, PARTFUN1:def_2, RELAT_1:def_18;
hence contradiction by A1, A9; ::_thesis: verum
end;
cluster Relation-like irreflexive co-well_founded -> strongly-normalizing for set ;
coherence
for b1 being Relation st b1 is co-well_founded & b1 is irreflexive holds
b1 is strongly-normalizing
proof
let R be Relation; ::_thesis: ( R is co-well_founded & R is irreflexive implies R is strongly-normalizing )
assume A10: for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) ; :: according to REWRITE1:def_16 ::_thesis: ( not R is irreflexive or R is strongly-normalizing )
assume A11: for x being set st x in field R holds
not [x,x] in R ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: R is strongly-normalizing
let f be ManySortedSet of NAT ; :: according to REWRITE1:def_15 ::_thesis: not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R
assume A12: for i being Element of NAT holds [(f . i),(f . (i + 1))] in R ; ::_thesis: contradiction
A13: rng f c= field R
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in field R )
assume y in rng f ; ::_thesis: y in field R
then consider x being set such that
A14: x in dom f and
A15: y = f . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A14, PARTFUN1:def_2;
[y,(f . (x + 1))] in R by A12, A15;
hence y in field R by RELAT_1:15; ::_thesis: verum
end;
A16: dom f = NAT by PARTFUN1:def_2;
then f . 0 in rng f by FUNCT_1:def_3;
then consider a being set such that
A17: a in rng f and
A18: for b being set st b in rng f & a <> b holds
not [a,b] in R by A10, A13;
consider x being set such that
A19: x in dom f and
A20: a = f . x by A17, FUNCT_1:def_3;
reconsider x = x as Element of NAT by A19, PARTFUN1:def_2;
A21: f . (x + 1) in rng f by A16, FUNCT_1:def_3;
A22: [a,(f . (x + 1))] in R by A12, A20;
then a <> f . (x + 1) by A11, A13, A17;
hence contradiction by A18, A22, A21; ::_thesis: verum
end;
end;
registration
cluster empty Relation-like -> weakly-normalizing strongly-normalizing for set ;
coherence
for b1 being Relation st b1 is empty holds
( b1 is weakly-normalizing & b1 is strongly-normalizing )
proof
let R be Relation; ::_thesis: ( R is empty implies ( R is weakly-normalizing & R is strongly-normalizing ) )
assume A1: R is empty ; ::_thesis: ( R is weakly-normalizing & R is strongly-normalizing )
thus R is weakly-normalizing ::_thesis: R is strongly-normalizing
proof
let x be set ; :: according to REWRITE1:def_14 ::_thesis: ( x in field R implies x has_a_normal_form_wrt R )
thus ( x in field R implies x has_a_normal_form_wrt R ) by A1, RELAT_1:40; ::_thesis: verum
end;
thus R is strongly-normalizing ::_thesis: verum
proof
let f be ManySortedSet of NAT ; :: according to REWRITE1:def_15 ::_thesis: not for i being Element of NAT holds [(f . i),(f . (i + 1))] in R
take 0 ; ::_thesis: not [(f . 0),(f . (0 + 1))] in R
thus not [(f . 0),(f . (0 + 1))] in R by A1; ::_thesis: verum
end;
end;
end;
theorem :: REWRITE1:47
for Q being co-well_founded Relation
for R being Relation st R c= Q holds
R is co-well_founded
proof
let Q be co-well_founded Relation; ::_thesis: for R being Relation st R c= Q holds
R is co-well_founded
let R be Relation; ::_thesis: ( R c= Q implies R is co-well_founded )
assume A1: R c= Q ; ::_thesis: R is co-well_founded
let Y be set ; :: according to REWRITE1:def_16 ::_thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
assume that
A2: Y c= field R and
A3: Y <> {} ; ::_thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
field R c= field Q by A1, RELAT_1:16;
then Y c= field Q by A2, XBOOLE_1:1;
then consider a being set such that
A4: a in Y and
A5: for b being set st b in Y & a <> b holds
not [a,b] in Q by A3, Def16;
take a ; ::_thesis: ( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
thus a in Y by A4; ::_thesis: for b being set st b in Y & a <> b holds
not [a,b] in R
let b be set ; ::_thesis: ( b in Y & a <> b implies not [a,b] in R )
assume ( b in Y & a <> b ) ; ::_thesis: not [a,b] in R
hence not [a,b] in R by A1, A5; ::_thesis: verum
end;
registration
cluster Relation-like strongly-normalizing -> weakly-normalizing for set ;
coherence
for b1 being Relation st b1 is strongly-normalizing holds
b1 is weakly-normalizing
proof
let R be Relation; ::_thesis: ( R is strongly-normalizing implies R is weakly-normalizing )
assume A1: R is strongly-normalizing ; ::_thesis: R is weakly-normalizing
let a be set ; :: according to REWRITE1:def_14 ::_thesis: ( a in field R implies a has_a_normal_form_wrt R )
assume A2: a in field R ; ::_thesis: a has_a_normal_form_wrt R
then reconsider X = field R as non empty set ;
set Y = { x where x is Element of X : R reduces a,x } ;
A3: { x where x is Element of X : R reduces a,x } c= field R
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of X : R reduces a,x } or y in field R )
assume y in { x where x is Element of X : R reduces a,x } ; ::_thesis: y in field R
then ex x being Element of X st
( y = x & R reduces a,x ) ;
hence y in field R ; ::_thesis: verum
end;
R reduces a,a by Th12;
then a in { x where x is Element of X : R reduces a,x } by A2;
then consider x being set such that
A4: x in { x where x is Element of X : R reduces a,x } and
A5: for b being set st b in { x where x is Element of X : R reduces a,x } & x <> b holds
not [x,b] in R by A1, A3, Def16;
take x ; :: according to REWRITE1:def_11 ::_thesis: x is_a_normal_form_of a,R
A6: ex y being Element of X st
( x = y & R reduces a,y ) by A4;
hereby :: according to REWRITE1:def_5,REWRITE1:def_6 ::_thesis: R reduces a,x
R is_irreflexive_in field R by A1, RELAT_2:def_10;
then A7: not [x,x] in R by A3, A4, RELAT_2:def_2;
given b being set such that A8: [x,b] in R ; ::_thesis: contradiction
R reduces x,b by A8, Th15;
then A9: R reduces a,b by A6, Th16;
b in X by A8, RELAT_1:15;
then b in { x where x is Element of X : R reduces a,x } by A9;
hence contradiction by A5, A8, A7; ::_thesis: verum
end;
thus R reduces a,x by A6; ::_thesis: verum
end;
end;
begin
definition
let R, Q be Relation;
predR commutes-weakly_with Q means :: REWRITE1:def 17
for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d );
symmetry
for R, Q being Relation st ( for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ) holds
for a, b, c being set st [a,b] in Q & [a,c] in R holds
ex d being set st
( R reduces b,d & Q reduces c,d )
proof
let R, Q be Relation; ::_thesis: ( ( for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ) implies for a, b, c being set st [a,b] in Q & [a,c] in R holds
ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume A1: for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ; ::_thesis: for a, b, c being set st [a,b] in Q & [a,c] in R holds
ex d being set st
( R reduces b,d & Q reduces c,d )
let a, b, c be set ; ::_thesis: ( [a,b] in Q & [a,c] in R implies ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume ( [a,b] in Q & [a,c] in R ) ; ::_thesis: ex d being set st
( R reduces b,d & Q reduces c,d )
then ex d being set st
( Q reduces c,d & R reduces b,d ) by A1;
hence ex d being set st
( R reduces b,d & Q reduces c,d ) ; ::_thesis: verum
end;
predR commutes_with Q means :Def18: :: REWRITE1:def 18
for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d );
symmetry
for R, Q being Relation st ( for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ) holds
for a, b, c being set st Q reduces a,b & R reduces a,c holds
ex d being set st
( R reduces b,d & Q reduces c,d )
proof
let R, Q be Relation; ::_thesis: ( ( for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ) implies for a, b, c being set st Q reduces a,b & R reduces a,c holds
ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume A2: for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ; ::_thesis: for a, b, c being set st Q reduces a,b & R reduces a,c holds
ex d being set st
( R reduces b,d & Q reduces c,d )
let a, b, c be set ; ::_thesis: ( Q reduces a,b & R reduces a,c implies ex d being set st
( R reduces b,d & Q reduces c,d ) )
assume ( Q reduces a,b & R reduces a,c ) ; ::_thesis: ex d being set st
( R reduces b,d & Q reduces c,d )
then ex d being set st
( Q reduces c,d & R reduces b,d ) by A2;
hence ex d being set st
( R reduces b,d & Q reduces c,d ) ; ::_thesis: verum
end;
end;
:: deftheorem defines commutes-weakly_with REWRITE1:def_17_:_
for R, Q being Relation holds
( R commutes-weakly_with Q iff for a, b, c being set st [a,b] in R & [a,c] in Q holds
ex d being set st
( Q reduces b,d & R reduces c,d ) );
:: deftheorem Def18 defines commutes_with REWRITE1:def_18_:_
for R, Q being Relation holds
( R commutes_with Q iff for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) );
theorem :: REWRITE1:48
for R, Q being Relation st R commutes_with Q holds
R commutes-weakly_with Q
proof
let R, Q be Relation; ::_thesis: ( R commutes_with Q implies R commutes-weakly_with Q )
assume A1: for a, b, c being set st R reduces a,b & Q reduces a,c holds
ex d being set st
( Q reduces b,d & R reduces c,d ) ; :: according to REWRITE1:def_18 ::_thesis: R commutes-weakly_with Q
let a, b, c be set ; :: according to REWRITE1:def_17 ::_thesis: ( [a,b] in R & [a,c] in Q implies ex d being set st
( Q reduces b,d & R reduces c,d ) )
assume ( [a,b] in R & [a,c] in Q ) ; ::_thesis: ex d being set st
( Q reduces b,d & R reduces c,d )
then ( R reduces a,b & Q reduces a,c ) by Th15;
hence ex d being set st
( Q reduces b,d & R reduces c,d ) by A1; ::_thesis: verum
end;
definition
let R be Relation;
attrR is with_UN_property means :Def19: :: REWRITE1:def 19
for a, b being set st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
a = b;
attrR is with_NF_property means :: REWRITE1:def 20
for a, b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
R reduces b,a;
attrR is subcommutative means :Def21: :: REWRITE1:def 21
for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent<=1_wrt R;
attrR is confluent means :Def22: :: REWRITE1:def 22
for a, b being set st a,b are_divergent_wrt R holds
a,b are_convergent_wrt R;
attrR is with_Church-Rosser_property means :Def23: :: REWRITE1:def 23
for a, b being set st a,b are_convertible_wrt R holds
a,b are_convergent_wrt R;
attrR is locally-confluent means :Def24: :: REWRITE1:def 24
for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent_wrt R;
end;
:: deftheorem Def19 defines with_UN_property REWRITE1:def_19_:_
for R being Relation holds
( R is with_UN_property iff for a, b being set st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
a = b );
:: deftheorem defines with_NF_property REWRITE1:def_20_:_
for R being Relation holds
( R is with_NF_property iff for a, b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
R reduces b,a );
:: deftheorem Def21 defines subcommutative REWRITE1:def_21_:_
for R being Relation holds
( R is subcommutative iff for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent<=1_wrt R );
:: deftheorem Def22 defines confluent REWRITE1:def_22_:_
for R being Relation holds
( R is confluent iff for a, b being set st a,b are_divergent_wrt R holds
a,b are_convergent_wrt R );
:: deftheorem Def23 defines with_Church-Rosser_property REWRITE1:def_23_:_
for R being Relation holds
( R is with_Church-Rosser_property iff for a, b being set st a,b are_convertible_wrt R holds
a,b are_convergent_wrt R );
:: deftheorem Def24 defines locally-confluent REWRITE1:def_24_:_
for R being Relation holds
( R is locally-confluent iff for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent_wrt R );
theorem Th49: :: REWRITE1:49
for R being Relation st R is subcommutative holds
for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R
proof
let R be Relation; ::_thesis: ( R is subcommutative implies for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )
assume A1: R is subcommutative ; ::_thesis: for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R
let a, b, c be set ; ::_thesis: ( R reduces a,b & [a,c] in R implies b,c are_convergent_wrt R )
given p being RedSequence of R such that A2: p . 1 = a and
A3: p . (len p) = b ; :: according to REWRITE1:def_3 ::_thesis: ( not [a,c] in R or b,c are_convergent_wrt R )
defpred S1[ Element of NAT ] means ( $1 in dom p implies ex d being set st
( ( [(p . $1),d] in R or p . $1 = d ) & R reduces c,d ) );
assume A4: [a,c] in R ; ::_thesis: b,c are_convergent_wrt R
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_S1[i]_)_&_i_+_1_in_dom_p_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies S1[i] ) & i + 1 in dom p implies S1[b1 + 1] )
assume that
A5: ( i in dom p implies S1[i] ) and
A6: i + 1 in dom p ; ::_thesis: S1[b1 + 1]
percases ( i = 0 or i > 0 ) ;
supposeA7: i = 0 ; ::_thesis: S1[b1 + 1]
R reduces c,c by Th12;
hence S1[i + 1] by A2, A4, A7; ::_thesis: verum
end;
supposeA8: i > 0 ; ::_thesis: S1[b1 + 1]
A9: i < len p by A6, Lm2;
then consider d being set such that
A10: ( [(p . i),d] in R or p . i = d ) and
A11: R reduces c,d by A5, A8, Lm3;
i in dom p by A8, A9, Lm3;
then A12: [(p . i),(p . (i + 1))] in R by A6, Def2;
A13: now__::_thesis:_(_[(p_._i),d]_in_R_implies_ex_e_being_set_st_
(_(_[(p_._(i_+_1)),e]_in_R_or_p_._(i_+_1)_=_e_)_&_R_reduces_c,e_)_)
assume [(p . i),d] in R ; ::_thesis: ex e being set st
( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )
then p . (i + 1),d are_convergent<=1_wrt R by A1, A12, Def21;
then consider e being set such that
A14: ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) and
A15: ( [d,e] in R or d = e ) by Def9;
take e = e; ::_thesis: ( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )
thus ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) by A14; ::_thesis: R reduces c,e
R reduces d,e by A15, Th12, Th15;
hence R reduces c,e by A11, Th16; ::_thesis: verum
end;
now__::_thesis:_(_p_._i_=_d_implies_R_reduces_c,p_._(i_+_1)_)
assume p . i = d ; ::_thesis: R reduces c,p . (i + 1)
then R reduces d,p . (i + 1) by A12, Th15;
hence R reduces c,p . (i + 1) by A11, Th16; ::_thesis: verum
end;
hence S1[i + 1] by A10, A13; ::_thesis: verum
end;
end;
end;
then A16: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A17: len p in dom p by FINSEQ_5:6;
A18: S1[ 0 ] by Lm1;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A18, A16);
then consider d being set such that
A19: ( ( [b,d] in R or b = d ) & R reduces c,d ) by A3, A17;
take d ; :: according to REWRITE1:def_7 ::_thesis: ( R reduces b,d & R reduces c,d )
thus ( R reduces b,d & R reduces c,d ) by A19, Th12, Th15; ::_thesis: verum
end;
theorem :: REWRITE1:50
for R being Relation holds
( R is confluent iff R commutes_with R )
proof
let R be Relation; ::_thesis: ( R is confluent iff R commutes_with R )
hereby ::_thesis: ( R commutes_with R implies R is confluent )
assume A1: R is confluent ; ::_thesis: R commutes_with R
thus R commutes_with R ::_thesis: verum
proof
let a, b, c be set ; :: according to REWRITE1:def_18 ::_thesis: ( R reduces a,b & R reduces a,c implies ex d being set st
( R reduces b,d & R reduces c,d ) )
assume ( R reduces a,b & R reduces a,c ) ; ::_thesis: ex d being set st
( R reduces b,d & R reduces c,d )
then b,c are_divergent_wrt R by Def8;
then b,c are_convergent_wrt R by A1, Def22;
hence ex d being set st
( R reduces b,d & R reduces c,d ) by Def7; ::_thesis: verum
end;
end;
assume A2: for a, b, c being set st R reduces a,b & R reduces a,c holds
ex d being set st
( R reduces b,d & R reduces c,d ) ; :: according to REWRITE1:def_18 ::_thesis: R is confluent
let a, b be set ; :: according to REWRITE1:def_22 ::_thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
assume ex c being set st
( R reduces c,a & R reduces c,b ) ; :: according to REWRITE1:def_8 ::_thesis: a,b are_convergent_wrt R
hence ex d being set st
( R reduces a,d & R reduces b,d ) by A2; :: according to REWRITE1:def_7 ::_thesis: verum
end;
theorem Th51: :: REWRITE1:51
for R being Relation holds
( R is confluent iff for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )
proof
let R be Relation; ::_thesis: ( R is confluent iff for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )
hereby ::_thesis: ( ( for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R ) implies R is confluent )
assume A1: R is confluent ; ::_thesis: for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R
let a, b, c be set ; ::_thesis: ( R reduces a,b & [a,c] in R implies b,c are_convergent_wrt R )
assume that
A2: R reduces a,b and
A3: [a,c] in R ; ::_thesis: b,c are_convergent_wrt R
R reduces a,c by A3, Th15;
then b,c are_divergent_wrt R by A2, Def8;
hence b,c are_convergent_wrt R by A1, Def22; ::_thesis: verum
end;
assume A4: for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R ; ::_thesis: R is confluent
let b, c be set ; :: according to REWRITE1:def_22 ::_thesis: ( b,c are_divergent_wrt R implies b,c are_convergent_wrt R )
given a being set such that A5: R reduces a,b and
A6: R reduces a,c ; :: according to REWRITE1:def_8 ::_thesis: b,c are_convergent_wrt R
consider p being RedSequence of R such that
A7: p . 1 = a and
A8: p . (len p) = b by A5, Def3;
consider q being RedSequence of R such that
A9: q . 1 = a and
A10: q . (len q) = c by A6, Def3;
defpred S1[ Element of NAT , Element of NAT ] means p . $1,q . $2 are_convergent_wrt R;
defpred S2[ Element of NAT ] means ( $1 in dom p implies for j being Element of NAT st j in dom q holds
S1[$1,j] );
A11: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume that
( i in dom p implies for j being Element of NAT st j in dom q holds
S1[i,j] ) and
A12: i + 1 in dom p ; ::_thesis: for j being Element of NAT st j in dom q holds
S1[i + 1,j]
defpred S3[ Element of NAT ] means ( $1 in dom q implies S1[i + 1,$1] );
A13: for j being Element of NAT st S3[j] holds
S3[j + 1]
proof
1 in dom p by FINSEQ_5:6;
then A14: R reduces a,p . (i + 1) by A7, A12, Th17, NAT_1:11;
let j be Element of NAT ; ::_thesis: ( S3[j] implies S3[j + 1] )
assume that
A15: ( j in dom q implies S1[i + 1,j] ) and
A16: j + 1 in dom q ; ::_thesis: S1[i + 1,j + 1]
percases ( j = 0 or j > 0 ) ;
suppose j = 0 ; ::_thesis: S1[i + 1,j + 1]
hence S1[i + 1,j + 1] by A9, A14, Th36; ::_thesis: verum
end;
supposeA17: j > 0 ; ::_thesis: S1[i + 1,j + 1]
A18: j < len q by A16, Lm2;
then consider d being set such that
A19: R reduces p . (i + 1),d and
A20: R reduces q . j,d by A15, A17, Def7, Lm3;
j in dom q by A17, A18, Lm3;
then [(q . j),(q . (j + 1))] in R by A16, Def2;
then d,q . (j + 1) are_convergent_wrt R by A4, A20;
hence S1[i + 1,j + 1] by A19, Th42; ::_thesis: verum
end;
end;
end;
A21: S3[ 0 ] by Lm1;
thus for j being Element of NAT holds S3[j] from NAT_1:sch_1(A21, A13); ::_thesis: verum
end;
A22: ( len p in dom p & len q in dom q ) by FINSEQ_5:6;
A23: S2[ 0 ] by Lm1;
for i being Element of NAT holds S2[i] from NAT_1:sch_1(A23, A11);
hence b,c are_convergent_wrt R by A8, A10, A22; ::_thesis: verum
end;
theorem :: REWRITE1:52
for R being Relation holds
( R is locally-confluent iff R commutes-weakly_with R )
proof
let R be Relation; ::_thesis: ( R is locally-confluent iff R commutes-weakly_with R )
hereby ::_thesis: ( R commutes-weakly_with R implies R is locally-confluent )
assume A1: R is locally-confluent ; ::_thesis: R commutes-weakly_with R
thus R commutes-weakly_with R ::_thesis: verum
proof
let a, b, c be set ; :: according to REWRITE1:def_17 ::_thesis: ( [a,b] in R & [a,c] in R implies ex d being set st
( R reduces b,d & R reduces c,d ) )
assume ( [a,b] in R & [a,c] in R ) ; ::_thesis: ex d being set st
( R reduces b,d & R reduces c,d )
then b,c are_convergent_wrt R by A1, Def24;
hence ex d being set st
( R reduces b,d & R reduces c,d ) by Def7; ::_thesis: verum
end;
end;
assume A2: for a, b, c being set st [a,b] in R & [a,c] in R holds
ex d being set st
( R reduces b,d & R reduces c,d ) ; :: according to REWRITE1:def_17 ::_thesis: R is locally-confluent
let a, b, c be set ; :: according to REWRITE1:def_24 ::_thesis: ( [a,b] in R & [a,c] in R implies b,c are_convergent_wrt R )
assume ( [a,b] in R & [a,c] in R ) ; ::_thesis: b,c are_convergent_wrt R
hence ex d being set st
( R reduces b,d & R reduces c,d ) by A2; :: according to REWRITE1:def_7 ::_thesis: verum
end;
registration
cluster Relation-like with_Church-Rosser_property -> confluent for set ;
coherence
for b1 being Relation st b1 is with_Church-Rosser_property holds
b1 is confluent
proof
let R be Relation; ::_thesis: ( R is with_Church-Rosser_property implies R is confluent )
assume A1: for a, b being set st a,b are_convertible_wrt R holds
a,b are_convergent_wrt R ; :: according to REWRITE1:def_23 ::_thesis: R is confluent
let a, b be set ; :: according to REWRITE1:def_22 ::_thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
assume a,b are_divergent_wrt R ; ::_thesis: a,b are_convergent_wrt R
then a,b are_convertible_wrt R by Th37;
hence a,b are_convergent_wrt R by A1; ::_thesis: verum
end;
cluster Relation-like confluent -> with_Church-Rosser_property locally-confluent for set ;
coherence
for b1 being Relation st b1 is confluent holds
( b1 is locally-confluent & b1 is with_Church-Rosser_property )
proof
let R be Relation; ::_thesis: ( R is confluent implies ( R is locally-confluent & R is with_Church-Rosser_property ) )
assume A2: for a, b being set st a,b are_divergent_wrt R holds
a,b are_convergent_wrt R ; :: according to REWRITE1:def_22 ::_thesis: ( R is locally-confluent & R is with_Church-Rosser_property )
hereby :: according to REWRITE1:def_24 ::_thesis: R is with_Church-Rosser_property
let a, b, c be set ; ::_thesis: ( [a,b] in R & [a,c] in R implies b,c are_convergent_wrt R )
assume ( [a,b] in R & [a,c] in R ) ; ::_thesis: b,c are_convergent_wrt R
then ( R reduces a,b & R reduces a,c ) by Th15;
then b,c are_divergent_wrt R by Def8;
hence b,c are_convergent_wrt R by A2; ::_thesis: verum
end;
let a, b be set ; :: according to REWRITE1:def_23 ::_thesis: ( a,b are_convertible_wrt R implies a,b are_convergent_wrt R )
given p being RedSequence of R \/ (R ~) such that A3: p . 1 = a and
A4: p . (len p) = b ; :: according to REWRITE1:def_3,REWRITE1:def_4 ::_thesis: a,b are_convergent_wrt R
defpred S1[ Element of NAT ] means ( c1 in dom p implies a,p . c1 are_convergent_wrt R );
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_a,p_._i_are_convergent_wrt_R_)_&_i_+_1_in_dom_p_holds_
a,p_._(i_+_1)_are_convergent_wrt_R
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies a,p . i are_convergent_wrt R ) & i + 1 in dom p implies a,p . (b1 + 1) are_convergent_wrt R )
assume that
A5: ( i in dom p implies a,p . i are_convergent_wrt R ) and
A6: i + 1 in dom p ; ::_thesis: a,p . (b1 + 1) are_convergent_wrt R
percases ( i in dom p or not i in dom p ) ;
supposeA7: i in dom p ; ::_thesis: a,p . (b1 + 1) are_convergent_wrt R
then consider c being set such that
A8: R reduces a,c and
A9: R reduces p . i,c by A5, Def7;
[(p . i),(p . (i + 1))] in R \/ (R ~) by A6, A7, Def2;
then ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in R ~ ) by XBOOLE_0:def_3;
then ( [(p . i),(p . (i + 1))] in R or [(p . (i + 1)),(p . i)] in R ) by RELAT_1:def_7;
then ( R reduces p . i,p . (i + 1) or R reduces p . (i + 1),p . i ) by Th15;
then ( c,p . (i + 1) are_divergent_wrt R or R reduces p . (i + 1),c ) by A9, Def8, Th16;
then ( c,p . (i + 1) are_convergent_wrt R or a,p . (i + 1) are_convergent_wrt R ) by A2, A8, Def7;
hence a,p . (i + 1) are_convergent_wrt R by A8, Th42; ::_thesis: verum
end;
suppose not i in dom p ; ::_thesis: a,p . (b1 + 1) are_convergent_wrt R
then ( i < 0 + 1 or ( i > len p & i + 1 <= len p ) ) by A6, Lm1, Lm3;
then i = 0 by NAT_1:13;
hence a,p . (i + 1) are_convergent_wrt R by A3, Th38; ::_thesis: verum
end;
end;
end;
then A10: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A11: len p in dom p by FINSEQ_5:6;
A12: S1[ 0 ] by Lm1;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A12, A10);
hence a,b are_convergent_wrt R by A4, A11; ::_thesis: verum
end;
cluster Relation-like subcommutative -> confluent for set ;
coherence
for b1 being Relation st b1 is subcommutative holds
b1 is confluent
proof
let R be Relation; ::_thesis: ( R is subcommutative implies R is confluent )
assume R is subcommutative ; ::_thesis: R is confluent
then for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R by Th49;
hence R is confluent by Th51; ::_thesis: verum
end;
cluster Relation-like with_Church-Rosser_property -> with_NF_property for set ;
coherence
for b1 being Relation st b1 is with_Church-Rosser_property holds
b1 is with_NF_property
proof
let R be Relation; ::_thesis: ( R is with_Church-Rosser_property implies R is with_NF_property )
assume A13: R is with_Church-Rosser_property ; ::_thesis: R is with_NF_property
let b, a be set ; :: according to REWRITE1:def_20 ::_thesis: ( b is_a_normal_form_wrt R & b,a are_convertible_wrt R implies R reduces a,b )
assume A14: b is_a_normal_form_wrt R ; ::_thesis: ( not b,a are_convertible_wrt R or R reduces a,b )
assume b,a are_convertible_wrt R ; ::_thesis: R reduces a,b
then b,a are_convergent_wrt R by A13, Def23;
then ex c being set st
( R reduces b,c & R reduces a,c ) by Def7;
hence R reduces a,b by A14, Th33; ::_thesis: verum
end;
cluster Relation-like with_NF_property -> with_UN_property for set ;
coherence
for b1 being Relation st b1 is with_NF_property holds
b1 is with_UN_property
proof
let R be Relation; ::_thesis: ( R is with_NF_property implies R is with_UN_property )
assume A15: for a, b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
R reduces b,a ; :: according to REWRITE1:def_20 ::_thesis: R is with_UN_property
let a, b be set ; :: according to REWRITE1:def_19 ::_thesis: ( a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R implies a = b )
assume ( a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R ) ; ::_thesis: a = b
hence a = b by A15, Th33; ::_thesis: verum
end;
cluster Relation-like weakly-normalizing with_UN_property -> with_Church-Rosser_property for set ;
coherence
for b1 being Relation st b1 is with_UN_property & b1 is weakly-normalizing holds
b1 is with_Church-Rosser_property
proof
let R be Relation; ::_thesis: ( R is with_UN_property & R is weakly-normalizing implies R is with_Church-Rosser_property )
assume that
A16: for a, b being set st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
a = b and
A17: for a being set st a in field R holds
a has_a_normal_form_wrt R ; :: according to REWRITE1:def_14,REWRITE1:def_19 ::_thesis: R is with_Church-Rosser_property
let a, b be set ; :: according to REWRITE1:def_23 ::_thesis: ( a,b are_convertible_wrt R implies a,b are_convergent_wrt R )
assume A18: R \/ (R ~) reduces a,b ; :: according to REWRITE1:def_4 ::_thesis: a,b are_convergent_wrt R
A19: field (R \/ (R ~)) = (field R) \/ (field (R ~)) by RELAT_1:18
.= (field R) \/ (field R) by RELAT_1:21
.= field R ;
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: a,b are_convergent_wrt R
hence a,b are_convergent_wrt R by Th38; ::_thesis: verum
end;
supposeA20: a <> b ; ::_thesis: a,b are_convergent_wrt R
then b in field R by A18, A19, Th18;
then b has_a_normal_form_wrt R by A17;
then consider b9 being set such that
A21: b9 is_a_normal_form_of b,R by Def11;
a in field R by A18, A19, A20, Th18;
then a has_a_normal_form_wrt R by A17;
then consider a9 being set such that
A22: a9 is_a_normal_form_of a,R by Def11;
A23: a9 is_a_normal_form_wrt R by A22, Def6;
A24: a,b are_convertible_wrt R by A18, Def4;
A25: R reduces a,a9 by A22, Def6;
then a9,a are_convertible_wrt R by Th25;
then A26: a9,b are_convertible_wrt R by A24, Th30;
A27: b9 is_a_normal_form_wrt R by A21, Def6;
A28: R reduces b,b9 by A21, Def6;
then b,b9 are_convertible_wrt R by Th25;
then a9 = b9 by A16, A23, A27, A26, Th30;
hence a,b are_convergent_wrt R by A25, A28, Def7; ::_thesis: verum
end;
end;
end;
end;
registration
cluster empty Relation-like -> subcommutative for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is subcommutative
proof
let R be Relation; ::_thesis: ( R is empty implies R is subcommutative )
assume A1: R is empty ; ::_thesis: R is subcommutative
let x be set ; :: according to REWRITE1:def_21 ::_thesis: for b, c being set st [x,b] in R & [x,c] in R holds
b,c are_convergent<=1_wrt R
thus for b, c being set st [x,b] in R & [x,c] in R holds
b,c are_convergent<=1_wrt R by A1; ::_thesis: verum
end;
end;
theorem Th53: :: REWRITE1:53
for R being with_UN_property Relation
for a, b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c
proof
let R be with_UN_property Relation; ::_thesis: for a, b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c
let a, b, c be set ; ::_thesis: ( b is_a_normal_form_of a,R & c is_a_normal_form_of a,R implies b = c )
assume that
A1: b is_a_normal_form_wrt R and
A2: R reduces a,b and
A3: c is_a_normal_form_wrt R and
A4: R reduces a,c ; :: according to REWRITE1:def_6 ::_thesis: b = c
b,c are_divergent_wrt R by A2, A4, Def8;
then b,c are_convertible_wrt R by Th37;
hence b = c by A1, A3, Def19; ::_thesis: verum
end;
theorem Th54: :: REWRITE1:54
for R being weakly-normalizing with_UN_property Relation
for a being set holds nf (a,R) is_a_normal_form_of a,R
proof
let R be weakly-normalizing with_UN_property Relation; ::_thesis: for a being set holds nf (a,R) is_a_normal_form_of a,R
let a be set ; ::_thesis: nf (a,R) is_a_normal_form_of a,R
( a in field R or not a in field R ) ;
then A1: a has_a_normal_form_wrt R by Def14, Th46;
for b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c by Th53;
hence nf (a,R) is_a_normal_form_of a,R by A1, Def12; ::_thesis: verum
end;
theorem Th55: :: REWRITE1:55
for R being weakly-normalizing with_UN_property Relation
for a, b being set st a,b are_convertible_wrt R holds
nf (a,R) = nf (b,R)
proof
let R be weakly-normalizing with_UN_property Relation; ::_thesis: for a, b being set st a,b are_convertible_wrt R holds
nf (a,R) = nf (b,R)
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt R implies nf (a,R) = nf (b,R) )
A1: nf (b,R) is_a_normal_form_of b,R by Th54;
then A2: nf (b,R) is_a_normal_form_wrt R by Def6;
R reduces b, nf (b,R) by A1, Def6;
then A3: b, nf (b,R) are_convertible_wrt R by Th25;
A4: nf (a,R) is_a_normal_form_of a,R by Th54;
then R reduces a, nf (a,R) by Def6;
then A5: nf (a,R),a are_convertible_wrt R by Th25;
assume a,b are_convertible_wrt R ; ::_thesis: nf (a,R) = nf (b,R)
then nf (a,R),b are_convertible_wrt R by A5, Th30;
then A6: nf (a,R), nf (b,R) are_convertible_wrt R by A3, Th30;
nf (a,R) is_a_normal_form_wrt R by A4, Def6;
hence nf (a,R) = nf (b,R) by A2, A6, Def19; ::_thesis: verum
end;
registration
cluster Relation-like strongly-normalizing locally-confluent -> confluent for set ;
coherence
for b1 being Relation st b1 is strongly-normalizing & b1 is locally-confluent holds
b1 is confluent
proof
let R be Relation; ::_thesis: ( R is strongly-normalizing & R is locally-confluent implies R is confluent )
assume A1: R is strongly-normalizing ; ::_thesis: ( not R is locally-confluent or R is confluent )
defpred S1[ set ] means for b, c being set st R reduces c1,b & R reduces c1,c holds
b,c are_convergent_wrt R;
assume A2: for a, b, c being set st [a,b] in R & [a,c] in R holds
b,c are_convergent_wrt R ; :: according to REWRITE1:def_24 ::_thesis: R is confluent
A3: for a being set st ( for b being set st [a,b] in R & a <> b holds
S1[b] ) holds
S1[a]
proof
let a be set ; ::_thesis: ( ( for b being set st [a,b] in R & a <> b holds
S1[b] ) implies S1[a] )
assume A4: for b being set st [a,b] in R & a <> b holds
S1[b] ; ::_thesis: S1[a]
let b, c be set ; ::_thesis: ( R reduces a,b & R reduces a,c implies b,c are_convergent_wrt R )
assume that
A5: R reduces a,b and
A6: R reduces a,c ; ::_thesis: b,c are_convergent_wrt R
consider p being RedSequence of R such that
A7: a = p . 1 and
A8: b = p . (len p) by A5, Def3;
A9: len p >= 0 + 1 by NAT_1:13;
consider q being RedSequence of R such that
A10: a = q . 1 and
A11: c = q . (len q) by A6, Def3;
A12: len q >= 0 + 1 by NAT_1:13;
percases ( len p = 1 or len q = 1 or ( len p <> 1 & len q <> 1 ) ) ;
suppose len p = 1 ; ::_thesis: b,c are_convergent_wrt R
hence b,c are_convergent_wrt R by A6, A7, A8, Th36; ::_thesis: verum
end;
suppose len q = 1 ; ::_thesis: b,c are_convergent_wrt R
hence b,c are_convergent_wrt R by A5, A10, A11, Th36; ::_thesis: verum
end;
supposeA13: ( len p <> 1 & len q <> 1 ) ; ::_thesis: b,c are_convergent_wrt R
then len q > 1 by A12, XXREAL_0:1;
then A14: 1 + 1 <= len q by NAT_1:13;
then A15: 1 + 1 in dom q by Lm3;
len q in dom q by FINSEQ_5:6;
then A16: R reduces q . 2,c by A11, A14, A15, Th17;
len p > 1 by A9, A13, XXREAL_0:1;
then A17: 1 + 1 <= len p by NAT_1:13;
then A18: 1 + 1 in dom p by Lm3;
len p in dom p by FINSEQ_5:6;
then A19: R reduces p . 2,b by A8, A17, A18, Th17;
1 in dom p by A9, Lm3;
then A20: [a,(p . 2)] in R by A7, A18, Def2;
then A21: a in field R by RELAT_1:15;
1 in dom q by A12, Lm3;
then A22: [a,(q . 2)] in R by A10, A15, Def2;
then p . 2,q . 2 are_convergent_wrt R by A2, A20;
then consider d being set such that
A23: R reduces p . 2,d and
A24: R reduces q . 2,d by Def7;
A25: R is_irreflexive_in field R by A1, RELAT_2:def_10;
then A26: a <> q . 2 by A22, A21, RELAT_2:def_2;
a <> p . 2 by A20, A21, A25, RELAT_2:def_2;
then b,d are_convergent_wrt R by A4, A20, A23, A19;
then consider e being set such that
A27: R reduces b,e and
A28: R reduces d,e by Def7;
R reduces q . 2,e by A24, A28, Th16;
then e,c are_convergent_wrt R by A4, A22, A26, A16;
hence b,c are_convergent_wrt R by A27, Th42; ::_thesis: verum
end;
end;
end;
A29: R is co-well_founded by A1;
A30: for a being set st a in field R holds
S1[a] from REWRITE1:sch_2(A29, A3);
given a0, b0 being set such that A31: a0,b0 are_divergent_wrt R and
A32: not a0,b0 are_convergent_wrt R ; :: according to REWRITE1:def_22 ::_thesis: contradiction
consider c0 being set such that
A33: ( R reduces c0,a0 & R reduces c0,b0 ) by A31, Def8;
( a0 <> c0 or b0 <> c0 ) by A32, Th38;
then c0 in field R by A33, Th18;
hence contradiction by A32, A33, A30; ::_thesis: verum
end;
end;
definition
let R be Relation;
attrR is complete means :Def25: :: REWRITE1:def 25
( R is confluent & R is strongly-normalizing );
end;
:: deftheorem Def25 defines complete REWRITE1:def_25_:_
for R being Relation holds
( R is complete iff ( R is confluent & R is strongly-normalizing ) );
registration
cluster Relation-like complete -> strongly-normalizing confluent for set ;
coherence
for b1 being Relation st b1 is complete holds
( b1 is confluent & b1 is strongly-normalizing ) by Def25;
cluster Relation-like strongly-normalizing confluent -> complete for set ;
coherence
for b1 being Relation st b1 is confluent & b1 is strongly-normalizing holds
b1 is complete by Def25;
end;
registration
cluster non empty Relation-like complete for set ;
existence
ex b1 being non empty Relation st b1 is complete
proof
reconsider R = {[0,1]} as non empty Relation ;
take R ; ::_thesis: R is complete
A1: field R = {0,1} by RELAT_1:17;
thus R is confluent :: according to REWRITE1:def_25 ::_thesis: R is strongly-normalizing
proof
let a, b be set ; :: according to REWRITE1:def_22 ::_thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
given c being set such that A2: R reduces c,a and
A3: R reduces c,b ; :: according to REWRITE1:def_8 ::_thesis: a,b are_convergent_wrt R
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: a,b are_convergent_wrt R
hence a,b are_convergent_wrt R by Th38; ::_thesis: verum
end;
suppose a <> b ; ::_thesis: a,b are_convergent_wrt R
then ( a <> c or b <> c ) ;
then A4: c in field R by A2, A3, Th18;
then a in {0,1} by A1, A2, Th18;
then A5: ( a = 0 or a = 1 ) by TARSKI:def_2;
b in {0,1} by A1, A3, A4, Th18;
then A6: ( b = 0 or b = 1 ) by TARSKI:def_2;
[0,1] in R by TARSKI:def_1;
then A7: R reduces 0 ,1 by Th15;
R reduces 1,1 by Th12;
hence a,b are_convergent_wrt R by A5, A6, A7, Def7; ::_thesis: verum
end;
end;
end;
A8: R is co-well_founded
proof
let Y be set ; :: according to REWRITE1:def_16 ::_thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
assume that
A9: Y c= field R and
A10: Y <> {} ; ::_thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
reconsider Y9 = Y as non empty set by A10;
set y = the Element of Y9;
percases ( 1 in Y or ( not 1 in Y & the Element of Y9 in Y ) ) ;
supposeA11: 1 in Y ; ::_thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
take 1 ; ::_thesis: ( 1 in Y & ( for b being set st b in Y & 1 <> b holds
not [1,b] in R ) )
thus 1 in Y by A11; ::_thesis: for b being set st b in Y & 1 <> b holds
not [1,b] in R
let b be set ; ::_thesis: ( b in Y & 1 <> b implies not [1,b] in R )
assume that
b in Y and
1 <> b ; ::_thesis: not [1,b] in R
[0,1] <> [1,b] by XTUPLE_0:1;
hence not [1,b] in R by TARSKI:def_1; ::_thesis: verum
end;
supposeA12: ( not 1 in Y & the Element of Y9 in Y ) ; ::_thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
take 0 ; ::_thesis: ( 0 in Y & ( for b being set st b in Y & 0 <> b holds
not [0,b] in R ) )
thus 0 in Y by A1, A9, A12, TARSKI:def_2; ::_thesis: for b being set st b in Y & 0 <> b holds
not [0,b] in R
let b be set ; ::_thesis: ( b in Y & 0 <> b implies not [0,b] in R )
assume b in Y ; ::_thesis: ( not 0 <> b or not [0,b] in R )
hence ( not 0 <> b or not [0,b] in R ) by A1, A9, A12, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
R is irreflexive
proof
let x be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( not x in field R or not [x,x] in R )
assume that
x in field R and
A13: [x,x] in R ; ::_thesis: contradiction
A14: [x,x] = [0,1] by A13, TARSKI:def_1;
then x = 0 by XTUPLE_0:1;
hence contradiction by A14, XTUPLE_0:1; ::_thesis: verum
end;
hence R is strongly-normalizing by A8; ::_thesis: verum
end;
end;
theorem :: REWRITE1:56
for R, Q being with_Church-Rosser_property Relation st R commutes_with Q holds
R \/ Q is with_Church-Rosser_property
proof
let R, Q be with_Church-Rosser_property Relation; ::_thesis: ( R commutes_with Q implies R \/ Q is with_Church-Rosser_property )
assume A1: R commutes_with Q ; ::_thesis: R \/ Q is with_Church-Rosser_property
R \/ Q is confluent
proof
let a, b be set ; :: according to REWRITE1:def_22 ::_thesis: ( a,b are_divergent_wrt R \/ Q implies a,b are_convergent_wrt R \/ Q )
given c being set such that A2: R \/ Q reduces c,a and
A3: R \/ Q reduces c,b ; :: according to REWRITE1:def_8 ::_thesis: a,b are_convergent_wrt R \/ Q
consider p being RedSequence of R \/ Q such that
A4: c = p . 1 and
A5: a = p . (len p) by A2, Def3;
defpred S1[ Element of NAT ] means ( $1 in dom p implies p . $1,b are_convergent_wrt R \/ Q );
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_p_._i,b_are_convergent_wrt_R_\/_Q_)_&_i_+_1_in_dom_p_holds_
p_._(i_+_1),b_are_convergent_wrt_R_\/_Q
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies p . i,b are_convergent_wrt R \/ Q ) & i + 1 in dom p implies p . (b1 + 1),b are_convergent_wrt R \/ Q )
assume that
A6: ( i in dom p implies p . i,b are_convergent_wrt R \/ Q ) and
A7: i + 1 in dom p ; ::_thesis: p . (b1 + 1),b are_convergent_wrt R \/ Q
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: p . (b1 + 1),b are_convergent_wrt R \/ Q
hence p . (i + 1),b are_convergent_wrt R \/ Q by A3, A4, Th36; ::_thesis: verum
end;
supposeA8: i > 0 ; ::_thesis: p . (b1 + 1),b are_convergent_wrt R \/ Q
A9: i < len p by A7, Lm2;
then consider d being set such that
A10: R \/ Q reduces p . i,d and
A11: R \/ Q reduces b,d by A6, A8, Def7, Lm3;
consider q being RedSequence of R \/ Q such that
A12: p . i = q . 1 and
A13: d = q . (len q) by A10, Def3;
defpred S2[ Element of NAT ] means ( $1 in dom q implies ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . $1,e or Q reduces q . $1,e ) ) );
i in dom p by A8, A9, Lm3;
then [(p . i),(p . (i + 1))] in R \/ Q by A7, Def2;
then A14: ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in Q ) by XBOOLE_0:def_3;
now__::_thesis:_for_j_being_Element_of_NAT_st_(_j_in_dom_q_implies_ex_e_being_set_st_
(_R_\/_Q_reduces_p_._(i_+_1),e_&_(_R_reduces_q_._j,e_or_Q_reduces_q_._j,e_)_)_)_&_j_+_1_in_dom_q_holds_
ex_e_being_set_st_
(_R_\/_Q_reduces_p_._(i_+_1),e_&_(_R_reduces_q_._(j_+_1),e_or_Q_reduces_q_._(j_+_1),e_)_)
let j be Element of NAT ; ::_thesis: ( ( j in dom q implies ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . j,e or Q reduces q . j,e ) ) ) & j + 1 in dom q implies ex e being set st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) ) )
assume that
A15: ( j in dom q implies ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . j,e or Q reduces q . j,e ) ) ) and
A16: j + 1 in dom q ; ::_thesis: ex e being set st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) )
A17: j < len q by A16, Lm2;
percases ( j = 0 or j > 0 ) ;
supposeA18: j = 0 ; ::_thesis: ex e being set st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) )
A19: R \/ Q reduces p . (i + 1),p . (i + 1) by Th12;
( R reduces q . (j + 1),p . (i + 1) or Q reduces q . (j + 1),p . (i + 1) ) by A12, A14, A18, Th15;
hence ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . (j + 1),e or Q reduces q . (j + 1),e ) ) by A19; ::_thesis: verum
end;
supposeA20: j > 0 ; ::_thesis: ex e being set st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) )
then consider e being set such that
A21: R \/ Q reduces p . (i + 1),e and
A22: ( R reduces q . j,e or Q reduces q . j,e ) by A15, A17, Lm3;
A23: now__::_thesis:_(_R_reduces_q_._j,q_._(j_+_1)_&_Q_reduces_q_._j,e_implies_ex_x_being_set_st_
(_R_\/_Q_reduces_p_._(i_+_1),x_&_(_R_reduces_q_._(j_+_1),x_or_Q_reduces_q_._(j_+_1),x_)_)_)
assume ( R reduces q . j,q . (j + 1) & Q reduces q . j,e ) ; ::_thesis: ex x being set st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then consider x being set such that
A24: Q reduces q . (j + 1),x and
A25: R reduces e,x by A1, Def18;
take x = x; ::_thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A25, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A24, Th16; ::_thesis: verum
end;
A26: now__::_thesis:_(_Q_reduces_q_._j,q_._(j_+_1)_&_Q_reduces_q_._j,e_implies_ex_x_being_set_st_
(_R_\/_Q_reduces_p_._(i_+_1),x_&_(_R_reduces_q_._(j_+_1),x_or_Q_reduces_q_._(j_+_1),x_)_)_)
assume ( Q reduces q . j,q . (j + 1) & Q reduces q . j,e ) ; ::_thesis: ex x being set st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then e,q . (j + 1) are_divergent_wrt Q by Def8;
then e,q . (j + 1) are_convergent_wrt Q by Def22;
then consider x being set such that
A27: Q reduces e,x and
A28: Q reduces q . (j + 1),x by Def7;
take x = x; ::_thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A27, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A28, Th16; ::_thesis: verum
end;
A29: now__::_thesis:_(_R_reduces_q_._j,q_._(j_+_1)_&_R_reduces_q_._j,e_implies_ex_x_being_set_st_
(_R_\/_Q_reduces_p_._(i_+_1),x_&_(_R_reduces_q_._(j_+_1),x_or_Q_reduces_q_._(j_+_1),x_)_)_)
assume ( R reduces q . j,q . (j + 1) & R reduces q . j,e ) ; ::_thesis: ex x being set st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then e,q . (j + 1) are_divergent_wrt R by Def8;
then e,q . (j + 1) are_convergent_wrt R by Def22;
then consider x being set such that
A30: R reduces e,x and
A31: R reduces q . (j + 1),x by Def7;
take x = x; ::_thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A30, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A31, Th16; ::_thesis: verum
end;
A32: now__::_thesis:_(_Q_reduces_q_._j,q_._(j_+_1)_&_R_reduces_q_._j,e_implies_ex_x_being_set_st_
(_R_\/_Q_reduces_p_._(i_+_1),x_&_(_R_reduces_q_._(j_+_1),x_or_Q_reduces_q_._(j_+_1),x_)_)_)
assume ( Q reduces q . j,q . (j + 1) & R reduces q . j,e ) ; ::_thesis: ex x being set st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then consider x being set such that
A33: R reduces q . (j + 1),x and
A34: Q reduces e,x by A1, Def18;
take x = x; ::_thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A34, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A33, Th16; ::_thesis: verum
end;
j in dom q by A17, A20, Lm3;
then [(q . j),(q . (j + 1))] in R \/ Q by A16, Def2;
then ( [(q . j),(q . (j + 1))] in R or [(q . j),(q . (j + 1))] in Q ) by XBOOLE_0:def_3;
hence ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . (j + 1),e or Q reduces q . (j + 1),e ) ) by A22, A29, A26, A23, A32, Th15; ::_thesis: verum
end;
end;
end;
then A35: for k being Element of NAT st S2[k] holds
S2[k + 1] ;
A36: S2[ 0 ] by Lm1;
A37: for j being Element of NAT holds S2[j] from NAT_1:sch_1(A36, A35);
thus p . (i + 1),b are_convergent_wrt R \/ Q ::_thesis: verum
proof
len q in dom q by FINSEQ_5:6;
then consider e being set such that
A38: R \/ Q reduces p . (i + 1),e and
A39: ( R reduces d,e or Q reduces d,e ) by A13, A37;
take e ; :: according to REWRITE1:def_7 ::_thesis: ( R \/ Q reduces p . (i + 1),e & R \/ Q reduces b,e )
R \/ Q reduces d,e by A39, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),e & R \/ Q reduces b,e ) by A11, A38, Th16; ::_thesis: verum
end;
end;
end;
end;
then A40: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A41: len p in dom p by FINSEQ_5:6;
A42: S1[ 0 ] by Lm1;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A42, A40);
hence a,b are_convergent_wrt R \/ Q by A5, A41; ::_thesis: verum
end;
hence R \/ Q is with_Church-Rosser_property ; ::_thesis: verum
end;
theorem :: REWRITE1:57
for R being Relation holds
( R is confluent iff R [*] is locally-confluent )
proof
let R be Relation; ::_thesis: ( R is confluent iff R [*] is locally-confluent )
hereby ::_thesis: ( R [*] is locally-confluent implies R is confluent )
assume A1: R is confluent ; ::_thesis: R [*] is locally-confluent
thus R [*] is locally-confluent ::_thesis: verum
proof
let a, b, c be set ; :: according to REWRITE1:def_24 ::_thesis: ( [a,b] in R [*] & [a,c] in R [*] implies b,c are_convergent_wrt R [*] )
assume ( [a,b] in R [*] & [a,c] in R [*] ) ; ::_thesis: b,c are_convergent_wrt R [*]
then ( R reduces a,b & R reduces a,c ) by Th20;
then b,c are_divergent_wrt R by Def8;
then b,c are_convergent_wrt R by A1, Def22;
then consider d being set such that
A2: ( R reduces b,d & R reduces c,d ) by Def7;
take d ; :: according to REWRITE1:def_7 ::_thesis: ( R [*] reduces b,d & R [*] reduces c,d )
thus ( R [*] reduces b,d & R [*] reduces c,d ) by A2, Th21; ::_thesis: verum
end;
end;
assume A3: for a, b, c being set st [a,b] in R [*] & [a,c] in R [*] holds
b,c are_convergent_wrt R [*] ; :: according to REWRITE1:def_24 ::_thesis: R is confluent
let a, b be set ; :: according to REWRITE1:def_22 ::_thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
given c being set such that A4: R reduces c,a and
A5: R reduces c,b ; :: according to REWRITE1:def_8 ::_thesis: a,b are_convergent_wrt R
A6: ( [c,b] in R [*] or c = b ) by A5, Th20;
( [c,a] in R [*] or c = a ) by A4, Th20;
then ( a,b are_convergent_wrt R [*] or R [*] reduces a,b or R [*] reduces b,a ) by A3, A6, Th15, Th38;
then a,b are_convergent_wrt R [*] by Th36;
then consider d being set such that
A7: ( R [*] reduces a,d & R [*] reduces b,d ) by Def7;
take d ; :: according to REWRITE1:def_7 ::_thesis: ( R reduces a,d & R reduces b,d )
thus ( R reduces a,d & R reduces b,d ) by A7, Th21; ::_thesis: verum
end;
theorem :: REWRITE1:58
for R being Relation holds
( R is confluent iff R [*] is subcommutative )
proof
let R be Relation; ::_thesis: ( R is confluent iff R [*] is subcommutative )
hereby ::_thesis: ( R [*] is subcommutative implies R is confluent )
assume A1: R is confluent ; ::_thesis: R [*] is subcommutative
thus R [*] is subcommutative ::_thesis: verum
proof
let a, b, c be set ; :: according to REWRITE1:def_21 ::_thesis: ( [a,b] in R [*] & [a,c] in R [*] implies b,c are_convergent<=1_wrt R [*] )
assume ( [a,b] in R [*] & [a,c] in R [*] ) ; ::_thesis: b,c are_convergent<=1_wrt R [*]
then ( R reduces a,b & R reduces a,c ) by Th20;
then b,c are_divergent_wrt R by Def8;
then b,c are_convergent_wrt R by A1, Def22;
then consider d being set such that
A2: ( R reduces b,d & R reduces c,d ) by Def7;
take d ; :: according to REWRITE1:def_9 ::_thesis: ( ( [b,d] in R [*] or b = d ) & ( [c,d] in R [*] or c = d ) )
thus ( ( [b,d] in R [*] or b = d ) & ( [c,d] in R [*] or c = d ) ) by A2, Th20; ::_thesis: verum
end;
end;
assume A3: for a, b, c being set st [a,b] in R [*] & [a,c] in R [*] holds
b,c are_convergent<=1_wrt R [*] ; :: according to REWRITE1:def_21 ::_thesis: R is confluent
let a, b be set ; :: according to REWRITE1:def_22 ::_thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
given c being set such that A4: R reduces c,a and
A5: R reduces c,b ; :: according to REWRITE1:def_8 ::_thesis: a,b are_convergent_wrt R
A6: ( [c,b] in R [*] or c = b ) by A5, Th20;
( [c,a] in R [*] or c = a ) by A4, Th20;
then a,b are_convergent<=1_wrt R [*] by A3, A6, Def9;
then a,b are_convergent_wrt R [*] by Th44;
then consider d being set such that
A7: ( R [*] reduces a,d & R [*] reduces b,d ) by Def7;
take d ; :: according to REWRITE1:def_7 ::_thesis: ( R reduces a,d & R reduces b,d )
thus ( R reduces a,d & R reduces b,d ) by A7, Th21; ::_thesis: verum
end;
begin
definition
let R, Q be Relation;
predR,Q are_equivalent means :: REWRITE1:def 26
for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q );
symmetry
for R, Q being Relation st ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) ) holds
for a, b being set holds
( a,b are_convertible_wrt Q iff a,b are_convertible_wrt R ) ;
end;
:: deftheorem defines are_equivalent REWRITE1:def_26_:_
for R, Q being Relation holds
( R,Q are_equivalent iff for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) );
definition
let R be Relation;
let a, b be set ;
preda,b are_critical_wrt R means :Def27: :: REWRITE1:def 27
( a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R );
end;
:: deftheorem Def27 defines are_critical_wrt REWRITE1:def_27_:_
for R being Relation
for a, b being set holds
( a,b are_critical_wrt R iff ( a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R ) );
theorem Th59: :: REWRITE1:59
for R being Relation
for a, b being set st a,b are_critical_wrt R holds
a,b are_convertible_wrt R
proof
let R be Relation; ::_thesis: for a, b being set st a,b are_critical_wrt R holds
a,b are_convertible_wrt R
let a, b be set ; ::_thesis: ( a,b are_critical_wrt R implies a,b are_convertible_wrt R )
assume that
A1: a,b are_divergent<=1_wrt R and
not a,b are_convergent_wrt R ; :: according to REWRITE1:def_27 ::_thesis: a,b are_convertible_wrt R
thus a,b are_convertible_wrt R by A1, Th37, Th45; ::_thesis: verum
end;
theorem :: REWRITE1:60
for R being Relation st ( for a, b being set holds not a,b are_critical_wrt R ) holds
R is locally-confluent
proof
let R be Relation; ::_thesis: ( ( for a, b being set holds not a,b are_critical_wrt R ) implies R is locally-confluent )
assume A1: for a, b being set holds not a,b are_critical_wrt R ; ::_thesis: R is locally-confluent
let a, b, c be set ; :: according to REWRITE1:def_24 ::_thesis: ( [a,b] in R & [a,c] in R implies b,c are_convergent_wrt R )
assume ( [a,b] in R & [a,c] in R ) ; ::_thesis: b,c are_convergent_wrt R
then A2: b,c are_divergent<=1_wrt R by Def10;
not b,c are_critical_wrt R by A1;
hence b,c are_convergent_wrt R by A2, Def27; ::_thesis: verum
end;
theorem :: REWRITE1:61
for R, Q being Relation st ( for a, b being set st [a,b] in Q holds
a,b are_critical_wrt R ) holds
R,R \/ Q are_equivalent
proof
let R, Q be Relation; ::_thesis: ( ( for a, b being set st [a,b] in Q holds
a,b are_critical_wrt R ) implies R,R \/ Q are_equivalent )
assume A1: for a, b being set st [a,b] in Q holds
a,b are_critical_wrt R ; ::_thesis: R,R \/ Q are_equivalent
let a, b be set ; :: according to REWRITE1:def_26 ::_thesis: ( a,b are_convertible_wrt R iff a,b are_convertible_wrt R \/ Q )
A2: R c= R \/ Q by XBOOLE_1:7;
A3: R ~ c= (R \/ Q) ~
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in R ~ or [x,y] in (R \/ Q) ~ )
assume [x,y] in R ~ ; ::_thesis: [x,y] in (R \/ Q) ~
then [y,x] in R by RELAT_1:def_7;
hence [x,y] in (R \/ Q) ~ by A2, RELAT_1:def_7; ::_thesis: verum
end;
hereby ::_thesis: ( a,b are_convertible_wrt R \/ Q implies a,b are_convertible_wrt R )
assume a,b are_convertible_wrt R ; ::_thesis: a,b are_convertible_wrt R \/ Q
then R \/ (R ~) reduces a,b by Def4;
then (R \/ Q) \/ ((R \/ Q) ~) reduces a,b by A2, A3, Th22, XBOOLE_1:13;
hence a,b are_convertible_wrt R \/ Q by Def4; ::_thesis: verum
end;
given p being RedSequence of (R \/ Q) \/ ((R \/ Q) ~) such that A4: a = p . 1 and
A5: b = p . (len p) ; :: according to REWRITE1:def_3,REWRITE1:def_4 ::_thesis: a,b are_convertible_wrt R
defpred S1[ Element of NAT ] means ( $1 in dom p implies a,p . $1 are_convertible_wrt R );
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_a,p_._i_are_convertible_wrt_R_)_&_i_+_1_in_dom_p_holds_
a,p_._(i_+_1)_are_convertible_wrt_R
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies a,p . i are_convertible_wrt R ) & i + 1 in dom p implies a,p . (b1 + 1) are_convertible_wrt R )
assume that
A6: ( i in dom p implies a,p . i are_convertible_wrt R ) and
A7: i + 1 in dom p ; ::_thesis: a,p . (b1 + 1) are_convertible_wrt R
A8: i < len p by A7, Lm2;
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: a,p . (b1 + 1) are_convertible_wrt R
hence a,p . (i + 1) are_convertible_wrt R by A4, Th26; ::_thesis: verum
end;
supposeA9: i > 0 ; ::_thesis: a,p . (b1 + 1) are_convertible_wrt R
then i in dom p by A8, Lm3;
then [(p . i),(p . (i + 1))] in (R \/ Q) \/ ((R \/ Q) ~) by A7, Def2;
then ( [(p . i),(p . (i + 1))] in R \/ Q or [(p . i),(p . (i + 1))] in (R \/ Q) ~ ) by XBOOLE_0:def_3;
then ( [(p . i),(p . (i + 1))] in R \/ Q or [(p . (i + 1)),(p . i)] in R \/ Q ) by RELAT_1:def_7;
then ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in Q or [(p . (i + 1)),(p . i)] in R or [(p . (i + 1)),(p . i)] in Q ) by XBOOLE_0:def_3;
then ( p . i,p . (i + 1) are_convertible_wrt R or p . (i + 1),p . i are_convertible_wrt R ) by A1, Th29, Th59;
then p . i,p . (i + 1) are_convertible_wrt R by Lm5;
hence a,p . (i + 1) are_convertible_wrt R by A6, A8, A9, Lm3, Th30; ::_thesis: verum
end;
end;
end;
then A10: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A11: len p in dom p by FINSEQ_5:6;
A12: S1[ 0 ] by Lm1;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A12, A10);
hence a,b are_convertible_wrt R by A5, A11; ::_thesis: verum
end;
theorem Th62: :: REWRITE1:62
for R being Relation ex Q being complete Relation st
( field Q c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )
proof
let R be Relation; ::_thesis: ex Q being complete Relation st
( field Q c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )
percases ( R = {} or R <> {} ) ;
supposeA1: R = {} ; ::_thesis: ex Q being complete Relation st
( field Q c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )
take E = {} ; ::_thesis: ( field E c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt E ) ) )
thus field E c= field R by XBOOLE_1:2; ::_thesis: for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt E )
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt E )
( a,b are_convertible_wrt R iff a = b ) by A1, Th26, Th27;
hence ( a,b are_convertible_wrt R iff a,b are_convergent_wrt E ) by Th38, Th39; ::_thesis: verum
end;
suppose R <> {} ; ::_thesis: ex Q being complete Relation st
( field Q c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )
then reconsider R9 = R as non empty Relation ;
set xx = the Element of R9;
consider x1, x2 being set such that
A2: the Element of R9 = [x1,x2] by RELAT_1:def_1;
defpred S1[ set , set ] means $1,$2 are_convertible_wrt R;
A3: for x, y being set st S1[x,y] holds
S1[y,x] by Lm5;
A4: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by Th30;
A5: for x being set st x in field R holds
S1[x,x] by Th26;
consider Q being Equivalence_Relation of (field R) such that
A6: for x, y being set holds
( [x,y] in Q iff ( x in field R & y in field R & S1[x,y] ) ) from EQREL_1:sch_1(A5, A3, A4);
A7: ( ( for X being set st X in Class Q holds
X <> {} ) & ( for X, Y being set st X in Class Q & Y in Class Q & X <> Y holds
X misses Y ) ) by EQREL_1:def_4;
x1 in field R by A2, RELAT_1:15;
then Class (Q,x1) in Class Q by EQREL_1:def_3;
then consider X being set such that
A8: for A being set st A in Class Q holds
ex x being set st X /\ A = {x} by A7, WELLORD2:18;
defpred S2[ set , set ] means ( $1 <> $2 & $1,$2 are_convertible_wrt R & $2 in X );
consider P being Relation such that
A9: for x, y being set holds
( [x,y] in P iff ( x in field R & y in field R & S2[x,y] ) ) from RELAT_1:sch_1();
A10: P is locally-confluent
proof
let a, b, c be set ; :: according to REWRITE1:def_24 ::_thesis: ( [a,b] in P & [a,c] in P implies b,c are_convergent_wrt P )
assume that
A11: [a,b] in P and
A12: [a,c] in P ; ::_thesis: b,c are_convergent_wrt P
A13: a in field R by A9, A11;
then Class (Q,a) in Class Q by EQREL_1:def_3;
then consider x being set such that
A14: X /\ (Class (Q,a)) = {x} by A8;
( c in field R & a,c are_convertible_wrt R ) by A9, A12;
then [a,c] in Q by A6, A13;
then [c,a] in Q by EQREL_1:6;
then A15: c in Class (Q,a) by EQREL_1:19;
c in X by A9, A12;
then c in {x} by A15, A14, XBOOLE_0:def_4;
then A16: c = x by TARSKI:def_1;
( b in field R & a,b are_convertible_wrt R ) by A9, A11;
then [a,b] in Q by A6, A13;
then [b,a] in Q by EQREL_1:6;
then A17: b in Class (Q,a) by EQREL_1:19;
take b ; :: according to REWRITE1:def_7 ::_thesis: ( P reduces b,b & P reduces c,b )
b in X by A9, A11;
then b in {x} by A17, A14, XBOOLE_0:def_4;
then b = x by TARSKI:def_1;
hence ( P reduces b,b & P reduces c,b ) by A16, Th12; ::_thesis: verum
end;
A18: for x, y being set st P reduces x,y holds
x,y are_convertible_wrt R
proof
let x, y be set ; ::_thesis: ( P reduces x,y implies x,y are_convertible_wrt R )
given p being RedSequence of P such that A19: x = p . 1 and
A20: y = p . (len p) ; :: according to REWRITE1:def_3 ::_thesis: x,y are_convertible_wrt R
defpred S3[ Element of NAT ] means ( $1 in dom p implies x,p . $1 are_convertible_wrt R );
now__::_thesis:_for_i_being_Element_of_NAT_st_(_i_in_dom_p_implies_x,p_._i_are_convertible_wrt_R_)_&_i_+_1_in_dom_p_holds_
x,p_._(i_+_1)_are_convertible_wrt_R
let i be Element of NAT ; ::_thesis: ( ( i in dom p implies x,p . i are_convertible_wrt R ) & i + 1 in dom p implies x,p . (b1 + 1) are_convertible_wrt R )
assume that
A21: ( i in dom p implies x,p . i are_convertible_wrt R ) and
A22: i + 1 in dom p ; ::_thesis: x,p . (b1 + 1) are_convertible_wrt R
A23: i < len p by A22, Lm2;
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: x,p . (b1 + 1) are_convertible_wrt R
hence x,p . (i + 1) are_convertible_wrt R by A19, Th26; ::_thesis: verum
end;
supposeA24: i > 0 ; ::_thesis: x,p . (b1 + 1) are_convertible_wrt R
then i in dom p by A23, Lm3;
then [(p . i),(p . (i + 1))] in P by A22, Def2;
then p . i,p . (i + 1) are_convertible_wrt R by A9;
hence x,p . (i + 1) are_convertible_wrt R by A21, A23, A24, Lm3, Th30; ::_thesis: verum
end;
end;
end;
then A25: for k being Element of NAT st S3[k] holds
S3[k + 1] ;
A26: len p in dom p by FINSEQ_5:6;
A27: S3[ 0 ] by Lm1;
for i being Element of NAT holds S3[i] from NAT_1:sch_1(A27, A25);
hence x,y are_convertible_wrt R by A20, A26; ::_thesis: verum
end;
P is strongly-normalizing
proof
let f be ManySortedSet of NAT ; :: according to REWRITE1:def_15 ::_thesis: not for i being Element of NAT holds [(f . i),(f . (i + 1))] in P
percases ( not [(f . 0),(f . (0 + 1))] in P or [(f . 0),(f . (0 + 1))] in P ) ;
suppose not [(f . 0),(f . (0 + 1))] in P ; ::_thesis: not for i being Element of NAT holds [(f . i),(f . (i + 1))] in P
hence not for i being Element of NAT holds [(f . i),(f . (i + 1))] in P ; ::_thesis: verum
end;
supposeA28: [(f . 0),(f . (0 + 1))] in P ; ::_thesis: not for i being Element of NAT holds [(f . i),(f . (i + 1))] in P
take j = 0 + 1; ::_thesis: not [(f . j),(f . (j + 1))] in P
A29: f . j in X by A9, A28;
assume A30: [(f . j),(f . (j + 1))] in P ; ::_thesis: contradiction
then A31: f . j in field R by A9;
then Class (Q,(f . j)) in Class Q by EQREL_1:def_3;
then consider x being set such that
A32: X /\ (Class (Q,(f . j))) = {x} by A8;
( f . (j + 1) in field R & f . j,f . (j + 1) are_convertible_wrt R ) by A9, A30;
then [(f . j),(f . (j + 1))] in Q by A6, A31;
then [(f . (j + 1)),(f . j)] in Q by EQREL_1:6;
then A33: f . (j + 1) in Class (Q,(f . j)) by EQREL_1:19;
f . j in Class (Q,(f . j)) by A31, EQREL_1:20;
then f . j in X /\ (Class (Q,(f . j))) by A29, XBOOLE_0:def_4;
then A34: f . j = x by A32, TARSKI:def_1;
f . (j + 1) in X by A9, A30;
then f . (j + 1) in X /\ (Class (Q,(f . j))) by A33, XBOOLE_0:def_4;
then f . (j + 1) = x by A32, TARSKI:def_1;
hence contradiction by A9, A30, A34; ::_thesis: verum
end;
end;
end;
then reconsider P = P as strongly-normalizing locally-confluent Relation by A10;
take P ; ::_thesis: ( field P c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt P ) ) )
thus field P c= field R ::_thesis: for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field P or x in field R )
assume x in field P ; ::_thesis: x in field R
then ( x in dom P or x in rng P ) by XBOOLE_0:def_3;
then ( ex y being set st [x,y] in P or ex y being set st [y,x] in P ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
hence x in field R by A9; ::_thesis: verum
end;
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )
thus ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P ) ::_thesis: verum
proof
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )
hence ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P ) by Th26, Th38; ::_thesis: verum
end;
supposeA35: a <> b ; ::_thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )
hereby ::_thesis: ( a,b are_convergent_wrt P implies a,b are_convertible_wrt R )
assume A36: a,b are_convertible_wrt R ; ::_thesis: a,b are_convergent_wrt P
then A37: b in field R by A35, Th32;
then Class (Q,b) in Class Q by EQREL_1:def_3;
then consider x being set such that
A38: X /\ (Class (Q,b)) = {x} by A8;
A39: a in field R by A35, A36, Th32;
then A40: [a,b] in Q by A6, A36, A37;
thus a,b are_convergent_wrt P ::_thesis: verum
proof
take x ; :: according to REWRITE1:def_7 ::_thesis: ( P reduces a,x & P reduces b,x )
A41: x in {x} by TARSKI:def_1;
then A42: x in X by A38, XBOOLE_0:def_4;
A43: x in Class (Q,b) by A38, A41, XBOOLE_0:def_4;
then [x,b] in Q by EQREL_1:19;
then [b,x] in Q by EQREL_1:6;
then b,x are_convertible_wrt R by A6;
then A44: ( b = x or [b,x] in P ) by A9, A37, A38, A41, A42;
a in Class (Q,b) by A40, EQREL_1:19;
then [a,x] in Q by A43, EQREL_1:22;
then a,x are_convertible_wrt R by A6;
then ( a = x or [a,x] in P ) by A9, A39, A38, A41, A42;
hence ( P reduces a,x & P reduces b,x ) by A44, Th12, Th15; ::_thesis: verum
end;
end;
given c being set such that A45: ( P reduces a,c & P reduces b,c ) ; :: according to REWRITE1:def_7 ::_thesis: a,b are_convertible_wrt R
( a,c are_convertible_wrt R & c,b are_convertible_wrt R ) by A18, A45, Lm5;
hence a,b are_convertible_wrt R by Th30; ::_thesis: verum
end;
end;
end;
end;
end;
end;
definition
let R be Relation;
mode Completion of R -> complete Relation means :Def28: :: REWRITE1:def 28
for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt it );
existence
ex b1 being complete Relation st
for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt b1 )
proof
ex Q being complete Relation st
( field Q c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) ) by Th62;
hence ex b1 being complete Relation st
for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt b1 ) ; ::_thesis: verum
end;
end;
:: deftheorem Def28 defines Completion REWRITE1:def_28_:_
for R being Relation
for b2 being complete Relation holds
( b2 is Completion of R iff for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt b2 ) );
theorem :: REWRITE1:63
for R being Relation
for C being Completion of R holds R,C are_equivalent
proof
let R be Relation; ::_thesis: for C being Completion of R holds R,C are_equivalent
let C be Completion of R; ::_thesis: R,C are_equivalent
let a, b be set ; :: according to REWRITE1:def_26 ::_thesis: ( a,b are_convertible_wrt R iff a,b are_convertible_wrt C )
( a,b are_convertible_wrt R iff a,b are_convergent_wrt C ) by Def28;
hence ( a,b are_convertible_wrt R iff a,b are_convertible_wrt C ) by Def23, Th37; ::_thesis: verum
end;
theorem :: REWRITE1:64
for R being Relation
for Q being complete Relation st R,Q are_equivalent holds
Q is Completion of R
proof
let R be Relation; ::_thesis: for Q being complete Relation st R,Q are_equivalent holds
Q is Completion of R
let Q be complete Relation; ::_thesis: ( R,Q are_equivalent implies Q is Completion of R )
assume A1: for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) ; :: according to REWRITE1:def_26 ::_thesis: Q is Completion of R
let a, b be set ; :: according to REWRITE1:def_28 ::_thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q )
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) by A1;
hence ( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) by Def23, Th37; ::_thesis: verum
end;
theorem :: REWRITE1:65
for R being Relation
for C being Completion of R
for a, b being set holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
proof
let R be Relation; ::_thesis: for C being Completion of R
for a, b being set holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
let C be Completion of R; ::_thesis: for a, b being set holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
let a, b be set ; ::_thesis: ( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
nf (a,C) is_a_normal_form_of a,C by Th54;
then A1: C reduces a, nf (a,C) by Def6;
( a,b are_convergent_wrt C implies a,b are_convertible_wrt C ) by Th37;
hence ( a,b are_convertible_wrt R implies nf (a,C) = nf (b,C) ) by Def28, Th55; ::_thesis: ( nf (a,C) = nf (b,C) implies a,b are_convertible_wrt R )
nf (b,C) is_a_normal_form_of b,C by Th54;
then A2: C reduces b, nf (b,C) by Def6;
( a,b are_convertible_wrt R iff a,b are_convergent_wrt C ) by Def28;
hence ( nf (a,C) = nf (b,C) implies a,b are_convertible_wrt R ) by A1, A2, Def7; ::_thesis: verum
end;