rewrite1.miz



    begin

    definition

      let p,q be FinSequence;

      :: REWRITE1:def1

      func p $^ q -> FinSequence means

      : Def1: it = (p ^ q) if p = {} or q = {}

      otherwise ex i be Nat, r be FinSequence st ( len p) = (i + 1) & r = (p | ( Seg i)) & it = (r ^ q);

      existence

      proof

        thus p = {} or q = {} implies ex r be FinSequence st r = (p ^ q);

        assume that

         A1: p <> {} and q <> {} ;

        ( len p) >= ( 0 + 1) by A1, NAT_1: 13;

        then

        consider i be Nat such that

         A2: ( len p) = (1 + i) by NAT_1: 10;

        reconsider i as Nat;

        reconsider r = (p | ( Seg i)) as FinSequence by FINSEQ_1: 15;

        take (r ^ q), i, r;

        thus thesis by A2;

      end;

      uniqueness ;

      consistency ;

    end

     Lm1:

    now

      let p be FinSequence, x be Nat;

      assume x in ( dom p);

      then

       A1: x in ( Seg ( len p)) by FINSEQ_1:def 3;

      hence x <= ( len p) & x >= ( 0 + 1) by FINSEQ_1: 1;

      thus x > 0 by A1, FINSEQ_1: 1;

    end;

     Lm2:

    now

      let p be FinSequence, x be Nat;

      assume (x + 1) in ( dom p);

      then (x + 1) <= ( len p) by Lm1;

      hence x < ( len p) by NAT_1: 13;

    end;

     Lm3:

    now

      let p be FinSequence, x be Nat;

      assume that

       A1: x <= ( len p) or x < ( len p) and

       A2: x >= 1 or x > 0 ;

      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;

    end;

     Lm4:

    now

      let p be FinSequence, x be Nat;

      assume x < ( len p);

      then (x + 1) <= ( len p) by NAT_1: 13;

      hence (x + 1) in ( dom p) by Lm3;

    end;

    reserve p,q,r for FinSequence,

x,y for object;

    theorem :: REWRITE1:1

    ( {} $^ p) = p & (p $^ {} ) = p

    proof

      ( {} ^ p) = p & (p ^ {} ) = p by FINSEQ_1: 34;

      hence thesis by Def1;

    end;

    theorem :: REWRITE1:2

    

     Th2: q <> {} implies ((p ^ <*x*>) $^ q) = (p ^ q)

    proof

      ( len <*x*>) = 1 by FINSEQ_1: 40;

      then

       A1: ( len (p ^ <*x*>)) = (( len p) + 1) by FINSEQ_1: 22;

      assume q <> {} ;

      then

      consider i be Nat, r be 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 be FinSequence st (p ^ <*x*>) = (r ^ s) by A3, FINSEQ_1: 80;

      then

      consider t be 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 thesis by A4, A6, FINSEQ_1: 34;

    end;

    theorem :: REWRITE1:3

    ((p ^ <*x*>) $^ ( <*y*> ^ q)) = ((p ^ <*y*>) ^ q)

    proof

      ((p ^ <*y*>) ^ q) = (p ^ ( <*y*> ^ q)) by FINSEQ_1: 32;

      hence thesis by Th2;

    end;

    theorem :: REWRITE1:4

    q <> {} implies ( <*x*> $^ q) = q

    proof

      ( {} ^ <*x*>) = <*x*> & ( {} ^ q) = q by FINSEQ_1: 34;

      hence thesis by Th2;

    end;

    theorem :: REWRITE1:5

    p <> {} implies ex x, q st p = ( <*x*> ^ q) & ( len p) = (( len q) + 1)

    proof

      defpred P[ Nat] means for p st p <> {} & ( len p) = $1 holds ex x, q st p = ( <*x*> ^ q) & ( len p) = (( len q) + 1);

      assume

       A1: p <> {} ;

      now

        let i be Nat;

        assume

         A2: for p st p <> {} & ( len p) = i holds ex x, q st p = ( <*x*> ^ q) & ( len p) = (( len q) + 1);

        let p;

        assume that

         A3: p <> {} and

         A4: ( len p) = (i + 1);

        consider q be FinSequence, y be object 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;

        per cases ;

          suppose

           A8: q = {} ;

          

          then p = <*y*> by A5, FINSEQ_1: 34

          .= ( <*y*> ^ {} ) by FINSEQ_1: 34;

          hence ex x, q st p = ( <*x*> ^ q) & ( len p) = (( len q) + 1) by A7, A6, A8;

        end;

          suppose q <> {} ;

          then

          consider x, r 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, q st p = ( <*x*> ^ q) & ( len p) = (( len q) + 1) by A7, A6, A10, A11;

        end;

      end;

      then

       A12: for i be Nat st P[i] holds P[(i + 1)];

      

       A13: P[ 0 ];

      for i be Nat holds P[i] from NAT_1:sch 2( A13, A12);

      hence thesis by A1;

    end;

    scheme :: REWRITE1:sch1

    PathCatenation { P[ set, set], p,q() -> FinSequence } :

