rewrite3.miz



    begin

    reserve x,x1,x2,y,y1,y2,z,z1,z2 for object,

X,X1,X2 for set;

    reserve E for non empty set;

    reserve e for Element of E;

    reserve u,u9,u1,u2,v,v1,v2,w,w1,w2 for Element of (E ^omega );

    reserve F,F1,F2 for Subset of (E ^omega );

    reserve i,k,l,n for Nat;

    theorem :: REWRITE3:1

    

     Th1: for p be FinSequence st k in ( dom p) holds (( <*x*> ^ p) . (k + 1)) = (p . k)

    proof

      let p be FinSequence such that

       A1: k in ( dom p);

      k >= 1 by A1, FINSEQ_3: 25;

      then k >= ( len <*x*>) by FINSEQ_1: 39;

      then

       A2: (( len <*x*>) + 0 ) < (k + 1) by XREAL_1: 8;

      (( len <*x*>) + k) in ( dom ( <*x*> ^ p)) by A1, FINSEQ_1: 28;

      then (k + 1) in ( dom ( <*x*> ^ p)) by FINSEQ_1: 39;

      then (k + 1) <= ( len ( <*x*> ^ p)) by FINSEQ_3: 25;

      

      then (( <*x*> ^ p) . (k + 1)) = (p . ((k + 1) - ( len <*x*>))) by A2, FINSEQ_1: 24

      .= (p . ((k + 1) - 1)) by FINSEQ_1: 39

      .= (p . (k + (1 - 1)));

      hence thesis;

    end;

    theorem :: REWRITE3:2

    

     Th2: for p be FinSequence holds p <> {} implies ex q be FinSequence, x st p = (q ^ <*x*>) & ( len p) = (( len q) + 1)

    proof

      let p be FinSequence;

      assume p <> {} ;

      then

      consider q be FinSequence, x be object such that

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

      take q, x;

      ( len p) = (( len q) + ( len <*x*>)) by A1, FINSEQ_1: 22

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

      hence thesis by A1;

    end;

    theorem :: REWRITE3:3

    

     Th3: for p be FinSequence st k in ( dom p) & not (k + 1) in ( dom p) holds ( len p) = k

    proof

      let p be FinSequence such that

       A1: k in ( dom p) and

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

      

       A3: 1 > (k + 1) or (k + 1) > ( len p) by A2, FINSEQ_3: 25;

      

       A4: (1 + 0 ) <= (k + 1) by XREAL_1: 7;

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

      hence thesis by A3, A4, NAT_1: 22;

    end;

    begin

    theorem :: REWRITE3:4

    

     Th4: for R be Relation, P be RedSequence of R, q1,q2 be FinSequence st P = (q1 ^ q2) & ( len q1) > 0 & ( len q2) > 0 holds q1 is RedSequence of R & q2 is RedSequence of R

    proof

      let R be Relation, P be RedSequence of R, q1,q2 be FinSequence such that

       A1: P = (q1 ^ q2) and

       A2: ( len q1) > 0 and

       A3: ( len q2) > 0 ;

      now

        let i be Nat;

        assume that

         A4: i in ( dom q1) and

         A5: (i + 1) in ( dom q1);

        

         A6: (i + 1) <= ( len q1) by A5, FINSEQ_3: 25;

        

         A7: 1 <= (i + 1) by A5, FINSEQ_3: 25;

        then

         A8: (q1 . (i + 1)) = ((q1 ^ q2) . (i + 1)) by A6, FINSEQ_1: 64;

        

         A9: ( len q1) <= ( len P) by A1, CALCUL_1: 6;

        then (i + 1) <= ( len P) by A6, XXREAL_0: 2;

        then

         A10: (i + 1) in ( dom P) by A7, FINSEQ_3: 25;

        

         A11: 1 <= i by A4, FINSEQ_3: 25;

        

         A12: i <= ( len q1) by A4, FINSEQ_3: 25;

        then i <= ( len P) by A9, XXREAL_0: 2;

        then

         A13: i in ( dom P) by A11, FINSEQ_3: 25;

        (q1 . i) = ((q1 ^ q2) . i) by A11, A12, FINSEQ_1: 64;

        hence [(q1 . i), (q1 . (i + 1))] in R by A1, A8, A13, A10, REWRITE1:def 2;

      end;

      hence q1 is RedSequence of R by A2, REWRITE1:def 2;

      now

        let i be Nat;

        assume that

         A14: i in ( dom q2) and

         A15: (i + 1) in ( dom q2);

        

         A16: 1 <= (i + 1) by A15, FINSEQ_3: 25;

        then

         A17: 1 <= ((i + 1) + ( len q1)) by NAT_1: 12;

        

         A18: 1 <= i by A14, FINSEQ_3: 25;

        then

         A19: 1 <= (i + ( len q1)) by NAT_1: 12;

        

         A20: (i + 1) <= ( len q2) by A15, FINSEQ_3: 25;

        then

         A21: (q2 . (i + 1)) = ((q1 ^ q2) . (( len q1) + (i + 1))) by A16, FINSEQ_1: 65;

        

         A22: (( len q1) + ( len q2)) = ( len P) by A1, FINSEQ_1: 22;

        then (( len q1) + (i + 1)) <= ((( len P) - ( len q2)) + ( len q2)) by A20, XREAL_1: 7;

        then

         A23: ((( len q1) + i) + 1) in ( dom P) by A17, FINSEQ_3: 25;

        

         A24: i <= ( len q2) by A14, FINSEQ_3: 25;

        then (( len q1) + i) <= ((( len P) - ( len q2)) + ( len q2)) by A22, XREAL_1: 7;

        then

         A25: (( len q1) + i) in ( dom P) by A19, FINSEQ_3: 25;

        (q2 . i) = ((q1 ^ q2) . (( len q1) + i)) by A18, A24, FINSEQ_1: 65;

        hence [(q2 . i), (q2 . (i + 1))] in R by A1, A21, A25, A23, REWRITE1:def 2;

      end;

      hence q2 is RedSequence of R by A3, REWRITE1:def 2;

    end;

    theorem :: REWRITE3:5

    

     Th5: for R be Relation, P be RedSequence of R st ( len P) > 1 holds ex Q be RedSequence of R st ( <*(P . 1)*> ^ Q) = P & (( len Q) + 1) = ( len P)

    proof

      let R be Relation, P be RedSequence of R such that

       A1: ( len P) > 1;

      consider x be object, Q be FinSequence such that

       A2: P = ( <*x*> ^ Q) and

       A3: ( len P) = (( len Q) + 1) by REWRITE1: 5;

      (1 + ( len Q)) > (1 + 0 ) by A1, A3;

      then ( len <*x*>) = 1 & ( len Q) > 0 by FINSEQ_1: 39;

      then

       A4: Q is RedSequence of R by A2, Th4;

      (P . 1) = x by A2, FINSEQ_1: 41;

      hence thesis by A2, A3, A4;

    end;

    theorem :: REWRITE3:6

    for R be Relation, P be RedSequence of R st ( len P) > 1 holds ex Q be RedSequence of R st (Q ^ <*(P . ( len P))*>) = P & (( len Q) + 1) = ( len P)

    proof

      let R be Relation, P be RedSequence of R such that

       A1: ( len P) > 1;

      consider Q be FinSequence, x such that

       A2: P = (Q ^ <*x*>) and

       A3: (( len Q) + 1) = ( len P) by Th2;

      (1 + ( len Q)) > (1 + 0 ) by A1, A3;

      then ( len <*x*>) = 1 & ( len Q) > 0 by FINSEQ_1: 39;

      then

       A4: Q is RedSequence of R by A2, Th4;

      (P . ( len P)) = x by A2, A3, FINSEQ_1: 42;

      hence thesis by A2, A3, A4;

    end;

    theorem :: REWRITE3:7

    for R be Relation, P be RedSequence of R st ( len P) > 1 holds ex Q be RedSequence of R st (( len Q) + 1) = ( len P) & for k st k in ( dom Q) holds (Q . k) = (P . (k + 1))

    proof

      let R be Relation, P be RedSequence of R;

      assume ( len P) > 1;

      then

      consider Q be RedSequence of R such that

       A1: P = ( <*(P . 1)*> ^ Q) & (( len Q) + 1) = ( len P) by Th5;

      take Q;

      thus thesis by A1, Th1;

    end;

    theorem :: REWRITE3:8

    

     Th8: for R be Relation holds <*x, y*> is RedSequence of R implies [x, y] in R

    proof

      let R be Relation;

      set P = <*x, y*>;

      

       A1: (P . 1) = x & (P . 2) = y by FINSEQ_1: 44;

      ( len P) = 2 by FINSEQ_1: 44;

      then

       A2: 1 in ( dom P) & (1 + 1) in ( dom P) by FINSEQ_3: 25;

      assume <*x, y*> is RedSequence of R;

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

    end;

    begin

    theorem :: REWRITE3:9

    

     Th9: w = (u ^ v) implies ( len u) <= ( len w) & ( len v) <= ( len w)

    proof

      assume w = (u ^ v);

      then ( len w) = (( len u) + ( len v)) by AFINSQ_1: 17;

      then (( len w) + ( len u)) >= ((( len u) + ( len v)) + 0 ) & (( len w) + ( len v)) >= ((( len u) + ( len v)) + 0 ) by XREAL_1: 7;

      hence thesis by XREAL_1: 6;

    end;

    theorem :: REWRITE3:10

    

     Th10: w = (u ^ v) & u <> ( <%> E) & v <> ( <%> E) implies ( len u) < ( len w) & ( len v) < ( len w)

    proof

      assume that

       A1: w = (u ^ v) and

       A2: u <> ( <%> E) and

       A3: v <> ( <%> E);

      

       A4: ( len w) = (( len u) + ( len v)) by A1, AFINSQ_1: 17;

      then (( len w) + ( len u)) > ((( len u) + ( len v)) + 0 ) by A2, XREAL_1: 8;

      hence thesis by A3, A4, XREAL_1: 6, XREAL_1: 8;

    end;

    theorem :: REWRITE3:11

    (w1 ^ v1) = (w2 ^ v2) & (( len w1) = ( len w2) or ( len v1) = ( len v2)) implies w1 = w2 & v1 = v2

    proof

      assume that

       A1: (w1 ^ v1) = (w2 ^ v2) and

       A2: ( len w1) = ( len w2) or ( len v1) = ( len v2);

      

       A3: (( len w1) + ( len v1)) = ( len (w2 ^ v2)) by A1, AFINSQ_1: 17

      .= (( len w2) + ( len v2)) by AFINSQ_1: 17;

      now

        let k be Nat;

        assume

         A4: k in ( dom w1);

        

        hence (w1 . k) = ((w2 ^ v2) . k) by A1, AFINSQ_1:def 3

        .= (w2 . k) by A2, A3, A4, AFINSQ_1:def 3;

      end;

      hence w1 = w2 by A2, A3, AFINSQ_1: 8;

      hence thesis by A1, AFINSQ_1: 28;

    end;

    theorem :: REWRITE3:12

    

     Th12: (w1 ^ v1) = (w2 ^ v2) & (( len w1) <= ( len w2) or ( len v1) >= ( len v2)) implies ex u st (w1 ^ u) = w2 & v1 = (u ^ v2)

    proof

      assume that

       A1: (w1 ^ v1) = (w2 ^ v2) and

       A2: ( len w1) <= ( len w2) or ( len v1) >= ( len v2);

      (( len w1) + ( len v1)) = ( len (w2 ^ v2)) by A1, AFINSQ_1: 17

      .= (( len w2) + ( len v2)) by AFINSQ_1: 17;

      then ( len v1) >= ( len v2) implies ((( len w1) + ( len v1)) - ( len v1)) <= ((( len w2) + ( len v2)) - ( len v2)) by XREAL_1: 13;

      then

      consider u9 be XFinSequence such that

       A3: (w1 ^ u9) = w2 by A1, A2, AFINSQ_1: 41;

      reconsider u = u9 as Element of (E ^omega ) by A3, FLANG_1: 5;

      take u;

      thus (w1 ^ u) = w2 by A3;

      (w2 ^ v2) = (w1 ^ (u ^ v2)) by A3, AFINSQ_1: 27;

      hence thesis by A1, AFINSQ_1: 28;

    end;

    theorem :: REWRITE3:13

    

     Th13: (w1 ^ v1) = (w2 ^ v2) implies (ex u st (w1 ^ u) = w2 & v1 = (u ^ v2)) or ex u st (w2 ^ u) = w1 & v2 = (u ^ v1)

    proof

      

       A1: ( len w1) < ( len w2) or ( len w1) >= ( len w2);

      assume (w1 ^ v1) = (w2 ^ v2);

      hence thesis by A1, Th12;

    end;

    begin

    definition

      let X;

      struct ( 1-sorted) transition-system over X (# the carrier -> set,

the Tran -> Relation of [: the carrier, X:], the carrier #)

       attr strict strict;

    end

    definition

      let E, F;

      let TS be transition-system over F;

      :: REWRITE3:def1

      attr TS is deterministic means

      : Def1: the Tran of TS is Function & not ( <%> E) in ( rng ( dom the Tran of TS)) & for s be Element of TS, u, v st u <> v & [s, u] in ( dom the Tran of TS) & [s, v] in ( dom the Tran of TS) holds not ex w st (u ^ w) = v or (v ^ w) = u;

    end

    theorem :: REWRITE3:14

    for TS be transition-system over F holds ( dom the Tran of TS) = {} implies TS is deterministic

    proof

      let TS be transition-system over F;

      assume ( dom the Tran of TS) = {} ;

      then the Tran of TS = {} & for s be Element of TS, u, v st u <> v & [s, u] in ( dom the Tran of TS) & [s, v] in ( dom the Tran of TS) holds not ex w st (u ^ w) = v or (v ^ w) = u;

      hence thesis;

    end;

    registration

      let E, F;

      cluster strict non empty finite deterministic for transition-system over F;

      existence

      proof

        set X = the non empty finite set;

        reconsider T = {} as Relation of [:X, F:], X by RELSET_1: 12;

        take TS = transition-system (# X, T #);

        thus TS is strict;

        thus TS is non empty;

        thus the carrier of TS is finite;

        thus TS is deterministic;

      end;

    end

    begin

    definition

      let X;

      let TS be transition-system over X;

      let x,y,z be object;

      :: REWRITE3:def2

      pred x,y -->. z,TS means [ [x, y], z] in the Tran of TS;

    end

    theorem :: REWRITE3:15

    

     Th15: for TS be transition-system over X holds (x,y) -->. (z,TS) implies x in TS & y in X & z in TS & x in ( dom ( dom the Tran of TS)) & y in ( rng ( dom the Tran of TS)) & z in ( rng the Tran of TS)

    proof

      let TS be transition-system over X;

      assume (x,y) -->. (z,TS);

      then

       A1: [ [x, y], z] in the Tran of TS;

      then [x, y] in [:the carrier of TS, X:] by ZFMISC_1: 87;

      hence x in the carrier of TS & y in X & z in the carrier of TS by A1, ZFMISC_1: 87;

       [x, y] in ( dom the Tran of TS) by A1, XTUPLE_0:def 12;

      hence x in ( dom ( dom the Tran of TS)) & y in ( rng ( dom the Tran of TS)) by XTUPLE_0:def 12, XTUPLE_0:def 13;

      thus z in ( rng the Tran of TS) by A1, XTUPLE_0:def 13;

    end;

    theorem :: REWRITE3:16

    for TS1 be transition-system over X1, TS2 be transition-system over X2 st the Tran of TS1 = the Tran of TS2 holds (x,y) -->. (z,TS1) implies (x,y) -->. (z,TS2);

    theorem :: REWRITE3:17

    

     Th17: for TS be transition-system over F st the Tran of TS is Function holds (x,y) -->. (z1,TS) & (x,y) -->. (z2,TS) implies z1 = z2 by FUNCT_1:def 1;

    theorem :: REWRITE3:18

    for TS be transition-system over F st not ( <%> E) in ( rng ( dom the Tran of TS)) holds not (x,( <%> E)) -->. (y,TS)

    proof

      let TS be transition-system over F such that

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume (x,( <%> E)) -->. (y,TS);

      then [ [x, ( <%> E)], y] in the Tran of TS;

      then [x, ( <%> E)] in ( dom the Tran of TS) by XTUPLE_0:def 12;

      hence contradiction by A1, XTUPLE_0:def 13;

    end;

    theorem :: REWRITE3:19

    

     Th19: for TS be deterministic transition-system over F holds u <> v & (x,u) -->. (z1,TS) & (x,v) -->. (z2,TS) implies not ex w st (u ^ w) = v or (v ^ w) = u

    proof

      let TS be deterministic transition-system over F;

      assume that

       A1: u <> v and

       A2: (x,u) -->. (z1,TS) and

       A3: (x,v) -->. (z2,TS);

      x in TS by A2, Th15;

      then

      reconsider x as Element of TS;

       [ [x, v], z2] in the Tran of TS by A3;

      then

       A4: [x, v] in ( dom the Tran of TS) by XTUPLE_0:def 12;

       [ [x, u], z1] in the Tran of TS by A2;

      then [x, u] in ( dom the Tran of TS) by XTUPLE_0:def 12;

      hence thesis by A1, A4, Def1;

    end;

    begin

    definition

      let E, F;

      let TS be transition-system over F;

      let x1,x2,y1,y2 be object;

      :: REWRITE3:def3

      pred x1,x2 ==>. y1,y2,TS means ex v, w st v = y2 & (x1,w) -->. (y1,TS) & x2 = (w ^ v);

    end

    theorem :: REWRITE3:20

    

     Th20: for TS be transition-system over F holds (x1,x2) ==>. (y1,y2,TS) implies x1 in TS & y1 in TS & x2 in (E ^omega ) & y2 in (E ^omega ) & x1 in ( dom ( dom the Tran of TS)) & y1 in ( rng the Tran of TS) by Th15;

    theorem :: REWRITE3:21

    

     Th21: for TS1 be transition-system over F1, TS2 be transition-system over F2 st the Tran of TS1 = the Tran of TS2 & (x1,x2) ==>. (y1,y2,TS1) holds (x1,x2) ==>. (y1,y2,TS2)

    proof

      let TS1 be transition-system over F1, TS2 be transition-system over F2 such that

       A1: the Tran of TS1 = the Tran of TS2 and

       A2: (x1,x2) ==>. (y1,y2,TS1);

      consider v, w such that

       A3: v = y2 & (x1,w) -->. (y1,TS1) & x2 = (w ^ v) by A2;

      take v, w;

      thus thesis by A1, A3;

    end;

    theorem :: REWRITE3:22

    for TS be transition-system over F holds (x,u) ==>. (y,v,TS) implies ex w st (x,w) -->. (y,TS) & u = (w ^ v);

    theorem :: REWRITE3:23

    

     Th23: for TS be transition-system over F holds (x,y) -->. (z,TS) iff (x,y) ==>. (z,( <%> E),TS)

    proof

      let TS be transition-system over F;

      thus (x,y) -->. (z,TS) implies (x,y) ==>. (z,( <%> E),TS)

      proof

        assume

         A1: (x,y) -->. (z,TS);

        then y in F by Th15;

        then

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

        w = (w ^ {} );

        hence thesis by A1;

      end;

      assume (x,y) ==>. (z,( <%> E),TS);

      then ex v, w st v = ( <%> E) & (x,w) -->. (z,TS) & y = (w ^ v);

      hence thesis;

    end;

    theorem :: REWRITE3:24

    

     Th24: for TS be transition-system over F holds (x,v) -->. (y,TS) iff (x,(v ^ w)) ==>. (y,w,TS) by AFINSQ_1: 28;

    theorem :: REWRITE3:25

    

     Th25: for TS be transition-system over F holds (x,u) ==>. (y,v,TS) implies (x,(u ^ w)) ==>. (y,(v ^ w),TS)

    proof

      let TS be transition-system over F;

      assume (x,u) ==>. (y,v,TS);

      then

      consider u1 such that

       A1: (x,u1) -->. (y,TS) and

       A2: u = (u1 ^ v);

      (u ^ w) = (u1 ^ (v ^ w)) by A2, AFINSQ_1: 27;

      hence thesis by A1;

    end;

    theorem :: REWRITE3:26

    

     Th26: for TS be transition-system over F holds (x,u) ==>. (y,v,TS) implies ( len u) >= ( len v) by Th9;

    theorem :: REWRITE3:27

    

     Th27: for TS be transition-system over F st the Tran of TS is Function holds (x1,x2) ==>. (y1,z,TS) & (x1,x2) ==>. (y2,z,TS) implies y1 = y2

    proof

      let TS be transition-system over F such that

       A1: the Tran of TS is Function;

      assume that

       A2: (x1,x2) ==>. (y1,z,TS) and

       A3: (x1,x2) ==>. (y2,z,TS);

      consider v1, w1 such that

       A4: v1 = z and

       A5: (x1,w1) -->. (y1,TS) and

       A6: x2 = (w1 ^ v1) by A2;

      consider v2, w2 such that

       A7: v2 = z and

       A8: (x1,w2) -->. (y2,TS) and

       A9: x2 = (w2 ^ v2) by A3;

      w1 = w2 by A4, A6, A7, A9, AFINSQ_1: 28;

      hence thesis by A1, A5, A8, Th17;

    end;

    theorem :: REWRITE3:28

    

     Th28: for TS be transition-system over F st not ( <%> E) in ( rng ( dom the Tran of TS)) holds not (x,z) ==>. (y,z,TS)

    proof

      let TS be transition-system over F such that

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume (x,z) ==>. (y,z,TS);

      then

      consider v, w such that

       A2: v = z and

       A3: (x,w) -->. (y,TS) and

       A4: z = (w ^ v);

       [ [x, w], y] in the Tran of TS by A3;

      then

       A5: [x, w] in ( dom the Tran of TS) by XTUPLE_0:def 12;

      w = ( <%> E) by A2, A4, FLANG_2: 4;

      hence contradiction by A1, A5, XTUPLE_0:def 13;

    end;

    theorem :: REWRITE3:29

    

     Th29: for TS be transition-system over F st not ( <%> E) in ( rng ( dom the Tran of TS)) holds (x,u) ==>. (y,v,TS) implies ( len u) > ( len v)

    proof

      let TS be transition-system over F such that

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume

       A2: (x,u) ==>. (y,v,TS);

      then

      consider w such that

       A3: (x,w) -->. (y,TS) and

       A4: u = (w ^ v);

      

       A5: w in ( rng ( dom the Tran of TS)) by A3, Th15;

      per cases ;

        suppose

         A6: v = ( <%> E);

        then u <> ( <%> E) by A1, A2, Th28;

        then ( len u) > 0 ;

        hence thesis by A6;

      end;

        suppose v <> ( <%> E);

        hence thesis by A1, A4, A5, Th10;

      end;

    end;

    theorem :: REWRITE3:30

    

     Th30: for TS be deterministic transition-system over F holds (x1,x2) ==>. (y1,z1,TS) & (x1,x2) ==>. (y2,z2,TS) implies y1 = y2 & z1 = z2

    proof

      let TS be deterministic transition-system over F;

      assume that

       A1: (x1,x2) ==>. (y1,z1,TS) and

       A2: (x1,x2) ==>. (y2,z2,TS);

      consider v2, w2 such that

       A3: v2 = z2 and

       A4: (x1,w2) -->. (y2,TS) and

       A5: x2 = (w2 ^ v2) by A2;

      consider v1, w1 such that

       A6: v1 = z1 and

       A7: (x1,w1) -->. (y1,TS) and

       A8: x2 = (w1 ^ v1) by A1;

      

       A9: the Tran of TS is Function by Def1;

      (ex u9 st (w1 ^ u9) = w2 & v1 = (u9 ^ v2)) or ex u9 st (w2 ^ u9) = w1 & v2 = (u9 ^ v1) by A8, A5, Th13;

      then w1 = w2 by A7, A4, Th19;

      then v1 = v2 by A8, A5, AFINSQ_1: 28;

      hence thesis by A1, A2, A6, A3, A9, Th27;

    end;

    begin

    reserve TS for non empty transition-system over F;

    reserve s,s9,s1,s2,t,t1,t2 for Element of TS;

    reserve S for Subset of TS;

    definition

      let E, F, TS;

      :: REWRITE3:def4

      func ==>.-relation (TS) -> Relation of [:the carrier of TS, (E ^omega ):] means

      : Def4: [ [x1, x2], [y1, y2]] in it iff (x1,x2) ==>. (y1,y2,TS);

      existence

      proof

        defpred P[ Element of [:the carrier of TS, (E ^omega ):], Element of [:the carrier of TS, (E ^omega ):]] means ex x1, x2, y1, y2 st [x1, x2] = $1 & [y1, y2] = $2 & (x1,x2) ==>. (y1,y2,TS);

        consider R be Relation of [:the carrier of TS, (E ^omega ):] such that

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

        take R;

        now

          let x1, x2, y1, y2;

          set s = [x1, x2];

          set t = [y1, y2];

          

           A2: ( dom R) c= [:the carrier of TS, (E ^omega ):] & ( rng R) c= [:the carrier of TS, (E ^omega ):] by RELAT_1:def 18, RELAT_1:def 19;

          thus (x1,x2) ==>. (y1,y2,TS) implies [ [x1, x2], [y1, y2]] in R

          proof

            assume

             A3: (x1,x2) ==>. (y1,y2,TS);

            then y1 in TS by Th20;

            then

             A4: y1 in the carrier of TS;

            x1 in TS by A3, Th20;

            then

             A5: x1 in the carrier of TS;

            y2 in (E ^omega ) by A3;

            then

             A6: t in [:the carrier of TS, (E ^omega ):] by A4, ZFMISC_1:def 2;

            x2 in (E ^omega ) by A3;

            then s in [:the carrier of TS, (E ^omega ):] by A5, ZFMISC_1:def 2;

            hence thesis by A1, A3, A6;

          end;

          assume

           A7: [ [x1, x2], [y1, y2]] in R;

          then [x1, x2] in ( dom R) & [y1, y2] in ( rng R) by XTUPLE_0:def 12, XTUPLE_0:def 13;

          then

          consider x19,x29,y19,y29 be object such that

           A8: [x19, x29] = s and

           A9: [y19, y29] = t and

           A10: (x19,x29) ==>. (y19,y29,TS) by A1, A7, A2;

          

           A11: y1 = y19 by A9, XTUPLE_0: 1;

          x1 = x19 & x2 = x29 by A8, XTUPLE_0: 1;

          hence (x1,x2) ==>. (y1,y2,TS) by A9, A10, A11, XTUPLE_0: 1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of [:the carrier of TS, (E ^omega ):] such that

         A12: [ [x1, x2], [y1, y2]] in R1 iff (x1,x2) ==>. (y1,y2,TS) and

         A13: [ [x1, x2], [y1, y2]] in R2 iff (x1,x2) ==>. (y1,y2,TS);

        now

          let s,t be Element of [:the carrier of TS, (E ^omega ):];

          consider x,u be object such that

           A14: x in the carrier of TS and

           A15: u in (E ^omega ) and

           A16: s = [x, u] by ZFMISC_1:def 2;

          reconsider u as Element of (E ^omega ) by A15;

          reconsider x as Element of TS by A14;

          consider y,v be object such that

           A17: y in the carrier of TS and

           A18: v in (E ^omega ) and

           A19: t = [y, v] by ZFMISC_1:def 2;

          reconsider v as Element of (E ^omega ) by A18;

          reconsider y as Element of TS by A17;

           [s, t] in R1 iff (x,u) ==>. (y,v,TS) by A12, A16, A19;

          hence [s, t] in R1 iff [s, t] in R2 by A13, A16, A19;

        end;

        hence thesis by RELSET_1:def 2;

      end;

    end

    theorem :: REWRITE3:31

    

     Th31: [x, y] in ( ==>.-relation TS) implies ex s, v, t, w st x = [s, v] & y = [t, w]

    proof

      assume

       A1: [x, y] in ( ==>.-relation TS);

      then y in [:the carrier of TS, (E ^omega ):] by ZFMISC_1: 87;

      then

       A2: ex y1,y2 be object st y1 in the carrier of TS & y2 in (E ^omega ) & y = [y1, y2] by ZFMISC_1:def 2;

      x in [:the carrier of TS, (E ^omega ):] by A1, ZFMISC_1: 87;

      then ex x1,x2 be object st x1 in the carrier of TS & x2 in (E ^omega ) & x = [x1, x2] by ZFMISC_1:def 2;

      hence thesis by A2;

    end;

    theorem :: REWRITE3:32

    

     Th32: [ [x1, x2], [y1, y2]] in ( ==>.-relation TS) implies x1 in TS & y1 in TS & x2 in (E ^omega ) & y2 in (E ^omega ) & x1 in ( dom ( dom the Tran of TS)) & y1 in ( rng the Tran of TS)

    proof

      assume [ [x1, x2], [y1, y2]] in ( ==>.-relation TS);

      then (x1,x2) ==>. (y1,y2,TS) by Def4;

      hence thesis by Th20;

    end;

    theorem :: REWRITE3:33

    

     Th33: x in ( ==>.-relation TS) implies ex s, t, v, w st x = [ [s, v], [t, w]]

    proof

      assume

       A1: x in ( ==>.-relation TS);

      then

      consider y,z be object such that

       A2: x = [y, z] by RELAT_1:def 1;

      ex s, v, t, w st y = [s, v] & z = [t, w] by A1, A2, Th31;

      hence thesis by A2;

    end;

    theorem :: REWRITE3:34

    

     Th34: for TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds ( ==>.-relation TS1) = ( ==>.-relation TS2)

    proof

      let TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 such that

       A1: the Tran of TS1 = the Tran of TS2;

       A2:

      now

        let x be object;

        assume

         A3: x in ( ==>.-relation TS1);

        then

        consider s,t be Element of TS1, v, w such that

         A4: x = [ [s, v], [t, w]] by Th33;

        (s,v) ==>. (t,w,TS1) by A3, A4, Def4;

        then (s,v) ==>. (t,w,TS2) by A1, Th21;

        hence x in ( ==>.-relation TS2) by A4, Def4;

      end;

      now

        let x be object;

        assume

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

        then

        consider s,t be Element of TS2, v, w such that

         A6: x = [ [s, v], [t, w]] by Th33;

        (s,v) ==>. (t,w,TS2) by A5, A6, Def4;

        then (s,v) ==>. (t,w,TS1) by A1, Th21;

        hence x in ( ==>.-relation TS1) by A6, Def4;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: REWRITE3:35

    

     Th35: [ [x1, x2], [y1, y2]] in ( ==>.-relation TS) implies ex v, w st v = y2 & (x1,w) -->. (y1,TS) & x2 = (w ^ v)

    proof

      assume [ [x1, x2], [y1, y2]] in ( ==>.-relation TS);

      then (x1,x2) ==>. (y1,y2,TS) by Def4;

      hence thesis;

    end;

    theorem :: REWRITE3:36

    

     Th36: [ [x, u], [y, v]] in ( ==>.-relation TS) implies ex w st (x,w) -->. (y,TS) & u = (w ^ v)

    proof

      assume [ [x, u], [y, v]] in ( ==>.-relation TS);

      then (x,u) ==>. (y,v,TS) by Def4;

      hence thesis;

    end;

    theorem :: REWRITE3:37

    

     Th37: (x,y) -->. (z,TS) iff [ [x, y], [z, ( <%> E)]] in ( ==>.-relation TS)

    proof

      thus (x,y) -->. (z,TS) implies [ [x, y], [z, ( <%> E)]] in ( ==>.-relation TS)

      proof

        assume (x,y) -->. (z,TS);

        then (x,y) ==>. (z,( <%> E),TS) by Th23;

        hence thesis by Def4;

      end;

      assume [ [x, y], [z, ( <%> E)]] in ( ==>.-relation TS);

      then (x,y) ==>. (z,( <%> E),TS) by Def4;

      hence thesis;

    end;

    theorem :: REWRITE3:38

    

     Th38: (x,v) -->. (y,TS) iff [ [x, (v ^ w)], [y, w]] in ( ==>.-relation TS)

    proof

      thus (x,v) -->. (y,TS) implies [ [x, (v ^ w)], [y, w]] in ( ==>.-relation TS)

      proof

        assume (x,v) -->. (y,TS);

        then (x,(v ^ w)) ==>. (y,w,TS);

        hence thesis by Def4;

      end;

      assume [ [x, (v ^ w)], [y, w]] in ( ==>.-relation TS);

      then (x,(v ^ w)) ==>. (y,w,TS) by Def4;

      hence thesis by Th24;

    end;

    theorem :: REWRITE3:39

     [ [x, u], [y, v]] in ( ==>.-relation TS) implies [ [x, (u ^ w)], [y, (v ^ w)]] in ( ==>.-relation TS)

    proof

      assume [ [x, u], [y, v]] in ( ==>.-relation TS);

      then (x,u) ==>. (y,v,TS) by Def4;

      then (x,(u ^ w)) ==>. (y,(v ^ w),TS) by Th25;

      hence thesis by Def4;

    end;

    theorem :: REWRITE3:40

     [ [x, u], [y, v]] in ( ==>.-relation TS) implies ( len u) >= ( len v)

    proof

      assume [ [x, u], [y, v]] in ( ==>.-relation TS);

      then (x,u) ==>. (y,v,TS) by Def4;

      hence thesis by Th26;

    end;

    theorem :: REWRITE3:41

    the Tran of TS is Function implies ( [x, [y1, z]] in ( ==>.-relation TS) & [x, [y2, z]] in ( ==>.-relation TS) implies y1 = y2)

    proof

      assume

       A1: the Tran of TS is Function;

      assume that

       A2: [x, [y1, z]] in ( ==>.-relation TS) and

       A3: [x, [y2, z]] in ( ==>.-relation TS);

      consider s, v, t, w such that

       A4: x = [s, v] and [y1, z] = [t, w] by A2, Th31;

      (s,v) ==>. (y1,z,TS) & (s,v) ==>. (y2,z,TS) by A2, A3, A4, Def4;

      hence thesis by A1, Th27;

    end;

    theorem :: REWRITE3:42

     not ( <%> E) in ( rng ( dom the Tran of TS)) implies ( [ [x, u], [y, v]] in ( ==>.-relation TS) implies ( len u) > ( len v))

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume [ [x, u], [y, v]] in ( ==>.-relation TS);

      then (x,u) ==>. (y,v,TS) by Def4;

      hence thesis by A1, Th29;

    end;

    theorem :: REWRITE3:43

    

     Th43: not ( <%> E) in ( rng ( dom the Tran of TS)) implies not [ [x, z], [y, z]] in ( ==>.-relation TS)

    proof

      assume not ( <%> E) in ( rng ( dom the Tran of TS));

      then not (x,z) ==>. (y,z,TS) by Th28;

      hence thesis by Def4;

    end;

    theorem :: REWRITE3:44

    

     Th44: TS is deterministic implies ( [x, y1] in ( ==>.-relation TS) & [x, y2] in ( ==>.-relation TS) implies y1 = y2)

    proof

      assume

       A1: TS is deterministic;

      assume that

       A2: [x, y1] in ( ==>.-relation TS) and

       A3: [x, y2] in ( ==>.-relation TS);

      consider s2, v2, t2, w2 such that x = [s2, v2] and

       A4: y2 = [t2, w2] by A3, Th31;

      consider s1, v1, t1, w1 such that

       A5: x = [s1, v1] and

       A6: y1 = [t1, w1] by A2, Th31;

      

       A7: (s1,v1) ==>. (t1,w1,TS) by A2, A5, A6, Def4;

      

       A8: (s1,v1) ==>. (t2,w2,TS) by A3, A5, A4, Def4;

      then t1 = t2 by A1, A7, Th30;

      hence thesis by A1, A6, A4, A7, A8, Th30;

    end;

    theorem :: REWRITE3:45

    TS is deterministic implies ( [x, [y1, z1]] in ( ==>.-relation TS) & [x, [y2, z2]] in ( ==>.-relation TS) implies y1 = y2 & z1 = z2)

    proof

      assume

       A1: TS is deterministic;

      assume [x, [y1, z1]] in ( ==>.-relation TS) & [x, [y2, z2]] in ( ==>.-relation TS);

      then [y1, z1] = [y2, z2] by A1, Th44;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: REWRITE3:46

    TS is deterministic implies ( ==>.-relation TS) is Function-like

    proof

      assume TS is deterministic;

      then for x,y,z be object st [x, y] in ( ==>.-relation TS) & [x, z] in ( ==>.-relation TS) holds y = z by Th44;

      hence thesis by FUNCT_1:def 1;

    end;

    begin

    definition

      let x, E;

      :: REWRITE3:def5

      func dim2 (x,E) -> Element of (E ^omega ) equals

      : Def5: (x `2 ) if ex y, u st x = [y, u]

      otherwise {} ;

      coherence

      proof

        thus (ex y, u st x = [y, u]) implies (x `2 ) is Element of (E ^omega );

         {} = ( <%> E);

        hence thesis;

      end;

      consistency ;

    end

    theorem :: REWRITE3:47

    

     Th47: for P be RedSequence of ( ==>.-relation TS), k st k in ( dom P) & (k + 1) in ( dom P) holds ex s, v, t, w st (P . k) = [s, v] & (P . (k + 1)) = [t, w]

    proof

      let P be RedSequence of ( ==>.-relation TS), k;

      assume k in ( dom P) & (k + 1) in ( dom P);

      then [(P . k), (P . (k + 1))] in ( ==>.-relation TS) by REWRITE1:def 2;

      hence thesis by Th31;

    end;

    theorem :: REWRITE3:48

    

     Th48: for P be RedSequence of ( ==>.-relation TS), k st k in ( dom P) & (k + 1) in ( dom P) holds (P . k) = [((P . k) `1 ), ((P . k) `2 )] & (P . (k + 1)) = [((P . (k + 1)) `1 ), ((P . (k + 1)) `2 )]

    proof

      let P be RedSequence of ( ==>.-relation TS), k;

      assume k in ( dom P) & (k + 1) in ( dom P);

      then ex s, v, t, w st (P . k) = [s, v] & (P . (k + 1)) = [t, w] by Th47;

      hence thesis;

    end;

    theorem :: REWRITE3:49

    

     Th49: for P be RedSequence of ( ==>.-relation TS), k st k in ( dom P) & (k + 1) in ( dom P) holds ((P . k) `1 ) in TS & ((P . k) `2 ) in (E ^omega ) & ((P . (k + 1)) `1 ) in TS & ((P . (k + 1)) `2 ) in (E ^omega ) & ((P . k) `1 ) in ( dom ( dom the Tran of TS)) & ((P . (k + 1)) `1 ) in ( rng the Tran of TS)

    proof

      let P be RedSequence of ( ==>.-relation TS), k;

      assume k in ( dom P) & (k + 1) in ( dom P);

      then

       A1: [(P . k), (P . (k + 1))] in ( ==>.-relation TS) by REWRITE1:def 2;

      then

      consider s, v, t, w such that

       A2: (P . k) = [s, v] & (P . (k + 1)) = [t, w] by Th31;

      

       A3: s in ( dom ( dom the Tran of TS)) & t in ( rng the Tran of TS) by A1, A2, Th32;

      thus thesis by A2, A3;

    end;

    theorem :: REWRITE3:50

    for TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds for P be RedSequence of ( ==>.-relation TS1) holds P is RedSequence of ( ==>.-relation TS2)

    proof

      let TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 such that

       A1: the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2;

      let P be RedSequence of ( ==>.-relation TS1);

       A2:

      now

        let i be Nat;

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

        then [(P . i), (P . (i + 1))] in ( ==>.-relation TS1) by REWRITE1:def 2;

        hence [(P . i), (P . (i + 1))] in ( ==>.-relation TS2) by A1, Th34;

      end;

      ( len P) > 0 ;

      hence thesis by A2, REWRITE1:def 2;

    end;

    theorem :: REWRITE3:51

    

     Th51: for P be RedSequence of ( ==>.-relation TS) st ex x, u st (P . 1) = [x, u] holds for k st k in ( dom P) holds ( dim2 ((P . k),E)) = ((P . k) `2 )

    proof

      let P be RedSequence of ( ==>.-relation TS);

      given x, u such that

       A1: (P . 1) = [x, u];

      let k such that

       A2: k in ( dom P);

      per cases ;

        suppose

         A3: k > 1;

        

         A4: k <= ( len P) by A2, FINSEQ_3: 25;

        consider l such that

         A5: k = (l + 1) by A3, NAT_1: 6;

        l <= k by A5, NAT_1: 11;

        then

         A6: l <= ( len P) by A4, XXREAL_0: 2;

        l >= 1 by A3, A5, NAT_1: 19;

        then l in ( dom P) by A6, FINSEQ_3: 25;

        then [(P . l), (P . k)] in ( ==>.-relation TS) by A2, A5, REWRITE1:def 2;

        then

         A7: (P . k) in ( rng ( ==>.-relation TS)) by XTUPLE_0:def 13;

        ( rng ( ==>.-relation TS)) c= [:the carrier of TS, (E ^omega ):] by RELAT_1:def 19;

        then ex x1,y1 be object st x1 in the carrier of TS & y1 in (E ^omega ) & (P . k) = [x1, y1] by A7, ZFMISC_1:def 2;

        hence thesis by Def5;

      end;

        suppose

         A8: k <= 1;

        k >= 1 by A2, FINSEQ_3: 25;

        then k = 1 by A8, XXREAL_0: 1;

        hence thesis by A1, Def5;

      end;

    end;

    theorem :: REWRITE3:52

    

     Th52: for P be RedSequence of ( ==>.-relation TS) st (P . ( len P)) = [y, w] holds for k st k in ( dom P) holds ex u st ((P . k) `2 ) = (u ^ w)

    proof

      let P be RedSequence of ( ==>.-relation TS);

      assume (P . ( len P)) = [y, w];

      

      then

       A1: ((P . ( len P)) `2 ) = ( {} ^ w)

      .= (( <%> E) ^ w);

      defpred P[ Nat] means (( len P) - $1) in ( dom P) implies ex u st ((P . (( len P) - $1)) `2 ) = (u ^ w);

       A2:

      now

        let k;

        assume

         A3: P[k];

        now

          set len2 = (( len P) - k);

          set len1 = (( len P) - (k + 1));

          

           A4: (len1 + 1) = len2;

          assume

           A5: (( len P) - (k + 1)) in ( dom P);

          thus ex u st ((P . (( len P) - (k + 1))) `2 ) = (u ^ w)

          proof

            per cases ;

              suppose

               A6: (( len P) - k) in ( dom P);

              then

              consider u1 such that

               A7: ((P . len2) `2 ) = (u1 ^ w) by A3;

              

               A8: [(P . len1), (P . len2)] in ( ==>.-relation TS) by A5, A4, A6, REWRITE1:def 2;

              then

              consider x be Element of TS, v1 be Element of (E ^omega ), y be Element of TS, v2 such that

               A9: (P . len1) = [x, v1] and

               A10: (P . len2) = [y, v2] by Th31;

              (x,v1) ==>. (y,v2,TS) by A8, A9, A10, Def4;

              then

              consider u2 such that (x,u2) -->. (y,TS) and

               A11: v1 = (u2 ^ v2);

              take (u2 ^ u1);

              ((P . len1) `2 ) = (u2 ^ v2) by A9, A11

              .= (u2 ^ (u1 ^ w)) by A7, A10

              .= ((u2 ^ u1) ^ w) by AFINSQ_1: 27;

              hence thesis;

            end;

              suppose not (( len P) - k) in ( dom P);

              then len1 = (( len P) - 0 ) by A5, A4, Th3;

              hence thesis;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A12: P[ 0 ] by A1;

      

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

      hereby

        let k such that

         A14: k in ( dom P);

        k <= ( len P) by A14, FINSEQ_3: 25;

        then

        consider l such that

         A15: (k + l) = ( len P) by NAT_1: 10;

        ((k + l) - l) = (( len P) - l) by A15;

        hence ex u st ((P . k) `2 ) = (u ^ w) by A13, A14;

      end;

    end;

    theorem :: REWRITE3:53

    

     Th53: for P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, v] & (P . ( len P)) = [y, w] holds ex u st v = (u ^ w)

    proof

      let P be RedSequence of ( ==>.-relation TS) such that

       A1: (P . 1) = [x, v] and

       A2: (P . ( len P)) = [y, w];

      ( 0 + 1) <= ( len P) by NAT_1: 8;

      then 1 in ( dom P) by FINSEQ_3: 25;

      then

      consider u such that

       A3: ((P . 1) `2 ) = (u ^ w) by A2, Th52;

      take u;

      thus thesis by A1, A3;

    end;

    theorem :: REWRITE3:54

    

     Th54: for P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, u] & (P . ( len P)) = [y, u] holds for k st k in ( dom P) holds ((P . k) `2 ) = u

    proof

      defpred P[ Nat] means for P be RedSequence of ( ==>.-relation TS), x, y st (P . 1) = [x, u] & (P . ( len P)) = [y, u] & ( len P) = $1 holds (for k st k in ( dom P) holds ((P . k) `2 ) = u);

       A1:

      now

        let k;

        assume

         A2: P[k];

        now

          let P be RedSequence of ( ==>.-relation TS), x, y such that

           A3: (P . 1) = [x, u] and

           A4: (P . ( len P)) = [y, u] and

           A5: ( len P) = (k + 1);

          per cases ;

            suppose

             A6: k = 0 ;

            hereby

              let l;

              assume l in ( dom P);

              then l <= 1 & 1 <= l by A5, A6, FINSEQ_3: 25;

              then l = 1 by XXREAL_0: 1;

              hence ((P . l) `2 ) = u by A3;

            end;

          end;

            suppose k <> 0 ;

            then

             A7: (k + 1) > ( 0 + 1) by XREAL_1: 6;

            then

             A8: 1 in ( dom P) by A5, FINSEQ_3: 25;

            ( len P) >= (1 + 1) by A5, A7, NAT_1: 8;

            then

             A9: (1 + 1) in ( dom P) by FINSEQ_3: 25;

            then

             A10: (P . (1 + 1)) = [((P . (1 + 1)) `1 ), ((P . (1 + 1)) `2 )] by A8, Th48;

            reconsider u1 = ((P . (1 + 1)) `2 ) as Element of (E ^omega ) by A8, A9, Th49;

            ( ==>.-relation TS) reduces ((P . 1),(P . (1 + 1))) by A8, A9, REWRITE1: 17;

            then ex P9 be RedSequence of ( ==>.-relation TS) st (P9 . 1) = (P . 1) & (P9 . ( len P9)) = (P . (1 + 1)) by REWRITE1:def 3;

            then

            consider w such that

             A11: u = (w ^ u1) by A3, A10, Th53;

            

             A12: ( len <*(P . 1)*>) = 1 by FINSEQ_1: 40;

            consider Q be RedSequence of ( ==>.-relation TS) such that

             A13: ( <*(P . 1)*> ^ Q) = P and

             A14: ( len P) = (( len Q) + 1) by A5, A7, Th5;

            

             A15: ( len Q) >= ( 0 + 1) by NAT_1: 8;

            then

             A16: (Q . 1) = [((P . (1 + 1)) `1 ), ((P . (1 + 1)) `2 )] by A13, A12, A10, FINSEQ_1: 65;

            

             A17: (Q . ( len Q)) = [y, u] by A4, A13, A14, A12, A15, FINSEQ_1: 65;

            then

            consider v such that

             A18: u1 = (v ^ u) by A16, Th53;

            

             A19: ( {} ^ u1) = u1;

            u = ((w ^ v) ^ u) by A18, A11, AFINSQ_1: 27;

            then (w ^ v) = {} by FLANG_2: 4;

            then

             A20: (Q . 1) = [((P . (1 + 1)) `1 ), u] by A16, A11, A19, AFINSQ_1: 30;

            hereby

              let l;

              assume

               A21: l in ( dom P);

              then

               A22: 1 <= l by FINSEQ_3: 25;

              then

              reconsider l9 = (l - 1) as Nat by NAT_1: 21;

              (1 + 1) <= (l + 1) by A22, XREAL_1: 6;

              then

               A23: (1 + 1) = (l + 1) or (1 + 1) <= l by NAT_1: 8;

              l <= ( len P) by A21, FINSEQ_3: 25;

              then 1 = l or ((1 + 1) - 1) <= (l - 1) & (l - 1) <= ((( len Q) + 1) - 1) by A14, A23, XREAL_1: 9;

              then

               A24: l = 1 or l9 in ( dom Q) by FINSEQ_3: 25;

              per cases by A24;

                suppose l = 1;

                hence ((P . l) `2 ) = u by A3;

              end;

                suppose

                 A25: (l - 1) in ( dom Q);

                then (l - 1) <= ( len Q) by FINSEQ_3: 25;

                then

                 A26: ((l - 1) + 1) <= (( len Q) + 1) by XREAL_1: 6;

                1 <= (l - 1) by A25, FINSEQ_3: 25;

                then

                 A27: (1 + 0 ) < ((l - 1) + 1) by XREAL_1: 6;

                ((Q . (l - 1)) `2 ) = u by A2, A5, A14, A17, A20, A25;

                hence ((P . l) `2 ) = u by A13, A14, A12, A27, A26, FINSEQ_1: 24;

              end;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A28: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A28, A1);

      hence thesis;

    end;

    theorem :: REWRITE3:55

    for P be RedSequence of ( ==>.-relation TS), k st k in ( dom P) & (k + 1) in ( dom P) holds ex v, w st v = ((P . (k + 1)) `2 ) & (((P . k) `1 ),w) -->. (((P . (k + 1)) `1 ),TS) & ((P . k) `2 ) = (w ^ v)

    proof

      let P be RedSequence of ( ==>.-relation TS), k such that

       A1: k in ( dom P) & (k + 1) in ( dom P);

      consider s, u, t, v such that

       A2: (P . k) = [s, u] and

       A3: (P . (k + 1)) = [t, v] by A1, Th47;

       [ [s, u], [t, v]] in ( ==>.-relation TS) by A1, A2, A3, REWRITE1:def 2;

      then

      consider v1, w1 such that

       A4: v1 = v and

       A5: (s,w1) -->. (t,TS) and

       A6: u = (w1 ^ v1) by Th35;

      take v1, w1;

      thus v1 = ((P . (k + 1)) `2 ) by A3, A4;

      (((P . k) `1 ),w1) -->. (t,TS) by A2, A5;

      hence thesis by A2, A3, A6;

    end;

    theorem :: REWRITE3:56

    for P be RedSequence of ( ==>.-relation TS), k st k in ( dom P) & (k + 1) in ( dom P) & (P . k) = [x, u] & (P . (k + 1)) = [y, v] holds ex w st (x,w) -->. (y,TS) & u = (w ^ v)

    proof

      let P be RedSequence of ( ==>.-relation TS), k;

      assume k in ( dom P) & (k + 1) in ( dom P) & (P . k) = [x, u] & (P . (k + 1)) = [y, v];

      then [ [x, u], [y, v]] in ( ==>.-relation TS) by REWRITE1:def 2;

      hence thesis by Th36;

    end;

    theorem :: REWRITE3:57

    

     Th57: (x,y) -->. (z,TS) iff <* [x, y], [z, ( <%> E)]*> is RedSequence of ( ==>.-relation TS)

    proof

      thus (x,y) -->. (z,TS) implies <* [x, y], [z, ( <%> E)]*> is RedSequence of ( ==>.-relation TS)

      proof

        assume (x,y) -->. (z,TS);

        then [ [x, y], [z, ( <%> E)]] in ( ==>.-relation TS) by Th37;

        hence thesis by REWRITE1: 7;

      end;

      assume <* [x, y], [z, ( <%> E)]*> is RedSequence of ( ==>.-relation TS);

      then [ [x, y], [z, ( <%> E)]] in ( ==>.-relation TS) by Th8;

      hence thesis by Th37;

    end;

    theorem :: REWRITE3:58

    

     Th58: (x,v) -->. (y,TS) iff <* [x, (v ^ w)], [y, w]*> is RedSequence of ( ==>.-relation TS)

    proof

      thus (x,v) -->. (y,TS) implies <* [x, (v ^ w)], [y, w]*> is RedSequence of ( ==>.-relation TS)

      proof

        assume (x,v) -->. (y,TS);

        then [ [x, (v ^ w)], [y, w]] in ( ==>.-relation TS) by Th38;

        hence thesis by REWRITE1: 7;

      end;

      assume <* [x, (v ^ w)], [y, w]*> is RedSequence of ( ==>.-relation TS);

      then [ [x, (v ^ w)], [y, w]] in ( ==>.-relation TS) by Th8;

      hence thesis by Th38;

    end;

    theorem :: REWRITE3:59

    

     Th59: for P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, v] & (P . ( len P)) = [y, w] holds ( len v) >= ( len w)

    proof

      let P be RedSequence of ( ==>.-relation TS);

      assume (P . 1) = [x, v] & (P . ( len P)) = [y, w];

      then ex u st v = (u ^ w) by Th53;

      hence thesis by Th9;

    end;

    theorem :: REWRITE3:60

    

     Th60: not ( <%> E) in ( rng ( dom the Tran of TS)) implies for P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, u] & (P . ( len P)) = [y, u] holds ( len P) = 1 & x = y

    proof

      defpred P[ Nat] means for P be RedSequence of ( ==>.-relation TS), x, y st (P . 1) = [x, u] & (P . ( len P)) = [y, u] & ( len P) = $1 & $1 <> 1 holds contradiction;

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

       A2:

      now

        let k;

        assume P[k];

        now

          let P be RedSequence of ( ==>.-relation TS), x, y such that

           A3: (P . 1) = [x, u] and

           A4: (P . ( len P)) = [y, u] and

           A5: ( len P) = (k + 1) & (k + 1) <> 1;

          consider Q be RedSequence of ( ==>.-relation TS) such that ( <*(P . 1)*> ^ Q) = P and

           A6: ( len P) = (( len Q) + 1) by A5, Th5, NAT_1: 25;

          ( len Q) >= ( 0 + 1) by NAT_1: 8;

          then (( len Q) + 1) >= (1 + 1) by XREAL_1: 6;

          then

           A7: (1 + 1) in ( dom P) by A6, FINSEQ_3: 25;

          ( len P) > 1 by A5, NAT_1: 25;

          then

           A8: 1 in ( dom P) by FINSEQ_3: 25;

          

          then (P . (1 + 1)) = [((P . (1 + 1)) `1 ), ((P . (1 + 1)) `2 )] by A7, Th48

          .= [((P . (1 + 1)) `1 ), u] by A3, A4, A7, Th54;

          then [ [x, u], [((P . (1 + 1)) `1 ), u]] in ( ==>.-relation TS) by A3, A8, A7, REWRITE1:def 2;

          then (x,u) ==>. (((P . (1 + 1)) `1 ),u,TS) by Def4;

          hence contradiction by A1, Th28;

        end;

        hence P[(k + 1)];

      end;

      let P be RedSequence of ( ==>.-relation TS) such that

       A9: (P . 1) = [x, u] & (P . ( len P)) = [y, u];

      

       A10: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A10, A2);

      hence ( len P) = 1 by A9;

      hence thesis by A9, XTUPLE_0: 1;

    end;

    theorem :: REWRITE3:61

    

     Th61: not ( <%> E) in ( rng ( dom the Tran of TS)) implies for P be RedSequence of ( ==>.-relation TS) st ((P . 1) `2 ) = ((P . ( len P)) `2 ) holds ( len P) = 1

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      let P be RedSequence of ( ==>.-relation TS) such that

       A2: ((P . 1) `2 ) = ((P . ( len P)) `2 );

      per cases ;

        suppose

         A3: ( len P) <= 1;

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

        hence ( len P) = 1 by A3, XXREAL_0: 1;

      end;

        suppose

         A4: ( len P) > 1;

        then

        reconsider p1 = (( len P) - 1) as Nat by NAT_1: 21;

        

         A5: (p1 + 1) = ( len P);

        then

         A6: p1 <= ( len P) by NAT_1: 13;

        (1 + 1) <= ( len P) by A4, NAT_1: 13;

        then

         A7: (1 + 1) in ( dom P) by FINSEQ_3: 25;

        ( 0 + 1) <= (p1 + 1) by XREAL_1: 6;

        then

         A8: (p1 + 1) in ( dom P) by FINSEQ_3: 25;

        1 <= p1 by A4, A5, NAT_1: 13;

        then p1 in ( dom P) by A6, FINSEQ_3: 25;

        then

        consider s2, v2, t2, w2 such that (P . p1) = [s2, v2] and

         A9: (P . (p1 + 1)) = [t2, w2] by A8, Th47;

        1 in ( dom P) by A4, FINSEQ_3: 25;

        then

        consider s1, v1, t1, w1 such that

         A10: (P . 1) = [s1, v1] and (P . (1 + 1)) = [t1, w1] by A7, Th47;

        ((P . ( len P)) `2 ) = w2 by A9;

        then v1 = w2 by A2, A10;

        hence ( len P) = 1 by A1, A10, A9, Th60;

      end;

    end;

    theorem :: REWRITE3:62

    

     Th62: not ( <%> E) in ( rng ( dom the Tran of TS)) implies for P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, u] & (P . ( len P)) = [y, ( <%> E)] holds ( len P) <= (( len u) + 1)

    proof

      defpred P[ Nat] means for P be RedSequence of ( ==>.-relation TS), u, x st ( len u) = $1 & (P . 1) = [x, u] & (P . ( len P)) = [y, ( <%> E)] holds ( len P) <= (( len u) + 1);

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

       A2:

      now

        let k;

        assume

         A3: for n st n < k holds P[n];

        now

          let P be RedSequence of ( ==>.-relation TS), u, x such that

           A4: ( len u) = k and

           A5: (P . 1) = [x, u] and

           A6: (P . ( len P)) = [y, ( <%> E)];

          per cases ;

            suppose ( len u) < 1;

            then u = ( <%> E) by NAT_1: 25;

            then ( len P) = 1 by A1, A5, A6, Th60;

            hence ( len P) <= (( len u) + 1) by NAT_1: 25;

          end;

            suppose

             A7: ( len u) >= 1;

            

             A8: ( len P) <> 1

            proof

              assume ( len P) = 1;

              then u = ( <%> E) by A5, A6, XTUPLE_0: 1;

              hence contradiction by A7;

            end;

            then

            consider P9 be RedSequence of ( ==>.-relation TS) such that

             A9: ( <*(P . 1)*> ^ P9) = P and

             A10: (( len P9) + 1) = ( len P) by Th5, NAT_1: 25;

            

             A11: ( len P) > 1 by A8, NAT_1: 25;

            then ( len P) >= (1 + 1) by NAT_1: 13;

            then

             A12: (1 + 1) in ( dom P) by FINSEQ_3: 25;

            

             A13: 1 in ( dom P) by A11, FINSEQ_3: 25;

            then

             A14: (P . (1 + 1)) = [((P . (1 + 1)) `1 ), ((P . (1 + 1)) `2 )] by A12, Th48;

            then

             A15: [ [x, u], [((P . (1 + 1)) `1 ), ((P . (1 + 1)) `2 )]] in ( ==>.-relation TS) by A5, A13, A12, REWRITE1:def 2;

            then

            reconsider u1 = ((P . (1 + 1)) `2 ) as Element of (E ^omega ) by Th32;

            

             A16: ( len <*(P . 1)*>) = 1 & ( len P9) >= 1 by FINSEQ_1: 39, NAT_1: 25;

            then

             A17: (P9 . 1) = [((P . (1 + 1)) `1 ), u1] by A9, A14, FINSEQ_1: 65;

            (x,u) ==>. (((P . (1 + 1)) `1 ),u1,TS) by A15, Def4;

            then

            consider v such that

             A18: (x,v) -->. (((P . (1 + 1)) `1 ),TS) & u = (v ^ u1);

            v <> ( <%> E) & ( len u) = (( len u1) + ( len v)) by A1, A18, Th15, AFINSQ_1: 17;

            then

             A19: (( len u) - 0 ) > ((( len u1) + ( len v)) - ( len v)) by XREAL_1: 15;

            then

             A20: (( len u1) + 1) <= ( len u) by NAT_1: 13;

            (P9 . ( len P9)) = [y, ( <%> E)] by A6, A9, A10, A16, FINSEQ_1: 65;

            then ( len P9) <= (( len u1) + 1) by A3, A4, A19, A17;

            then ( len P9) <= ( len u) by A20, XXREAL_0: 2;

            hence ( len P) <= (( len u) + 1) by A10, XREAL_1: 6;

          end;

        end;

        hence P[k];

      end;

      for k holds P[k] from NAT_1:sch 4( A2);

      hence thesis;

    end;

    theorem :: REWRITE3:63

    

     Th63: not ( <%> E) in ( rng ( dom the Tran of TS)) implies for P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, <%e%>] & (P . ( len P)) = [y, ( <%> E)] holds ( len P) = 2

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      let P be RedSequence of ( ==>.-relation TS) such that

       A2: (P . 1) = [x, <%e%>] & (P . ( len P)) = [y, ( <%> E)];

      ( len P) <= (( len <%e%>) + 1) by A1, A2, Th62;

      then ( len P) <= (1 + 1) by AFINSQ_1: 34;

      then

       A3: ( len P) = 0 or ... or ( len P) = 2;

      ( len P) <> 1 by A2, XTUPLE_0: 1;

      hence thesis by A3;

    end;

    theorem :: REWRITE3:64

    

     Th64: not ( <%> E) in ( rng ( dom the Tran of TS)) implies for P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, v] & (P . ( len P)) = [y, w] holds ( len v) > ( len w) or ( len P) = 1 & x = y & v = w

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      let P be RedSequence of ( ==>.-relation TS) such that

       A2: (P . 1) = [x, v] & (P . ( len P)) = [y, w];

      consider u such that

       A3: v = (u ^ w) by A2, Th53;

      

       A4: ( len v) >= ( len w) by A2, Th59;

      per cases ;

        suppose ( len v) > ( len w);

        hence thesis;

      end;

        suppose

         A5: ( len v) <= ( len w);

        

         A6: ( len v) = (( len u) + ( len w)) by A3, AFINSQ_1: 17;

        ( len v) = ( len w) by A4, A5, XXREAL_0: 1;

        then u = ( <%> E) by A6;

        hence thesis by A1, A2, Th60, A3;

      end;

    end;

    theorem :: REWRITE3:65

     not ( <%> E) in ( rng ( dom the Tran of TS)) implies for P be RedSequence of ( ==>.-relation TS), k st k in ( dom P) & (k + 1) in ( dom P) holds ((P . k) `2 ) <> ((P . (k + 1)) `2 )

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      let P be RedSequence of ( ==>.-relation TS), k such that

       A2: k in ( dom P) & (k + 1) in ( dom P);

      consider s, u, t, v such that

       A3: (P . k) = [s, u] and

       A4: (P . (k + 1)) = [t, v] by A2, Th47;

       [ [s, u], [t, v]] in ( ==>.-relation TS) by A2, A3, A4, REWRITE1:def 2;

      then u <> v by A1, Th43;

      then ((P . k) `2 ) <> v by A3;

      hence thesis by A4;

    end;

    theorem :: REWRITE3:66

    

     Th66: not ( <%> E) in ( rng ( dom the Tran of TS)) implies for P be RedSequence of ( ==>.-relation TS), k, l st k in ( dom P) & l in ( dom P) & k < l holds ((P . k) `2 ) <> ((P . l) `2 )

    proof

      defpred P[ Nat] means for P be RedSequence of ( ==>.-relation TS), k, l st ( len P) = $1 & k in ( dom P) & l in ( dom P) & k < l holds ((P . k) `2 ) <> ((P . l) `2 );

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

       A2:

      now

        let i;

        assume

         A3: P[i];

        now

          let P be RedSequence of ( ==>.-relation TS), k, l such that

           A4: ( len P) = (i + 1) and

           A5: k in ( dom P) and

           A6: l in ( dom P) and

           A7: k < l;

          

           A8: i < ( len P) by A4, NAT_1: 13;

          

           A9: k <= ( len P) by A5, FINSEQ_3: 25;

          

           A10: 1 <= k by A5, FINSEQ_3: 25;

          

           A11: 1 <= l by A6, FINSEQ_3: 25;

          

           A12: l <= ( len P) by A6, FINSEQ_3: 25;

          per cases ;

            suppose k = 1 & l = ( len P);

            hence ((P . k) `2 ) <> ((P . l) `2 ) by A1, A7, Th61;

          end;

            suppose

             A13: k <> 1 & l = ( len P);

            reconsider k1 = (k - 1) as Nat by A10, NAT_1: 21;

            

             A14: k > 1 by A10, A13, XXREAL_0: 1;

            then k1 > (1 - 1) by XREAL_1: 9;

            then

             A15: k1 >= ( 0 + 1) by NAT_1: 13;

            reconsider l1 = (l - 1) as Nat by A11, NAT_1: 21;

            

             A16: k1 < l1 by A7, XREAL_1: 9;

            

             A17: l > 1 by A7, A10, A11, XXREAL_0: 1;

            then

            consider Q be RedSequence of ( ==>.-relation TS) such that

             A18: ( <*(P . 1)*> ^ Q) = P and

             A19: (( len Q) + 1) = ( len P) by A13, Th5;

            l1 > (1 - 1) by A17, XREAL_1: 9;

            then

             A20: l1 >= ( 0 + 1) by NAT_1: 13;

            k1 <= ((( len Q) + 1) - 1) by A9, A19, XREAL_1: 9;

            then

             A21: k1 in ( dom Q) by A15, FINSEQ_3: 25;

            

             A22: ( len <*(P . 1)*>) = 1 by FINSEQ_1: 40;

            then

             A23: (P . l) = (Q . l1) by A12, A17, A18, FINSEQ_1: 24;

            l1 <= ((( len Q) + 1) - 1) by A12, A19, XREAL_1: 9;

            then

             A24: l1 in ( dom Q) by A20, FINSEQ_3: 25;

            (P . k) = (Q . k1) by A9, A14, A18, A22, FINSEQ_1: 24;

            hence ((P . k) `2 ) <> ((P . l) `2 ) by A3, A4, A19, A21, A24, A16, A23;

          end;

            suppose

             A25: l <> ( len P);

            k < (i + 1) by A4, A7, A12, XXREAL_0: 2;

            then

             A26: k <= i by NAT_1: 13;

            then

            reconsider Q = (P | i) as RedSequence of ( ==>.-relation TS) by A10, REWRITE2: 3, XXREAL_0: 2;

            

             A27: (P . k) = (Q . k) by A26, FINSEQ_3: 112;

            l < (i + 1) by A4, A12, A25, XXREAL_0: 1;

            then

             A28: l <= i by NAT_1: 13;

            then

             A29: (P . l) = (Q . l) by FINSEQ_3: 112;

            k <= ( len Q) by A8, A26, FINSEQ_1: 59;

            then

             A30: k in ( dom Q) by A10, FINSEQ_3: 25;

            l <= ( len Q) by A8, A28, FINSEQ_1: 59;

            then

             A31: l in ( dom Q) by A11, FINSEQ_3: 25;

            ( len Q) = i by A8, FINSEQ_1: 59;

            hence ((P . k) `2 ) <> ((P . l) `2 ) by A3, A7, A30, A31, A27, A29;

          end;

        end;

        hence P[(i + 1)];

      end;

      

       A32: P[ 0 ];

      

       A33: for i holds P[i] from NAT_1:sch 2( A32, A2);

      let P be RedSequence of ( ==>.-relation TS), k, l such that

       A34: k in ( dom P) & l in ( dom P) & k < l;

      ( len P) = ( len P);

      hence thesis by A33, A34;

    end;

    theorem :: REWRITE3:67

    

     Th67: TS is deterministic implies for P,Q be RedSequence of ( ==>.-relation TS) st (P . 1) = (Q . 1) holds for k st k in ( dom P) & k in ( dom Q) holds (P . k) = (Q . k)

    proof

      assume

       A1: TS is deterministic;

      let P,Q be RedSequence of ( ==>.-relation TS) such that

       A2: (P . 1) = (Q . 1);

      defpred P[ Nat] means $1 in ( dom P) & $1 in ( dom Q) implies (P . $1) = (Q . $1);

       A3:

      now

        let k;

        assume

         A4: P[k];

        now

          assume

           A5: (k + 1) in ( dom P) & (k + 1) in ( dom Q);

          per cases ;

            suppose

             A6: k in ( dom P) & k in ( dom Q);

            then [(P . k), (P . (k + 1))] in ( ==>.-relation TS) & [(Q . k), (Q . (k + 1))] in ( ==>.-relation TS) by A5, REWRITE1:def 2;

            hence (P . (k + 1)) = (Q . (k + 1)) by A1, A4, A6, Th44;

          end;

            suppose not k in ( dom P) or not k in ( dom Q);

            then k = 0 by A5, REWRITE2: 1;

            hence (P . (k + 1)) = (Q . (k + 1)) by A2;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A7: P[ 0 ] by FINSEQ_3: 25;

      for k holds P[k] from NAT_1:sch 2( A7, A3);

      hence thesis;

    end;

    theorem :: REWRITE3:68

    

     Th68: TS is deterministic implies for P,Q be RedSequence of ( ==>.-relation TS) st (P . 1) = (Q . 1) & ( len P) = ( len Q) holds P = Q

    proof

      assume

       A1: TS is deterministic;

      let P,Q be RedSequence of ( ==>.-relation TS) such that

       A2: (P . 1) = (Q . 1) and

       A3: ( len P) = ( len Q);

      now

        let k;

        assume

         A4: k in ( dom P);

        then 1 <= k & k <= ( len P) by FINSEQ_3: 25;

        then k in ( dom Q) by A3, FINSEQ_3: 25;

        hence (P . k) = (Q . k) by A1, A2, A4, Th67;

      end;

      hence thesis by A3, FINSEQ_2: 9;

    end;

    theorem :: REWRITE3:69

    

     Th69: TS is deterministic implies for P,Q be RedSequence of ( ==>.-relation TS) st (P . 1) = (Q . 1) & ((P . ( len P)) `2 ) = ((Q . ( len Q)) `2 ) holds P = Q

    proof

      assume

       A1: TS is deterministic;

      then

       A2: not ( <%> E) in ( rng ( dom the Tran of TS));

      let P,Q be RedSequence of ( ==>.-relation TS) such that

       A3: (P . 1) = (Q . 1) and

       A4: ((P . ( len P)) `2 ) = ((Q . ( len Q)) `2 );

      per cases by XXREAL_0: 1;

        suppose ( len P) = ( len Q);

        hence thesis by A1, A3, Th68;

      end;

        suppose

         A5: ( len P) > ( len Q);

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

        then

         A6: ( len P) in ( dom P) by FINSEQ_3: 25;

        set k = ( len Q);

        

         A7: k >= ( 0 + 1) by NAT_1: 13;

        then

         A8: k in ( dom P) by A5, FINSEQ_3: 25;

        k in ( dom Q) by A7, FINSEQ_3: 25;

        then ((P . ( len Q)) `2 ) = ((P . ( len P)) `2 ) by A1, A3, A4, A8, Th67;

        hence thesis by A2, A5, A8, A6, Th66;

      end;

        suppose

         A9: ( len P) < ( len Q);

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

        then

         A10: ( len Q) in ( dom Q) by FINSEQ_3: 25;

        set k = ( len P);

        

         A11: k >= ( 0 + 1) by NAT_1: 13;

        then

         A12: k in ( dom Q) by A9, FINSEQ_3: 25;

        k in ( dom P) by A11, FINSEQ_3: 25;

        then ((Q . ( len P)) `2 ) = ((Q . ( len Q)) `2 ) by A1, A3, A4, A12, Th67;

        hence thesis by A2, A9, A12, A10, Th66;

      end;

    end;

    begin

    theorem :: REWRITE3:70

    

     Th70: ( ==>.-relation TS) reduces ( [x, v], [y, w]) implies ex u st v = (u ^ w)

    proof

      assume ( ==>.-relation TS) reduces ( [x, v], [y, w]);

      then ex P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, v] & (P . ( len P)) = [y, w] by REWRITE1:def 3;

      hence thesis by Th53;

    end;

    theorem :: REWRITE3:71

    

     Th71: ( ==>.-relation TS) reduces ( [x, u], [y, v]) implies ( ==>.-relation TS) reduces ( [x, (u ^ w)], [y, (v ^ w)])

    proof

      assume ( ==>.-relation TS) reduces ( [x, u], [y, v]);

      then

      consider P be RedSequence of ( ==>.-relation TS) such that

       A1: (P . 1) = [x, u] and

       A2: (P . ( len P)) = [y, v] by REWRITE1:def 3;

      

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

      then ( len P) in ( dom P) by FINSEQ_3: 25;

      

      then

       A4: ( dim2 ((P . ( len P)),E)) = ((P . ( len P)) `2 ) by A1, Th51

      .= v by A2;

      deffunc F( set) = [((P . $1) `1 ), (( dim2 ((P . $1),E)) ^ w)];

      consider Q be FinSequence such that

       A5: ( len Q) = ( len P) and

       A6: for k st k in ( dom Q) holds (Q . k) = F(k) from FINSEQ_1:sch 2;

      for k be Nat st k in ( dom Q) & (k + 1) in ( dom Q) holds [(Q . k), (Q . (k + 1))] in ( ==>.-relation TS)

      proof

        let k be Nat such that

         A7: k in ( dom Q) and

         A8: (k + 1) in ( dom Q);

        1 <= (k + 1) & (k + 1) <= ( len Q) by A8, FINSEQ_3: 25;

        then

         A9: (k + 1) in ( dom P) by A5, FINSEQ_3: 25;

        1 <= k & k <= ( len Q) by A7, FINSEQ_3: 25;

        then

         A10: k in ( dom P) by A5, FINSEQ_3: 25;

        then [(P . k), (P . (k + 1))] in ( ==>.-relation TS) by A9, REWRITE1:def 2;

        then [ [((P . k) `1 ), ((P . k) `2 )], (P . (k + 1))] in ( ==>.-relation TS) by A10, A9, Th48;

        then [ [((P . k) `1 ), ((P . k) `2 )], [((P . (k + 1)) `1 ), ((P . (k + 1)) `2 )]] in ( ==>.-relation TS) by A10, A9, Th48;

        then [ [((P . k) `1 ), ( dim2 ((P . k),E))], [((P . (k + 1)) `1 ), ((P . (k + 1)) `2 )]] in ( ==>.-relation TS) by A1, A10, Th51;

        then [ [((P . k) `1 ), ( dim2 ((P . k),E))], [((P . (k + 1)) `1 ), ( dim2 ((P . (k + 1)),E))]] in ( ==>.-relation TS) by A1, A9, Th51;

        then (((P . k) `1 ),( dim2 ((P . k),E))) ==>. (((P . (k + 1)) `1 ),( dim2 ((P . (k + 1)),E)),TS) by Def4;

        then (((P . k) `1 ),(( dim2 ((P . k),E)) ^ w)) ==>. (((P . (k + 1)) `1 ),(( dim2 ((P . (k + 1)),E)) ^ w),TS) by Th25;

        then [ [((P . k) `1 ), (( dim2 ((P . k),E)) ^ w)], [((P . (k + 1)) `1 ), (( dim2 ((P . (k + 1)),E)) ^ w)]] in ( ==>.-relation TS) by Def4;

        then [ [((P . k) `1 ), (( dim2 ((P . k),E)) ^ w)], (Q . (k + 1))] in ( ==>.-relation TS) by A6, A8;

        hence thesis by A6, A7;

      end;

      then

      reconsider Q as RedSequence of ( ==>.-relation TS) by A5, REWRITE1:def 2;

      

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

      then ( len Q) in ( dom Q) by FINSEQ_3: 25;

      then (Q . ( len Q)) = [((P . ( len Q)) `1 ), (( dim2 ((P . ( len Q)),E)) ^ w)] by A6;

      then

       A12: (Q . ( len Q)) = [y, (v ^ w)] by A2, A5, A4;

      1 in ( dom P) by A3, FINSEQ_3: 25;

      

      then

       A13: ( dim2 ((P . 1),E)) = ((P . 1) `2 ) by A1, Th51

      .= u by A1;

      1 in ( dom Q) by A11, FINSEQ_3: 25;

      

      then (Q . 1) = [((P . 1) `1 ), (( dim2 ((P . 1),E)) ^ w)] by A6

      .= [x, (u ^ w)] by A1, A13;

      hence thesis by A12, REWRITE1:def 3;

    end;

    theorem :: REWRITE3:72

    

     Th72: (x,y) -->. (z,TS) implies ( ==>.-relation TS) reduces ( [x, y], [z, ( <%> E)])

    proof

      assume (x,y) -->. (z,TS);

      then <* [x, y], [z, ( <%> E)]*> is RedSequence of ( ==>.-relation TS) by Th57;

      then [ [x, y], [z, ( <%> E)]] in ( ==>.-relation TS) by Th8;

      hence thesis by REWRITE1: 15;

    end;

    theorem :: REWRITE3:73

    

     Th73: (x,v) -->. (y,TS) implies ( ==>.-relation TS) reduces ( [x, (v ^ w)], [y, w])

    proof

      assume (x,v) -->. (y,TS);

      then <* [x, (v ^ w)], [y, w]*> is RedSequence of ( ==>.-relation TS) by Th58;

      then [ [x, (v ^ w)], [y, w]] in ( ==>.-relation TS) by Th8;

      hence thesis by REWRITE1: 15;

    end;

    theorem :: REWRITE3:74

    

     Th74: (x1,x2) ==>. (y1,y2,TS) implies ( ==>.-relation TS) reduces ( [x1, x2], [y1, y2])

    proof

      assume (x1,x2) ==>. (y1,y2,TS);

      then [ [x1, x2], [y1, y2]] in ( ==>.-relation TS) by Def4;

      hence thesis by REWRITE1: 15;

    end;

    theorem :: REWRITE3:75

    

     Th75: ( ==>.-relation TS) reduces ( [x, v], [y, w]) implies ( len v) >= ( len w)

    proof

      assume ( ==>.-relation TS) reduces ( [x, v], [y, w]);

      then ex P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, v] & (P . ( len P)) = [y, w] by REWRITE1:def 3;

      hence thesis by Th59;

    end;

    theorem :: REWRITE3:76

    ( ==>.-relation TS) reduces ( [x, w], [y, (v ^ w)]) implies v = ( <%> E)

    proof

      assume ( ==>.-relation TS) reduces ( [x, w], [y, (v ^ w)]);

      then ( len w) >= ( len (v ^ w)) by Th75;

      then (( len v) + ( len w)) <= ( 0 + ( len w)) by AFINSQ_1: 17;

      hence thesis by XREAL_1: 6;

    end;

    theorem :: REWRITE3:77

    

     Th77: not ( <%> E) in ( rng ( dom the Tran of TS)) implies (( ==>.-relation TS) reduces ( [x, v], [y, w]) implies ( len v) > ( len w) or x = y & v = w)

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume ( ==>.-relation TS) reduces ( [x, v], [y, w]);

      then ex P be RedSequence of ( ==>.-relation TS) st (P . 1) = [x, v] & (P . ( len P)) = [y, w] by REWRITE1:def 3;

      hence thesis by A1, Th64;

    end;

    theorem :: REWRITE3:78

     not ( <%> E) in ( rng ( dom the Tran of TS)) implies (( ==>.-relation TS) reduces ( [x, u], [y, u]) implies x = y)

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume ( ==>.-relation TS) reduces ( [x, u], [y, u]);

      then ( len u) > ( len u) or x = y by A1, Th77;

      hence thesis;

    end;

    theorem :: REWRITE3:79

    

     Th79: not ( <%> E) in ( rng ( dom the Tran of TS)) implies (( ==>.-relation TS) reduces ( [x, <%e%>], [y, ( <%> E)]) implies [ [x, <%e%>], [y, ( <%> E)]] in ( ==>.-relation TS))

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume ( ==>.-relation TS) reduces ( [x, <%e%>], [y, ( <%> E)]);

      then

      consider P be RedSequence of ( ==>.-relation TS) such that

       A2: (P . 1) = [x, <%e%>] & (P . ( len P)) = [y, ( <%> E)] by REWRITE1:def 3;

      

       A3: ( len P) = (1 + 1) by A1, A2, Th63;

      then 1 in ( dom P) & (1 + 1) in ( dom P) by FINSEQ_3: 25;

      hence thesis by A2, A3, REWRITE1:def 2;

    end;

    theorem :: REWRITE3:80

    

     Th80: TS is deterministic implies (( ==>.-relation TS) reduces (x, [y1, z]) & ( ==>.-relation TS) reduces (x, [y2, z]) implies y1 = y2)

    proof

      assume

       A1: TS is deterministic;

      assume that

       A2: ( ==>.-relation TS) reduces (x, [y1, z]) and

       A3: ( ==>.-relation TS) reduces (x, [y2, z]);

      consider P be RedSequence of ( ==>.-relation TS) such that

       A4: (P . 1) = x and

       A5: (P . ( len P)) = [y1, z] by A2, REWRITE1:def 3;

      consider Q be RedSequence of ( ==>.-relation TS) such that

       A6: (Q . 1) = x and

       A7: (Q . ( len Q)) = [y2, z] by A3, REWRITE1:def 3;

      

       A8: ((Q . ( len Q)) `2 ) = z by A7;

      ((P . ( len P)) `2 ) = z by A5;

      then P = Q by A1, A4, A6, A8, Th69;

      hence thesis by A5, A7, XTUPLE_0: 1;

    end;

    begin

    definition

      let E, F, TS;

      let x1,x2,y1,y2 be object;

      :: REWRITE3:def6

      pred x1,x2 ==>* y1,y2,TS means ( ==>.-relation TS) reduces ( [x1, x2], [y1, y2]);

    end

    theorem :: REWRITE3:81

    

     Th81: for TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds (x1,x2) ==>* (y1,y2,TS1) implies (x1,x2) ==>* (y1,y2,TS2) by Th34;

    theorem :: REWRITE3:82

    

     Th82: (x,y) ==>* (x,y,TS) by REWRITE1: 12;

    theorem :: REWRITE3:83

    

     Th83: (x1,x2) ==>* (y1,y2,TS) & (y1,y2) ==>* (z1,z2,TS) implies (x1,x2) ==>* (z1,z2,TS) by REWRITE1: 16;

    theorem :: REWRITE3:84

    

     Th84: (x,y) -->. (z,TS) implies (x,y) ==>* (z,( <%> E),TS) by Th72;

    theorem :: REWRITE3:85

    (x,v) -->. (y,TS) implies (x,(v ^ w)) ==>* (y,w,TS) by Th73;

    theorem :: REWRITE3:86

    

     Th86: (x,u) ==>* (y,v,TS) implies (x,(u ^ w)) ==>* (y,(v ^ w),TS) by Th71;

    theorem :: REWRITE3:87

    

     Th87: (x1,x2) ==>. (y1,y2,TS) implies (x1,x2) ==>* (y1,y2,TS) by Th74;

    theorem :: REWRITE3:88

    

     Th88: (x,v) ==>* (y,w,TS) implies ex u st v = (u ^ w) by Th70;

    theorem :: REWRITE3:89

    

     Th89: (x,v) ==>* (y,w,TS) implies ( len w) <= ( len v)

    proof

      assume (x,v) ==>* (y,w,TS);

      then ex u st v = (u ^ w) by Th88;

      hence thesis by Th9;

    end;

    theorem :: REWRITE3:90

    (x,w) ==>* (y,(v ^ w),TS) implies v = ( <%> E)

    proof

      assume (x,w) ==>* (y,(v ^ w),TS);

      then ( len (v ^ w)) <= ( len w) by Th89;

      then (( len v) + ( len w)) <= ( 0 + ( len w)) by AFINSQ_1: 17;

      hence thesis by XREAL_1: 6;

    end;

    theorem :: REWRITE3:91

    

     Th91: not ( <%> E) in ( rng ( dom the Tran of TS)) implies ((x,u) ==>* (y,u,TS) iff x = y)

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      thus (x,u) ==>* (y,u,TS) implies x = y

      proof

        assume (x,u) ==>* (y,u,TS);

        then ( ==>.-relation TS) reduces ( [x, u], [y, u]);

        then ex p be RedSequence of ( ==>.-relation TS) st (p . 1) = [x, u] & (p . ( len p)) = [y, u] by REWRITE1:def 3;

        hence thesis by A1, Th60;

      end;

      assume x = y;

      hence thesis by Th82;

    end;

    theorem :: REWRITE3:92

    

     Th92: not ( <%> E) in ( rng ( dom the Tran of TS)) implies ((x, <%e%>) ==>* (y,( <%> E),TS) implies (x, <%e%>) ==>. (y,( <%> E),TS))

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

      assume (x, <%e%>) ==>* (y,( <%> E),TS);

      then ( ==>.-relation TS) reduces ( [x, <%e%>], [y, ( <%> E)]);

      then [ [x, <%e%>], [y, ( <%> E)]] in ( ==>.-relation TS) by A1, Th79;

      hence thesis by Def4;

    end;

    theorem :: REWRITE3:93

    

     Th93: TS is deterministic implies ((x1,x2) ==>* (y1,z,TS) & (x1,x2) ==>* (y2,z,TS) implies y1 = y2) by Th80;

    begin

    definition

      let E, F, TS;

      let x1,x2,y be object;

      :: REWRITE3:def7

      pred x1,x2 ==>* y,TS means (x1,x2) ==>* (y,( <%> E),TS);

    end

    theorem :: REWRITE3:94

    

     Th94: for TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds (x,y) ==>* (z,TS1) implies (x,y) ==>* (z,TS2) by Th81;

    theorem :: REWRITE3:95

    

     Th95: (x,( <%> E)) ==>* (x,TS) by Th82;

    theorem :: REWRITE3:96

    

     Th96: (x,u) ==>* (y,TS) implies (x,(u ^ v)) ==>* (y,v,TS)

    proof

      assume (x,u) ==>* (y,TS);

      then (x,u) ==>* (y,( <%> E),TS);

      then (x,(u ^ v)) ==>* (y,( {} ^ v),TS) by Th86;

      hence thesis;

    end;

    theorem :: REWRITE3:97

    (x,y) -->. (z,TS) implies (x,y) ==>* (z,TS) by Th84;

    theorem :: REWRITE3:98

    (x1,x2) ==>. (y,( <%> E),TS) implies (x1,x2) ==>* (y,TS) by Th87;

    theorem :: REWRITE3:99

    (x,u) ==>* (y,TS) & (y,v) ==>* (z,TS) implies (x,(u ^ v)) ==>* (z,TS)

    proof

      assume that

       A1: (x,u) ==>* (y,TS) and

       A2: (y,v) ==>* (z,TS);

      (x,((u ^ v) ^ {} )) ==>* (y,v,TS) by A1, Th96;

      then

       A3: (x,((u ^ v) ^ ( <%> E))) ==>* (y,(v ^ {} ),TS);

      (y,v) ==>* (z,( <%> E),TS) by A2;

      then (x,((u ^ v) ^ {} )) ==>* (z,( <%> E),TS) by A3, Th83;

      hence thesis;

    end;

    theorem :: REWRITE3:100

    

     Th100: not ( <%> E) in ( rng ( dom the Tran of TS)) implies ((x,( <%> E)) ==>* (y,TS) iff x = y) by Th91;

    theorem :: REWRITE3:101

     not ( <%> E) in ( rng ( dom the Tran of TS)) implies ((x, <%e%>) ==>* (y,TS) implies (x, <%e%>) ==>. (y,( <%> E),TS)) by Th92;

    theorem :: REWRITE3:102

    TS is deterministic implies ((x1,x2) ==>* (y1,TS) & (x1,x2) ==>* (y2,TS) implies y1 = y2) by Th93;

    begin

    definition

      let E, F, TS, x, X;

      :: REWRITE3:def8

      func x -succ_of (X,TS) -> Subset of TS equals { s : ex t st t in X & (t,x) ==>* (s,TS) };

      coherence

      proof

        set Y = { s : ex t st t in X & (t,x) ==>* (s,TS) };

        Y c= the carrier of TS

        proof

          let y be object;

          assume y in Y;

          then ex s st s = y & ex t st t in X & (t,x) ==>* (s,TS);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: REWRITE3:103

    

     Th103: s in (x -succ_of (X,TS)) iff ex t st t in X & (t,x) ==>* (s,TS)

    proof

      thus s in (x -succ_of (X,TS)) implies ex t st t in X & (t,x) ==>* (s,TS)

      proof

        assume s in (x -succ_of (X,TS));

        then ex s9 st s9 = s & ex t st t in X & (t,x) ==>* (s9,TS);

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: REWRITE3:104

     not ( <%> E) in ( rng ( dom the Tran of TS)) implies (( <%> E) -succ_of (S,TS)) = S

    proof

      assume

       A1: not ( <%> E) in ( rng ( dom the Tran of TS));

       A2:

      now

        let x be object;

        assume x in (( <%> E) -succ_of (S,TS));

        then ex s st s in S & (s,( <%> E)) ==>* (x,TS) by Th103;

        hence x in S by A1, Th100;

      end;

      now

        let x be object;

        assume

         A3: x in S;

        (x,( <%> E)) ==>* (x,TS) by Th95;

        hence x in (( <%> E) -succ_of (S,TS)) by A3;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: REWRITE3:105

    for TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds (x -succ_of (X,TS1)) = (x -succ_of (X,TS2))

    proof

      let TS1 be non empty transition-system over F1, TS2 be non empty transition-system over F2 such that

       A1: the carrier of TS1 = the carrier of TS2 and

       A2: the Tran of TS1 = the Tran of TS2;

       A3:

      now

        let y be object;

        assume

         A4: y in (x -succ_of (X,TS2));

        then

        reconsider q = y as Element of TS2;

        consider p be Element of TS2 such that

         A5: p in X and

         A6: (p,x) ==>* (q,TS2) by A4, Th103;

        reconsider q as Element of TS1 by A1;

        reconsider p as Element of TS1 by A1;

        (p,x) ==>* (q,TS1) by A1, A2, A6, Th94;

        hence y in (x -succ_of (X,TS1)) by A5;

      end;

      now

        let y be object;

        assume

         A7: y in (x -succ_of (X,TS1));

        then

        reconsider q = y as Element of TS1;

        consider p be Element of TS1 such that

         A8: p in X and

         A9: (p,x) ==>* (q,TS1) by A7, Th103;

        reconsider q as Element of TS2 by A1;

        reconsider p as Element of TS2 by A1;

        (p,x) ==>* (q,TS2) by A1, A2, A9, Th94;

        hence y in (x -succ_of (X,TS2)) by A8;

      end;

      hence thesis by A3, TARSKI: 2;

    end;