ami_4.miz



    begin

    reserve i,j,k for Nat;

    set a = ( dl. 0 ), b = ( dl. 1), c = ( dl. 2);

    

     Lm1: a <> b & b <> c by AMI_3: 10;

    

     Lm2: c <> a by AMI_3: 10;

    begin

    definition

      :: AMI_4:def1

      func Euclid-Algorithm -> NAT -definedthe InstructionsF of SCM -valued finite Function equals (( 0 .--> (( dl. 2) := ( dl. 1))) +* ((1 .--> ( Divide (( dl. 0 ),( dl. 1)))) +* ((2 .--> (( dl. 0 ) := ( dl. 2))) +* ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM ))))));

      coherence ;

    end

    defpred P[ Instruction-Sequence of SCM ] means ($1 . 0 ) = (c := b) & ($1 . 1) = ( Divide (a,b)) & ($1 . 2) = (a := c) & ($1 . 3) = (b >0_goto 0 ) & $1 halts_at 4;

    set IN0 = ( 0 .--> (( dl. 2) := b));

    set IN1 = (1 .--> ( Divide (a,b)));

    set IN2 = (2 .--> (a := ( dl. 2)));

    set IN3 = (3 .--> (b >0_goto 0 ));

    set IN4 = (4 .--> ( halt SCM ));

    set EA3 = (IN3 +* IN4);

    set EA2 = (IN2 +* EA3);

    set EA1 = (IN1 +* EA2);

    set EA0 = (IN0 +* EA1);

    theorem :: AMI_4:1

    

     Th1: ( dom Euclid-Algorithm qua Function) = 5

    proof

      ( dom IN3) = {3} & ( dom IN4) = {4};

      

      then

       A1: ( dom EA3) = ( {3} \/ {4}) by FUNCT_4:def 1

      .= {3, 4} by ENUMSET1: 1;

      

       A2: ( dom IN1) = {1};

      ( dom IN2) = {2};

      

      then ( dom EA2) = ( {2} \/ {3, 4}) by A1, FUNCT_4:def 1

      .= {2, 3, 4} by ENUMSET1: 2;

      

      then

       A3: ( dom EA1) = ( {1} \/ {2, 3, 4}) by A2, FUNCT_4:def 1

      .= {1, 2, 3, 4} by ENUMSET1: 4;

      ( dom IN0) = { 0 };

      

      then ( dom EA0) = ( { 0 } \/ {1, 2, 3, 4}) by A3, FUNCT_4:def 1

      .= 5 by CARD_1: 53, ENUMSET1: 7;

      hence thesis;

    end;

    

     Lm3: for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds P[P]

    proof

      let P be Instruction-Sequence of SCM ;

      assume

       A1: Euclid-Algorithm c= P;

      EA1 c= EA0 by FUNCT_4: 25;

      then

       A2: EA1 c= P by A1;

      EA2 c= EA1 by FUNCT_4: 25;

      then

       A3: EA2 c= P by A2;

      EA3 c= EA2 by FUNCT_4: 25;

      then

       A4: EA3 c= P by A3;

      

       A5: ( dom IN4) = {4};

      

       A6: not 3 in ( dom IN4) by TARSKI:def 1;

      ( dom IN3) = {3};

      

      then

       A7: ( dom EA3) = ( {3} \/ {4}) by A5, FUNCT_4:def 1

      .= {3, 4} by ENUMSET1: 1;

      then

       A8: not 2 in ( dom EA3) by TARSKI:def 2;

      ( dom IN2) = {2};

      

      then

       A9: ( dom EA2) = ( {2} \/ {3, 4}) by A7, FUNCT_4:def 1

      .= {2, 3, 4} by ENUMSET1: 2;

      then

       A10: not 1 in ( dom EA2) by ENUMSET1:def 1;

      ( dom IN1) = {1};

      

      then

       A11: ( dom EA1) = ( {1} \/ {2, 3, 4}) by A9, FUNCT_4:def 1

      .= {1, 2, 3, 4} by ENUMSET1: 4;

      then

       A12: not 0 in ( dom EA1);

       0 in ( dom EA0) by Th1, CARD_1: 53, ENUMSET1:def 3;

      

      hence (P . 0 ) = (EA0 . 0 ) by A1, GRFUNC_1: 2

      .= (IN0 . 0 ) by A12, FUNCT_4: 11

      .= (c := b) by FUNCOP_1: 72;

      1 in ( dom EA1) by A11, ENUMSET1:def 2;

      

      hence (P . 1) = (EA1 . 1) by A2, GRFUNC_1: 2

      .= (IN1 . 1) by A10, FUNCT_4: 11

      .= ( Divide (a,b)) by FUNCOP_1: 72;

      2 in ( dom EA2) by A9, ENUMSET1:def 1;

      

      hence (P . 2) = (EA2 . 2) by A3, GRFUNC_1: 2

      .= (IN2 . 2) by A8, FUNCT_4: 11

      .= (a := c) by FUNCOP_1: 72;

      

       A13: 4 in ( dom IN4) by TARSKI:def 1;

      3 in ( dom EA3) by A7, TARSKI:def 2;

      

      hence (P . 3) = (EA3 . 3) by A4, GRFUNC_1: 2

      .= (IN3 . 3) by A6, FUNCT_4: 11

      .= (b >0_goto 0 ) by FUNCOP_1: 72;

      

       A14: 4 in ( dom EA3) by A7, TARSKI:def 2;

      

      thus (P . 4) = (EA3 . 4) by A4, A14, GRFUNC_1: 2

      .= (IN4 . 4) by A13, FUNCT_4: 13

      .= ( halt SCM ) by FUNCOP_1: 72;

    end;

    begin

    theorem :: AMI_4:2

    

     Th2: for s be State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds for k st ( IC ( Comput (P,s,k))) = 0 holds ( IC ( Comput (P,s,(k + 1)))) = 1 & (( Comput (P,s,(k + 1))) . ( dl. 0 )) = (( Comput (P,s,k)) . ( dl. 0 )) & (( Comput (P,s,(k + 1))) . ( dl. 1)) = (( Comput (P,s,k)) . ( dl. 1)) & (( Comput (P,s,(k + 1))) . ( dl. 2)) = (( Comput (P,s,k)) . ( dl. 1))

    proof

      let s be State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P;

      let k;

      assume

       A2: ( IC ( Comput (P,s,k))) = 0 ;

      

       A3: ( Comput (P,s,(k + 1))) = ( Exec ((P . ( IC ( Comput (P,s,k)))),( Comput (P,s,k)))) by EXTPRO_1: 6

      .= ( Exec ((c := b),( Comput (P,s,k)))) by A1, A2, Lm3;

      

      hence ( IC ( Comput (P,s,(k + 1)))) = (( IC ( Comput (P,s,k))) + 1) by AMI_3: 2

      .= 1 by A2;

      thus (( Comput (P,s,(k + 1))) . a) = (( Comput (P,s,k)) . a) & (( Comput (P,s,(k + 1))) . b) = (( Comput (P,s,k)) . b) by A3, AMI_3: 2, AMI_3: 10;

      thus thesis by A3, AMI_3: 2;

    end;

    theorem :: AMI_4:3

    

     Th3: for s be State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds for k st ( IC ( Comput (P,s,k))) = 1 holds ( IC ( Comput (P,s,(k + 1)))) = 2 & (( Comput (P,s,(k + 1))) . ( dl. 0 )) = ((( Comput (P,s,k)) . ( dl. 0 )) div (( Comput (P,s,k)) . ( dl. 1))) & (( Comput (P,s,(k + 1))) . ( dl. 1)) = ((( Comput (P,s,k)) . ( dl. 0 )) mod (( Comput (P,s,k)) . ( dl. 1))) & (( Comput (P,s,(k + 1))) . ( dl. 2)) = (( Comput (P,s,k)) . ( dl. 2))

    proof

      let s be State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P;

      let k such that

       A2: ( IC ( Comput (P,s,k))) = 1;

      

       A3: ( Comput (P,s,(k + 1))) = ( Exec ((P . ( IC ( Comput (P,s,k)))),( Comput (P,s,k)))) by EXTPRO_1: 6

      .= ( Exec (( Divide (a,b)),( Comput (P,s,k)))) by A1, A2, Lm3;

      

      hence ( IC ( Comput (P,s,(k + 1)))) = (( IC ( Comput (P,s,k))) + 1) by AMI_3: 6

      .= 2 by A2;

      thus thesis by A3, Lm1, Lm2, AMI_3: 6;

    end;

    theorem :: AMI_4:4

    

     Th4: for s be State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds for k st ( IC ( Comput (P,s,k))) = 2 holds ( IC ( Comput (P,s,(k + 1)))) = 3 & (( Comput (P,s,(k + 1))) . ( dl. 0 )) = (( Comput (P,s,k)) . ( dl. 2)) & (( Comput (P,s,(k + 1))) . ( dl. 1)) = (( Comput (P,s,k)) . ( dl. 1)) & (( Comput (P,s,(k + 1))) . ( dl. 2)) = (( Comput (P,s,k)) . ( dl. 2))

    proof

      let s be State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P;

      let k;

      assume

       A2: ( IC ( Comput (P,s,k))) = 2;

      

       A3: ( Comput (P,s,(k + 1))) = ( Exec ((P . ( IC ( Comput (P,s,k)))),( Comput (P,s,k)))) by EXTPRO_1: 6

      .= ( Exec ((a := c),( Comput (P,s,k)))) by A1, A2, Lm3;

      

      hence ( IC ( Comput (P,s,(k + 1)))) = (( IC ( Comput (P,s,k))) + 1) by AMI_3: 2

      .= 3 by A2;

      thus (( Comput (P,s,(k + 1))) . a) = (( Comput (P,s,k)) . c) by A3, AMI_3: 2;

      thus thesis by A3, AMI_3: 2, AMI_3: 10;

    end;

    theorem :: AMI_4:5

    

     Th5: for s be State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds for k st ( IC ( Comput (P,s,k))) = 3 holds ((( Comput (P,s,k)) . ( dl. 1)) > 0 implies ( IC ( Comput (P,s,(k + 1)))) = 0 ) & ((( Comput (P,s,k)) . ( dl. 1)) <= 0 implies ( IC ( Comput (P,s,(k + 1)))) = 4) & (( Comput (P,s,(k + 1))) . ( dl. 0 )) = (( Comput (P,s,k)) . ( dl. 0 )) & (( Comput (P,s,(k + 1))) . ( dl. 1)) = (( Comput (P,s,k)) . ( dl. 1))

    proof

      let s be State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P;

      let k;

      assume

       A2: ( IC ( Comput (P,s,k))) = 3;

      

       A3: ( Comput (P,s,(k + 1))) = ( Exec ((P . ( IC ( Comput (P,s,k)))),( Comput (P,s,k)))) by EXTPRO_1: 6

      .= ( Exec ((b >0_goto 0 ),( Comput (P,s,k)))) by A1, A2, Lm3;

      hence (( Comput (P,s,k)) . b) > 0 implies ( IC ( Comput (P,s,(k + 1)))) = 0 by AMI_3: 9;

      thus (( Comput (P,s,k)) . b) <= 0 implies ( IC ( Comput (P,s,(k + 1)))) = 4

      proof

        assume (( Comput (P,s,k)) . b) <= 0 ;

        

        hence ( IC ( Comput (P,s,(k + 1)))) = (( IC ( Comput (P,s,k))) + 1) by A3, AMI_3: 9

        .= 4 by A2;

      end;

      thus thesis by A3, AMI_3: 9;

    end;

    theorem :: AMI_4:6

    

     Th6: for s be State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds for k, i st ( IC ( Comput (P,s,k))) = 4 holds ( Comput (P,s,(k + i))) = ( Comput (P,s,k))

    proof

      let s be State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P;

      let k, i;

      assume ( IC ( Comput (P,s,k))) = 4;

      then P halts_at ( IC ( Comput (P,s,k))) by A1, Lm3;

      hence thesis by EXTPRO_1: 20, NAT_1: 11;

    end;

    

     Lm4: for s be 0 -started State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P & (s . a) > 0 & (s . b) > 0 holds (( Comput (P,s,(4 * k))) . a) > 0 & ((( Comput (P,s,(4 * k))) . b) > 0 & ( IC ( Comput (P,s,(4 * k)))) = 0 or (( Comput (P,s,(4 * k))) . b) = 0 & ( IC ( Comput (P,s,(4 * k)))) = 4)

    proof

      let s be 0 -started State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P and

       A2: (s . a) > 0 & (s . b) > 0 ;

      

       A3: ( IC s) = 0 by MEMSTR_0:def 12;

      defpred P[ Nat] means (( Comput (P,s,(4 * $1))) . a) > 0 & ((( Comput (P,s,(4 * $1))) . b) > 0 & ( IC ( Comput (P,s,(4 * $1)))) = 0 or (( Comput (P,s,(4 * $1))) . b) = 0 & ( IC ( Comput (P,s,(4 * $1)))) = 4);

      

       A4: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        set c4 = ( Comput (P,s,(4 * k))), c5 = ( Comput (P,s,((4 * k) + 1))), c6 = ( Comput (P,s,((4 * k) + 2))), c7 = ( Comput (P,s,((4 * k) + 3))), c8 = ( Comput (P,s,((4 * k) + 4)));

        

         A5: c7 = ( Comput (P,s,(((4 * k) + 2) + 1)));

        

         A6: c8 = ( Comput (P,s,(((4 * k) + 3) + 1)));

        assume

         A7: (c4 . a) > 0 ;

        assume

         A8: (c4 . b) > 0 & ( IC c4) = 0 or (c4 . b) = 0 & ( IC c4) = 4;

        

         A9: c6 = ( Comput (P,s,(((4 * k) + 1) + 1)));

        now

          per cases by A8;

            case

             A10: (c4 . b) > 0 ;

            then

             A11: ( IC c5) = 1 by A1, A8, Th2;

            then

             A12: ( IC c6) = 2 by A1, A9, Th3;

            then

             A13: ( IC c7) = 3 by A1, A5, Th4;

            then

             A14: (c8 . b) = (c7 . b) by A1, A6, Th5;

            

             A15: (c7 . a) = (c6 . c) & (c7 . b) = (c6 . b) by A1, A5, A12, Th4;

            

             A16: (c6 . b) = ((c5 . a) mod (c5 . b)) & (c6 . c) = (c5 . c) by A1, A9, A11, Th3;

            

             A17: (c5 . b) = (c4 . b) & (c5 . c) = (c4 . b) by A1, A8, A10, Th2;

            thus (c8 . a) > 0 by A1, A6, A10, A17, A16, A13, A15, Th5;

            (c8 . b) is positive or (c8 . b) is zero by A10, A17, A16, A15, A14, NEWTON: 64;

            hence (c8 . b) > 0 & ( IC c8) = 0 or (c8 . b) = 0 & ( IC c8) = 4 by A1, A6, A13, A14, Th5;

          end;

            case (c4 . b) = 0 ;

            hence (c8 . a) > 0 & (c8 . b) = 0 & ( IC c8) = 4 by A1, A7, A8, Th6;

          end;

        end;

        hence thesis;

      end;

      

       A18: P[ 0 ] by A3, A2, EXTPRO_1: 2;

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

      hence thesis;

    end;

    

     Lm5: for s be 0 -started State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P & (s . a) > 0 & (s . b) > 0 holds (( Comput (P,s,(4 * k))) . b) > 0 implies (( Comput (P,s,(4 * (k + 1)))) . a) = (( Comput (P,s,(4 * k))) . b) & (( Comput (P,s,(4 * (k + 1)))) . b) = ((( Comput (P,s,(4 * k))) . a) mod (( Comput (P,s,(4 * k))) . b))

    proof

      let s be 0 -started State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P and

       A2: (s . a) > 0 & (s . b) > 0 and

       A3: (( Comput (P,s,(4 * k))) . b) > 0 ;

      set c4 = ( Comput (P,s,(4 * k))), c5 = ( Comput (P,s,((4 * k) + 1))), c6 = ( Comput (P,s,((4 * k) + 2))), c7 = ( Comput (P,s,((4 * k) + 3)));

      

       A4: (c4 . b) > 0 & ( IC c4) = 0 or (c4 . b) = 0 & ( IC c4) = 4 by A1, A2, Lm4;

      then

       A5: c6 = ( Comput (P,s,(((4 * k) + 1) + 1))) & ( IC c5) = 1 by A1, A3, Th2;

      then

       A6: (c6 . c) = (c5 . c) by A1, Th3;

      

       A7: c7 = ( Comput (P,s,(((4 * k) + 2) + 1))) & ( IC c6) = 2 by A1, A5, Th3;

      then

       A8: ( Comput (P,s,((4 * k) + 4))) = ( Comput (P,s,(((4 * k) + 3) + 1))) & ( IC c7) = 3 by A1, Th4;

      

       A9: (c7 . a) = (c6 . c) by A1, A7, Th4;

      (c5 . c) = (c4 . b) by A1, A3, A4, Th2;

      hence (( Comput (P,s,(4 * (k + 1)))) . a) = (( Comput (P,s,(4 * k))) . b) by A1, A6, A8, A9, Th5;

      

       A10: (c7 . b) = (c6 . b) by A1, A7, Th4;

      

       A11: (c6 . b) = ((c5 . a) mod (c5 . b)) by A1, A5, Th3;

      (c5 . a) = (c4 . a) & (c5 . b) = (c4 . b) by A1, A3, A4, Th2;

      hence thesis by A1, A11, A8, A10, Th5;

    end;

    

     Lm6: for s be 0 -started State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds for x,y be Integer st (s . a) = x & (s . b) = y & x > y & y > 0 holds (( Result (P,s)) . a) = (x gcd y) & ex k st P halts_at ( IC ( Comput (P,s,k)))

    proof

      let s be 0 -started State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P;

      deffunc G( Nat) = |.(( Comput (P,s,(4 * $1))) . b).|;

      deffunc F( Nat) = |.(( Comput (P,s,(4 * $1))) . a).|;

      let x,y be Integer such that

       A2: (s . a) = x and

       A3: (s . b) = y and

       A4: x > y and

       A5: y > 0 ;

       A6:

      now

        let k be Nat;

        

         A7: (( Comput (P,s,(4 * k))) . b) > 0 or (( Comput (P,s,(4 * k))) . b) = 0 by A1, A2, A3, A4, A5, Lm4;

        assume

         A8: G(k) > 0 ;

        hence F(+) = G(k) by A1, A2, A3, A4, A5, A7, Lm5, ABSVALUE: 2;

        

         A9: (( Comput (P,s,(4 * k))) . a) >= 0 by A1, A2, A3, A4, A5, Lm4;

        (( Comput (P,s,(4 * (k + 1)))) . b) >= 0 by A1, A2, A3, A4, A5, Lm4;

        

        hence G(+) = (( Comput (P,s,(4 * (k + 1)))) . b) by ABSVALUE:def 1

        .= ((( Comput (P,s,(4 * k))) . a) mod (( Comput (P,s,(4 * k))) . b)) by A1, A2, A3, A4, A5, A7, A8, Lm5, ABSVALUE: 2

        .= ( F(k) mod G(k)) by A7, A9, INT_2: 32;

      end;

      reconsider x9 = x, y9 = y as Element of NAT by A4, A5, INT_1: 3;

      

       A10: y9 < x9 by A4;

      

       A11: F(0) = |.x.| by A2, EXTPRO_1: 2

      .= x9 by ABSVALUE:def 1;

      

       A12: G(0) = |.y.| by A3, EXTPRO_1: 2

      .= y9 by ABSVALUE:def 1;

      

       A13: 0 < y9 by A5;

      consider k be Nat such that

       A14: F(k) = (x9 gcd y9) and

       A15: G(k) = 0 from NEWTON:sch 1( A13, A10, A11, A12, A6);

      

       A16: (( Comput (P,s,(4 * k))) . a) > 0 by A1, A2, A3, A4, A5, Lm4;

      (( Comput (P,s,(4 * k))) . b) = 0 by A15, ABSVALUE: 2;

      then

       A17: ( IC ( Comput (P,s,(4 * k)))) = 4 by A1, A2, A3, A4, A5, Lm4;

      

       A18: P halts_at 4 by A1, Lm3;

      

      hence (( Result (P,s)) . a) = (( Comput (P,s,(4 * k))) . a) by A17, EXTPRO_1: 18

      .= (x gcd y) by A14, A16, ABSVALUE:def 1;

      thus thesis by A17, A18;

    end;

    theorem :: AMI_4:7

    

     Th7: for s be 0 -started State of SCM holds for P be Instruction-Sequence of SCM st Euclid-Algorithm c= P holds for x,y be Integer st (s . ( dl. 0 )) = x & (s . ( dl. 1)) = y & x > 0 & y > 0 holds (( Result (P,s)) . ( dl. 0 )) = (x gcd y)

    proof

      let s be 0 -started State of SCM ;

      let P be Instruction-Sequence of SCM such that

       A1: Euclid-Algorithm c= P;

      let x,y be Integer such that

       A2: (s . a) = x & (s . b) = y and

       A3: x > 0 and

       A4: y > 0 ;

      

       A5: |.y.| = y by A4, ABSVALUE:def 1;

      now

        per cases by XXREAL_0: 1;

          case x > y;

          hence thesis by A1, A2, A4, Lm6;

        end;

          case

           A6: x = y;

          reconsider x9 = x, y9 = y as Element of NAT by A3, A4, INT_1: 3;

          take s9 = ( Comput (P,s,4));

          

           A7: s = ( Comput (P,s,(4 * 0 ))) by EXTPRO_1: 2;

          

           A8: s9 = ( Comput (P,s,(4 * ( 0 + 1))));

          (x mod y) = (x9 mod y9)

          .= 0 by A6, NAT_D: 25;

          then (s9 . b) = 0 by A1, A2, A3, A4, A7, A8, Lm5;

          then ( IC s9) = 4 by A1, A2, A3, A4, A8, Lm4;

          then P halts_at ( IC s9) by A1, Lm3;

          

          hence (( Result (P,s)) . a) = (s9 . a) by EXTPRO_1: 18

          .= y by A1, A2, A3, A4, A7, A8, Lm5

          .= (x gcd y) by A5, A6, NAT_D: 32;

        end;

          case

           A9: y > x;

          reconsider x9 = x, y9 = y as Element of NAT by A3, A4, INT_1: 3;

          take s9 = ( Comput (P,s,4));

          

           A10: s9 = ( Comput (P,s,(4 * ( 0 + 1))));

          

           A11: s = ( Comput (P,s,(4 * 0 ))) by EXTPRO_1: 2;

          then

           A12: (s9 . a) = y by A1, A2, A3, A4, A10, Lm5;

          (x mod y) = (x9 mod y9)

          .= x9 by A9, NAT_D: 24;

          then

           A13: (s9 . b) = x by A1, A2, A3, A4, A11, A10, Lm5;

          then ( IC s9) = 0 by A1, A2, A3, A4, A10, Lm4;

          then

           A14: s9 is 0 -started;

          then

          consider k0 be Nat such that

           A15: P halts_at ( IC ( Comput (P,s9,k0))) by A3, A9, A12, A13, A1, Lm6;

          

           A16: P halts_at ( IC ( Comput (P,s,(k0 + 4)))) by A15, EXTPRO_1: 4;

          (( Result (P,s9)) . a) = (x gcd y) by A3, A9, A12, A13, A14, A1, Lm6;

          hence thesis by A16, EXTPRO_1: 21;

        end;

      end;

      hence thesis;

    end;

    definition

      :: AMI_4:def2

      func Euclid-Function -> PartFunc of ( FinPartSt SCM ), ( FinPartSt SCM ) means

      : Def2: for p,q be FinPartState of SCM holds [p, q] in it iff ex x,y be Integer st x > 0 & y > 0 & p = ((( dl. 0 ),( dl. 1)) --> (x,y)) & q = (( dl. 0 ) .--> (x gcd y));

      existence

      proof

        defpred P[ object, object] means ex x,y be Integer st x > 0 & y > 0 & $1 = ((a,b) --> (x,y)) & $2 = (a .--> (x gcd y));

        

         A1: for p,q1,q2 be object st P[p, q1] & P[p, q2] holds q1 = q2

        proof

          let p,q1,q2 be object;

          given x1,y1 be Integer such that x1 > 0 and y1 > 0 and

           A2: p = ((a,b) --> (x1,y1)) and

           A3: q1 = (a .--> (x1 gcd y1));

          given x2,y2 be Integer such that x2 > 0 and y2 > 0 and

           A4: p = ((a,b) --> (x2,y2)) and

           A5: q2 = (a .--> (x2 gcd y2));

          

           A6: y1 = (((a,b) --> (x1,y1)) . b) by FUNCT_4: 63

          .= y2 by A2, A4, FUNCT_4: 63;

          x1 = (((a,b) --> (x1,y1)) . a) by AMI_3: 10, FUNCT_4: 63

          .= x2 by A2, A4, AMI_3: 10, FUNCT_4: 63;

          hence thesis by A3, A5, A6;

        end;

        consider f be Function such that

         A7: for p,q be object holds [p, q] in f iff p in ( FinPartSt SCM ) & P[p, q] from FUNCT_1:sch 1( A1);

        

         A8: ( rng f) c= ( FinPartSt SCM )

        proof

          let q be object;

          assume q in ( rng f);

          then

          consider p be object such that

           A9: [p, q] in f by XTUPLE_0:def 13;

          ex x,y be Integer st x > 0 & y > 0 & p = ((a,b) --> (x,y)) & q = (a .--> (x gcd y)) by A7, A9;

          hence thesis by MEMSTR_0: 75;

        end;

        ( dom f) c= ( FinPartSt SCM )

        proof

          let e be object;

          assume e in ( dom f);

          then [e, (f . e)] in f by FUNCT_1: 1;

          hence thesis by A7;

        end;

        then

        reconsider f as PartFunc of ( FinPartSt SCM ), ( FinPartSt SCM ) by A8, RELSET_1: 4;

        take f;

        let p,q be FinPartState of SCM ;

        thus [p, q] in f implies ex x,y be Integer st x > 0 & y > 0 & p = ((a,b) --> (x,y)) & q = (a .--> (x gcd y)) by A7;

        given x,y be Integer such that

         A10: x > 0 & y > 0 & p = ((a,b) --> (x,y)) & q = (a .--> (x gcd y));

        p in ( FinPartSt SCM ) by MEMSTR_0: 75;

        hence thesis by A7, A10;

      end;

      uniqueness

      proof

        defpred P[ set, set] means ex x,y be Integer st x > 0 & y > 0 & $1 = ((a,b) --> (x,y)) & $2 = (a .--> (x gcd y));

        let IT1,IT2 be PartFunc of ( FinPartSt SCM ), ( FinPartSt SCM ) such that

         A11: for p,q be FinPartState of SCM holds [p, q] in IT1 iff P[p, q] and

         A12: for p,q be FinPartState of SCM holds [p, q] in IT2 iff P[p, q];

        

         A13: for p,q be Element of ( FinPartSt SCM ) holds [p, q] in IT2 iff P[p, q]

        proof

          let p,q be Element of ( FinPartSt SCM );

          thus [p, q] in IT2 implies P[p, q]

          proof

            assume

             A14: [p, q] in IT2;

            reconsider p, q as FinPartState of SCM by MEMSTR_0: 76;

             P[p, q] by A12, A14;

            hence thesis;

          end;

          thus thesis by A12;

        end;

        

         A15: for p,q be Element of ( FinPartSt SCM ) holds [p, q] in IT1 iff P[p, q]

        proof

          let p,q be Element of ( FinPartSt SCM );

          thus [p, q] in IT1 implies P[p, q]

          proof

            assume

             A16: [p, q] in IT1;

            reconsider p, q as FinPartState of SCM by MEMSTR_0: 76;

             P[p, q] by A11, A16;

            hence thesis;

          end;

          thus thesis by A11;

        end;

        thus IT1 = IT2 from RELSET_1:sch 4( A15, A13);

      end;

    end

    theorem :: AMI_4:8

    

     Th8: for p be set holds p in ( dom Euclid-Function ) iff ex x,y be Integer st x > 0 & y > 0 & p = ((( dl. 0 ),( dl. 1)) --> (x,y))

    proof

      let p be set;

      

       A1: ( dom Euclid-Function ) c= ( FinPartSt SCM ) by RELAT_1:def 18;

      

       A2: p in ( dom Euclid-Function ) iff [p, ( Euclid-Function . p)] in Euclid-Function by FUNCT_1: 1;

      hereby

        assume

         A3: p in ( dom Euclid-Function );

        then ( Euclid-Function . p) in ( FinPartSt SCM ) by PARTFUN1: 4;

        then

         A4: ( Euclid-Function . p) is FinPartState of SCM by MEMSTR_0: 76;

        p is FinPartState of SCM by A1, A3, MEMSTR_0: 76;

        then ex x,y be Integer st x > 0 & y > 0 & p = ((a,b) --> (x,y)) & ( Euclid-Function . p) = (a .--> (x gcd y)) by A2, A3, A4, Def2;

        hence ex x,y be Integer st x > 0 & y > 0 & p = ((a,b) --> (x,y));

      end;

      given x,y be Integer such that

       A5: x > 0 & y > 0 & p = ((a,b) --> (x,y));

       [p, (a .--> (x gcd y))] in Euclid-Function by A5, Def2;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: AMI_4:9

    

     Th9: for i,j be Integer st i > 0 & j > 0 holds ( Euclid-Function . ((( dl. 0 ),( dl. 1)) --> (i,j))) = (( dl. 0 ) .--> (i gcd j))

    proof

      let i,j be Integer;

      assume i > 0 & j > 0 ;

      then [((a,b) --> (i,j)), (a .--> (i gcd j))] in Euclid-Function by Def2;

      hence thesis by FUNCT_1: 1;

    end;

    registration

      cluster Euclid-Algorithm -> the InstructionsF of SCM -valued;

      coherence ;

    end

    registration

      cluster Euclid-Algorithm -> non halt-free;

      coherence

      proof

        ( rng (4 .--> ( halt SCM ))) = {( halt SCM )} by FUNCOP_1: 8;

        then

         A1: ( halt SCM ) in ( rng (4 .--> ( halt SCM ))) by TARSKI:def 1;

        ( rng (4 .--> ( halt SCM ))) c= ( rng ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM )))) by FUNCT_4: 18;

        then

         A2: ( halt SCM ) in ( rng ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM )))) by A1;

        ( rng ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM )))) c= ( rng ((2 .--> (( dl. 0 ) := ( dl. 2))) +* ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM ))))) by FUNCT_4: 18;

        then

         A3: ( halt SCM ) in ( rng ((2 .--> (( dl. 0 ) := ( dl. 2))) +* ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM ))))) by A2;

        ( rng ((2 .--> (( dl. 0 ) := ( dl. 2))) +* ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM ))))) c= ( rng ((1 .--> ( Divide (( dl. 0 ),( dl. 1)))) +* ((2 .--> (( dl. 0 ) := ( dl. 2))) +* ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM )))))) by FUNCT_4: 18;

        then

         A4: ( halt SCM ) in ( rng ((1 .--> ( Divide (( dl. 0 ),( dl. 1)))) +* ((2 .--> (( dl. 0 ) := ( dl. 2))) +* ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM )))))) by A3;

        ( rng ((1 .--> ( Divide (( dl. 0 ),( dl. 1)))) +* ((2 .--> (( dl. 0 ) := ( dl. 2))) +* ((3 .--> (( dl. 1) >0_goto 0 )) +* (4 .--> ( halt SCM )))))) c= ( rng Euclid-Algorithm ) by FUNCT_4: 18;

        then ( halt SCM ) in ( rng Euclid-Algorithm ) by A4;

        hence thesis;

      end;

    end

    theorem :: AMI_4:10

    ( Euclid-Algorithm ,( Start-At ( 0 , SCM ))) computes Euclid-Function

    proof

      set q = Euclid-Algorithm ;

      set p = ( Start-At ( 0 , SCM ));

      let x be set;

      ( DataPart p) = {} by MEMSTR_0: 20;

      then

       A1: ( dom ( DataPart p)) = {} ;

      assume x in ( dom Euclid-Function );

      then

      consider i1,i2 be Integer such that

       A2: i1 > 0 and

       A3: i2 > 0 and

       A4: x = ((a,b) --> (i1,i2)) by Th8;

      x = ((a .--> i1) +* (b .--> i2)) by A4;

      then

      reconsider d = x as FinPartState of SCM ;

      consider t be State of SCM such that

       A5: (p +* d) c= t by PBOOLE: 141;

      consider T be Instruction-Sequence of SCM such that

       A6: q c= T by PBOOLE: 145;

      

       A7: ( dom d) = {a, b} by A4, FUNCT_4: 62;

      then

       A8: b in ( dom d) by TARSKI:def 2;

      

       A9: a in ( dom d) by A7, TARSKI:def 2;

      

       A10: for t be State of SCM st (p +* d) c= t holds (t . a) = i1 & (t . b) = i2

      proof

        let t be State of SCM ;

        assume

         A11: (p +* d) c= t;

        d c= (p +* d) by FUNCT_4: 25;

        then

         A12: d c= t by A11;

        

        hence (t . a) = (d . a) by A9, GRFUNC_1: 2

        .= i1 by A4, AMI_3: 10, FUNCT_4: 63;

        

        thus (t . b) = (d . b) by A8, A12, GRFUNC_1: 2

        .= i2 by A4, FUNCT_4: 63;

      end;

       A14:

      now

        assume ( dom p) meets ( dom d);

        then

        consider x be object such that

         A15: x in ( dom p) and

         A16: x in ( dom d) by XBOOLE_0: 3;

        

         A17: x = ( IC SCM ) by A15, TARSKI:def 1;

        x = a or x = b by A7, A16, TARSKI:def 2;

        hence contradiction by A17, AMI_3: 13;

      end;

      then

       A18: p c= (p +* d) by FUNCT_4: 32;

      

       A19: ( IC SCM ) in ( dom p) by TARSKI:def 1;

      (( dom p) /\ ( dom d)) = {} by A14, XBOOLE_0:def 7;

      then

       A20: not ( IC SCM ) in ( dom d) by A19, XBOOLE_0:def 4;

      set A = {( IC SCM ), a, b}, C = 5;

      

       A21: ( dom (p +* d)) = ( dom (p +* d))

      .= (( dom p) \/ ( dom d)) by FUNCT_4:def 1

      .= (( {( IC SCM )} \/ ( dom ( DataPart p))) \/ ( dom d)) by A19, MEMSTR_0: 24

      .= ( {( IC SCM )} \/ {a, b}) by A4, A1, FUNCT_4: 62

      .= A by ENUMSET1: 2;

      

       A22: ( dom p) c= ( dom (p +* d)) by A18, RELAT_1: 11;

      ( IC (p +* d)) = ( IC p) by A20, FUNCT_4: 11

      .= 0 by FUNCOP_1: 72;

      then

       A23: (p +* d) is 0 -started by A22, A19;

      then

       A24: t is 0 -started by A5, MEMSTR_0: 17;

      

       A25: (p +* d) is q -autonomic

      proof

        set A = {( IC SCM ), a, b}, C = 5;

        let P,Q be Instruction-Sequence of SCM such that

         A26: q c= P and

         A27: q c= Q;

        let s1,s2 be State of SCM such that

         A28: (p +* d) c= s1 and

         A29: (p +* d) c= s2;

        

         A30: (s2 . a) = i1 & (s2 . b) = i2 by A10, A29;

        let k;

        defpred P[ Nat] means ( IC ( Comput (P,s1,$1))) = ( IC ( Comput (Q,s2,$1))) & (( Comput (P,s1,$1)) . a) = (( Comput (Q,s2,$1)) . a) & (( Comput (P,s1,$1)) . b) = (( Comput (Q,s2,$1)) . b);

        

         A31: ( Comput (P,s1, 0 )) = s1 & ( Comput (Q,s2, 0 )) = s2 by EXTPRO_1: 2;

        

         A32: s1 is 0 -started by A23, A28, MEMSTR_0: 17;

        

         A33: ( dom ( Comput (P,s1,k))) = the carrier of SCM by PARTFUN1:def 2

        .= ( dom ( Comput (Q,s2,k))) by PARTFUN1:def 2;

        

         A34: s2 is 0 -started by A23, A29, MEMSTR_0: 17;

        

         A35: for i,j be Nat st P[(4 * i)] & j <> 0 & j <= 4 holds P[((4 * i) + j)]

        proof

          let i,j be Nat;

          assume that

           A36: ( IC ( Comput (P,s1,(4 * i)))) = ( IC ( Comput (Q,s2,(4 * i)))) and

           A37: (( Comput (P,s1,(4 * i))) . a) = (( Comput (Q,s2,(4 * i))) . a) and

           A38: (( Comput (P,s1,(4 * i))) . b) = (( Comput (Q,s2,(4 * i))) . b);

          assume

           A39: j <> 0 & j <= 4;

          then j = 0 or ... or j = 4;

          then

           A40: j = 1 or ... or j = 4 by A39;

          per cases by A2, A3, A34, A27, A30, Lm4;

            suppose

             A41: ( IC ( Comput (Q,s2,(4 * i)))) = 0 ;

            

             A42: (( Comput (P,s1,((4 * i) + 1))) . a) = (( Comput (P,s1,(4 * i))) . a) by A26, A36, A41, Th2

            .= (( Comput (Q,s2,((4 * i) + 1))) . a) by A27, A37, A41, Th2;

            

             A43: (( Comput (P,s1,((4 * i) + 1))) . ( dl. 2)) = (( Comput (P,s1,(4 * i))) . b) by A26, A36, A41, Th2

            .= (( Comput (Q,s2,((4 * i) + 1))) . ( dl. 2)) by A27, A38, A41, Th2;

            

             A44: (( Comput (P,s1,((4 * i) + 1))) . b) = (( Comput (P,s1,(4 * i))) . b) by A26, A36, A41, Th2

            .= (( Comput (Q,s2,((4 * i) + 1))) . b) by A27, A38, A41, Th2;

            

             A45: (((4 * i) + 1) + 1) = ((4 * i) + (1 + 1));

            

             A46: (((4 * i) + 2) + 1) = ((4 * i) + (2 + 1));

            

             A47: ( IC ( Comput (Q,s2,((4 * i) + 1)))) = 1 by A27, A41, Th2;

            then

             A48: ( IC ( Comput (Q,s2,((4 * i) + 2)))) = 2 by A27, A45, Th3;

            then

             A49: ( IC ( Comput (Q,s2,((4 * i) + 3)))) = 3 by A27, A46, Th4;

            

             A50: ( IC ( Comput (P,s1,((4 * i) + 1)))) = 1 by A26, A36, A41, Th2;

            

            then

             A51: (( Comput (P,s1,((4 * i) + 2))) . ( dl. 2)) = (( Comput (P,s1,((4 * i) + 1))) . ( dl. 2)) by A26, A45, Th3

            .= (( Comput (Q,s2,((4 * i) + 2))) . ( dl. 2)) by A27, A45, A47, A43, Th3;

            

             A52: (( Comput (P,s1,((4 * i) + 2))) . b) = ((( Comput (P,s1,((4 * i) + 1))) . a) mod (( Comput (P,s1,((4 * i) + 1))) . b)) by A26, A45, A50, Th3

            .= (( Comput (Q,s2,((4 * i) + 2))) . b) by A27, A45, A47, A42, A44, Th3;

            

             A53: ( IC ( Comput (P,s1,((4 * i) + 2)))) = 2 by A26, A45, A50, Th3;

            then

             A54: ( IC ( Comput (P,s1,((4 * i) + 3)))) = 3 by A26, A46, Th4;

            

             A55: (( Comput (P,s1,((4 * i) + 2))) . a) = ((( Comput (P,s1,((4 * i) + 1))) . a) div (( Comput (P,s1,((4 * i) + 1))) . b)) by A26, A45, A50, Th3

            .= (( Comput (Q,s2,((4 * i) + 2))) . a) by A27, A45, A47, A42, A44, Th3;

            

             A56: (((4 * i) + 3) + 1) = ((4 * i) + (3 + 1));

            

             A57: (( Comput (P,s1,((4 * i) + 3))) . a) = (( Comput (P,s1,((4 * i) + 2))) . ( dl. 2)) by A26, A46, A53, Th4

            .= (( Comput (Q,s2,((4 * i) + 3))) . a) by A27, A46, A48, A51, Th4;

            

             A58: (( Comput (P,s1,((4 * i) + 3))) . b) = (( Comput (P,s1,((4 * i) + 2))) . b) by A26, A46, A53, Th4

            .= (( Comput (Q,s2,((4 * i) + 3))) . b) by A27, A46, A48, A52, Th4;

            (( Comput (P,s1,((4 * i) + 3))) . b) <= 0 or (( Comput (P,s1,((4 * i) + 3))) . b) > 0 ;

            then ( IC ( Comput (P,s1,((4 * i) + 4)))) = 4 & ( IC ( Comput (Q,s2,((4 * i) + 4)))) = 4 or ( IC ( Comput (P,s1,((4 * i) + 4)))) = 0 & ( IC ( Comput (Q,s2,((4 * i) + 4)))) = 0 by A26, A27, A56, A54, A49, A58, Th5;

            hence ( IC ( Comput (P,s1,((4 * i) + j)))) = ( IC ( Comput (Q,s2,((4 * i) + j)))) by A40, A50, A27, A41, Th2, A26, A45, Th3, A48, A54, A46, Th4;

            (( Comput (P,s1,((4 * i) + 4))) . a) = (( Comput (P,s1,((4 * i) + 3))) . a) by A26, A56, A54, Th5

            .= (( Comput (Q,s2,((4 * i) + 4))) . a) by A27, A56, A49, A57, Th5;

            hence (( Comput (P,s1,((4 * i) + j))) . a) = (( Comput (Q,s2,((4 * i) + j))) . a) by A40, A42, A55, A57;

            (( Comput (P,s1,((4 * i) + 4))) . b) = (( Comput (P,s1,((4 * i) + 3))) . b) by A26, A56, A54, Th5

            .= (( Comput (Q,s2,((4 * i) + 4))) . b) by A27, A56, A49, A58, Th5;

            hence thesis by A40, A44, A52, A58;

          end;

            suppose

             A59: ( IC ( Comput (Q,s2,(4 * i)))) = 4;

            then P halts_at ( IC ( Comput (P,s1,(4 * i)))) by A26, A36, Lm3;

            then

             A60: ( Comput (P,s1,((4 * i) + j))) = ( Comput (P,s1,(4 * i))) by EXTPRO_1: 20, NAT_1: 11;

            Q halts_at ( IC ( Comput (Q,s2,(4 * i)))) by A27, A59, Lm3;

            hence thesis by A36, A37, A38, A60, EXTPRO_1: 20, NAT_1: 11;

          end;

        end;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        (( Comput (P,s1, 0 )) . ( IC SCM )) = ( IC s1) by EXTPRO_1: 2

        .= 0 by A32

        .= ( IC s2) by A34

        .= (( Comput (Q,s2, 0 )) . ( IC SCM )) by EXTPRO_1: 2;

        then

         A61: P[ 0 ] by A10, A28, A30, A31;

        

         A62: 4 > 0 ;

         P[k] from NAT_D:sch 2( A61, A62, A35);

        hence thesis by A21, A33, GRFUNC_1: 31;

      end;

      take d;

      thus x = d;

      

       A63: (p +* d) is q -halted

      proof

        reconsider i19 = i1, i29 = i2 as Element of NAT by A2, A3, INT_1: 3;

        let t be State of SCM ;

        assume

         A64: (p +* d) c= t;

        let P be Instruction-Sequence of SCM such that

         A65: q c= P;

        set t9 = ( Comput (P,t,4));

        

         A66: (t . b) = i2 by A10, A64;

        

         A67: t is 0 -started & (t . a) = i1 by A23, A10, A64, MEMSTR_0: 17;

        per cases by XXREAL_0: 1;

          suppose i1 > i2;

          then ex k st P halts_at ( IC ( Comput (P,t,k))) by A3, A65, A67, A66, Lm6;

          hence thesis by EXTPRO_1: 16;

        end;

          suppose

           A68: i1 = i2;

          

           A69: (i1 mod i2) = (i19 mod i29)

          .= 0 by A68, NAT_D: 25;

          

           A70: t9 = ( Comput (P,t,(4 * ( 0 + 1))));

          t = ( Comput (P,t,(4 * 0 ))) by EXTPRO_1: 2;

          then (t9 . b) = ((t . a) mod (t . b)) by A2, A3, A65, A67, A66, A70, Lm5;

          then ( IC t9) = 4 by A2, A3, A65, A67, A66, A69, A70, Lm4;

          then P halts_at ( IC t9) by A65, Lm3;

          hence thesis by EXTPRO_1: 16;

        end;

          suppose

           A71: i1 < i2;

          

           A72: t9 = ( Comput (P,t,(4 * ( 0 + 1))));

          

           A73: t = ( Comput (P,t,(4 * 0 ))) by EXTPRO_1: 2;

          (i1 mod i2) = (i19 mod i29)

          .= i19 by A71, NAT_D: 24;

          then

           A74: (t9 . b) = i1 by A2, A3, A65, A67, A66, A73, A72, Lm5;

          then ( IC t9) = 0 by A2, A3, A65, A67, A66, A72, Lm4;

          then

           A75: t9 is 0 -started;

          (t9 . a) = i2 by A2, A3, A65, A67, A66, A73, A72, Lm5;

          then

          consider k0 be Nat such that

           A76: P halts_at ( IC ( Comput (P,t9,k0))) by A2, A71, A74, A75, A65, Lm6;

          P halts_at ( IC ( Comput (P,t,(k0 + 4)))) by A76, EXTPRO_1: 4;

          hence thesis by EXTPRO_1: 16;

        end;

      end;

      thus (p +* d) is Autonomy of q by A25, A63, EXTPRO_1:def 12;

      then

       A77: ( Result (q,(p +* d))) = (( Result (T,t)) | ( dom (p +* d))) by A6, A5, EXTPRO_1:def 13;

      a in the carrier of SCM ;

      then

       A78: a in ( dom ( Result (T,t))) by PARTFUN1:def 2;

      

       A79: (d . a) = i1 by A4, AMI_3: 10, FUNCT_4: 63;

      

       A80: (d . b) = i2 by A4, FUNCT_4: 63;

      

       A81: d c= (p +* d) by FUNCT_4: 25;

      

       A82: ( dom d) c= ( dom (p +* d)) by A81, RELAT_1: 11;

      

       A83: d c= t by A81, A5;

      

       A84: ( dom d) = {a, b} by A4, FUNCT_4: 62;

      then

       A85: b in ( dom d) by TARSKI:def 2;

      

       A86: (t . b) = i2 by A83, A80, A85, GRFUNC_1: 2;

      

       A87: a in ( dom d) by A84, TARSKI:def 2;

      (t . a) = i1 by A83, A79, A87, GRFUNC_1: 2;

      then

       A88: (( Result (T,t)) . a) = (i1 gcd i2) by A2, A3, A24, A86, Th7, A6;

      ( dom (a .--> (i1 gcd i2))) c= ( dom d) by A84, ZFMISC_1: 7;

      then

       A90: ( dom (a .--> (i1 gcd i2))) c= ( dom (p +* d)) by A82;

      (a .--> (i1 gcd i2)) c= (( Result (T,t)) | ( dom (p +* d))) by A90, A78, A88, FUNCT_4: 85, RELAT_1: 151;

      hence ( Euclid-Function . d) c= ( Result (q,(p +* d))) by A77, A2, A3, A4, Th9;

    end;