for i be Nat st i in ( dom (p() $^ q())) & (i + 1) in ( dom (p() $^ q())) holds for x,y be set st x = ((p() $^ q()) . i) & y = ((p() $^ q()) . (i + 1)) holds P[x, y]

      provided

       A1: for i be Nat st i in ( dom p()) & (i + 1) in ( dom p()) holds P[(p() . i), (p() . (i + 1))]

       and

       A2: for i be Nat st i in ( dom q()) & (i + 1) in ( dom q()) holds P[(q() . i), (q() . (i + 1))]

       and

       A3: ( len p()) > 0 & ( len q()) > 0 & (p() . ( len p())) = (q() . 1);

      p() <> {} by A3;

      then

      consider r be FinSequence, a be object such that

       A4: p() = (r ^ <*a*>) by FINSEQ_1: 46;

      q() <> {} by A3;

      then

       A5: (p() $^ q()) = (r ^ q()) by A4, Th2;

      ( 0 + 1) <= ( len q()) by A3, NAT_1: 13;

      then

       A6: 1 in ( Seg ( len q())) by FINSEQ_1: 1;

      

       A7: ( Seg ( len q())) = ( dom q()) by FINSEQ_1:def 3;

      let i be Nat;

      assume that

       A8: i in ( dom (p() $^ q())) and

       A9: (i + 1) in ( dom (p() $^ q()));

      

       A10: i >= ( 0 + 1) by A8, Lm1;

      let x,y be set;

      

       A11: (i + 1) >= 1 by NAT_1: 11;

      

       A12: ( len p()) = (( len r) + ( len <*a*>)) by A4, FINSEQ_1: 22

      .= (( len r) + 1) by FINSEQ_1: 40;

      assume that

       A13: x = ((p() $^ q()) . i) and

       A14: y = ((p() $^ q()) . (i + 1));

      per cases ;

        suppose

         A15: i < ( len p());

        then i in ( dom p()) & (i + 1) in ( dom p()) by A10, Lm3, Lm4;

        then

         A16: P[(p() . i), (p() . (i + 1))] by A1;

         A17:

        now

          assume (i + 1) <= ( len r);

          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)) = (p() . (i + 1)) by A14, A4, A5, FINSEQ_1:def 7;

        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) = (p() . i) by A13, A4, A5, FINSEQ_1:def 7;

        i = ( len r) or i < ( len r) by A18, XXREAL_0: 1;

        hence thesis by A3, A6, A7, A14, A5, A12, A16, A19, A17, FINSEQ_1:def 7, NAT_1: 13;

      end;

        suppose i >= ( len p());

        then

        consider k be Nat such that

         A20: i = (( len p()) + k) by NAT_1: 10;

        reconsider k as Nat;

        

         A21: i = (( len r) + (1 + k)) by A12, A20;

        ( len (p() $^ q())) = (( len r) + ( len q())) by A5, FINSEQ_1: 22;

        then

         A22: (k + 1) < ( len q()) by A9, A21, Lm2, XREAL_1: 7;

        then

         A23: ((k + 1) + 1) in ( dom q()) by Lm4;

        

         A24: (k + 1) in ( dom q()) by A22, Lm3;

        then

         A25: x = (q() . (k + 1)) by A13, A5, A21, FINSEQ_1:def 7;

        ((( len r) + (1 + k)) + 1) = (( len r) + ((k + 1) + 1));

        then y = (q() . ((k + 1) + 1)) by A14, A5, A12, A20, A23, FINSEQ_1:def 7;

        hence thesis by A2, A24, A23, A25;

      end;

    end;

    definition

      let R be Relation;

      :: REWRITE1:def2

      mode RedSequence of R -> FinSequence means

      : Def2: ( len it ) > 0 & for i be Nat st i in ( dom it ) & (i + 1) in ( dom it ) holds [(it . i), (it . (i + 1))] in R;

      existence

      proof

        take p = <* {} *>;

        thus ( len p) > 0 ;

        let i be Nat;

        assume that

         A1: i in ( dom p) and

         A2: (i + 1) in ( dom p);

        

         A3: ( dom p) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then i = 1 by A1, TARSKI:def 1;

        hence thesis by A3, A2, TARSKI:def 1;

      end;

    end

    registration

      let R be Relation;

      cluster -> non empty for RedSequence of R;

      coherence by Def2, CARD_1: 27;

    end

    theorem :: REWRITE1:6

    

     Th6: for R be Relation, a be object holds <*a*> is RedSequence of R

    proof

      let R be Relation, a be object;

      set p = <*a*>;

      thus ( len p) > 0 ;

      let i be Nat;

      assume that

       A1: i in ( dom p) and

       A2: (i + 1) in ( dom p);

      

       A3: ( dom p) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then i = 1 by A1, TARSKI:def 1;

      hence thesis by A3, A2, TARSKI:def 1;

    end;

    theorem :: REWRITE1:7

    

     Th7: for R be Relation, a,b be object st [a, b] in R holds <*a, b*> is RedSequence of R

    proof

      let R be Relation, a,b be object;

      assume

       A1: [a, b] in R;

      set p = <*a, b*>;

      thus ( len p) > 0 ;

      let i be Nat;

      assume that

       A2: i in ( dom p) and

       A3: (i + 1) in ( dom p);

      ( len p) = (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 (p . 1) = a & i = 1 by A4, FINSEQ_1: 44, XXREAL_0: 1;

      hence thesis by A1, FINSEQ_1: 44;

    end;

    theorem :: REWRITE1:8

    

     Th8: for R be Relation, p,q be RedSequence of R st (p . ( len p)) = (q . 1) holds (p $^ q) is RedSequence of R

    proof

      let R be Relation, p,q be RedSequence of R;

      defpred P[ set, set] means [$1, $2] in R;

      set r = (p $^ q);

      consider p1 be FinSequence, x be object such that

       A1: p = (p1 ^ <*x*>) by FINSEQ_1: 46;

      assume (p . ( len p)) = (q . 1);

      then

       A2: ( len p) > 0 & ( len q) > 0 & (p . ( len p)) = (q . 1);

      r = (p1 ^ q) by A1, Th2;

      hence ( len r) > 0 ;

      

       A3: for i be Nat st i in ( dom q) & (i + 1) in ( dom q) holds P[(q . i), (q . (i + 1))] by Def2;

      

       A4: for i be Nat st i in ( dom p) & (i + 1) in ( dom p) holds P[(p . i), (p . (i + 1))] by Def2;

      for i be Nat st i in ( dom (p $^ q)) & (i + 1) in ( dom (p $^ q)) holds for x,y be set st x = ((p $^ q) . i) & y = ((p $^ q) . (i + 1)) holds P[x, y] from PathCatenation( A4, A3, A2);

      hence thesis;

    end;

    theorem :: REWRITE1:9

    

     Th9: for R be Relation, p be RedSequence of R holds ( Rev p) is RedSequence of (R ~ )

    proof

      let R be Relation, p be RedSequence of R;

      ( len p) > 0 ;

      hence ( len ( Rev p)) > 0 by FINSEQ_5:def 3;

      let i be Nat;

      assume that

       A1: i in ( dom ( Rev p)) and

       A2: (i + 1) in ( dom ( Rev p));

      

       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 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 thesis by A7, RELAT_1:def 7;

    end;

    theorem :: REWRITE1:10

    

     Th10: for R,Q be Relation st R c= Q holds for p be RedSequence of R holds p is RedSequence of Q

    proof

      let R,Q be Relation such that

       A1: R c= Q;

      let p be RedSequence of R;

      thus ( len p) > 0 ;

      let i be Nat;

      assume i in ( dom p) & (i + 1) in ( dom p);

      then [(p . i), (p . (i + 1))] in R by Def2;

      hence thesis by A1;

    end;

    begin

    definition

      let R be Relation;

      let a,b be object;

      :: REWRITE1:def3

      pred R reduces a,b means ex p be RedSequence of R st (p . 1) = a & (p . ( len p)) = b;

    end

    definition

      let R be Relation;

      let a,b be object;

      :: REWRITE1:def4

      pred a,b are_convertible_wrt R means (R \/ (R ~ )) reduces (a,b);

    end

    theorem :: REWRITE1:11

    

     Th11: for R be Relation, a,b be object holds R reduces (a,b) iff ex p be FinSequence st ( len p) > 0 & (p . 1) = a & (p . ( len p)) = b & for i be Nat st i in ( dom p) & (i + 1) in ( dom p) holds [(p . i), (p . (i + 1))] in R

    proof

      let R be Relation, a,b be object;

      thus R reduces (a,b) implies ex p be FinSequence st ( len p) > 0 & (p . 1) = a & (p . ( len p)) = b & for i be Nat st i in ( dom p) & (i + 1) in ( dom p) holds [(p . i), (p . (i + 1))] in R

      proof

        given p be RedSequence of R such that

         A1: (p . 1) = a & (p . ( len p)) = b;

        take p;

        thus thesis by A1, Def2;

      end;

      given p be FinSequence such that

       A2: ( len p) > 0 and

       A3: (p . 1) = a & (p . ( len p)) = b and

       A4: for i be Nat st i in ( dom p) & (i + 1) in ( dom p) holds [(p . i), (p . (i + 1))] in R;

      reconsider p as RedSequence of R by A2, A4, Def2;

      take p;

      thus thesis by A3;

    end;

    theorem :: REWRITE1:12

    

     Th12: for R be Relation, a be object holds R reduces (a,a)

    proof

      let R be Relation;

      let a be object;

      reconsider p = <*a*> as RedSequence of R by Th6;

      take p;

      ( len p) = 1 by FINSEQ_1: 40;

      hence thesis by FINSEQ_1: 40;

    end;

    theorem :: REWRITE1:13

    

     Th13: for a,b be object st {} reduces (a,b) holds a = b

    proof

      let a,b be object;

      given p be RedSequence of {} such that

       A1: (p . 1) = a & (p . ( len p)) = b;

       A2:

      now

        assume ( len p) > 1;

        then 1 in ( dom p) & (1 + 1) in ( dom p) by Lm3, Lm4;

        hence contradiction by Def2;

      end;

      ( len p) >= ( 0 + 1) by NAT_1: 13;

      hence thesis by A1, A2, XXREAL_0: 1;

    end;

    theorem :: REWRITE1:14

    

     Th14: for R be Relation, a,b be object st R reduces (a,b) & not a in ( field R) holds a = b

    proof

      let R be Relation, a,b be object;

      given p be RedSequence of R such that

       A1: (p . 1) = a and

       A2: (p . ( len p)) = b;

      assume

       A3: not a in ( field R);

       A4:

      now

        assume ( len p) > 1;

        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;

      end;

      ( len p) >= ( 0 + 1) by NAT_1: 13;

      hence thesis by A1, A2, A4, XXREAL_0: 1;

    end;

    theorem :: REWRITE1:15

    

     Th15: for R be Relation, a,b be object st [a, b] in R holds R reduces (a,b)

    proof

      let R be Relation, a,b be object;

      assume [a, b] in R;

      then

      reconsider p = <*a, b*> as RedSequence of R by Th7;

      take p;

      ( len p) = 2 by FINSEQ_1: 44;

      hence thesis by FINSEQ_1: 44;

    end;

    theorem :: REWRITE1:16

    

     Th16: for R be Relation, a,b,c be object st R reduces (a,b) & R reduces (b,c) holds R reduces (a,c)

    proof

      let R be Relation, a,b,c be object;

      given p be RedSequence of R such that

       A1: (p . 1) = a and

       A2: (p . ( len p)) = b;

      given q be RedSequence of R such that

       A3: (q . 1) = b and

       A4: (q . ( len q)) = c;

      reconsider r = (p $^ q) as RedSequence of R by A2, A3, Th8;

      take r;

      consider p1 be FinSequence, x be object 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;

      ( len r) = (( len p1) + ( len q)) by A7, FINSEQ_1: 22;

      hence thesis by A4, A7, A6, FINSEQ_1:def 7;

    end;

    theorem :: REWRITE1:17

    

     Th17: for R be Relation, p be RedSequence of R, i,j be Nat st i in ( dom p) & j in ( dom p) & i <= j holds R reduces ((p . i),(p . j))

    proof

      let R be Relation, p be RedSequence of R, i,j be Nat;

      defpred Q[ 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;

      consider k be Nat such that

       A4: j = (i + k) by A3, NAT_1: 10;

      now

        

         A5: i >= 1 by A1, Lm1;

        let j be Nat such that

         A6: (i + j) in ( dom p) implies R reduces ((p . i),(p . (i + j))) and

         A7: (i + (j + 1)) in ( dom p);

        

         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;

      end;

      then

       A10: for k be Nat st Q[k] holds Q[(k + 1)];

      

       A11: Q[ 0 ] by Th12;

      

       A12: for j be Nat holds Q[j] from NAT_1:sch 2( A11, A10);

      thus thesis by A2, A12, A4;

    end;

    theorem :: REWRITE1:18

    

     Th18: for R be Relation, a,b be object st R reduces (a,b) & a <> b holds a in ( field R) & b in ( field R)

    proof

      let R be Relation, a,b be object;

      given p be RedSequence of R such that

       A1: a = (p . 1) and

       A2: b = (p . ( len p));

      

       A3: ( len p) >= ( 0 + 1) by NAT_1: 13;

      assume a <> b;

      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;

      defpred P[ Nat] means $1 in ( dom p) implies (p . $1) in ( field R);

      

       A6: ( len p) in ( dom p) by FINSEQ_5: 6;

      now

        let i be Nat such that i in ( dom p) implies (p . i) in ( field R) and

         A7: (i + 1) in ( dom p);

        

         A8: i < ( len p) by A7, Lm2;

        per cases ;

          suppose i = 0 ;

          hence (p . (i + 1)) in ( field R) by A1, A5, RELAT_1: 15;

        end;

          suppose i > 0 ;

          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;

        end;

      end;

      then

       A9: for k be Nat st P[k] holds P[(k + 1)];

      

       A10: P[ 0 ] by Lm1;

      for i be Nat holds P[i] from NAT_1:sch 2( A10, A9);

      hence thesis by A2, A6;

    end;

    theorem :: REWRITE1:19

    for R be Relation, a,b be object st R reduces (a,b) holds a in ( field R) iff b in ( field R) by Th18;

    theorem :: REWRITE1:20

    

     Th20: for R be Relation, a,b be object holds R reduces (a,b) iff a = b or [a, b] in (R [*] )

    proof

      let R be Relation, a,b be object;

      hereby

        assume

         A1: R reduces (a,b);

        then

        consider p be RedSequence of R such that

         A2: a = (p . 1) & b = (p . ( len p));

         A3:

        now

          let i be Nat;

          assume i >= 1 & i < ( len p);

          then i in ( dom p) & (i + 1) in ( dom p) by Lm3, Lm4;

          hence [(p . i), (p . (i + 1))] in R by Def2;

        end;

        assume a <> b;

        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;

      end;

      assume that

       A5: a = b or [a, b] in (R [*] ) and

       A6: not R reduces (a,b);

      consider p be FinSequence such that

       A7: ( len p) >= 1 and

       A8: (p . 1) = a & (p . ( len p)) = b and

       A9: for i be 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;

        let i be Nat;

        assume that

         A10: i in ( dom p) and

         A11: (i + 1) in ( dom p);

        i >= 1 by A10, Lm1;

        hence thesis by A9, A11, Lm2;

      end;

      hence contradiction by A6, A8;

    end;

    theorem :: REWRITE1:21

    

     Th21: for R be Relation, a,b be object holds R reduces (a,b) iff (R [*] ) reduces (a,b)

    proof

      let R be Relation, a,b be object;

      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;

      given p be RedSequence of (R [*] ) such that

       A1: a = (p . 1) and

       A2: b = (p . ( len p));

      defpred P[ Nat] means $1 in ( dom p) implies R reduces (a,(p . $1));

      now

        let i be Nat such that

         A3: i in ( dom p) implies R reduces (a,(p . i)) and

         A4: (i + 1) in ( dom p);

        

         A5: i < ( len p) by A4, Lm2;

        per cases ;

          suppose i = 0 ;

          hence R reduces (a,(p . (i + 1))) by A1, Th12;

        end;

          suppose

           A6: i > 0 ;

          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;

        end;

      end;

      then

       A7: for k be Nat st P[k] holds P[(k + 1)];

      

       A8: ( len p) in ( dom p) by FINSEQ_5: 6;

      

       A9: P[ 0 ] by Lm1;

      for i be Nat holds P[i] from NAT_1:sch 2( A9, A7);

      hence thesis by A2, A8;

    end;

    theorem :: REWRITE1:22

    

     Th22: for R,Q be Relation st R c= Q holds for a,b be object st R reduces (a,b) holds Q reduces (a,b)

    proof

      let R,Q be Relation such that

       A1: R c= Q;

      let a,b be object;

      given p be RedSequence of R such that

       A2: (p . 1) = a & (p . ( len p)) = b;

      p is RedSequence of Q by A1, Th10;

      hence ex p be RedSequence of Q st (p . 1) = a & (p . ( len p)) = b by A2;

    end;

    theorem :: REWRITE1:23

    for R be Relation, X be set, a,b be object holds R reduces (a,b) iff (R \/ ( id X)) reduces (a,b)

    proof

      let R be Relation, X be set, a,b be object;

      thus R reduces (a,b) implies (R \/ ( id X)) reduces (a,b) by Th22, XBOOLE_1: 7;

      given p be RedSequence of (R \/ ( id X)) such that

       A1: (p . 1) = a and

       A2: (p . ( len p)) = b;

      defpred P[ Nat] means $1 in ( dom p) implies R reduces (a,(p . $1));

      now

        let i be Nat;

        assume

         A3: i in ( dom p) implies R reduces (a,(p . i));

        assume

         A4: (i + 1) in ( dom p);

        per cases ;

          suppose

           A5: i in ( dom p);

          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;

        end;

          suppose not i in ( dom p);

          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;

        end;

      end;

      then

       A6: for k be Nat st P[k] holds P[(k + 1)];

      

       A7: ( len p) in ( dom p) by Lm3;

      

       A8: P[ 0 ] by Lm1;

      for i be Nat holds P[i] from NAT_1:sch 2( A8, A6);

      hence thesis by A2, A7;

    end;

    theorem :: REWRITE1:24

    

     Th24: for R be Relation, a,b be object st R reduces (a,b) holds (R ~ ) reduces (b,a)

    proof

      let R be Relation, a,b be object;

      given p be RedSequence of R such that

       A1: (p . 1) = a and

       A2: (p . ( len p)) = b;

      reconsider q = ( Rev p) as RedSequence of (R ~ ) by Th9;

      take q;

      1 in ( dom q) by FINSEQ_5: 6;

      

      hence (q . 1) = (p . ((( len p) - 1) + 1)) by FINSEQ_5:def 3

      .= b by A2;

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

    end;

    

     Lm5: for R be Relation, a,b be object st (a,b) are_convertible_wrt R holds (b,a) are_convertible_wrt R

    proof

      let R be Relation;

      let a,b be object;

      assume (R \/ (R ~ )) reduces (a,b);

      then ((R \/ (R ~ )) ~ ) reduces (b,a) by Th24;

      then ((R ~ ) \/ ((R ~ ) ~ )) reduces (b,a) by RELAT_1: 23;

      hence (R \/ (R ~ )) reduces (b,a);

    end;

    theorem :: REWRITE1:25

    

     Th25: for R be Relation, a,b be object st R reduces (a,b) holds (a,b) are_convertible_wrt R & (b,a) are_convertible_wrt R

    proof

      let R be Relation, a,b be object;

      given p be RedSequence of R such that

       A1: (p . 1) = a & (p . ( len p)) = b;

      p is RedSequence of (R \/ (R ~ ))

      proof

        thus ( len p) > 0 ;

        let i be Nat;

        assume i in ( dom p) & (i + 1) in ( dom p);

        then [(p . i), (p . (i + 1))] in R by Def2;

        hence thesis by XBOOLE_0:def 3;

      end;

      then (R \/ (R ~ )) reduces (a,b) by A1;

      hence (a,b) are_convertible_wrt R;

      hence thesis by Lm5;

    end;

    theorem :: REWRITE1:26

    

     Th26: for R be Relation, a be object holds (a,a) are_convertible_wrt R by Th12;

    theorem :: REWRITE1:27

    

     Th27: for a,b be object st (a,b) are_convertible_wrt {} holds a = b by Th13;

    theorem :: REWRITE1:28

    for R be Relation, a,b be object st (a,b) are_convertible_wrt R & not a in ( field R) holds a = b

    proof

      let R be Relation;

      let a,b be object;

      

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

      hence thesis by A1, Th14;

    end;

    theorem :: REWRITE1:29

    

     Th29: for R be Relation, a,b be object st [a, b] in R holds (a,b) are_convertible_wrt R

    proof

      let R be Relation, a,b be object;

      assume [a, b] in R;

      then R reduces (a,b) by Th15;

      hence thesis by Th25;

    end;

    theorem :: REWRITE1:30

    

     Th30: for R be Relation, a,b,c be object st (a,b) are_convertible_wrt R & (b,c) are_convertible_wrt R holds (a,c) are_convertible_wrt R by Th16;

    theorem :: REWRITE1:31

    for R be Relation, a,b be object st (a,b) are_convertible_wrt R holds (b,a) are_convertible_wrt R by Lm5;

    theorem :: REWRITE1:32

    

     Th32: for R be Relation, a,b be object st (a,b) are_convertible_wrt R & a <> b holds a in ( field R) & b in ( field R)

    proof

      let R be Relation, a,b be object;

      

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

      hence thesis by A1, Th18;

    end;

    definition

      let R be Relation;

      let a be object;

      :: REWRITE1:def5

      pred a is_a_normal_form_wrt R means not ex b be object st [a, b] in R;

    end

    theorem :: REWRITE1:33

    

     Th33: for R be Relation, a,b be object st a is_a_normal_form_wrt R & R reduces (a,b) holds a = b

    proof

      let R be Relation;

      let a,b be object;

      assume

       A1: not ex b be object st [a, b] in R;

      assume R reduces (a,b);

      then

      consider p be FinSequence such that

       A2: ( len p) > 0 and

       A3: (p . 1) = a and

       A4: (p . ( len p)) = b and

       A5: for i be Nat st i in ( dom p) & (i + 1) in ( dom p) holds [(p . i), (p . (i + 1))] in R by Th11;

       A6:

      now

        assume ( len p) > 1;

        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;

      end;

      ( len p) >= ( 0 + 1) by A2, NAT_1: 13;

      hence thesis by A3, A4, A6, XXREAL_0: 1;

    end;

    theorem :: REWRITE1:34

    

     Th34: for R be Relation, a be object st not a in ( field R) holds a is_a_normal_form_wrt R by RELAT_1: 15;

    definition

      let R be Relation;

      let a,b be object;

      :: REWRITE1:def6

      pred b is_a_normal_form_of a,R means b is_a_normal_form_wrt R & R reduces (a,b);

      :: REWRITE1:def7

      pred a,b are_convergent_wrt R means

      : Def7: ex c be object st R reduces (a,c) & R reduces (b,c);

      :: REWRITE1:def8

      pred a,b are_divergent_wrt R means ex c be object st R reduces (c,a) & R reduces (c,b);

      :: REWRITE1:def9

      pred a,b are_convergent<=1_wrt R means ex c be object st ( [a, c] in R or a = c) & ( [b, c] in R or b = c);

      :: REWRITE1:def10

      pred a,b are_divergent<=1_wrt R means ex c be object st ( [c, a] in R or a = c) & ( [c, b] in R or b = c);

    end

    theorem :: REWRITE1:35

    

     Th35: for R be Relation, a be object st not a in ( field R) holds a is_a_normal_form_of (a,R) by Th12, Th34;

    theorem :: REWRITE1:36

    

     Th36: for R be Relation, a,b be object 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, a,b be object;

      R reduces (a,a) & R reduces (b,b) by Th12;

      hence thesis;

    end;

    theorem :: REWRITE1:37

    

     Th37: for R be Relation, a,b be object 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, a,b be object;

      assume

       A1: (a,b) are_convergent_wrt R or (a,b) are_divergent_wrt R;

      per cases by A1;

        suppose (a,b) are_convergent_wrt R;

        then

        consider c be object such that

         A2: R reduces (a,c) & R reduces (b,c);

        (a,c) are_convertible_wrt R & (c,b) are_convertible_wrt R by A2, Th25;

        hence thesis by Th30;

      end;

        suppose (a,b) are_divergent_wrt R;

        then

        consider c be object such that

         A3: R reduces (c,a) & R reduces (c,b);

        (c,b) are_convertible_wrt R & (a,c) are_convertible_wrt R by A3, Th25;

        hence thesis by Th30;

      end;

    end;

    theorem :: REWRITE1:38

    

     Th38: for R be Relation, a be object holds (a,a) are_convergent_wrt R & (a,a) are_divergent_wrt R by Th12;

    theorem :: REWRITE1:39

    

     Th39: for a,b be object st (a,b) are_convergent_wrt {} or (a,b) are_divergent_wrt {} holds a = b

    proof

      let a,b be object;

       A1:

      now

        assume (a,b) are_convergent_wrt {} ;

        then

        consider c be object such that

         A2: {} reduces (a,c) and

         A3: {} reduces (b,c);

        a = c by A2, Th13;

        hence thesis by A3, Th13;

      end;

       A4:

      now

        assume (a,b) are_divergent_wrt {} ;

        then

        consider c be object such that

         A5: {} reduces (c,a) and

         A6: {} reduces (c,b);

        a = c by A5, Th13;

        hence thesis by A6, Th13;

      end;

      assume (a,b) are_convergent_wrt {} or (a,b) are_divergent_wrt {} ;

      hence thesis by A1, A4;

    end;

    theorem :: REWRITE1:40

    for R be Relation, a,b be object st (a,b) are_convergent_wrt R holds (b,a) are_convergent_wrt R;

    theorem :: REWRITE1:41

    for R be Relation, a,b be object st (a,b) are_divergent_wrt R holds (b,a) are_divergent_wrt R;

    theorem :: REWRITE1:42

    

     Th42: for R be Relation, a,b,c be object 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, a,b,c be object;

      assume

       A1: R reduces (a,b) & (b,c) are_convergent_wrt R or (a,b) are_convergent_wrt R & R reduces (c,b);

      per cases by A1;

        suppose

         A2: R reduces (a,b) & (b,c) are_convergent_wrt R;

        then

        consider d be object such that

         A3: R reduces (b,d) and

         A4: R reduces (c,d);

        R reduces (a,d) by A2, A3, Th16;

        hence thesis by A4;

      end;

        suppose

         A5: (a,b) are_convergent_wrt R & R reduces (c,b);

        then

        consider d be object such that

         A6: R reduces (a,d) and

         A7: R reduces (b,d);

        R reduces (c,d) by A5, A7, Th16;

        hence thesis by A6;

      end;

    end;

    theorem :: REWRITE1:43

    for R be Relation, a,b,c be object 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, a,b,c be object;

      assume

       A1: R reduces (b,a) & (b,c) are_divergent_wrt R or (a,b) are_divergent_wrt R & R reduces (b,c);

      per cases by A1;

        suppose

         A2: R reduces (b,a) & (b,c) are_divergent_wrt R;

        then

        consider d be object such that

         A3: R reduces (d,b) and

         A4: R reduces (d,c);

        R reduces (d,a) by A2, A3, Th16;

        hence thesis by A4;

      end;

        suppose

         A5: (a,b) are_divergent_wrt R & R reduces (b,c);

        then

        consider d be object such that

         A6: R reduces (d,a) and

         A7: R reduces (d,b);

        R reduces (d,c) by A5, A7, Th16;

        hence thesis by A6;

      end;

    end;

    theorem :: REWRITE1:44

    

     Th44: for R be Relation, a,b be object st (a,b) are_convergent<=1_wrt R holds (a,b) are_convergent_wrt R

    proof

      let R be Relation, a,b be object;

      given c be object such that

       A1: ( [a, c] in R or a = c) & ( [b, c] in R or b = c);

      take c;

      thus thesis by A1, Th12, Th15;

    end;

    theorem :: REWRITE1:45

    

     Th45: for R be Relation, a,b be object st (a,b) are_divergent<=1_wrt R holds (a,b) are_divergent_wrt R

    proof

      let R be Relation, a,b be object;

      given c be object such that

       A1: ( [c, a] in R or a = c) & ( [c, b] in R or b = c);

      take c;

      thus thesis by A1, Th12, Th15;

    end;

    definition

      let R be Relation;

      let a be object;

      :: REWRITE1:def11

      pred a has_a_normal_form_wrt R means ex b be object st b is_a_normal_form_of (a,R);

    end

    theorem :: REWRITE1:46

    

     Th46: for R be Relation, a be object st not a in ( field R) holds a has_a_normal_form_wrt R by Th35;

    definition

      let R be Relation, a be object;

      assume that

       A1: a has_a_normal_form_wrt R and

       A2: for b,c be object st b is_a_normal_form_of (a,R) & c is_a_normal_form_of (a,R) holds b = c;

      :: REWRITE1:def12

      func nf (a,R) -> set means

      : Def12: it is_a_normal_form_of (a,R);

      existence

      proof

        consider x such that

         A3: x is_a_normal_form_of (a,R) by A1;

        x is set by TARSKI: 1;

        hence thesis by A3;

      end;

      uniqueness by A2;

    end

    begin

    definition

      let R be Relation;

      :: REWRITE1:def13

      attr R is co-well_founded means (R ~ ) is well_founded;

      :: REWRITE1:def14

      attr R is weakly-normalizing means

      : Def14: for a be object st a in ( field R) holds a has_a_normal_form_wrt R;

      :: REWRITE1:def15

      attr R is strongly-normalizing means for f be ManySortedSet of NAT holds ex i be Nat st not [(f . i), (f . (i + 1))] in R;

    end

    definition

      let R be Relation;

      :: original: co-well_founded

      redefine

      :: REWRITE1:def16

      attr R is co-well_founded means

      : Def16: for Y be set st Y c= ( field R) & Y <> {} holds ex a be object st a in Y & for b be object st b in Y & a <> b holds not [a, b] in R;

      compatibility

      proof

        

         A1: ( field R) = ( field (R ~ )) by RELAT_1: 21;

        hereby

          assume R is co-well_founded;

          then

           A2: (R ~ ) is well_founded;

          let Y be set;

          assume Y c= ( field R) & Y <> {} ;

          then

          consider a be object such that

           A3: a in Y and

           A4: ((R ~ ) -Seg a) misses Y by A1, A2;

          take a;

          thus a in Y by A3;

          let b be object;

          assume b in Y;

          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;

        end;

        hereby

          assume

           A5: for Y be set st Y c= ( field R) & Y <> {} holds ex a be object st a in Y & for b be object st b in Y & a <> b holds not [a, b] in R;

          (R ~ ) is well_founded

          proof

            let Y be set;

            assume Y c= ( field (R ~ )) & Y <> {} ;

            then

            consider a be object such that

             A6: a in Y and

             A7: for b be object st b in Y & a <> b holds not [a, b] in R by A1, A5;

            take a;

            thus a in Y by A6;

            now

              assume (((R ~ ) -Seg a) /\ Y) is non empty;

              then

              reconsider A = (((R ~ ) -Seg a) /\ Y) as non empty set;

              set x = the Element of A;

              

               A8: x in ((R ~ ) -Seg a) by XBOOLE_0:def 4;

              then x in Y & x <> a by WELLORD1: 1, XBOOLE_0:def 4;

              then

               A9: not [a, x] in R by A7;

               [x, a] in (R ~ ) by A8, WELLORD1: 1;

              hence contradiction by A9, RELAT_1:def 7;

            end;

            hence thesis by XBOOLE_0:def 7;

          end;

          hence R is co-well_founded;

        end;

      end;

    end

    scheme :: REWRITE1:sch2

    coNoetherianInduction { R() -> Relation , P[ object] } :

for a be object st a in ( field R()) holds P[a]

      provided

       A1: R() is co-well_founded

       and

       A2: for a be object st for b be object st [a, b] in R() & a <> b holds P[b] holds P[a];

      given a be object such that

       A3: a in ( field R()) and

       A4: not P[a];

      reconsider X = ( field R()) as non empty set by A3;

      reconsider a as Element of X by A3;

      set Y = { x where x be Element of X : not P[x] };

      

       A5: a in Y by A4;

      Y c= ( field R())

      proof

        let y be object;

        assume y in Y;

        then ex x be Element of X st y = x & not P[x];

        hence thesis;

      end;

      then

      consider a be object such that

       A6: a in Y and

       A7: for b be object st b in Y & a <> b holds not [a, b] in R() by A1, A5;

       A8:

      now

        let b be object;

        assume that

         A9: [a, b] in R() & a <> b and

         A10: not P[b];

        ( not b in Y) & b in X by A7, A9, RELAT_1: 15;

        hence contradiction by A10;

      end;

      ex x be Element of X st a = x & not P[x] by A6;

      hence thesis by A2, A8;

    end;

    registration

      cluster strongly-normalizing -> irreflexive co-well_founded for Relation;

      coherence

      proof

        defpred Q[ object] means not contradiction;

        let R be Relation such that

         A1: for f be ManySortedSet of NAT holds ex i be Nat st not [(f . i), (f . (i + 1))] in R;

        thus R is irreflexive

        proof

          given x be object such that x in ( field R) and

           A2: [x, x] in R;

          ( 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 be Nat such that

           A3: not [(f . i), (f . (i + 1))] in R by A1;

          i in NAT by ORDINAL1:def 12;

          then (f . i) = x by FUNCOP_1: 7;

          hence contradiction by A2, A3, FUNCOP_1: 7;

        end;

        defpred P[ object, object] means [$1, $2] in R;

        let Y be set;

        assume that Y c= ( field R) and

         A4: Y <> {} and

         A5: for a be object st a in Y holds ex b be object st b in Y & a <> b & [a, b] in R;

        reconsider Y as non empty set by A4;

        now

          let x be set;

          assume x in Y;

          then ex b be object st b in Y & x <> b & [x, b] in R by A5;

          hence ex y be object st y in Y & [x, y] in R;

        end;

        then

         A6: for x be object st x in Y & Q[x] holds ex y be object st y in Y & P[x, y] & Q[y];

        set y = the Element of Y;

        

         A7: y in Y & Q[y];

        consider f be Function such that

         A8: ( dom f) = NAT & ( rng f) c= Y & (f . 0 ) = y and

         A9: for k be Nat holds P[(f . k), (f . (k + 1))] & Q[(f . k)] from TREES_2:sch 5( A7, A6);

        f is ManySortedSet of NAT by A8, PARTFUN1:def 2, RELAT_1:def 18;

        hence thesis by A1, A9;

      end;

      cluster co-well_founded irreflexive -> strongly-normalizing for Relation;

      coherence

      proof

        let R be Relation such that

         A10: for Y be set st Y c= ( field R) & Y <> {} holds ex a be object st a in Y & for b be object st b in Y & a <> b holds not [a, b] in R;

        assume

         A11: for x be object st x in ( field R) holds not [x, x] in R;

        let f be ManySortedSet of NAT ;

        assume

         A12: for i be Nat holds [(f . i), (f . (i + 1))] in R;

        

         A13: ( rng f) c= ( field R)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A14: x in ( dom f) and

           A15: y = (f . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A14, PARTFUN1:def 2;

           [y, (f . (x + 1))] in R by A12, A15;

          hence thesis by RELAT_1: 15;

        end;

        

         A16: ( dom f) = NAT by PARTFUN1:def 2;

        then (f . 0 ) in ( rng f) by FUNCT_1:def 3;

        then

        consider a be object such that

         A17: a in ( rng f) and

         A18: for b be object st b in ( rng f) & a <> b holds not [a, b] in R by A10, A13;

        consider x be object such that

         A19: x in ( dom f) and

         A20: a = (f . x) by A17, FUNCT_1:def 3;

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

      end;

    end

    registration

      cluster empty -> weakly-normalizing strongly-normalizing for Relation;

      coherence by RELAT_1: 40;

    end

    theorem :: REWRITE1:47

    for Q be co-well_founded Relation, R be Relation st R c= Q holds R is co-well_founded

    proof

      let Q be co-well_founded Relation, R be Relation;

      assume

       A1: R c= Q;

      let Y be set;

      assume that

       A2: Y c= ( field R) and

       A3: Y <> {} ;

      ( field R) c= ( field Q) by A1, RELAT_1: 16;

      then Y c= ( field Q) by A2;

      then

      consider a be object such that

       A4: a in Y and

       A5: for b be object st b in Y & a <> b holds not [a, b] in Q by A3, Def16;

      take a;

      thus a in Y by A4;

      let b be object;

      assume b in Y & a <> b;

      hence thesis by A1, A5;

    end;

    registration

      cluster strongly-normalizing -> weakly-normalizing for Relation;

      coherence

      proof

        let R be Relation such that

         A1: R is strongly-normalizing;

        let a be object;

        assume

         A2: a in ( field R);

        then

        reconsider X = ( field R) as non empty set;

        set Y = { x where x be Element of X : R reduces (a,x) };

        

         A3: Y c= ( field R)

        proof

          let y be object;

          assume y in Y;

          then ex x be Element of X st y = x & R reduces (a,x);

          hence thesis;

        end;

        R reduces (a,a) by Th12;

        then a in Y by A2;

        then

        consider x be object such that

         A4: x in Y and

         A5: for b be object st b in Y & x <> b holds not [x, b] in R by A1, A3, Def16;

        take x;

        

         A6: ex y be Element of X st x = y & R reduces (a,y) by A4;

        hereby

          R is_irreflexive_in ( field R) by A1, RELAT_2:def 10;

          then

           A7: not [x, x] in R by A3, A4;

          given b be object such that

           A8: [x, b] in R;

          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 Y by A9;

          hence contradiction by A5, A8, A7;

        end;

        thus thesis by A6;

      end;

    end

    begin

    definition

      let R,Q be Relation;

      :: REWRITE1:def17

      pred R commutes-weakly_with Q means for a,b,c be object st [a, b] in R & [a, c] in Q holds ex d be object st Q reduces (b,d) & R reduces (c,d);

      symmetry

      proof

        let R,Q be Relation such that

         A1: for a,b,c be object st [a, b] in R & [a, c] in Q holds ex d be object st Q reduces (b,d) & R reduces (c,d);

        let a,b,c be object;

        assume [a, b] in Q & [a, c] in R;

        then ex d be object st Q reduces (c,d) & R reduces (b,d) by A1;

        hence thesis;

      end;

      :: REWRITE1:def18

      pred R commutes_with Q means

      : Def18: for a,b,c be object st R reduces (a,b) & Q reduces (a,c) holds ex d be object st Q reduces (b,d) & R reduces (c,d);

      symmetry

      proof

        let R,Q be Relation such that

         A2: for a,b,c be object st R reduces (a,b) & Q reduces (a,c) holds ex d be object st Q reduces (b,d) & R reduces (c,d);

        let a,b,c be object;

        assume Q reduces (a,b) & R reduces (a,c);

        then ex d be object st Q reduces (c,d) & R reduces (b,d) by A2;

        hence thesis;

      end;

    end

    theorem :: REWRITE1:48

    for R,Q be Relation st R commutes_with Q holds R commutes-weakly_with Q

    proof

      let R,Q be Relation;

      assume

       A1: for a,b,c be object st R reduces (a,b) & Q reduces (a,c) holds ex d be object st Q reduces (b,d) & R reduces (c,d);

      let a,b,c be object;

      assume [a, b] in R & [a, c] in Q;

      then R reduces (a,b) & Q reduces (a,c) by Th15;

      hence thesis by A1;

    end;

    definition

      let R be Relation;

      :: REWRITE1:def19

      attr R is with_UN_property means

      : Def19: for a,b be object st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & (a,b) are_convertible_wrt R holds a = b;

      :: REWRITE1:def20

      attr R is with_NF_property means for a,b be object st a is_a_normal_form_wrt R & (a,b) are_convertible_wrt R holds R reduces (b,a);

      :: REWRITE1:def21

      attr R is subcommutative means for a,b,c be object st [a, b] in R & [a, c] in R holds (b,c) are_convergent<=1_wrt R;

      :: REWRITE1:def22

      attr R is confluent means

      : Def22: for a,b be object st (a,b) are_divergent_wrt R holds (a,b) are_convergent_wrt R;

      :: REWRITE1:def23

      attr R is with_Church-Rosser_property means

      : Def23: for a,b be object st (a,b) are_convertible_wrt R holds (a,b) are_convergent_wrt R;

      :: REWRITE1:def24

      attr R is locally-confluent means for a,b,c be object st [a, b] in R & [a, c] in R holds (b,c) are_convergent_wrt R;

    end

    theorem :: REWRITE1:49

    

     Th49: for R be Relation st R is subcommutative holds for a,b,c be object st R reduces (a,b) & [a, c] in R holds (b,c) are_convergent_wrt R

    proof

      let R be Relation;

      assume

       A1: R is subcommutative;

      let a,b,c be object;

      given p be RedSequence of R such that

       A2: (p . 1) = a and

       A3: (p . ( len p)) = b;

      defpred P[ Nat] means $1 in ( dom p) implies ex d be object st ( [(p . $1), d] in R or (p . $1) = d) & R reduces (c,d);

      assume

       A4: [a, c] in R;

      now

        let i be Nat such that

         A5: i in ( dom p) implies P[i] and

         A6: (i + 1) in ( dom p);

        per cases ;

          suppose

           A7: i = 0 ;

          R reduces (c,c) by Th12;

          hence P[(i + 1)] by A2, A4, A7;

        end;

          suppose

           A8: i > 0 ;

          

           A9: i < ( len p) by A6, Lm2;

          then

          consider d be object 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

            assume [(p . i), d] in R;

            then ((p . (i + 1)),d) are_convergent<=1_wrt R by A1, A12;

            then

            consider e be object such that

             A14: [(p . (i + 1)), e] in R or (p . (i + 1)) = e and

             A15: [d, e] in R or d = e;

            take e;

            thus [(p . (i + 1)), e] in R or (p . (i + 1)) = e by A14;

            R reduces (d,e) by A15, Th12, Th15;

            hence R reduces (c,e) by A11, Th16;

          end;

          now

            assume (p . i) = d;

            then R reduces (d,(p . (i + 1))) by A12, Th15;

            hence R reduces (c,(p . (i + 1))) by A11, Th16;

          end;

          hence P[(i + 1)] by A10, A13;

        end;

      end;

      then

       A16: for k be Nat st P[k] holds P[(k + 1)];

      

       A17: ( len p) in ( dom p) by FINSEQ_5: 6;

      

       A18: P[ 0 ] by Lm1;

      for i be Nat holds P[i] from NAT_1:sch 2( A18, A16);

      then

      consider d be object such that

       A19: ( [b, d] in R or b = d) & R reduces (c,d) by A3, A17;

      take d;

      thus thesis by A19, Th12, Th15;

    end;

    theorem :: REWRITE1:50

    for R be Relation holds R is confluent iff R commutes_with R

    proof

      let R be Relation;

      hereby

        assume

         A1: R is confluent;

        thus R commutes_with R

        proof

          let a,b,c be object;

          assume R reduces (a,b) & R reduces (a,c);

          then (b,c) are_divergent_wrt R;

          then (b,c) are_convergent_wrt R by A1;

          hence thesis;

        end;

      end;

      assume

       A2: for a,b,c be object st R reduces (a,b) & R reduces (a,c) holds ex d be object st R reduces (b,d) & R reduces (c,d);

      let a,b be object;

      assume ex c be object st R reduces (c,a) & R reduces (c,b);

      hence ex d be object st R reduces (a,d) & R reduces (b,d) by A2;

    end;

    theorem :: REWRITE1:51

    

     Th51: for R be Relation holds R is confluent iff for a,b,c be object st R reduces (a,b) & [a, c] in R holds (b,c) are_convergent_wrt R

    proof

      let R be Relation;

      hereby

        assume

         A1: R is confluent;

        let a,b,c be object;

        assume that

         A2: R reduces (a,b) and

         A3: [a, c] in R;

        R reduces (a,c) by A3, Th15;

        then (b,c) are_divergent_wrt R by A2;

        hence (b,c) are_convergent_wrt R by A1;

      end;

      assume

       A4: for a,b,c be object st R reduces (a,b) & [a, c] in R holds (b,c) are_convergent_wrt R;

      let b,c be object;

      given a be object such that

       A5: R reduces (a,b) and

       A6: R reduces (a,c);

      consider p be RedSequence of R such that

       A7: (p . 1) = a and

       A8: (p . ( len p)) = b by A5;

      consider q be RedSequence of R such that

       A9: (q . 1) = a and

       A10: (q . ( len q)) = c by A6;

      defpred P[ Nat, Nat] means ((p . $1),(q . $2)) are_convergent_wrt R;

      defpred Q[ Nat] means $1 in ( dom p) implies for j be Nat st j in ( dom q) holds P[$1, j];

      

       A11: for i be Nat st Q[i] holds Q[(i + 1)]

      proof

        let i be Nat such that i in ( dom p) implies for j be Nat st j in ( dom q) holds P[i, j] and

         A12: (i + 1) in ( dom p);

        defpred R[ Nat] means $1 in ( dom q) implies P[(i + 1), $1];

        

         A13: for j be Nat st R[j] holds R[(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 Nat such that

           A15: j in ( dom q) implies P[(i + 1), j] and

           A16: (j + 1) in ( dom q);

          per cases ;

            suppose j = 0 ;

            hence thesis by A9, A14, Th36;

          end;

            suppose

             A17: j > 0 ;

            

             A18: j < ( len q) by A16, Lm2;

            then

            consider d be object 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 thesis by A19, Th42;

          end;

        end;

        

         A21: R[ 0 ] by Lm1;

        thus for j be Nat holds R[j] from NAT_1:sch 2( A21, A13);

      end;

      

       A22: ( len p) in ( dom p) & ( len q) in ( dom q) by FINSEQ_5: 6;

      

       A23: Q[ 0 ] by Lm1;

      for i be Nat holds Q[i] from NAT_1:sch 2( A23, A11);

      hence thesis by A8, A10, A22;

    end;

    theorem :: REWRITE1:52

    for R be Relation holds R is locally-confluent iff R commutes-weakly_with R

    proof

      let R be Relation;

      hereby

        assume

         A1: R is locally-confluent;

        thus R commutes-weakly_with R

        proof

          let a,b,c be object;

          assume [a, b] in R & [a, c] in R;

          then (b,c) are_convergent_wrt R by A1;

          hence thesis;

        end;

      end;

      assume

       A2: for a,b,c be object st [a, b] in R & [a, c] in R holds ex d be object st R reduces (b,d) & R reduces (c,d);

      let a,b,c be object;

      assume [a, b] in R & [a, c] in R;

      hence ex d be object st R reduces (b,d) & R reduces (c,d) by A2;

    end;

    registration

      cluster with_Church-Rosser_property -> confluent for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: for a,b be object st (a,b) are_convertible_wrt R holds (a,b) are_convergent_wrt R;

        let a,b be object;

        assume (a,b) are_divergent_wrt R;

        then (a,b) are_convertible_wrt R by Th37;

        hence thesis by A1;

      end;

      cluster confluent -> locally-confluent with_Church-Rosser_property for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A2: for a,b be object st (a,b) are_divergent_wrt R holds (a,b) are_convergent_wrt R;

        hereby

          let a,b,c be object;

          assume [a, b] in R & [a, c] in R;

          then R reduces (a,b) & R reduces (a,c) by Th15;

          then (b,c) are_divergent_wrt R;

          hence (b,c) are_convergent_wrt R by A2;

        end;

        let a,b be object;

        given p be RedSequence of (R \/ (R ~ )) such that

         A3: (p . 1) = a and

         A4: (p . ( len p)) = b;

        defpred P[ Nat] means $1 in ( dom p) implies (a,(p . $1)) are_convergent_wrt R;

        now

          let i be Nat;

          assume that

           A5: i in ( dom p) implies (a,(p . i)) are_convergent_wrt R and

           A6: (i + 1) in ( dom p);

          per cases ;

            suppose

             A7: i in ( dom p);

            then

            consider c be object such that

             A8: R reduces (a,c) and

             A9: R reduces ((p . i),c) by A5;

             [(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, Th16;

            then (c,(p . (i + 1))) are_convergent_wrt R or (a,(p . (i + 1))) are_convergent_wrt R by A2, A8;

            hence (a,(p . (i + 1))) are_convergent_wrt R by A8, Th42;

          end;

            suppose not i in ( dom p);

            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;

          end;

        end;

        then

         A10: for k be Nat st P[k] holds P[(k + 1)];

        

         A11: ( len p) in ( dom p) by FINSEQ_5: 6;

        

         A12: P[ 0 ] by Lm1;

        for i be Nat holds P[i] from NAT_1:sch 2( A12, A10);

        hence thesis by A4, A11;

      end;

      cluster subcommutative -> confluent for Relation;

      coherence

      proof

        let R be Relation;

        assume R is subcommutative;

        then for a,b,c be object st R reduces (a,b) & [a, c] in R holds (b,c) are_convergent_wrt R by Th49;

        hence thesis by Th51;

      end;

      cluster with_Church-Rosser_property -> with_NF_property for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A13: R is with_Church-Rosser_property;

        let b,a be object;

        assume

         A14: b is_a_normal_form_wrt R;

        assume (b,a) are_convertible_wrt R;

        then (b,a) are_convergent_wrt R by A13;

        then ex c be object st R reduces (b,c) & R reduces (a,c);

        hence thesis by A14, Th33;

      end;

      cluster with_NF_property -> with_UN_property for Relation;

      coherence by Th33;

      cluster with_UN_property weakly-normalizing -> with_Church-Rosser_property for Relation;

      coherence

      proof

        let R be Relation such that

         A15: for a,b be object 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

         A16: for a be object st a in ( field R) holds a has_a_normal_form_wrt R;

        let a,b be object;

        assume

         A17: (R \/ (R ~ )) reduces (a,b);

        

         A18: ( field (R \/ (R ~ ))) = (( field R) \/ ( field (R ~ ))) by RELAT_1: 18

        .= (( field R) \/ ( field R)) by RELAT_1: 21

        .= ( field R);

        per cases ;

          suppose a = b;

          hence thesis by Th38;

        end;

          suppose

           A19: a <> b;

          then b in ( field R) by A17, A18, Th18;

          then b has_a_normal_form_wrt R by A16;

          then

          consider b9 be object such that

           A20: b9 is_a_normal_form_of (b,R);

          a in ( field R) by A17, A18, A19, Th18;

          then a has_a_normal_form_wrt R by A16;

          then

          consider a9 be object such that

           A21: a9 is_a_normal_form_of (a,R);

          

           A22: a9 is_a_normal_form_wrt R by A21;

          

           A23: (a,b) are_convertible_wrt R by A17;

          

           A24: R reduces (a,a9) by A21;

          then (a9,a) are_convertible_wrt R by Th25;

          then

           A25: (a9,b) are_convertible_wrt R by A23, Th30;

          

           A26: b9 is_a_normal_form_wrt R by A20;

          

           A27: R reduces (b,b9) by A20;

          then (b,b9) are_convertible_wrt R by Th25;

          then a9 = b9 by A15, A22, A26, A25, Th30;

          hence thesis by A24, A27;

        end;

      end;

    end

    registration

      cluster empty -> subcommutative for Relation;

      coherence ;

    end

    theorem :: REWRITE1:53

    

     Th53: for R be with_UN_property Relation holds for a,b,c be object 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;

      let a,b,c be object such 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);

      (b,c) are_divergent_wrt R by A2, A4;

      then (b,c) are_convertible_wrt R by Th37;

      hence thesis by A1, A3, Def19;

    end;

    theorem :: REWRITE1:54

    

     Th54: for R be with_UN_property weakly-normalizing Relation holds for a be object holds ( nf (a,R)) is_a_normal_form_of (a,R)

    proof

      let R be with_UN_property weakly-normalizing Relation;

      let a be object;

      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 be object st b is_a_normal_form_of (a,R) & c is_a_normal_form_of (a,R) holds b = c by Th53;

      hence thesis by A1, Def12;

    end;

    theorem :: REWRITE1:55

    

     Th55: for R be with_UN_property weakly-normalizing Relation holds for a,b be object st (a,b) are_convertible_wrt R holds ( nf (a,R)) = ( nf (b,R))

    proof

      let R be with_UN_property weakly-normalizing Relation;

      let a,b be object;

      

       A1: ( nf (b,R)) is_a_normal_form_of (b,R) by Th54;

      then

       A2: ( nf (b,R)) is_a_normal_form_wrt R;

      R reduces (b,( nf (b,R))) by A1;

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

      then

       A5: (( nf (a,R)),a) are_convertible_wrt R by Th25;

      assume (a,b) are_convertible_wrt 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;

      hence thesis by A2, A6, Def19;

    end;

    registration

      cluster strongly-normalizing locally-confluent -> confluent for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: R is strongly-normalizing;

        defpred P[ object] means for b,c be object st R reduces ($1,b) & R reduces ($1,c) holds (b,c) are_convergent_wrt R;

        assume

         A2: for a,b,c be object st [a, b] in R & [a, c] in R holds (b,c) are_convergent_wrt R;

        

         A3: for a be object st for b be object st [a, b] in R & a <> b holds P[b] holds P[a]

        proof

          let a be object;

          assume

           A4: for b be object st [a, b] in R & a <> b holds P[b];

          let b,c be object;

          assume that

           A5: R reduces (a,b) and

           A6: R reduces (a,c);

          consider p be RedSequence of R such that

           A7: a = (p . 1) and

           A8: b = (p . ( len p)) by A5;

          

           A9: ( len p) >= ( 0 + 1) by NAT_1: 13;

          consider q be RedSequence of R such that

           A10: a = (q . 1) and

           A11: c = (q . ( len q)) by A6;

          

           A12: ( len q) >= ( 0 + 1) by NAT_1: 13;

          per cases ;

            suppose ( len p) = 1;

            hence thesis by A6, A7, A8, Th36;

          end;

            suppose ( len q) = 1;

            hence thesis by A5, A10, A11, Th36;

          end;

            suppose

             A13: ( len p) <> 1 & ( len q) <> 1;

            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 be object such that

             A23: R reduces ((p . 2),d) and

             A24: R reduces ((q . 2),d);

            

             A25: R is_irreflexive_in ( field R) by A1, RELAT_2:def 10;

            then

             A26: a <> (q . 2) by A22, A21;

            a <> (p . 2) by A20, A21, A25;

            then (b,d) are_convergent_wrt R by A4, A20, A23, A19;

            then

            consider e be object such that

             A27: R reduces (b,e) and

             A28: R reduces (d,e);

            R reduces ((q . 2),e) by A24, A28, Th16;

            then (e,c) are_convergent_wrt R by A4, A22, A26, A16;

            hence thesis by A27, Th42;

          end;

        end;

        

         A29: R is co-well_founded by A1;

        

         A30: for a be object st a in ( field R) holds P[a] from coNoetherianInduction( A29, A3);

        given a0,b0 be object such that

         A31: (a0,b0) are_divergent_wrt R and

         A32: not (a0,b0) are_convergent_wrt R;

        consider c0 be object such that

         A33: R reduces (c0,a0) & R reduces (c0,b0) by A31;

        a0 <> c0 or b0 <> c0 by A32, Th38;

        then c0 in ( field R) by A33, Th18;

        hence thesis by A32, A33, A30;

      end;

    end

    definition

      let R be Relation;

      :: REWRITE1:def25

      attr R is complete means R is confluent strongly-normalizing;

    end

    registration

      cluster complete -> confluent strongly-normalizing for Relation;

      coherence ;

      cluster confluent strongly-normalizing -> complete for Relation;

      coherence ;

    end

    registration

      cluster complete for non empty Relation;

      existence

      proof

        reconsider R = { [ 0 , 1]} as non empty Relation;

        take R;

        

         A1: ( field R) = { 0 , 1} by RELAT_1: 17;

        thus R is confluent

        proof

          let a,b be object;

          given c be object such that

           A2: R reduces (c,a) and

           A3: R reduces (c,b);

          per cases ;

            suppose a = b;

            hence thesis by Th38;

          end;

            suppose a <> b;

            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 thesis by A5, A6, A7;

          end;

        end;

        

         A8: R is co-well_founded

        proof

          let Y be set;

          assume that

           A9: Y c= ( field R) and

           A10: Y <> {} ;

          reconsider Y9 = Y as non empty set by A10;

          set y = the Element of Y9;

          per cases ;

            suppose

             A11: 1 in Y;

            take 1;

            thus 1 in Y by A11;

            let b be object;

            assume that b in Y and 1 <> b;

             [ 0 , 1] <> [1, b] by XTUPLE_0: 1;

            hence thesis by TARSKI:def 1;

          end;

            suppose

             A12: not 1 in Y & y in Y;

            take 0 ;

            thus 0 in Y by A1, A9, A12, TARSKI:def 2;

            let b be object;

            assume b in Y;

            hence thesis by A1, A9, A12, TARSKI:def 2;

          end;

        end;

        R is irreflexive

        proof

          let x be object;

          assume that x in ( field R) and

           A13: [x, x] in R;

          

           A14: [x, x] = [ 0 , 1] by A13, TARSKI:def 1;

          then x = 0 by XTUPLE_0: 1;

          hence contradiction by A14, XTUPLE_0: 1;

        end;

        hence thesis by A8;

      end;

    end

    theorem :: REWRITE1:56

    for R,Q be 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;

      assume

       A1: R commutes_with Q;

      (R \/ Q) is confluent

      proof

        let a,b be object;

        given c be object such that

         A2: (R \/ Q) reduces (c,a) and

         A3: (R \/ Q) reduces (c,b);

        consider p be RedSequence of (R \/ Q) such that

         A4: c = (p . 1) and

         A5: a = (p . ( len p)) by A2;

        defpred Z[ Nat] means $1 in ( dom p) implies ((p . $1),b) are_convergent_wrt (R \/ Q);

        now

          let i be Nat such that

           A6: i in ( dom p) implies ((p . i),b) are_convergent_wrt (R \/ Q) and

           A7: (i + 1) in ( dom p);

          per cases ;

            suppose i = 0 ;

            hence ((p . (i + 1)),b) are_convergent_wrt (R \/ Q) by A3, A4, Th36;

          end;

            suppose

             A8: i > 0 ;

            

             A9: i < ( len p) by A7, Lm2;

            then

            consider d be object such that

             A10: (R \/ Q) reduces ((p . i),d) and

             A11: (R \/ Q) reduces (b,d) by A6, A8, Lm3;

            consider q be RedSequence of (R \/ Q) such that

             A12: (p . i) = (q . 1) and

             A13: d = (q . ( len q)) by A10;

            defpred P[ Nat] means $1 in ( dom q) implies ex e be object 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

              let j be Nat such that

               A15: j in ( dom q) implies ex e be object 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);

              

               A17: j < ( len q) by A16, Lm2;

              per cases ;

                suppose

                 A18: j = 0 ;

                

                 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 be object st (R \/ Q) reduces ((p . (i + 1)),e) & (R reduces ((q . (j + 1)),e) or Q reduces ((q . (j + 1)),e)) by A19;

              end;

                suppose

                 A20: j > 0 ;

                then

                consider e be object 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

                  assume R reduces ((q . j),(q . (j + 1))) & Q reduces ((q . j),e);

                  then

                  consider x be object such that

                   A24: Q reduces ((q . (j + 1)),x) and

                   A25: R reduces (e,x) by A1;

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

                end;

                 A26:

                now

                  assume Q reduces ((q . j),(q . (j + 1))) & Q reduces ((q . j),e);

                  then (e,(q . (j + 1))) are_divergent_wrt Q;

                  then (e,(q . (j + 1))) are_convergent_wrt Q by Def22;

                  then

                  consider x be object such that

                   A27: Q reduces (e,x) and

                   A28: Q reduces ((q . (j + 1)),x);

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

                end;

                 A29:

                now

                  assume R reduces ((q . j),(q . (j + 1))) & R reduces ((q . j),e);

                  then (e,(q . (j + 1))) are_divergent_wrt R;

                  then (e,(q . (j + 1))) are_convergent_wrt R by Def22;

                  then

                  consider x be object such that

                   A30: R reduces (e,x) and

                   A31: R reduces ((q . (j + 1)),x);

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

                end;

                 A32:

                now

                  assume Q reduces ((q . j),(q . (j + 1))) & R reduces ((q . j),e);

                  then

                  consider x be object such that

                   A33: R reduces ((q . (j + 1)),x) and

                   A34: Q reduces (e,x) by A1, Def18;

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

                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 be object 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;

              end;

            end;

            then

             A35: for k be Nat st P[k] holds P[(k + 1)];

            

             A36: P[ 0 ] by Lm1;

            

             A37: for j be Nat holds P[j] from NAT_1:sch 2( A36, A35);

            thus ((p . (i + 1)),b) are_convergent_wrt (R \/ Q)

            proof

              ( len q) in ( dom q) by FINSEQ_5: 6;

              then

              consider e be object 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;

              (R \/ Q) reduces (d,e) by A39, Th22, XBOOLE_1: 7;

              hence thesis by A11, A38, Th16;

            end;

          end;

        end;

        then

         A40: for k be Nat st Z[k] holds Z[(k + 1)];

        

         A41: ( len p) in ( dom p) by FINSEQ_5: 6;

        

         A42: Z[ 0 ] by Lm1;

        for i be Nat holds Z[i] from NAT_1:sch 2( A42, A40);

        hence thesis by A5, A41;

      end;

      hence thesis;

    end;

    theorem :: REWRITE1:57

    for R be Relation holds R is confluent iff (R [*] ) is locally-confluent

    proof

      let R be Relation;

      hereby

        assume

         A1: R is confluent;

        thus (R [*] ) is locally-confluent

        proof

          let a,b,c be object;

          assume [a, b] in (R [*] ) & [a, c] in (R [*] );

          then R reduces (a,b) & R reduces (a,c) by Th20;

          then (b,c) are_divergent_wrt R;

          then (b,c) are_convergent_wrt R by A1;

          then

          consider d be object such that

           A2: R reduces (b,d) & R reduces (c,d);

          take d;

          thus thesis by A2, Th21;

        end;

      end;

      assume

       A3: for a,b,c be object st [a, b] in (R [*] ) & [a, c] in (R [*] ) holds (b,c) are_convergent_wrt (R [*] );

      let a,b be object;

      given c be object such that

       A4: R reduces (c,a) and

       A5: R reduces (c,b);

      

       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 be object such that

       A7: (R [*] ) reduces (a,d) & (R [*] ) reduces (b,d);

      take d;

      thus thesis by A7, Th21;

    end;

    theorem :: REWRITE1:58

    for R be Relation holds R is confluent iff (R [*] ) is subcommutative

    proof

      let R be Relation;

      hereby

        assume

         A1: R is confluent;

        thus (R [*] ) is subcommutative

        proof

          let a,b,c be object;

          assume [a, b] in (R [*] ) & [a, c] in (R [*] );

          then R reduces (a,b) & R reduces (a,c) by Th20;

          then (b,c) are_divergent_wrt R;

          then (b,c) are_convergent_wrt R by A1;

          then

          consider d be object such that

           A2: R reduces (b,d) & R reduces (c,d);

          take d;

          thus thesis by A2, Th20;

        end;

      end;

      assume

       A3: for a,b,c be object st [a, b] in (R [*] ) & [a, c] in (R [*] ) holds (b,c) are_convergent<=1_wrt (R [*] );

      let a,b be object;

      given c be object such that

       A4: R reduces (c,a) and

       A5: R reduces (c,b);

      

       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;

      then (a,b) are_convergent_wrt (R [*] ) by Th44;

      then

      consider d be object such that

       A7: (R [*] ) reduces (a,d) & (R [*] ) reduces (b,d);

      take d;

      thus thesis by A7, Th21;

    end;

    begin

    definition

      let R,Q be Relation;

      :: REWRITE1:def26

      pred R,Q are_equivalent means for a,b be object holds (a,b) are_convertible_wrt R iff (a,b) are_convertible_wrt Q;

      symmetry ;

    end

    definition

      let R be Relation;

      let a,b be object;

      :: REWRITE1:def27

      pred a,b are_critical_wrt R means (a,b) are_divergent<=1_wrt R & not (a,b) are_convergent_wrt R;

    end

    theorem :: REWRITE1:59

    

     Th59: for R be Relation, a,b be object st (a,b) are_critical_wrt R holds (a,b) are_convertible_wrt R by Th37, Th45;

    theorem :: REWRITE1:60

    for R be Relation st not ex a,b be object st (a,b) are_critical_wrt R holds R is locally-confluent

    proof

      let R be Relation such that

       A1: not ex a,b be object st (a,b) are_critical_wrt R;

      let a,b,c be object;

      assume [a, b] in R & [a, c] in R;

      then

       A2: (b,c) are_divergent<=1_wrt R;

       not (b,c) are_critical_wrt R by A1;

      hence thesis by A2;

    end;

    theorem :: REWRITE1:61

    for R,Q be Relation st for a,b be object st [a, b] in Q holds (a,b) are_critical_wrt R holds (R,(R \/ Q)) are_equivalent

    proof

      let R,Q be Relation;

      assume

       A1: for a,b be object st [a, b] in Q holds (a,b) are_critical_wrt R;

      let a,b be object;

      

       A2: R c= (R \/ Q) by XBOOLE_1: 7;

      

       A3: (R ~ ) c= ((R \/ Q) ~ )

      proof

        let x,y be object;

        assume [x, y] in (R ~ );

        then [y, x] in R by RELAT_1:def 7;

        hence thesis by A2, RELAT_1:def 7;

      end;

      thus (a,b) are_convertible_wrt R implies (a,b) are_convertible_wrt (R \/ Q) by A2, A3, Th22, XBOOLE_1: 13;

      given p be RedSequence of ((R \/ Q) \/ ((R \/ Q) ~ )) such that

       A4: a = (p . 1) and

       A5: b = (p . ( len p));

      defpred Z[ Nat] means $1 in ( dom p) implies (a,(p . $1)) are_convertible_wrt R;

      now

        let i be Nat such that

         A6: i in ( dom p) implies (a,(p . i)) are_convertible_wrt R and

         A7: (i + 1) in ( dom p);

        

         A8: i < ( len p) by A7, Lm2;

        per cases ;

          suppose i = 0 ;

          hence (a,(p . (i + 1))) are_convertible_wrt R by A4, Th26;

        end;

          suppose

           A9: i > 0 ;

          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;

        end;

      end;

      then

       A10: for k be Nat st Z[k] holds Z[(k + 1)];

      

       A11: ( len p) in ( dom p) by FINSEQ_5: 6;

      

       A12: Z[ 0 ] by Lm1;

      for i be Nat holds Z[i] from NAT_1:sch 2( A12, A10);

      hence thesis by A5, A11;

    end;

    theorem :: REWRITE1:62

    

     Th62: for R be Relation holds ex Q be complete Relation st ( field Q) c= ( field R) & for a,b be object holds (a,b) are_convertible_wrt R iff (a,b) are_convergent_wrt Q

    proof

      let R be Relation;

      per cases ;

        suppose

         A1: R = {} ;

        take E = {} ;

        thus ( field E) c= ( field R);

        let a,b be object;

        (a,b) are_convertible_wrt R iff a = b by A1, Th26, Th27;

        hence thesis by Th38, Th39;

      end;

        suppose R <> {} ;

        then

        reconsider R9 = R as non empty Relation;

        set xx = the Element of R9;

        consider x1,x2 be object such that

         A2: xx = [x1, x2] by RELAT_1:def 1;

        defpred P[ object, object] means ($1,$2) are_convertible_wrt R;

        

         A3: for x,y be object st P[x, y] holds P[y, x] by Lm5;

        

         A4: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z] by Th30;

        

         A5: for x be object st x in ( field R) holds P[x, x] by Th26;

        consider Q be Equivalence_Relation of ( field R) such that

         A6: for x,y be object holds [x, y] in Q iff x in ( field R) & y in ( field R) & P[x, y] from EQREL_1:sch 1( A5, A3, A4);

        

         A7: (for X be set st X in ( Class Q) holds X <> {} ) & for X,Y be 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 be set such that

         A8: for A be set st A in ( Class Q) holds ex x st (X /\ A) = {x} by A7, WELLORD2: 18;

        defpred Z[ object, object] means $1 <> $2 & ($1,$2) are_convertible_wrt R & $2 in X;

        consider P be Relation such that

         A9: for x,y be object holds [x, y] in P iff x in ( field R) & y in ( field R) & Z[x, y] from RELAT_1:sch 1;

        

         A10: P is locally-confluent

        proof

          let a,b,c be object;

          assume that

           A11: [a, b] in P and

           A12: [a, c] in P;

          

           A13: a in ( field R) by A9, A11;

          then ( Class (Q,a)) in ( Class Q) by EQREL_1:def 3;

          then

          consider x 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;

          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 thesis by A16, Th12;

        end;

        

         A18: for x, y st P reduces (x,y) holds (x,y) are_convertible_wrt R

        proof

          let x, y;

          given p be RedSequence of P such that

           A19: x = (p . 1) and

           A20: y = (p . ( len p));

          defpred Z[ Nat] means $1 in ( dom p) implies (x,(p . $1)) are_convertible_wrt R;

          now

            let i be Nat such that

             A21: i in ( dom p) implies (x,(p . i)) are_convertible_wrt R and

             A22: (i + 1) in ( dom p);

            

             A23: i < ( len p) by A22, Lm2;

            per cases ;

              suppose i = 0 ;

              hence (x,(p . (i + 1))) are_convertible_wrt R by A19, Th26;

            end;

              suppose

               A24: i > 0 ;

              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;

            end;

          end;

          then

           A25: for k be Nat st Z[k] holds Z[(k + 1)];

          

           A26: ( len p) in ( dom p) by FINSEQ_5: 6;

          

           A27: Z[ 0 ] by Lm1;

          for i be Nat holds Z[i] from NAT_1:sch 2( A27, A25);

          hence thesis by A20, A26;

        end;

        P is strongly-normalizing

        proof

          let f be ManySortedSet of NAT ;

          per cases ;

            suppose not [(f . 0 ), (f . ( 0 + 1))] in P;

            hence thesis;

          end;

            suppose

             A28: [(f . 0 ), (f . ( 0 + 1))] in P;

            take j = ( 0 + 1);

            

             A29: (f . j) in X by A9, A28;

            assume

             A30: [(f . j), (f . (j + 1))] in P;

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

          end;

        end;

        then

        reconsider P as strongly-normalizing locally-confluent Relation by A10;

        take P;

        thus ( field P) c= ( field R)

        proof

          let x be object;

          assume x in ( field P);

          then x in ( dom P) or x in ( rng P) by XBOOLE_0:def 3;

          then (ex y be object st [x, y] in P) or ex y be object st [y, x] in P by XTUPLE_0:def 12, XTUPLE_0:def 13;

          hence thesis by A9;

        end;

        let a,b be object;

        thus thesis

        proof

          per cases ;

            suppose a = b;

            hence thesis by Th26, Th38;

          end;

            suppose

             A35: a <> b;

            hereby

              assume

               A36: (a,b) are_convertible_wrt R;

              then

               A37: b in ( field R) by A35, Th32;

              then ( Class (Q,b)) in ( Class Q) by EQREL_1:def 3;

              then

              consider x 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

              proof

                take 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 thesis by A44, Th12, Th15;

              end;

            end;

            given c be object such that

             A45: P reduces (a,c) & P reduces (b,c);

            (a,c) are_convertible_wrt R & (c,b) are_convertible_wrt R by A18, A45, Lm5;

            hence thesis by Th30;

          end;

        end;

      end;

    end;

    definition

      let R be Relation;

      :: REWRITE1:def28

      mode Completion of R -> complete Relation means

      : Def28: for a,b be object holds (a,b) are_convertible_wrt R iff (a,b) are_convergent_wrt it ;

      existence

      proof

        ex Q be complete Relation st ( field Q) c= ( field R) & for a,b be object holds (a,b) are_convertible_wrt R iff (a,b) are_convergent_wrt Q by Th62;

        hence thesis;

      end;

    end

    theorem :: REWRITE1:63

    for R be Relation, C be Completion of R holds (R,C) are_equivalent

    proof

      let R be Relation, C be Completion of R, a,b be object;

      (a,b) are_convertible_wrt R iff (a,b) are_convergent_wrt C by Def28;

      hence thesis by Def23, Th37;

    end;

    theorem :: REWRITE1:64

    for R be Relation, Q be complete Relation st (R,Q) are_equivalent holds Q is Completion of R

    proof

      let R be Relation, Q be complete Relation such that

       A1: for a,b be object holds (a,b) are_convertible_wrt R iff (a,b) are_convertible_wrt Q;

      let a,b be object;

      (a,b) are_convertible_wrt R iff (a,b) are_convertible_wrt Q by A1;

      hence thesis by Def23, Th37;

    end;

    theorem :: REWRITE1:65

    for R be Relation, C be Completion of R, a,b be object holds (a,b) are_convertible_wrt R iff ( nf (a,C)) = ( nf (b,C))

    proof

      let R be Relation, C be Completion of R, a,b be object;

      ( nf (a,C)) is_a_normal_form_of (a,C) by Th54;

      then

       A1: C reduces (a,( nf (a,C)));

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

      ( nf (b,C)) is_a_normal_form_of (b,C) by Th54;

      then

       A2: C reduces (b,( nf (b,C)));

      (a,b) are_convertible_wrt R iff (a,b) are_convergent_wrt C by Def28;

      hence thesis by A1, A2;

    end;