:: Reduction Relations :: by Grzegorz Bancerek :: :: Received November 14, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users 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 ) ) ) proofend; 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 ) proofend; theorem Th2: :: REWRITE1:2 for q, p being FinSequence for x being set st q <> {} holds (p ^ <*x*>) $^ q = p ^ q proofend; theorem :: REWRITE1:3 for p, q being FinSequence for x, y being set holds (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q proofend; theorem :: REWRITE1:4 for q being FinSequence for x being set st q <> {} holds <*x*> $^ q = q proofend; 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 ) proofend; 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 ) proofend; 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 ) ) proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th9: :: REWRITE1:9 for R being Relation for p being RedSequence of R holds Rev p is RedSequence of R ~ proofend; 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 proofend; 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 ) ) ) proofend; theorem Th12: :: REWRITE1:12 for R being Relation for a being set holds R reduces a,a proofend; theorem Th13: :: REWRITE1:13 for a, b being set st {} reduces a,b holds a = b proofend; 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 proofend; theorem Th15: :: REWRITE1:15 for R being Relation for a, b being set st [a,b] in R holds R reduces a,b proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 [*] ) ) proofend; theorem Th21: :: REWRITE1:21 for R being Relation for a, b being set holds ( R reduces a,b iff R [*] reduces a,b ) proofend; 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 proofend; 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 ) proofend; theorem Th24: :: REWRITE1:24 for R being Relation for a, b being set st R reduces a,b holds R ~ reduces b,a proofend; Lm5: for R being Relation for a, b being set st a,b are_convertible_wrt R holds b,a are_convertible_wrt R proofend; 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 ) proofend; theorem Th26: :: REWRITE1:26 for R being Relation for a being set holds a,a are_convertible_wrt R proofend; theorem Th27: :: REWRITE1:27 for a, b being set st a,b are_convertible_wrt {} holds a = b proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 ) proofend; theorem Th39: :: REWRITE1:39 for a, b being set st ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) holds a = b proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) ) ) proofend; 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] proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; theorem :: REWRITE1:50 for R being Relation holds ( R is confluent iff R commutes_with R ) proofend; 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 ) proofend; theorem :: REWRITE1:52 for R being Relation holds ( R is locally-confluent iff R commutes-weakly_with R ) proofend; 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 proofend; 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 ) proofend; cluster Relation-like subcommutative -> confluent for set ; coherence for b1 being Relation st b1 is subcommutative holds b1 is confluent proofend; 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 proofend; 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 proofend; 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 proofend; end; registration cluster empty Relation-like -> subcommutative for set ; coherence for b1 being Relation st b1 is empty holds b1 is subcommutative proofend; 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 proofend; 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 proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: REWRITE1:57 for R being Relation holds ( R is confluent iff R [*] is locally-confluent ) proofend; theorem :: REWRITE1:58 for R being Relation holds ( R is confluent iff R [*] is subcommutative ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) ) ) proofend; 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 ) proofend; 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 proofend; theorem :: REWRITE1:64 for R being Relation for Q being complete Relation st R,Q are_equivalent holds Q is Completion of R proofend; 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) ) proofend;