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