rewrite2.miz



    begin

    reserve x for set;

    reserve k,l for Nat;

    reserve p,q for FinSequence;

    theorem :: REWRITE2:1

    

     Th1: not k in ( dom p) & (k + 1) in ( dom p) implies k = 0

    proof

      assume that

       A1: not k in ( dom p) and

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

      

       A3: (k + 1) <= ( len p) by A2, FINSEQ_3: 25;

      per cases by A1, FINSEQ_3: 25;

        suppose k < 1;

        hence thesis by NAT_1: 14;

      end;

        suppose k > ( len p);

        hence thesis by A3, NAT_1: 13;

      end;

    end;

    theorem :: REWRITE2:2

    

     Th2: k > ( len p) & k <= ( len (p ^ q)) implies ex l st k = (( len p) + l) & l >= 1 & l <= ( len q)

    proof

      

       A1: ( 0 + 1) = 1;

      assume that

       A2: k > ( len p) and

       A3: k <= ( len (p ^ q));

      consider l such that

       A4: k = (( len p) + l) by A2, NAT_1: 10;

      take l;

      thus k = (( len p) + l) by A4;

      (( len p) + l) > (( len p) + 0 ) by A2, A4;

      then l > 0 ;

      hence l >= 1 by A1, NAT_1: 13;

      (( len p) + l) <= (( len p) + ( len q)) by A3, A4, FINSEQ_1: 22;

      hence thesis by XREAL_1: 6;

    end;

    reserve R for Relation;

    reserve p,q for RedSequence of R;

    theorem :: REWRITE2:3

    

     Th3: k >= 1 implies (p | k) is RedSequence of R

    proof

      assume

       A1: k >= 1;

      per cases ;

        suppose k >= ( len p);

        hence thesis by FINSEQ_1: 58;

      end;

        suppose

         A2: k < ( len p);

         A3:

        now

          

           A4: ( dom (p | k)) c= ( dom p) by RELAT_1: 60;

          let i be Nat such that

           A5: i in ( dom (p | k)) & (i + 1) in ( dom (p | k));

          ((p | k) . i) = (p . i) & ((p | k) . (i + 1)) = (p . (i + 1)) by A5, FUNCT_1: 47;

          hence [((p | k) . i), ((p | k) . (i + 1))] in R by A5, A4, REWRITE1:def 2;

        end;

        ( len (p | k)) > 0 by A1, A2, FINSEQ_1: 59;

        hence thesis by A3, REWRITE1:def 2;

      end;

    end;

    theorem :: REWRITE2:4

    

     Th4: k in ( dom p) implies ex q st ( len q) = k & (q . 1) = (p . 1) & (q . ( len q)) = (p . k)

    proof

      assume

       A1: k in ( dom p);

      set q = (p | k);

      take q;

      

       A2: 1 <= k by A1, FINSEQ_3: 25;

      hence q is RedSequence of R by Th3;

      k <= ( len p) by A1, FINSEQ_3: 25;

      hence ( len q) = k by FINSEQ_1: 59;

      hence thesis by A2, FINSEQ_3: 112;

    end;

    begin

    definition

      let f be Function;

      :: REWRITE2:def1

      attr f is XFinSequence-yielding means

      : Def1: x in ( dom f) implies (f . x) is XFinSequence;

    end

    registration

      cluster empty -> XFinSequence-yielding for Function;

      coherence ;

    end

    registration

      let f be XFinSequence;

      cluster <*f*> -> XFinSequence-yielding;

      coherence

      proof

        let x be set;

        assume x in ( dom <*f*>);

        then x in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then x = 1 by TARSKI:def 1;

        hence thesis by FINSEQ_1: 40;

      end;

    end

    registration

      let p be XFinSequence-yielding Function;

      let x be object;

      cluster (p . x) -> finite Function-like Relation-like;

      coherence

      proof

        per cases ;

          suppose x in ( dom p);

          hence thesis by Def1;

        end;

          suppose not x in ( dom p);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let p be XFinSequence-yielding Function;

      let x be object;

      cluster (p . x) -> Sequence-like;

      coherence

      proof

        per cases ;

          suppose x in ( dom p);

          hence thesis by Def1;

        end;

          suppose not x in ( dom p);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      cluster XFinSequence-yielding for FinSequence;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      let E be set;

      cluster -> XFinSequence-yielding for FinSequence of (E ^omega );

      coherence

      proof

        let f be FinSequence of (E ^omega );

        let x;

        assume

         A1: x in ( dom f);

        then

        reconsider x as Nat;

        (f . x) in (E ^omega ) by A1, FINSEQ_2: 11;

        hence thesis;

      end;

    end

    registration

      let p,q be XFinSequence-yielding FinSequence;

      cluster (p ^ q) -> XFinSequence-yielding;

      coherence

      proof

        now

          let x;

          assume

           A1: x in ( dom (p ^ q));

          then

          reconsider x1 = x as Nat;

          per cases by A1, FINSEQ_1: 25;

            suppose x1 in ( dom p);

            then (p . x1) = ((p ^ q) . x1) by FINSEQ_1:def 7;

            hence ((p ^ q) . x) is XFinSequence;

          end;

            suppose ex l be Nat st l in ( dom q) & x1 = (( len p) + l);

            then

            consider l be Nat such that

             A2: l in ( dom q) and

             A3: x = (( len p) + l);

            ((p ^ q) . (( len p) + l)) = (q . l) by A2, FINSEQ_1:def 7;

            hence ((p ^ q) . x) is XFinSequence by A3;

          end;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let s be XFinSequence;

      let p be XFinSequence-yielding Function;

      :: REWRITE2:def2

      func s ^+ p -> XFinSequence-yielding Function means

      : Def2: ( dom it ) = ( dom p) & for x st x in ( dom p) holds (it . x) = (s ^ (p . x));

      existence

      proof

        defpred P[ object, object] means for x st x = $1 holds $2 = (s ^ (p . x));

        

         A1: for x be object st x in ( dom p) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in ( dom p);

          take (s ^ (p . x));

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = ( dom p) & for x be object st x in ( dom p) holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        now

          let x;

          assume x in ( dom f);

          then (f . x) = (s ^ (p . x)) by A2;

          hence (f . x) is XFinSequence;

        end;

        then

        reconsider g = f as XFinSequence-yielding Function by Def1;

        take g;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be XFinSequence-yielding Function such that

         A3: ( dom f) = ( dom p) and

         A4: for x st x in ( dom p) holds (f . x) = (s ^ (p . x)) and

         A5: ( dom g) = ( dom p) and

         A6: for x st x in ( dom p) holds (g . x) = (s ^ (p . x));

        now

          let x be object;

          assume

           A7: x in ( dom f);

          then (f . x) = (s ^ (p . x)) by A3, A4;

          hence (f . x) = (g . x) by A3, A6, A7;

        end;

        hence thesis by A3, A5, FUNCT_1: 2;

      end;

      :: REWRITE2:def3

      func p +^ s -> XFinSequence-yielding Function means

      : Def3: ( dom it ) = ( dom p) & for x st x in ( dom p) holds (it . x) = ((p . x) ^ s);

      existence

      proof

        defpred P[ object, object] means for x st x = $1 holds $2 = ((p . x) ^ s);

        

         A8: for x be object st x in ( dom p) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in ( dom p);

          take ((p . x) ^ s);

          thus thesis;

        end;

        consider f be Function such that

         A9: ( dom f) = ( dom p) & for x be object st x in ( dom p) holds P[x, (f . x)] from CLASSES1:sch 1( A8);

        now

          let x;

          assume x in ( dom f);

          then (f . x) = ((p . x) ^ s) by A9;

          hence (f . x) is XFinSequence;

        end;

        then

        reconsider g = f as XFinSequence-yielding Function by Def1;

        take g;

        thus thesis by A9;

      end;

      uniqueness

      proof

        let f,g be XFinSequence-yielding Function such that

         A10: ( dom f) = ( dom p) and

         A11: for x st x in ( dom p) holds (f . x) = ((p . x) ^ s) and

         A12: ( dom g) = ( dom p) and

         A13: for x st x in ( dom p) holds (g . x) = ((p . x) ^ s);

        now

          let x be object;

          assume

           A14: x in ( dom f);

          then (f . x) = ((p . x) ^ s) by A10, A11;

          hence (f . x) = (g . x) by A10, A13, A14;

        end;

        hence thesis by A10, A12, FUNCT_1: 2;

      end;

    end

    registration

      let s be XFinSequence;

      let p be XFinSequence-yielding FinSequence;

      cluster (s ^+ p) -> FinSequence-like;

      coherence

      proof

        consider n be Nat such that

         A1: ( dom p) = ( Seg n) by FINSEQ_1:def 2;

        ( dom (s ^+ p)) = ( Seg n) by A1, Def2;

        hence thesis;

      end;

      cluster (p +^ s) -> FinSequence-like;

      coherence

      proof

        consider n be Nat such that

         A2: ( dom p) = ( Seg n) by FINSEQ_1:def 2;

        ( dom (p +^ s)) = ( Seg n) by A2, Def3;

        hence thesis;

      end;

    end

    reserve E for set;

    reserve s,t for XFinSequence;

    reserve p,q for XFinSequence-yielding FinSequence;

    theorem :: REWRITE2:5

    

     Th5: ( len (s ^+ p)) = ( len p) & ( len (p +^ s)) = ( len p)

    proof

      ( dom (s ^+ p)) = ( dom p) & ( dom (p +^ s)) = ( dom p) by Def2, Def3;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: REWRITE2:6

    (( <%> E) ^+ p) = p & (p +^ ( <%> E)) = p

    proof

       A1:

      now

        let k be Nat;

        assume k in ( dom p);

        

        hence ((( <%> E) ^+ p) . k) = ( {} ^ (p . k)) by Def2

        .= (p . k);

      end;

      ( dom (( <%> E) ^+ p)) = ( dom p) by Def2;

      hence (( <%> E) ^+ p) = p by A1, FINSEQ_1: 13;

       A2:

      now

        let k be Nat;

        assume k in ( dom p);

        

        hence ((p +^ ( <%> E)) . k) = ((p . k) ^ {} ) by Def3

        .= (p . k);

      end;

      ( dom (p +^ ( <%> E))) = ( dom p) by Def3;

      hence thesis by A2, FINSEQ_1: 13;

    end;

    theorem :: REWRITE2:7

    (s ^+ (t ^+ p)) = ((s ^ t) ^+ p) & ((p +^ t) +^ s) = (p +^ (t ^ s))

    proof

       A1:

      now

        let k be Nat;

        assume k in ( dom (s ^+ (t ^+ p)));

        then

         A2: k in ( dom (t ^+ p)) by Def2;

        then

         A3: k in ( dom p) by Def2;

        

        thus ((s ^+ (t ^+ p)) . k) = (s ^ ((t ^+ p) . k)) by A2, Def2

        .= (s ^ (t ^ (p . k))) by A3, Def2

        .= ((s ^ t) ^ (p . k)) by AFINSQ_1: 27

        .= (((s ^ t) ^+ p) . k) by A3, Def2;

      end;

      ( dom (s ^+ (t ^+ p))) = ( dom (t ^+ p)) by Def2

      .= ( dom p) by Def2

      .= ( dom ((s ^ t) ^+ p)) by Def2;

      hence (s ^+ (t ^+ p)) = ((s ^ t) ^+ p) by A1, FINSEQ_1: 13;

       A4:

      now

        let k be Nat;

        assume k in ( dom ((p +^ t) +^ s));

        then

         A5: k in ( dom (p +^ t)) by Def3;

        then

         A6: k in ( dom p) by Def3;

        

        thus (((p +^ t) +^ s) . k) = (((p +^ t) . k) ^ s) by A5, Def3

        .= (((p . k) ^ t) ^ s) by A6, Def3

        .= ((p . k) ^ (t ^ s)) by AFINSQ_1: 27

        .= ((p +^ (t ^ s)) . k) by A6, Def3;

      end;

      ( dom ((p +^ t) +^ s)) = ( dom (p +^ t)) by Def3

      .= ( dom p) by Def3

      .= ( dom (p +^ (t ^ s))) by Def3;

      hence thesis by A4, FINSEQ_1: 13;

    end;

    theorem :: REWRITE2:8

    (s ^+ (p +^ t)) = ((s ^+ p) +^ t)

    proof

       A1:

      now

        let k be Nat;

        assume k in ( dom (s ^+ (p +^ t)));

        then

         A2: k in ( dom (p +^ t)) by Def2;

        then

         A3: k in ( dom p) by Def3;

        then

         A4: k in ( dom (s ^+ p)) by Def2;

        

        thus ((s ^+ (p +^ t)) . k) = (s ^ ((p +^ t) . k)) by A2, Def2

        .= (s ^ ((p . k) ^ t)) by A3, Def3

        .= ((s ^ (p . k)) ^ t) by AFINSQ_1: 27

        .= (((s ^+ p) . k) ^ t) by A3, Def2

        .= (((s ^+ p) +^ t) . k) by A4, Def3;

      end;

      ( dom (s ^+ (p +^ t))) = ( dom (p +^ t)) by Def2

      .= ( dom p) by Def3

      .= ( dom (s ^+ p)) by Def2

      .= ( dom ((s ^+ p) +^ t)) by Def3;

      hence thesis by A1, FINSEQ_1: 13;

    end;

    theorem :: REWRITE2:9

    (s ^+ (p ^ q)) = ((s ^+ p) ^ (s ^+ q)) & ((p ^ q) +^ s) = ((p +^ s) ^ (q +^ s))

    proof

       A1:

      now

        let k be Nat;

        assume

         A2: k in ( dom (s ^+ (p ^ q)));

        then

         A3: k in ( dom (p ^ q)) by Def2;

        now

          per cases ;

            suppose

             A4: k in ( dom p);

            then

             A5: k in ( dom (s ^+ p)) by Def2;

            

            thus ((s ^+ (p ^ q)) . k) = (s ^ ((p ^ q) . k)) by A3, Def2

            .= (s ^ (p . k)) by A4, FINSEQ_1:def 7

            .= ((s ^+ p) . k) by A4, Def2

            .= (((s ^+ p) ^ (s ^+ q)) . k) by A5, FINSEQ_1:def 7;

          end;

            suppose

             A6: not k in ( dom p);

            

             A7: k <= ( len (p ^ q)) by A3, FINSEQ_3: 25;

            k < 1 or k > ( len p) by A6, FINSEQ_3: 25;

            then

            consider i be Nat such that

             A8: k = (( len p) + i) and

             A9: i >= 1 & i <= ( len q) by A2, A7, Th2, FINSEQ_3: 25;

            

             A10: i in ( dom q) by A9, FINSEQ_3: 25;

            then

             A11: i in ( dom (s ^+ q)) by Def2;

            

             A12: ( len (s ^+ p)) = ( len p) by Th5;

            

            thus ((s ^+ (p ^ q)) . k) = (s ^ ((p ^ q) . (( len p) + i))) by A3, A8, Def2

            .= (s ^ (q . i)) by A10, FINSEQ_1:def 7

            .= ((s ^+ q) . i) by A10, Def2

            .= (((s ^+ p) ^ (s ^+ q)) . k) by A8, A11, A12, FINSEQ_1:def 7;

          end;

        end;

        hence ((s ^+ (p ^ q)) . k) = (((s ^+ p) ^ (s ^+ q)) . k);

      end;

      ( len (s ^+ (p ^ q))) = ( len (p ^ q)) by Th5

      .= (( len p) + ( len q)) by FINSEQ_1: 22

      .= (( len (s ^+ p)) + ( len q)) by Th5

      .= (( len (s ^+ p)) + ( len (s ^+ q))) by Th5

      .= ( len ((s ^+ p) ^ (s ^+ q))) by FINSEQ_1: 22;

      then ( dom (s ^+ (p ^ q))) = ( dom ((s ^+ p) ^ (s ^+ q))) by FINSEQ_3: 29;

      hence (s ^+ (p ^ q)) = ((s ^+ p) ^ (s ^+ q)) by A1, FINSEQ_1: 13;

       A13:

      now

        let k be Nat;

        assume

         A14: k in ( dom ((p ^ q) +^ s));

        then

         A15: k in ( dom (p ^ q)) by Def3;

        now

          per cases ;

            suppose

             A16: k in ( dom p);

            then

             A17: k in ( dom (p +^ s)) by Def3;

            

            thus (((p ^ q) +^ s) . k) = (((p ^ q) . k) ^ s) by A15, Def3

            .= ((p . k) ^ s) by A16, FINSEQ_1:def 7

            .= ((p +^ s) . k) by A16, Def3

            .= (((p +^ s) ^ (q +^ s)) . k) by A17, FINSEQ_1:def 7;

          end;

            suppose

             A18: not k in ( dom p);

            

             A19: k <= ( len (p ^ q)) by A15, FINSEQ_3: 25;

            k < 1 or k > ( len p) by A18, FINSEQ_3: 25;

            then

            consider i be Nat such that

             A20: k = (( len p) + i) and

             A21: i >= 1 & i <= ( len q) by A14, A19, Th2, FINSEQ_3: 25;

            

             A22: i in ( dom q) by A21, FINSEQ_3: 25;

            then

             A23: i in ( dom (q +^ s)) by Def3;

            

             A24: ( len (p +^ s)) = ( len p) by Th5;

            

            thus (((p ^ q) +^ s) . k) = (((p ^ q) . (( len p) + i)) ^ s) by A15, A20, Def3

            .= ((q . i) ^ s) by A22, FINSEQ_1:def 7

            .= ((q +^ s) . i) by A22, Def3

            .= (((p +^ s) ^ (q +^ s)) . k) by A20, A23, A24, FINSEQ_1:def 7;

          end;

        end;

        hence (((p ^ q) +^ s) . k) = (((p +^ s) ^ (q +^ s)) . k);

      end;

      ( len ((p ^ q) +^ s)) = ( len (p ^ q)) by Th5

      .= (( len p) + ( len q)) by FINSEQ_1: 22

      .= (( len (p +^ s)) + ( len q)) by Th5

      .= (( len (p +^ s)) + ( len (q +^ s))) by Th5

      .= ( len ((p +^ s) ^ (q +^ s))) by FINSEQ_1: 22;

      then ( dom ((p ^ q) +^ s)) = ( dom ((p +^ s) ^ (q +^ s))) by FINSEQ_3: 29;

      hence thesis by A13, FINSEQ_1: 13;

    end;

    begin

    definition

      let E be set;

      let p be FinSequence of (E ^omega );

      let k be Nat;

      :: original: .

      redefine

      func p . k -> Element of (E ^omega ) ;

      coherence

      proof

        per cases ;

          suppose k in ( dom p);

          hence thesis by FINSEQ_2: 11;

        end;

          suppose not k in ( dom p);

          then (p . k) = {} by FUNCT_1:def 2;

          then (p . k) is XFinSequence of E by AFINSQ_1: 16;

          hence thesis by AFINSQ_1:def 7;

        end;

      end;

    end

    definition

      let E be set;

      let s be Element of (E ^omega );

      let p be FinSequence of (E ^omega );

      :: original: ^+

      redefine

      func s ^+ p -> FinSequence of (E ^omega ) ;

      coherence

      proof

        now

          let i be Nat;

          assume i in ( dom (s ^+ p));

          then i in ( dom p) by Def2;

          then ((s ^+ p) . i) = (s ^ (p . i)) by Def2;

          hence ((s ^+ p) . i) in (E ^omega );

        end;

        hence thesis by FINSEQ_2: 12;

      end;

      :: original: +^

      redefine

      func p +^ s -> FinSequence of (E ^omega ) ;

      coherence

      proof

        now

          let i be Nat;

          assume i in ( dom (p +^ s));

          then i in ( dom p) by Def3;

          then ((p +^ s) . i) = ((p . i) ^ s) by Def3;

          hence ((p +^ s) . i) in (E ^omega );

        end;

        hence thesis by FINSEQ_2: 12;

      end;

    end

    definition

      let E be set;

      mode semi-Thue-system of E is Relation of (E ^omega );

    end

    reserve E for set;

    reserve S,T,U for semi-Thue-system of E;

    registration

      let S be Relation;

      cluster (S \/ (S ~ )) -> symmetric;

      coherence

      proof

        (S \/ (S ~ )) = ((((S ~ ) ~ ) \/ (S ~ )) ~ ) by RELAT_1: 23

        .= ((S \/ (S ~ )) ~ );

        hence thesis by RELAT_2: 13;

      end;

    end

    registration

      let E;

      cluster symmetric for semi-Thue-system of E;

      existence

      proof

        set S = the semi-Thue-system of E;

        take (S \/ (S ~ ));

        thus thesis;

      end;

    end

    definition

      let E be set;

      mode Thue-system of E is symmetric semi-Thue-system of E;

    end

    begin

    reserve s,t,s1,t1,u,v,u1,v1,w for Element of (E ^omega );

    reserve p for FinSequence of (E ^omega );

    definition

      let E, S, s, t;

      :: REWRITE2:def4

      pred s -->. t,S means [s, t] in S;

    end

    definition

      let E, S, s, t;

      :: REWRITE2:def5

      pred s ==>. t,S means ex v, w, s1, t1 st s = ((v ^ s1) ^ w) & t = ((v ^ t1) ^ w) & s1 -->. (t1,S);

    end

    theorem :: REWRITE2:10

    

     Th10: s -->. (t,S) implies s ==>. (t,S)

    proof

      assume

       A1: s -->. (t,S);

      take e = ( <%> E);

      

       A2: t = (( {} ^ t) ^ {} )

      .= ((e ^ t) ^ e);

      s = (( {} ^ s) ^ {} )

      .= ((e ^ s) ^ e);

      hence thesis by A1, A2;

    end;

    theorem :: REWRITE2:11

    s ==>. (s,S) implies ex v, w, s1 st s = ((v ^ s1) ^ w) & s1 -->. (s1,S)

    proof

      given v, w, s1, t1 such that

       A1: s = ((v ^ s1) ^ w) and

       A2: s = ((v ^ t1) ^ w) and

       A3: s1 -->. (t1,S);

      (v ^ s1) = (v ^ t1) by A1, A2, AFINSQ_1: 28;

      then s1 = t1 by AFINSQ_1: 28;

      hence thesis by A1, A3;

    end;

    theorem :: REWRITE2:12

    

     Th12: s ==>. (t,S) implies (u ^ s) ==>. ((u ^ t),S) & (s ^ u) ==>. ((t ^ u),S)

    proof

      given v, w, s1, t1 such that

       A1: s = ((v ^ s1) ^ w) and

       A2: t = ((v ^ t1) ^ w) and

       A3: s1 -->. (t1,S);

      

       A4: (u ^ t) = ((u ^ (v ^ t1)) ^ w) by A2, AFINSQ_1: 27

      .= (((u ^ v) ^ t1) ^ w) by AFINSQ_1: 27;

      (u ^ s) = ((u ^ (v ^ s1)) ^ w) by A1, AFINSQ_1: 27

      .= (((u ^ v) ^ s1) ^ w) by AFINSQ_1: 27;

      hence (u ^ s) ==>. ((u ^ t),S) by A3, A4;

      (s ^ u) = ((v ^ s1) ^ (w ^ u)) & (t ^ u) = ((v ^ t1) ^ (w ^ u)) by A1, A2, AFINSQ_1: 27;

      hence thesis by A3;

    end;

    theorem :: REWRITE2:13

    

     Th13: s ==>. (t,S) implies ((u ^ s) ^ v) ==>. (((u ^ t) ^ v),S)

    proof

      assume s ==>. (t,S);

      then (u ^ s) ==>. ((u ^ t),S) by Th12;

      hence thesis by Th12;

    end;

    theorem :: REWRITE2:14

    s -->. (t,S) implies (u ^ s) ==>. ((u ^ t),S) & (s ^ u) ==>. ((t ^ u),S)

    proof

      assume s -->. (t,S);

      then s ==>. (t,S) by Th10;

      hence thesis by Th12;

    end;

    theorem :: REWRITE2:15

    s -->. (t,S) implies ((u ^ s) ^ v) ==>. (((u ^ t) ^ v),S);

    theorem :: REWRITE2:16

    

     Th16: S is Thue-system of E & s -->. (t,S) implies t -->. (s,S)

    proof

      assume S is Thue-system of E & s -->. (t,S);

      then S = (S ~ ) & [s, t] in S by RELAT_2: 13;

      then [t, s] in S by RELAT_1:def 7;

      hence thesis;

    end;

    theorem :: REWRITE2:17

    

     Th17: S is Thue-system of E & s ==>. (t,S) implies t ==>. (s,S) by Th16;

    theorem :: REWRITE2:18

    S c= T & s -->. (t,S) implies s -->. (t,T);

    theorem :: REWRITE2:19

    

     Th19: S c= T & s ==>. (t,S) implies s ==>. (t,T)

    proof

      assume that

       A1: S c= T and

       A2: s ==>. (t,S);

      consider v, w, s1, t1 such that

       A3: s = ((v ^ s1) ^ w) & t = ((v ^ t1) ^ w) and

       A4: s1 -->. (t1,S) by A2;

      s1 -->. (t1,T) by A1, A4;

      hence thesis by A3;

    end;

    theorem :: REWRITE2:20

    

     Th20: not s ==>. (t,( {} ((E ^omega ),(E ^omega ))))

    proof

      assume s ==>. (t,( {} ((E ^omega ),(E ^omega ))));

      then

      consider v, w, s1, t1 such that s = ((v ^ s1) ^ w) and t = ((v ^ t1) ^ w) and

       A1: s1 -->. (t1,( {} ((E ^omega ),(E ^omega ))));

       [s1, t1] in ( {} ((E ^omega ),(E ^omega ))) by A1;

      hence contradiction by PARTIT_2:def 1;

    end;

    theorem :: REWRITE2:21

    

     Th21: s ==>. (t,(S \/ T)) implies s ==>. (t,S) or s ==>. (t,T)

    proof

      assume s ==>. (t,(S \/ T));

      then

      consider v, w, s1, t1 such that

       A1: s = ((v ^ s1) ^ w) & t = ((v ^ t1) ^ w) and

       A2: s1 -->. (t1,(S \/ T));

      

       A3: [s1, t1] in (S \/ T) by A2;

      per cases by A3, XBOOLE_0:def 3;

        suppose [s1, t1] in S;

        then s1 -->. (t1,S);

        hence thesis by A1;

      end;

        suppose [s1, t1] in T;

        then s1 -->. (t1,T);

        hence thesis by A1;

      end;

    end;

    begin

    definition

      let E;

      :: original: id

      redefine

      func id E -> Relation of E ;

      coherence by RELSET_1: 14;

    end

    definition

      let E, S;

      :: REWRITE2:def6

      func ==>.-relation (S) -> Relation of (E ^omega ) means

      : Def6: [s, t] in it iff s ==>. (t,S);

      existence

      proof

        defpred P[ Element of (E ^omega ), Element of (E ^omega )] means $1 ==>. ($2,S);

        consider R be Relation of (E ^omega ) such that

         A1: for s,t be Element of (E ^omega ) holds [s, t] in R iff P[s, t] from RELSET_1:sch 2;

        take R;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of (E ^omega ) such that

         A2: for s,t be Element of (E ^omega ) holds [s, t] in R1 iff s ==>. (t,S) and

         A3: for s,t be Element of (E ^omega ) holds [s, t] in R2 iff s ==>. (t,S);

        for s,t be Element of (E ^omega ) holds [s, t] in R1 iff [s, t] in R2 by A2, A3;

        hence thesis by RELSET_1:def 2;

      end;

    end

    theorem :: REWRITE2:22

    

     Th22: S c= ( ==>.-relation S)

    proof

      let x be object;

      assume

       A1: x in S;

      then

      consider a,b be object such that

       A2: a in (E ^omega ) & b in (E ^omega ) and

       A3: x = [a, b] by ZFMISC_1:def 2;

      reconsider a, b as Element of (E ^omega ) by A2;

      a -->. (b,S) by A1, A3;

      then a ==>. (b,S) by Th10;

      hence thesis by A3, Def6;

    end;

    theorem :: REWRITE2:23

    

     Th23: p is RedSequence of ( ==>.-relation S) implies (p +^ u) is RedSequence of ( ==>.-relation S) & (u ^+ p) is RedSequence of ( ==>.-relation S)

    proof

      assume

       A1: p is RedSequence of ( ==>.-relation S);

       A2:

      now

        let i be Nat such that

         A3: i in ( dom (p +^ u)) and

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

        

         A5: (i + 1) in ( dom p) by A4, Def3;

        then

         A6: ((p +^ u) . (i + 1)) = ((p . (i + 1)) ^ u) by Def3;

        

         A7: i in ( dom p) by A3, Def3;

        then [(p . i), (p . (i + 1))] in ( ==>.-relation S) by A1, A5, REWRITE1:def 2;

        then (p . i) ==>. ((p . (i + 1)),S) by Def6;

        then

         A8: ((p . i) ^ u) ==>. (((p . (i + 1)) ^ u),S) by Th12;

        ((p +^ u) . i) = ((p . i) ^ u) by A7, Def3;

        hence [((p +^ u) . i), ((p +^ u) . (i + 1))] in ( ==>.-relation S) by A6, A8, Def6;

      end;

       A9:

      now

        let i be Nat such that

         A10: i in ( dom (u ^+ p)) and

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

        

         A12: (i + 1) in ( dom p) by A11, Def2;

        then

         A13: ((u ^+ p) . (i + 1)) = (u ^ (p . (i + 1))) by Def2;

        

         A14: i in ( dom p) by A10, Def2;

        then [(p . i), (p . (i + 1))] in ( ==>.-relation S) by A1, A12, REWRITE1:def 2;

        then (p . i) ==>. ((p . (i + 1)),S) by Def6;

        then

         A15: (u ^ (p . i)) ==>. ((u ^ (p . (i + 1))),S) by Th12;

        ((u ^+ p) . i) = (u ^ (p . i)) by A14, Def2;

        hence [((u ^+ p) . i), ((u ^+ p) . (i + 1))] in ( ==>.-relation S) by A13, A15, Def6;

      end;

      ( len (p +^ u)) = ( len p) by Th5;

      hence (p +^ u) is RedSequence of ( ==>.-relation S) by A1, A2, REWRITE1:def 2;

      ( len (u ^+ p)) = ( len p) by Th5;

      hence thesis by A1, A9, REWRITE1:def 2;

    end;

    theorem :: REWRITE2:24

    p is RedSequence of ( ==>.-relation S) implies ((t ^+ p) +^ u) is RedSequence of ( ==>.-relation S)

    proof

      assume p is RedSequence of ( ==>.-relation S);

      then (t ^+ p) is RedSequence of ( ==>.-relation S) by Th23;

      hence thesis by Th23;

    end;

    theorem :: REWRITE2:25

    

     Th25: S is Thue-system of E implies ( ==>.-relation S) = (( ==>.-relation S) ~ )

    proof

      assume

       A1: S is Thue-system of E;

      now

        let x be object;

        thus x in ( ==>.-relation S) implies x in (( ==>.-relation S) ~ )

        proof

          assume

           A2: x in ( ==>.-relation S);

          then

          consider a,b be object such that

           A3: a in (E ^omega ) & b in (E ^omega ) and

           A4: x = [a, b] by ZFMISC_1:def 2;

          reconsider a, b as Element of (E ^omega ) by A3;

          a ==>. (b,S) by A2, A4, Def6;

          then b ==>. (a,S) by A1, Th17;

          then [b, a] in ( ==>.-relation S) by Def6;

          hence thesis by A4, RELAT_1:def 7;

        end;

        thus x in (( ==>.-relation S) ~ ) implies x in ( ==>.-relation S)

        proof

          assume

           A5: x in (( ==>.-relation S) ~ );

          then

          consider a,b be object such that

           A6: a in (E ^omega ) & b in (E ^omega ) and

           A7: x = [a, b] by ZFMISC_1:def 2;

          reconsider a, b as Element of (E ^omega ) by A6;

           [b, a] in ( ==>.-relation S) by A5, A7, RELAT_1:def 7;

          then b ==>. (a,S) by Def6;

          then a ==>. (b,S) by A1, Th17;

          hence thesis by A7, Def6;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: REWRITE2:26

    

     Th26: S c= T implies ( ==>.-relation S) c= ( ==>.-relation T)

    proof

      assume

       A1: S c= T;

      let x be object;

      assume

       A2: x in ( ==>.-relation S);

      then

      consider s,t be object such that

       A3: x = [s, t] and

       A4: s in (E ^omega ) & t in (E ^omega ) by RELSET_1: 2;

      reconsider s, t as Element of (E ^omega ) by A4;

      s ==>. (t,S) by A2, A3, Def6;

      then s ==>. (t,T) by A1, Th19;

      hence thesis by A3, Def6;

    end;

    theorem :: REWRITE2:27

    

     Th27: ( ==>.-relation ( id (E ^omega ))) = ( id (E ^omega ))

    proof

      

       A1: ( ==>.-relation ( id (E ^omega ))) c= ( id (E ^omega ))

      proof

        let x be object;

        assume

         A2: x in ( ==>.-relation ( id (E ^omega )));

        then

        consider a,b be object such that

         A3: a in (E ^omega ) & b in (E ^omega ) and

         A4: x = [a, b] by ZFMISC_1:def 2;

        reconsider a, b as Element of (E ^omega ) by A3;

        a ==>. (b,( id (E ^omega ))) by A2, A4, Def6;

        then

        consider v, w, s1, t1 such that

         A5: a = ((v ^ s1) ^ w) & b = ((v ^ t1) ^ w) and

         A6: s1 -->. (t1,( id (E ^omega )));

         [s1, t1] in ( id (E ^omega )) by A6;

        then s1 = t1 by RELAT_1:def 10;

        hence thesis by A4, A5, RELAT_1:def 10;

      end;

      ( id (E ^omega )) c= ( ==>.-relation ( id (E ^omega ))) by Th22;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: REWRITE2:28

    

     Th28: ( ==>.-relation (S \/ ( id (E ^omega )))) = (( ==>.-relation S) \/ ( id (E ^omega )))

    proof

      

       A1: ( ==>.-relation (S \/ ( id (E ^omega )))) c= (( ==>.-relation S) \/ ( id (E ^omega )))

      proof

        let x be object;

        assume

         A2: x in ( ==>.-relation (S \/ ( id (E ^omega ))));

        then

        consider a,b be object such that

         A3: a in (E ^omega ) & b in (E ^omega ) and

         A4: x = [a, b] by ZFMISC_1:def 2;

        reconsider a, b as Element of (E ^omega ) by A3;

        a ==>. (b,(S \/ ( id (E ^omega )))) by A2, A4, Def6;

        then

        consider v, w, s1, t1 such that

         A5: a = ((v ^ s1) ^ w) & b = ((v ^ t1) ^ w) and

         A6: s1 -->. (t1,(S \/ ( id (E ^omega ))));

        

         A7: [s1, t1] in (S \/ ( id (E ^omega ))) by A6;

        per cases by A7, XBOOLE_0:def 3;

          suppose [s1, t1] in S;

          then s1 -->. (t1,S);

          then ((v ^ s1) ^ w) ==>. (((v ^ t1) ^ w),S);

          then x in ( ==>.-relation S) by A4, A5, Def6;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose [s1, t1] in ( id (E ^omega ));

          then s1 = t1 by RELAT_1:def 10;

          then x in ( id (E ^omega )) by A4, A5, RELAT_1:def 10;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      (( ==>.-relation S) \/ ( id (E ^omega ))) c= ( ==>.-relation (S \/ ( id (E ^omega ))))

      proof

        let x be object;

        assume

         A8: x in (( ==>.-relation S) \/ ( id (E ^omega )));

        per cases by A8, XBOOLE_0:def 3;

          suppose

           A9: x in ( ==>.-relation S);

          ( ==>.-relation S) c= ( ==>.-relation (S \/ ( id (E ^omega )))) by Th26, XBOOLE_1: 7;

          hence thesis by A9;

        end;

          suppose

           A10: x in ( id (E ^omega ));

          

           A11: ( ==>.-relation ( id (E ^omega ))) c= ( ==>.-relation (S \/ ( id (E ^omega )))) by Th26, XBOOLE_1: 7;

          x in ( ==>.-relation ( id (E ^omega ))) by A10, Th27;

          hence thesis by A11;

        end;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: REWRITE2:29

    

     Th29: ( ==>.-relation ( {} ((E ^omega ),(E ^omega )))) = ( {} ((E ^omega ),(E ^omega )))

    proof

      

       A1: ( ==>.-relation ( {} ((E ^omega ),(E ^omega )))) c= ( {} ((E ^omega ),(E ^omega )))

      proof

        let x be object;

        assume

         A2: x in ( ==>.-relation ( {} ((E ^omega ),(E ^omega ))));

        then

        consider a,b be object such that

         A3: a in (E ^omega ) & b in (E ^omega ) and

         A4: x = [a, b] by ZFMISC_1:def 2;

        reconsider a, b as Element of (E ^omega ) by A3;

        a ==>. (b,( {} ((E ^omega ),(E ^omega )))) by A2, A4, Def6;

        hence thesis by Th20;

      end;

      ( {} ((E ^omega ),(E ^omega ))) = {} by PARTIT_2:def 1;

      then ( {} ((E ^omega ),(E ^omega ))) c= ( ==>.-relation ( {} ((E ^omega ),(E ^omega ))));

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: REWRITE2:30

    

     Th30: s ==>. (t,( ==>.-relation S)) implies s ==>. (t,S)

    proof

      assume s ==>. (t,( ==>.-relation S));

      then

      consider v, w, s1, t1 such that

       A1: s = ((v ^ s1) ^ w) & t = ((v ^ t1) ^ w) and

       A2: s1 -->. (t1,( ==>.-relation S));

       [s1, t1] in ( ==>.-relation S) by A2;

      then s1 ==>. (t1,S) by Def6;

      hence thesis by A1, Th13;

    end;

    theorem :: REWRITE2:31

    

     Th31: ( ==>.-relation ( ==>.-relation S)) = ( ==>.-relation S)

    proof

      

       A1: ( ==>.-relation ( ==>.-relation S)) c= ( ==>.-relation S)

      proof

        let x be object;

        assume

         A2: x in ( ==>.-relation ( ==>.-relation S));

        then

        consider a,b be object such that

         A3: a in (E ^omega ) & b in (E ^omega ) and

         A4: x = [a, b] by ZFMISC_1:def 2;

        reconsider a, b as Element of (E ^omega ) by A3;

        a ==>. (b,( ==>.-relation S)) by A2, A4, Def6;

        then a ==>. (b,S) by Th30;

        hence thesis by A4, Def6;

      end;

      ( ==>.-relation S) c= ( ==>.-relation ( ==>.-relation S)) by Th22;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    begin

    definition

      let E, S, s, t;

      :: REWRITE2:def7

      pred s ==>* t,S means ( ==>.-relation S) reduces (s,t);

    end

    theorem :: REWRITE2:32

    

     Th32: s ==>* (s,S) by REWRITE1: 12;

    theorem :: REWRITE2:33

    

     Th33: s ==>. (t,S) implies s ==>* (t,S)

    proof

      assume s ==>. (t,S);

      then [s, t] in ( ==>.-relation S) by Def6;

      then ( ==>.-relation S) reduces (s,t) by REWRITE1: 15;

      hence thesis;

    end;

    theorem :: REWRITE2:34

    s -->. (t,S) implies s ==>* (t,S) by Th10, Th33;

    theorem :: REWRITE2:35

    

     Th35: s ==>* (t,S) & t ==>* (u,S) implies s ==>* (u,S) by REWRITE1: 16;

    theorem :: REWRITE2:36

    

     Th36: s ==>* (t,S) implies (s ^ u) ==>* ((t ^ u),S) & (u ^ s) ==>* ((u ^ t),S)

    proof

      assume s ==>* (t,S);

      then ( ==>.-relation S) reduces (s,t);

      then

      consider p be RedSequence of ( ==>.-relation S) such that

       A1: (p . 1) = s and

       A2: (p . ( len p)) = t by REWRITE1:def 3;

      reconsider p as FinSequence of (E ^omega ) by A1, ABCMIZ_0: 73;

      1 in ( dom p) by FINSEQ_5: 6;

      then

       A3: ((p +^ u) . 1) = (s ^ u) by A1, Def3;

      

       A4: ( len p) = ( len (p +^ u)) by Th5;

      then ( len (p +^ u)) in ( dom p) by FINSEQ_5: 6;

      then

       A5: ((p +^ u) . ( len (p +^ u))) = (t ^ u) by A2, A4, Def3;

      (p +^ u) is RedSequence of ( ==>.-relation S) by Th23;

      then ( ==>.-relation S) reduces ((s ^ u),(t ^ u)) by A3, A5, REWRITE1:def 3;

      hence (s ^ u) ==>* ((t ^ u),S);

      1 in ( dom p) by FINSEQ_5: 6;

      then

       A6: ((u ^+ p) . 1) = (u ^ s) by A1, Def2;

      

       A7: ( len p) = ( len (u ^+ p)) by Th5;

      then ( len (u ^+ p)) in ( dom p) by FINSEQ_5: 6;

      then

       A8: ((u ^+ p) . ( len (u ^+ p))) = (u ^ t) by A2, A7, Def2;

      (u ^+ p) is RedSequence of ( ==>.-relation S) by Th23;

      then ( ==>.-relation S) reduces ((u ^ s),(u ^ t)) by A6, A8, REWRITE1:def 3;

      hence thesis;

    end;

    theorem :: REWRITE2:37

    

     Th37: s ==>* (t,S) implies ((u ^ s) ^ v) ==>* (((u ^ t) ^ v),S)

    proof

      assume s ==>* (t,S);

      then (u ^ s) ==>* ((u ^ t),S) by Th36;

      hence thesis by Th36;

    end;

    theorem :: REWRITE2:38

    s ==>* (t,S) & u ==>* (v,S) implies (s ^ u) ==>* ((t ^ v),S) & (u ^ s) ==>* ((v ^ t),S)

    proof

      assume

       A1: s ==>* (t,S) & u ==>* (v,S);

      then (s ^ u) ==>* ((t ^ u),S) & (t ^ u) ==>* ((t ^ v),S) by Th36;

      hence (s ^ u) ==>* ((t ^ v),S) by Th35;

      (u ^ s) ==>* ((u ^ t),S) & (u ^ t) ==>* ((v ^ t),S) by A1, Th36;

      hence thesis by Th35;

    end;

    theorem :: REWRITE2:39

    S is Thue-system of E & s ==>* (t,S) implies t ==>* (s,S)

    proof

      assume that

       A1: S is Thue-system of E and

       A2: s ==>* (t,S);

      ( ==>.-relation S) reduces (s,t) by A2;

      then

      consider p be RedSequence of ( ==>.-relation S) such that

       A3: (p . 1) = s and

       A4: (p . ( len p)) = t by REWRITE1:def 3;

      set q = ( Rev p);

      (q . ( len p)) = s by A3, FINSEQ_5: 62;

      then

       A5: (q . ( len q)) = s by FINSEQ_5:def 3;

      q is RedSequence of (( ==>.-relation S) ~ ) by REWRITE1: 9;

      then

       A6: q is RedSequence of ( ==>.-relation S) by A1, Th25;

      (q . 1) = t by A4, FINSEQ_5: 62;

      then ( ==>.-relation S) reduces (t,s) by A6, A5, REWRITE1:def 3;

      hence thesis;

    end;

    theorem :: REWRITE2:40

    

     Th40: S c= T & s ==>* (t,S) implies s ==>* (t,T) by Th26, REWRITE1: 22;

    theorem :: REWRITE2:41

    

     Th41: s ==>* (t,S) iff s ==>* (t,(S \/ ( id (E ^omega ))))

    proof

      thus s ==>* (t,S) implies s ==>* (t,(S \/ ( id (E ^omega )))) by Th40, XBOOLE_1: 7;

      assume s ==>* (t,(S \/ ( id (E ^omega ))));

      then ( ==>.-relation (S \/ ( id (E ^omega )))) reduces (s,t);

      then (( ==>.-relation S) \/ ( id (E ^omega ))) reduces (s,t) by Th28;

      then ( ==>.-relation S) reduces (s,t) by REWRITE1: 23;

      hence thesis;

    end;

    theorem :: REWRITE2:42

    

     Th42: s ==>* (t,( {} ((E ^omega ),(E ^omega )))) implies s = t

    proof

      assume s ==>* (t,( {} ((E ^omega ),(E ^omega ))));

      then ( ==>.-relation ( {} ((E ^omega ),(E ^omega )))) reduces (s,t);

      then ( {} ((E ^omega ),(E ^omega ))) reduces (s,t) by Th29;

      then {} reduces (s,t) by PARTIT_2:def 1;

      hence thesis by REWRITE1: 13;

    end;

    theorem :: REWRITE2:43

    

     Th43: s ==>* (t,( ==>.-relation S)) implies s ==>* (t,S) by Th31;

    theorem :: REWRITE2:44

    

     Th44: s ==>* (t,S) & u ==>. (v, { [s, t]}) implies u ==>* (v,S)

    proof

      assume that

       A1: s ==>* (t,S) and

       A2: u ==>. (v, { [s, t]});

      consider u1, v1, s1, t1 such that

       A3: u = ((u1 ^ s1) ^ v1) & v = ((u1 ^ t1) ^ v1) and

       A4: s1 -->. (t1, { [s, t]}) by A2;

       [s1, t1] in { [s, t]} by A4;

      then [s1, t1] = [s, t] by TARSKI:def 1;

      then s1 = s & t1 = t by XTUPLE_0: 1;

      hence thesis by A1, A3, Th37;

    end;

    theorem :: REWRITE2:45

    

     Th45: s ==>* (t,S) & u ==>* (v,(S \/ { [s, t]})) implies u ==>* (v,S)

    proof

      assume that

       A1: s ==>* (t,S) and

       A2: u ==>* (v,(S \/ { [s, t]}));

      ( ==>.-relation (S \/ { [s, t]})) reduces (u,v) by A2;

      then

       A3: ex p2 be RedSequence of ( ==>.-relation (S \/ { [s, t]})) st (p2 . 1) = u & (p2 . ( len p2)) = v by REWRITE1:def 3;

      defpred P[ Nat] means for p be RedSequence of ( ==>.-relation (S \/ { [s, t]})), s1, t1 st ( len p) = $1 & (p . 1) = s1 & (p . ( len p)) = t1 holds ex q be RedSequence of ( ==>.-relation S) st (q . 1) = s1 & (q . ( len q)) = t1;

       A4:

      now

        let k;

        assume

         A5: P[k];

        thus P[(k + 1)]

        proof

          let p be RedSequence of ( ==>.-relation (S \/ { [s, t]})), s1, t1 such that

           A6: ( len p) = (k + 1) and

           A7: (p . 1) = s1 and

           A8: (p . ( len p)) = t1;

          per cases ;

            suppose not k in ( dom p) & (k + 1) in ( dom p);

            then k = 0 by Th1;

            then p = <*s1*> by A6, A7, FINSEQ_1: 40;

            then

            reconsider p as RedSequence of ( ==>.-relation S) by REWRITE1: 6;

            take p;

            thus thesis by A7, A8;

          end;

            suppose not (k + 1) in ( dom p);

            then ( 0 + 1) > (k + 1) by A6, FINSEQ_3: 25;

            hence thesis by XREAL_1: 6;

          end;

            suppose

             A9: k in ( dom p) & (k + 1) in ( dom p);

            set w = (p . k);

            

             A10: [(p . k), (p . (k + 1))] in ( ==>.-relation (S \/ { [s, t]})) by A9, REWRITE1:def 2;

            then

            reconsider w as Element of (E ^omega ) by ZFMISC_1: 87;

            

             A11: w ==>. (t1,(S \/ { [s, t]})) by A6, A8, A10, Def6;

            

             A12: w ==>* (t1,S)

            proof

              per cases by A11, Th21;

                suppose w ==>. (t1,S);

                hence thesis by Th33;

              end;

                suppose w ==>. (t1, { [s, t]});

                hence thesis by A1, Th44;

              end;

            end;

            ex p1 be RedSequence of ( ==>.-relation (S \/ { [s, t]})) st ( len p1) = k & (p1 . 1) = s1 & (p1 . ( len p1)) = w by A7, A9, Th4;

            then ex q be RedSequence of ( ==>.-relation S) st (q . 1) = s1 & (q . ( len q)) = w by A5;

            then ( ==>.-relation S) reduces (s1,w) by REWRITE1:def 3;

            then s1 ==>* (w,S);

            then s1 ==>* (t1,S) by A12, Th35;

            then ( ==>.-relation S) reduces (s1,t1);

            hence thesis by REWRITE1:def 3;

          end;

        end;

      end;

      

       A13: P[ 0 ] by REWRITE1:def 2;

      for k holds P[k] from NAT_1:sch 2( A13, A4);

      then ex q be RedSequence of ( ==>.-relation S) st (q . 1) = u & (q . ( len q)) = v by A3;

      then ( ==>.-relation S) reduces (u,v) by REWRITE1:def 3;

      hence thesis;

    end;

    begin

    definition

      let E, S, w;

      :: REWRITE2:def8

      func Lang (w,S) -> Subset of (E ^omega ) equals { s : w ==>* (s,S) };

      coherence

      proof

        set X = { s : w ==>* (s,S) };

        X c= (E ^omega )

        proof

          let x be object;

          assume x in X;

          then ex t st t = x & w ==>* (t,S);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: REWRITE2:46

    

     Th46: s in ( Lang (w,S)) iff w ==>* (s,S)

    proof

      thus s in ( Lang (w,S)) implies w ==>* (s,S)

      proof

        assume s in ( Lang (w,S));

        then ex t st t = s & w ==>* (t,S);

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: REWRITE2:47

    

     Th47: w in ( Lang (w,S))

    proof

      w ==>* (w,S) by Th32;

      hence thesis;

    end;

    registration

      let E be non empty set;

      let S be semi-Thue-system of E;

      let w be Element of (E ^omega );

      cluster ( Lang (w,S)) -> non empty;

      coherence by Th47;

    end

    theorem :: REWRITE2:48

    

     Th48: S c= T implies ( Lang (w,S)) c= ( Lang (w,T))

    proof

      assume

       A1: S c= T;

      let x be object;

      assume

       A2: x in ( Lang (w,S));

      then

      reconsider y = x as Element of (E ^omega );

      w ==>* (y,S) by A2, Th46;

      then w ==>* (y,T) by A1, Th40;

      hence thesis;

    end;

    theorem :: REWRITE2:49

    

     Th49: ( Lang (w,S)) = ( Lang (w,(S \/ ( id (E ^omega )))))

    proof

      

       A1: ( Lang (w,(S \/ ( id (E ^omega ))))) c= ( Lang (w,S))

      proof

        let x be object;

        assume

         A2: x in ( Lang (w,(S \/ ( id (E ^omega )))));

        then

        reconsider s = x as Element of (E ^omega );

        w ==>* (s,(S \/ ( id (E ^omega )))) by A2, Th46;

        then w ==>* (s,S) by Th41;

        hence thesis;

      end;

      ( Lang (w,S)) c= ( Lang (w,(S \/ ( id (E ^omega ))))) by Th48, XBOOLE_1: 7;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: REWRITE2:50

    

     Th50: ( Lang (w,( {} ((E ^omega ),(E ^omega ))))) = {w}

    proof

      for x holds not (x <> w & x in ( Lang (w,( {} ((E ^omega ),(E ^omega )))))) by Th46, Th42;

      then for x be object holds x in ( Lang (w,( {} ((E ^omega ),(E ^omega ))))) iff x = w by Th47;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: REWRITE2:51

    ( Lang (w,( id (E ^omega )))) = {w}

    proof

      (( {} ((E ^omega ),(E ^omega ))) \/ ( id (E ^omega ))) = ( {} \/ ( id (E ^omega ))) by PARTIT_2:def 1

      .= ( id (E ^omega ));

      

      hence ( Lang (w,( id (E ^omega )))) = ( Lang (w,( {} ((E ^omega ),(E ^omega ))))) by Th49

      .= {w} by Th50;

    end;

    begin

    definition

      let E, S, T, w;

      :: REWRITE2:def9

      pred S,T are_equivalent_wrt w means ( Lang (w,S)) = ( Lang (w,T));

    end

    theorem :: REWRITE2:52

    (S,S) are_equivalent_wrt w;

    theorem :: REWRITE2:53

    (S,T) are_equivalent_wrt w implies (T,S) are_equivalent_wrt w;

    theorem :: REWRITE2:54

    (S,T) are_equivalent_wrt w & (T,U) are_equivalent_wrt w implies (S,U) are_equivalent_wrt w;

    theorem :: REWRITE2:55

    (S,(S \/ ( id (E ^omega )))) are_equivalent_wrt w by Th49;

    theorem :: REWRITE2:56

    

     Th56: (S,T) are_equivalent_wrt w & S c= U & U c= T implies (S,U) are_equivalent_wrt w & (U,T) are_equivalent_wrt w

    proof

      assume that

       A1: ( Lang (w,S)) = ( Lang (w,T)) and

       A2: S c= U & U c= T;

      ( Lang (w,S)) c= ( Lang (w,U)) & ( Lang (w,U)) c= ( Lang (w,T)) by A2, Th48;

      hence ( Lang (w,S)) = ( Lang (w,U)) by A1, XBOOLE_0:def 10;

      hence thesis by A1;

    end;

    theorem :: REWRITE2:57

    

     Th57: (S,( ==>.-relation S)) are_equivalent_wrt w

    proof

      

       A1: ( Lang (w,( ==>.-relation S))) c= ( Lang (w,S))

      proof

        let x be object such that

         A2: x in ( Lang (w,( ==>.-relation S)));

        reconsider s = x as Element of (E ^omega ) by A2;

        w ==>* (s,( ==>.-relation S)) by A2, Th46;

        then w ==>* (s,S) by Th43;

        hence thesis;

      end;

      ( Lang (w,S)) c= ( Lang (w,( ==>.-relation S))) by Th22, Th48;

      hence ( Lang (w,S)) = ( Lang (w,( ==>.-relation S))) by A1, XBOOLE_0:def 10;

    end;

    theorem :: REWRITE2:58

    

     Th58: (S,T) are_equivalent_wrt w & ( ==>.-relation (S \/ T)) reduces (w,s) implies ( ==>.-relation S) reduces (w,s)

    proof

      assume that

       A1: ( Lang (w,S)) = ( Lang (w,T)) and

       A2: ( ==>.-relation (S \/ T)) reduces (w,s);

      

       A3: ex p be RedSequence of ( ==>.-relation (S \/ T)) st (p . 1) = w & (p . ( len p)) = s by A2, REWRITE1:def 3;

      defpred P[ Nat] means for p be RedSequence of ( ==>.-relation (S \/ T)), t st ( len p) = $1 & (p . 1) = w & (p . ( len p)) = t holds ex q be RedSequence of ( ==>.-relation S) st (q . 1) = w & (q . ( len q)) = t;

       A4:

      now

        let k;

        assume

         A5: P[k];

        thus P[(k + 1)]

        proof

          let p be RedSequence of ( ==>.-relation (S \/ T)), t such that

           A6: ( len p) = (k + 1) and

           A7: (p . 1) = w and

           A8: (p . ( len p)) = t;

          per cases ;

            suppose not k in ( dom p) & (k + 1) in ( dom p);

            then k = 0 by Th1;

            then p = <*w*> by A6, A7, FINSEQ_1: 40;

            then

            reconsider p as RedSequence of ( ==>.-relation S) by REWRITE1: 6;

            take p;

            thus thesis by A7, A8;

          end;

            suppose not (k + 1) in ( dom p);

            then ( 0 + 1) > (k + 1) by A6, FINSEQ_3: 25;

            hence thesis by XREAL_1: 6;

          end;

            suppose

             A9: k in ( dom p) & (k + 1) in ( dom p);

            set u = (p . k);

            

             A10: [(p . k), (p . (k + 1))] in ( ==>.-relation (S \/ T)) by A9, REWRITE1:def 2;

            then

            reconsider u as Element of (E ^omega ) by ZFMISC_1: 87;

            

             A11: u ==>. (t,(S \/ T)) by A6, A8, A10, Def6;

            ex p1 be RedSequence of ( ==>.-relation (S \/ T)) st ( len p1) = k & (p1 . 1) = w & (p1 . ( len p1)) = u by A7, A9, Th4;

            then ex q be RedSequence of ( ==>.-relation S) st (q . 1) = w & (q . ( len q)) = u by A5;

            then ( ==>.-relation S) reduces (w,u) by REWRITE1:def 3;

            then

             A12: w ==>* (u,S);

            per cases by A11, Th21;

              suppose u ==>. (t,S);

              then u ==>* (t,S) by Th33;

              then w ==>* (t,S) by A12, Th35;

              then ( ==>.-relation S) reduces (w,t);

              hence thesis by REWRITE1:def 3;

            end;

              suppose

               A13: u ==>. (t,T);

              u in ( Lang (w,S)) by A12;

              then

               A14: w ==>* (u,T) by A1, Th46;

              u ==>* (t,T) by A13, Th33;

              then w ==>* (t,T) by A14, Th35;

              then t in ( Lang (w,T));

              then w ==>* (t,S) by A1, Th46;

              then ( ==>.-relation S) reduces (w,t);

              hence thesis by REWRITE1:def 3;

            end;

          end;

        end;

      end;

      

       A15: P[ 0 ] by REWRITE1:def 2;

      for k holds P[k] from NAT_1:sch 2( A15, A4);

      then ex q be RedSequence of ( ==>.-relation S) st (q . 1) = w & (q . ( len q)) = s by A3;

      hence thesis by REWRITE1:def 3;

    end;

    theorem :: REWRITE2:59

    

     Th59: (S,T) are_equivalent_wrt w & w ==>* (s,(S \/ T)) implies w ==>* (s,S) by Th58;

    theorem :: REWRITE2:60

    

     Th60: (S,T) are_equivalent_wrt w implies (S,(S \/ T)) are_equivalent_wrt w

    proof

      assume

       A1: (S,T) are_equivalent_wrt w;

      

       A2: ( Lang (w,(S \/ T))) c= ( Lang (w,S))

      proof

        let x be object such that

         A3: x in ( Lang (w,(S \/ T)));

        reconsider s = x as Element of (E ^omega ) by A3;

        w ==>* (s,(S \/ T)) by A3, Th46;

        then w ==>* (s,S) by A1, Th59;

        hence thesis;

      end;

      ( Lang (w,S)) c= ( Lang (w,(S \/ T))) by Th48, XBOOLE_1: 7;

      hence ( Lang (w,S)) = ( Lang (w,(S \/ T))) by A2, XBOOLE_0:def 10;

    end;

    theorem :: REWRITE2:61

    s ==>. (t,S) implies (S,(S \/ { [s, t]})) are_equivalent_wrt w

    proof

      assume s ==>. (t,S);

      then [s, t] in ( ==>.-relation S) by Def6;

      then { [s, t]} c= ( ==>.-relation S) by ZFMISC_1: 31;

      then

       A1: (S \/ { [s, t]}) c= (S \/ ( ==>.-relation S)) by XBOOLE_1: 9;

      (S,(S \/ ( ==>.-relation S))) are_equivalent_wrt w & S c= (S \/ { [s, t]}) by Th57, Th60, XBOOLE_1: 7;

      hence thesis by A1, Th56;

    end;

    theorem :: REWRITE2:62

    s ==>* (t,S) implies (S,(S \/ { [s, t]})) are_equivalent_wrt w

    proof

      assume

       A1: s ==>* (t,S);

      

       A2: ( Lang (w,(S \/ { [s, t]}))) c= ( Lang (w,S))

      proof

        let x be object such that

         A3: x in ( Lang (w,(S \/ { [s, t]})));

        reconsider u = x as Element of (E ^omega ) by A3;

        w ==>* (u,(S \/ { [s, t]})) by A3, Th46;

        then w ==>* (u,S) by A1, Th45;

        hence thesis;

      end;

      ( Lang (w,S)) c= ( Lang (w,(S \/ { [s, t]}))) by Th48, XBOOLE_1: 7;

      hence ( Lang (w,S)) = ( Lang (w,(S \/ { [s, t]}))) by A2, XBOOLE_0:def 10;

    end;