scmp_gcd.miz



    begin

    reserve m,n for Nat,

a,b for Int_position,

i,j for Instruction of SCMPDS ,

s,s1,s2 for State of SCMPDS ,

I,J for Program of SCMPDS ;

    definition

      let k be Nat;

      :: SCMP_GCD:def1

      func intpos k -> Int_position equals ( dl. k);

      coherence by SCMPDS_2:def 1;

    end

    theorem :: SCMP_GCD:1

    

     Th1: for n1,n2 be Nat holds ( DataLoc (n1,n2)) = ( intpos (n1 + n2))

    proof

      let n1,n2 be Nat;

      

      thus ( DataLoc (n1,n2)) = [1, |.(n1 + n2).|] by SCMPDS_2:def 3

      .= [1, (n1 + n2)] by ABSVALUE:def 1

      .= ( intpos (n1 + n2));

    end;

    theorem :: SCMP_GCD:2

    

     Th2: for s be State of SCMPDS , m1,m2 be Nat st ( IC s) = (m1 + m2) holds ( ICplusConst (s,( - m2))) = m1

    proof

      let s be State of SCMPDS , m1,m2 be Nat;

      assume

       A1: ( IC s) = (m1 + m2);

      consider m be Element of NAT such that

       A2: m = ( IC s) and

       A3: ( ICplusConst (s,( - m2))) = |.(m + ( - m2)).| by SCMPDS_2:def 18;

      

       A4: m = (m1 + m2) by A1, A2

      .= (m1 + m2);

      

      thus ( ICplusConst (s,( - m2))) = m1 by A3, A4, ABSVALUE:def 1

      .= m1

      .= m1;

    end;

    definition

      :: SCMP_GCD:def2

      func GBP -> Int_position equals ( intpos 0 );

      coherence ;

      :: SCMP_GCD:def3

      func SBP -> Int_position equals ( intpos 1);

      coherence ;

    end

    theorem :: SCMP_GCD:3

     GBP <> SBP by AMI_3: 10;

    theorem :: SCMP_GCD:4

    

     Th4: ( card (I ';' i)) = (( card I) + 1)

    proof

      

      thus ( card (I ';' i)) = ( card (I ';' ( Load i))) by SCMPDS_4:def 3

      .= (( card I) + ( card ( Load i))) by AFINSQ_1: 17

      .= (( card I) + 1) by COMPOS_1: 54;

    end;

    theorem :: SCMP_GCD:5

    

     Th5: ( card (i ';' j)) = 2

    proof

      

      thus ( card (i ';' j)) = ( card (( Load i) ';' ( Load j))) by SCMPDS_4:def 4

      .= (( card ( Load i)) + ( card ( Load j))) by AFINSQ_1: 17

      .= (1 + ( card ( Load j))) by COMPOS_1: 54

      .= (1 + 1) by COMPOS_1: 54

      .= 2;

    end;

    theorem :: SCMP_GCD:6

    

     Th6: ((I ';' i) . ( card I)) = i & ( card I) in ( dom (I ';' i))

    proof

      

       A1: 0 in ( dom ( Load i)) by COMPOS_1: 50;

      

      thus ((I ';' i) . ( card I)) = ((I ';' i) . ( 0 + ( card I)))

      .= ((I ';' i) . ( 0 + ( card I)))

      .= ((I ';' ( Load i)) . ( 0 + ( card I))) by SCMPDS_4:def 3

      .= (( Load i) . 0 ) by A1, AFINSQ_1:def 3

      .= i;

      ( card (I ';' i)) = (( card I) + 1) by Th4;

      then ( card I) < ( card (I ';' i)) by XREAL_1: 29;

      hence thesis by AFINSQ_1: 66;

    end;

    theorem :: SCMP_GCD:7

    

     Th7: (((I ';' i) ';' J) . ( card I)) = i

    proof

      ( card I) in ( dom (I ';' i)) by Th6;

      

      hence (((I ';' i) ';' J) . ( card I)) = ((I ';' i) . ( card I)) by AFINSQ_1:def 3

      .= i by Th6;

    end;

    begin

    definition

      :: SCMP_GCD:def4

      func GCD-Algorithm -> Program of SCMPDS equals ((((((((((((((( GBP := 0 ) ';' ( SBP := 7)) ';' ( saveIC ( SBP , RetIC ))) ';' ( goto 2)) ';' ( halt SCMPDS )) ';' (( SBP ,3) <=0_goto 9)) ';' (( SBP ,6) := ( SBP ,3))) ';' ( Divide ( SBP ,2, SBP ,3))) ';' (( SBP ,7) := ( SBP ,3))) ';' (( SBP ,(4 + RetSP )) := ( GBP ,1))) ';' ( AddTo ( GBP ,1,4))) ';' ( saveIC ( SBP , RetIC ))) ';' ( goto ( - 7))) ';' (( SBP ,2) := ( SBP ,6))) ';' ( return SBP ));

      coherence ;

    end

    set i00 = ( GBP := 0 ), i01 = ( SBP := 7), i02 = ( saveIC ( SBP , RetIC )), i03 = ( goto 2), i04 = ( halt SCMPDS ), i05 = (( SBP ,3) <=0_goto 9), i06 = (( SBP ,6) := ( SBP ,3)), i07 = ( Divide ( SBP ,2, SBP ,3)), i08 = (( SBP ,7) := ( SBP ,3)), i09 = (( SBP ,(4 + RetSP )) := ( GBP ,1)), i10 = ( AddTo ( GBP ,1,4)), i11 = ( saveIC ( SBP , RetIC )), i12 = ( goto ( - 7)), i13 = (( SBP ,2) := ( SBP ,6)), i14 = ( return SBP );

    begin

    theorem :: SCMP_GCD:8

    

     Th8: ( card GCD-Algorithm ) = 15

    proof

      set GCD1 = ((((i00 ';' i01) ';' i02) ';' i03) ';' i04), GCD2 = (((((GCD1 ';' i05) ';' i06) ';' i07) ';' i08) ';' i09);

      

       A1: ( card GCD1) = (( card (((i00 ';' i01) ';' i02) ';' i03)) + 1) by Th4

      .= ((( card ((i00 ';' i01) ';' i02)) + 1) + 1) by Th4

      .= (((( card (i00 ';' i01)) + 1) + 1) + 1) by Th4

      .= (((2 + 1) + 1) + 1) by Th5

      .= 5;

      

       A2: ( card GCD2) = (( card ((((GCD1 ';' i05) ';' i06) ';' i07) ';' i08)) + 1) by Th4

      .= ((( card (((GCD1 ';' i05) ';' i06) ';' i07)) + 1) + 1) by Th4

      .= (((( card ((GCD1 ';' i05) ';' i06)) + 1) + 1) + 1) by Th4

      .= ((((( card (GCD1 ';' i05)) + 1) + 1) + 1) + 1) by Th4

      .= (((((5 + 1) + 1) + 1) + 1) + 1) by A1, Th4

      .= 10;

      

      thus ( card GCD-Algorithm ) = (( card ((((GCD2 ';' i10) ';' i11) ';' i12) ';' i13)) + 1) by Th4

      .= ((( card (((GCD2 ';' i10) ';' i11) ';' i12)) + 1) + 1) by Th4

      .= (((( card ((GCD2 ';' i10) ';' i11)) + 1) + 1) + 1) by Th4

      .= ((((( card (GCD2 ';' i10)) + 1) + 1) + 1) + 1) by Th4

      .= (((((10 + 1) + 1) + 1) + 1) + 1) by A2, Th4

      .= 15;

    end;

    theorem :: SCMP_GCD:9

    n < 15 iff n in ( dom GCD-Algorithm ) by Th8, AFINSQ_1: 66;

    theorem :: SCMP_GCD:10

    

     Th10: ( GCD-Algorithm . 0 ) = ( GBP := 0 ) & ( GCD-Algorithm . 1) = ( SBP := 7) & ( GCD-Algorithm . 2) = ( saveIC ( SBP , RetIC )) & ( GCD-Algorithm . 3) = ( goto 2) & ( GCD-Algorithm . 4) = ( halt SCMPDS ) & ( GCD-Algorithm . 5) = (( SBP ,3) <=0_goto 9) & ( GCD-Algorithm . 6) = (( SBP ,6) := ( SBP ,3)) & ( GCD-Algorithm . 7) = ( Divide ( SBP ,2, SBP ,3)) & ( GCD-Algorithm . 8) = (( SBP ,7) := ( SBP ,3)) & ( GCD-Algorithm . 9) = (( SBP ,(4 + RetSP )) := ( GBP ,1)) & ( GCD-Algorithm . 10) = ( AddTo ( GBP ,1,4)) & ( GCD-Algorithm . 11) = ( saveIC ( SBP , RetIC )) & ( GCD-Algorithm . 12) = ( goto ( - 7)) & ( GCD-Algorithm . 13) = (( SBP ,2) := ( SBP ,6)) & ( GCD-Algorithm . 14) = ( return SBP )

    proof

      set I2 = (i00 ';' i01), I3 = (I2 ';' i02), I4 = (I3 ';' i03), I5 = (I4 ';' i04), I6 = (I5 ';' i05), I7 = (I6 ';' i06), I8 = (I7 ';' i07), I9 = (I8 ';' i08), I10 = (I9 ';' i09), I11 = (I10 ';' i10), I12 = (I11 ';' i11), I13 = (I12 ';' i12), I14 = (I13 ';' i13);

      

       A1: ( card I2) = 2 by Th5;

      then

       A2: ( card I3) = (2 + 1) by Th4;

      then

       A3: ( card I4) = (3 + 1) by Th4;

      then

       A4: ( card I5) = (4 + 1) by Th4;

      then

       A5: ( card I6) = (5 + 1) by Th4;

      then

       A6: ( card I7) = (6 + 1) by Th4;

      then

       A7: ( card I8) = (7 + 1) by Th4;

      then

       A8: ( card I9) = (8 + 1) by Th4;

      then

       A9: ( card I10) = (9 + 1) by Th4;

      then

       A10: ( card I11) = (10 + 1) by Th4;

      then

       A11: ( card I12) = (11 + 1) by Th4;

      then

       A12: ( card I13) = (12 + 1) by Th4;

      then

       A13: ( card I14) = (13 + 1) by Th4;

      set J14 = (i13 ';' i14), J13 = (i12 ';' J14), J12 = (i11 ';' J13), J11 = (i10 ';' J12), J10 = (i09 ';' J11), J9 = (i08 ';' J10), J8 = (i07 ';' J9), J7 = (i06 ';' J8), J6 = (i05 ';' J7), J5 = (i04 ';' J6), J4 = (i03 ';' J5), J3 = (i02 ';' J4), J2 = (i01 ';' J3);

      

       A14: GCD-Algorithm = (I13 ';' J14) by SCMPDS_4: 13;

      then

       A15: GCD-Algorithm = (I12 ';' J13) by SCMPDS_4: 12;

      then

       A16: GCD-Algorithm = (I11 ';' J12) by SCMPDS_4: 12;

      then

       A17: GCD-Algorithm = (I10 ';' J11) by SCMPDS_4: 12;

      then

       A18: GCD-Algorithm = (I9 ';' J10) by SCMPDS_4: 12;

      then

       A19: GCD-Algorithm = (I8 ';' J9) by SCMPDS_4: 12;

      then

       A20: GCD-Algorithm = (I7 ';' J8) by SCMPDS_4: 12;

      then

       A21: GCD-Algorithm = (I6 ';' J7) by SCMPDS_4: 12;

      then

       A22: GCD-Algorithm = (I5 ';' J6) by SCMPDS_4: 12;

      then

       A23: GCD-Algorithm = (I4 ';' J5) by SCMPDS_4: 12;

      then

       A24: GCD-Algorithm = (I3 ';' J4) by SCMPDS_4: 12;

      then

       A25: GCD-Algorithm = (I2 ';' J3) by SCMPDS_4: 12;

      then GCD-Algorithm = (i00 ';' J2) by SCMPDS_4: 16;

      hence ( GCD-Algorithm . 0 ) = i00 by SCMPDS_6: 7;

      

       A26: ( card ( Load i00)) = 1 by COMPOS_1: 54;

       GCD-Algorithm = ((( Load i00) ';' i01) ';' J3) by A25, SCMPDS_4: 9;

      hence ( GCD-Algorithm . 1) = i01 by A26, Th7;

      thus ( GCD-Algorithm . 2) = i02 by A1, A24, Th7;

      thus ( GCD-Algorithm . 3) = i03 by A2, A23, Th7;

      thus ( GCD-Algorithm . 4) = i04 by A3, A22, Th7;

      thus ( GCD-Algorithm . 5) = i05 by A4, A21, Th7;

      thus ( GCD-Algorithm . 6) = i06 by A5, A20, Th7;

      thus ( GCD-Algorithm . 7) = i07 by A6, A19, Th7;

      thus ( GCD-Algorithm . 8) = i08 by A7, A18, Th7;

      thus ( GCD-Algorithm . 9) = i09 by A8, A17, Th7;

      thus ( GCD-Algorithm . 10) = i10 by A9, A16, Th7;

      thus ( GCD-Algorithm . 11) = i11 by A10, A15, Th7;

      thus ( GCD-Algorithm . 12) = i12 by A11, A14, Th7;

       GCD-Algorithm = (I14 ';' ( Load i14)) by SCMPDS_4:def 3;

      hence ( GCD-Algorithm . 13) = i13 by A12, Th7;

      thus thesis by A13, Th6;

    end;

    reserve P,P1,P2 for Instruction-Sequence of SCMPDS ;

    

     Lm1: GCD-Algorithm c= P implies (P . 0 ) = i00 & (P . 1) = i01 & (P . 2) = i02 & (P . 3) = i03 & (P . 4) = i04 & (P . 5) = i05 & (P . 6) = i06 & (P . 7) = i07 & (P . 8) = i08 & (P . 9) = i09 & (P . 10) = i10 & (P . 11) = i11 & (P . 12) = i12 & (P . 13) = i13 & (P . 14) = i14 by Th8, AFINSQ_1: 66, Th10, GRFUNC_1: 2;

    theorem :: SCMP_GCD:11

    

     Th11: for P be Instruction-Sequence of SCMPDS st GCD-Algorithm c= P holds for s be 0 -started State of SCMPDS holds ( IC ( Comput (P,s,4))) = 5 & (( Comput (P,s,4)) . GBP ) = 0 & (( Comput (P,s,4)) . SBP ) = 7 & (( Comput (P,s,4)) . ( intpos (7 + RetIC ))) = 2 & (( Comput (P,s,4)) . ( intpos 9)) = (s . ( intpos 9)) & (( Comput (P,s,4)) . ( intpos 10)) = (s . ( intpos 10))

    proof

      let P be Instruction-Sequence of SCMPDS such that

       A1: GCD-Algorithm c= P;

      let s be 0 -started State of SCMPDS ;

      set GA = GCD-Algorithm ;

      

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

      

       A3: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

      

       A4: (P /. ( IC ( Comput (P,s,1)))) = (P . ( IC ( Comput (P,s,1)))) by PBOOLE: 143;

      

       A5: ( Comput (P,s,( 0 + 1))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

      .= ( Following (P,s)) by EXTPRO_1: 2

      .= ( Exec (i00,s)) by A2, Lm1, A3, A1;

      

      then

       A6: ( IC ( Comput (P,s,1))) = (( IC s) + 1) by SCMPDS_2: 45

      .= ( 0 + 1) by A2;

      

      then

       A7: ( CurInstr (P,( Comput (P,s,1)))) = (P . 1) by A4

      .= i01 by Lm1, A1;

      

       A8: ( Comput (P,s,(1 + 1))) = ( Following (P,( Comput (P,s,1)))) by EXTPRO_1: 3

      .= ( Exec (i01,( Comput (P,s,1)))) by A7;

      

       A9: (( Comput (P,s,1)) . GBP ) = 0 by A5, SCMPDS_2: 45;

      

       A10: (( Comput (P,s,1)) . ( intpos 9)) = (s . ( intpos 9)) by A5, AMI_3: 10, SCMPDS_2: 45;

      

       A11: (( Comput (P,s,1)) . ( intpos 10)) = (s . ( intpos 10)) by A5, AMI_3: 10, SCMPDS_2: 45;

      

       A12: (P /. ( IC ( Comput (P,s,2)))) = (P . ( IC ( Comput (P,s,2)))) by PBOOLE: 143;

      

       A13: ( IC ( Comput (P,s,2))) = (( IC ( Comput (P,s,1))) + 1) by A8, SCMPDS_2: 45

      .= (1 + 1) by A6;

      

      then

       A14: ( CurInstr (P,( Comput (P,s,2)))) = (P . 2) by A12

      .= i02 by Lm1, A1;

      

       A15: ( Comput (P,s,(2 + 1))) = ( Following (P,( Comput (P,s,2)))) by EXTPRO_1: 3

      .= ( Exec (i02,( Comput (P,s,2)))) by A14;

      

       A16: (( Comput (P,s,2)) . GBP ) = 0 by A8, A9, AMI_3: 10, SCMPDS_2: 45;

      

       A17: (( Comput (P,s,2)) . SBP ) = 7 by A8, SCMPDS_2: 45;

      

       A18: (( Comput (P,s,2)) . ( intpos 9)) = (s . ( intpos 9)) by A8, A10, AMI_3: 10, SCMPDS_2: 45;

      

       A19: (( Comput (P,s,2)) . ( intpos 10)) = (s . ( intpos 10)) by A8, A11, AMI_3: 10, SCMPDS_2: 45;

      

       A20: (P /. ( IC ( Comput (P,s,3)))) = (P . ( IC ( Comput (P,s,3)))) by PBOOLE: 143;

      

       A21: ( IC ( Comput (P,s,3))) = (( IC ( Comput (P,s,2))) + 1) by A15, SCMPDS_2: 59

      .= (2 + 1) by A13;

      

      then

       A22: ( CurInstr (P,( Comput (P,s,3)))) = (P . 3) by A20

      .= i03 by Lm1, A1;

      

       A23: ( Comput (P,s,(3 + 1))) = ( Following (P,( Comput (P,s,3)))) by EXTPRO_1: 3

      .= ( Exec (i03,( Comput (P,s,3)))) by A22;

      

       A24: ( DataLoc ((( Comput (P,s,2)) . SBP ), RetIC )) = ( intpos (7 + 1)) by A17, Th1, SCMPDS_I:def 14;

      then

       A25: (( Comput (P,s,3)) . GBP ) = 0 by A15, A16, AMI_3: 10, SCMPDS_2: 59;

      

       A26: (( Comput (P,s,3)) . SBP ) = 7 by A15, A17, A24, AMI_3: 10, SCMPDS_2: 59;

      

       A27: (( Comput (P,s,3)) . ( intpos 8)) = 2 by A13, A15, A24, SCMPDS_2: 59;

      

       A28: (( Comput (P,s,3)) . ( intpos 9)) = (s . ( intpos 9)) by A15, A18, A24, AMI_3: 10, SCMPDS_2: 59;

      

       A29: (( Comput (P,s,3)) . ( intpos 10)) = (s . ( intpos 10)) by A15, A19, A24, AMI_3: 10, SCMPDS_2: 59;

      

      thus ( IC ( Comput (P,s,4))) = ( ICplusConst (( Comput (P,s,3)),2)) by A23, SCMPDS_2: 54

      .= (3 + 2) by A21, SCMPDS_6: 12

      .= 5;

      thus (( Comput (P,s,4)) . GBP ) = 0 by A23, A25, SCMPDS_2: 54;

      thus (( Comput (P,s,4)) . SBP ) = 7 by A23, A26, SCMPDS_2: 54;

      thus (( Comput (P,s,4)) . ( intpos (7 + RetIC ))) = 2 by A23, A27, SCMPDS_2: 54, SCMPDS_I:def 14;

      thus (( Comput (P,s,4)) . ( intpos 9)) = (s . ( intpos 9)) by A23, A28, SCMPDS_2: 54;

      thus thesis by A23, A29, SCMPDS_2: 54;

    end;

    

     Lm2: n > 0 implies GBP <> ( intpos (m + n)) by AMI_3: 10;

    

     Lm3: n > 1 implies SBP <> ( intpos (m + n))

    proof

      assume

       A1: n > 1;

      n <= (m + n) by NAT_1: 11;

      hence thesis by A1, AMI_3: 10;

    end;

    

     Lm4: GCD-Algorithm c= P & ( IC s) = 5 & n = (s . SBP ) & (s . GBP ) = 0 & (s . ( DataLoc ((s . SBP ),3))) > 0 implies ( IC ( Comput (P,s,7))) = (5 + 7) & ( Comput (P,s,8)) = ( Exec (i12,( Comput (P,s,7)))) & (( Comput (P,s,7)) . SBP ) = (n + 4) & (( Comput (P,s,7)) . GBP ) = 0 & (( Comput (P,s,7)) . ( intpos (n + 7))) = ((s . ( DataLoc ((s . SBP ),2))) mod (s . ( DataLoc ((s . SBP ),3)))) & (( Comput (P,s,7)) . ( intpos (n + 6))) = (s . ( DataLoc ((s . SBP ),3))) & (( Comput (P,s,7)) . ( intpos (n + 4))) = n & (( Comput (P,s,7)) . ( intpos (n + 5))) = 11

    proof

      set x = (s . ( DataLoc ((s . SBP ),2))), y = (s . ( DataLoc ((s . SBP ),3)));

      assume

       A1: GCD-Algorithm c= P;

      assume

       A2: ( IC s) = 5;

      assume

       A3: n = (s . SBP );

      assume

       A4: (s . GBP ) = 0 ;

      assume

       A5: y > 0 ;

      

       A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

      

       A7: (P /. ( IC ( Comput (P,s,1)))) = (P . ( IC ( Comput (P,s,1)))) by PBOOLE: 143;

      

       A8: ( Comput (P,s,(1 + 0 ))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

      .= ( Following (P,s)) by EXTPRO_1: 2

      .= ( Exec (i05,s)) by A2, A6, Lm1, A1;

      

      then

       A9: ( IC ( Comput (P,s,1))) = (( IC s) + 1) by A5, SCMPDS_2: 56

      .= (5 + 1) by A2;

      

      then

       A10: ( CurInstr (P,( Comput (P,s,1)))) = (P . 6) by A7

      .= i06 by Lm1, A1;

      

       A11: ( Comput (P,s,(1 + 1))) = ( Following (P,( Comput (P,s,1)))) by EXTPRO_1: 3

      .= ( Exec (i06,( Comput (P,s,1)))) by A10;

      

       A12: (( Comput (P,s,1)) . SBP ) = n by A3, A8, SCMPDS_2: 56;

      

       A13: (( Comput (P,s,1)) . GBP ) = 0 by A4, A8, SCMPDS_2: 56;

      

       A14: (( Comput (P,s,1)) . ( intpos (n + 3))) = (( Comput (P,s,1)) . ( DataLoc (n,3))) by Th1

      .= y by A3, A8, SCMPDS_2: 56;

      

       A15: (( Comput (P,s,1)) . ( intpos (n + 2))) = (( Comput (P,s,1)) . ( DataLoc (n,2))) by Th1

      .= x by A3, A8, SCMPDS_2: 56;

      

       A16: (P /. ( IC ( Comput (P,s,2)))) = (P . ( IC ( Comput (P,s,2)))) by PBOOLE: 143;

      

       A17: ( IC ( Comput (P,s,2))) = (( IC ( Comput (P,s,1))) + 1) by A11, SCMPDS_2: 47

      .= (6 + 1) by A9;

      

      then

       A18: ( CurInstr (P,( Comput (P,s,2)))) = (P . 7) by A16

      .= i07 by Lm1, A1;

      

       A19: ( Comput (P,s,(2 + 1))) = ( Following (P,( Comput (P,s,2)))) by EXTPRO_1: 3

      .= ( Exec (i07,( Comput (P,s,2)))) by A18;

      

       A20: ( DataLoc ((( Comput (P,s,1)) . SBP ),6)) = ( intpos (n + 6)) by A12, Th1;

      then

       A21: (( Comput (P,s,2)) . SBP ) = n by A11, A12, Lm3, SCMPDS_2: 47;

      

       A22: (( Comput (P,s,2)) . GBP ) = 0 by A11, A13, A20, Lm2, SCMPDS_2: 47;

      

       A23: (( Comput (P,s,2)) . ( intpos (n + 6))) = (( Comput (P,s,1)) . ( DataLoc (n,3))) by A11, A12, A20, SCMPDS_2: 47

      .= y by A14, Th1;

      (n + 3) <> (n + 6);

      then

       A24: (( Comput (P,s,2)) . ( intpos (n + 3))) = y by A11, A14, A20, AMI_3: 10, SCMPDS_2: 47;

      (n + 2) <> (n + 6);

      then

       A25: (( Comput (P,s,2)) . ( intpos (n + 2))) = x by A11, A15, A20, AMI_3: 10, SCMPDS_2: 47;

      

       A26: (P /. ( IC ( Comput (P,s,3)))) = (P . ( IC ( Comput (P,s,3)))) by PBOOLE: 143;

      

       A27: ( IC ( Comput (P,s,3))) = (( IC ( Comput (P,s,2))) + 1) by A19, SCMPDS_2: 52

      .= (7 + 1) by A17;

      

      then

       A28: ( CurInstr (P,( Comput (P,s,3)))) = (P . 8) by A26

      .= i08 by Lm1, A1;

      

       A29: ( Comput (P,s,(3 + 1))) = ( Following (P,( Comput (P,s,3)))) by EXTPRO_1: 3

      .= ( Exec (i08,( Comput (P,s,3)))) by A28;

      

       A30: ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) = ( intpos (n + 2)) by A21, Th1;

      then

       A31: SBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) by Lm3;

      

       A32: ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) = ( intpos (n + 3)) by A21, Th1;

      then SBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) by Lm3;

      then

       A33: (( Comput (P,s,3)) . SBP ) = n by A19, A21, A31, SCMPDS_2: 52;

      

       A34: GBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) by A30, Lm2;

       GBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) by A32, Lm2;

      then

       A35: (( Comput (P,s,3)) . GBP ) = 0 by A19, A22, A34, SCMPDS_2: 52;

      

       A36: (( Comput (P,s,3)) . ( intpos (n + 3))) = (x mod y) by A19, A24, A25, A30, A32, SCMPDS_2: 52;

      (n + 6) <> (n + 2);

      then

       A37: ( intpos (n + 6)) <> ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) by A30, AMI_3: 10;

      (n + 6) <> (n + 3);

      then ( intpos (n + 6)) <> ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) by A32, AMI_3: 10;

      then

       A38: (( Comput (P,s,3)) . ( intpos (n + 6))) = y by A19, A23, A37, SCMPDS_2: 52;

      

       A39: (P /. ( IC ( Comput (P,s,4)))) = (P . ( IC ( Comput (P,s,4)))) by PBOOLE: 143;

      

       A40: ( IC ( Comput (P,s,4))) = (( IC ( Comput (P,s,3))) + 1) by A29, SCMPDS_2: 47

      .= (8 + 1) by A27;

      

      then

       A41: ( CurInstr (P,( Comput (P,s,4)))) = (P . 9) by A39

      .= i09 by Lm1, A1;

      

       A42: ( Comput (P,s,(4 + 1))) = ( Following (P,( Comput (P,s,4)))) by EXTPRO_1: 3

      .= ( Exec (i09,( Comput (P,s,4)))) by A41;

      

       A43: ( DataLoc ((( Comput (P,s,3)) . SBP ),7)) = ( intpos (n + 7)) by A33, Th1;

      then

       A44: (( Comput (P,s,4)) . SBP ) = n by A29, A33, Lm3, SCMPDS_2: 47;

      

       A45: (( Comput (P,s,4)) . GBP ) = 0 by A29, A35, A43, Lm2, SCMPDS_2: 47;

      

       A46: (( Comput (P,s,4)) . ( intpos (n + 7))) = (( Comput (P,s,3)) . ( DataLoc (n,3))) by A29, A33, A43, SCMPDS_2: 47

      .= (x mod y) by A36, Th1;

      (n + 6) <> (n + 7);

      then

       A47: (( Comput (P,s,4)) . ( intpos (n + 6))) = y by A29, A38, A43, AMI_3: 10, SCMPDS_2: 47;

      

       A48: (P /. ( IC ( Comput (P,s,5)))) = (P . ( IC ( Comput (P,s,5)))) by PBOOLE: 143;

      

       A49: ( IC ( Comput (P,s,5))) = (( IC ( Comput (P,s,4))) + 1) by A42, SCMPDS_2: 47

      .= (9 + 1) by A40;

      

      then

       A50: ( CurInstr (P,( Comput (P,s,5)))) = (P . 10) by A48

      .= i10 by Lm1, A1;

      

       A51: ( Comput (P,s,(5 + 1))) = ( Following (P,( Comput (P,s,5)))) by EXTPRO_1: 3

      .= ( Exec (i10,( Comput (P,s,5)))) by A50;

      

       A52: ( DataLoc ((( Comput (P,s,4)) . SBP ),(4 + RetSP ))) = ( intpos (n + (4 + 0 ))) by A44, Th1, SCMPDS_I:def 13;

      then

       A53: (( Comput (P,s,5)) . SBP ) = n by A42, A44, Lm3, SCMPDS_2: 47;

      

       A54: (( Comput (P,s,5)) . GBP ) = 0 by A42, A45, A52, Lm2, SCMPDS_2: 47;

      (n + 7) <> (n + 4);

      then

       A55: (( Comput (P,s,5)) . ( intpos (n + 7))) = (x mod y) by A42, A46, A52, AMI_3: 10, SCMPDS_2: 47;

      (n + 6) <> (n + 4);

      then

       A56: (( Comput (P,s,5)) . ( intpos (n + 6))) = y by A42, A47, A52, AMI_3: 10, SCMPDS_2: 47;

      

       A57: (( Comput (P,s,5)) . ( intpos (n + 4))) = (( Comput (P,s,4)) . ( DataLoc ( 0 ,1))) by A42, A45, A52, SCMPDS_2: 47

      .= (( Comput (P,s,4)) . ( intpos ( 0 + 1))) by Th1

      .= n by A29, A33, A43, Lm3, SCMPDS_2: 47;

      

       A58: (P /. ( IC ( Comput (P,s,6)))) = (P . ( IC ( Comput (P,s,6)))) by PBOOLE: 143;

      

       A59: ( IC ( Comput (P,s,6))) = (( IC ( Comput (P,s,5))) + 1) by A51, SCMPDS_2: 48

      .= (10 + 1) by A49;

      

      then

       A60: ( CurInstr (P,( Comput (P,s,6)))) = (P . 11) by A58

      .= i11 by Lm1, A1;

      

       A61: ( Comput (P,s,(6 + 1))) = ( Following (P,( Comput (P,s,6)))) by EXTPRO_1: 3

      .= ( Exec (i11,( Comput (P,s,6)))) by A60;

      

       A62: ( DataLoc ((( Comput (P,s,5)) . GBP ),1)) = ( intpos ( 0 + 1)) by A54, Th1;

      then

       A63: (( Comput (P,s,6)) . SBP ) = (n + 4) by A51, A53, SCMPDS_2: 48;

      

       A64: (( Comput (P,s,6)) . GBP ) = 0 by A51, A54, A62, AMI_3: 10, SCMPDS_2: 48;

      (n + 7) <> 1 by NAT_1: 11;

      then

       A65: (( Comput (P,s,6)) . ( intpos (n + 7))) = (x mod y) by A51, A55, A62, AMI_3: 10, SCMPDS_2: 48;

      (n + 6) <> 1 by NAT_1: 11;

      then

       A66: (( Comput (P,s,6)) . ( intpos (n + 6))) = y by A51, A56, A62, AMI_3: 10, SCMPDS_2: 48;

      (n + 4) <> 1 by NAT_1: 11;

      then

       A67: (( Comput (P,s,6)) . ( intpos (n + 4))) = n by A51, A57, A62, AMI_3: 10, SCMPDS_2: 48;

      

       A68: (P /. ( IC ( Comput (P,s,7)))) = (P . ( IC ( Comput (P,s,7)))) by PBOOLE: 143;

      

      thus ( IC ( Comput (P,s,7))) = (( IC ( Comput (P,s,6))) + 1) by A61, SCMPDS_2: 59

      .= (11 + 1) by A59

      .= (5 + 7);

      

      then

       A69: ( CurInstr (P,( Comput (P,s,7)))) = (P . 12) by A68

      .= i12 by Lm1, A1;

      

      thus ( Comput (P,s,8)) = ( Comput (P,s,(7 + 1)))

      .= ( Following (P,( Comput (P,s,7)))) by EXTPRO_1: 3

      .= ( Exec (i12,( Comput (P,s,7)))) by A69;

      

       A70: ( DataLoc ((( Comput (P,s,6)) . SBP ), RetIC )) = ( intpos ((n + 4) + 1)) by A63, Th1, SCMPDS_I:def 14

      .= ( intpos (n + (4 + 1)));

      then SBP <> ( DataLoc ((( Comput (P,s,6)) . SBP ), RetIC )) by Lm3;

      hence (( Comput (P,s,7)) . SBP ) = (n + 4) by A61, A63, SCMPDS_2: 59;

       GBP <> ( DataLoc ((( Comput (P,s,6)) . SBP ), RetIC )) by A70, Lm2;

      hence (( Comput (P,s,7)) . GBP ) = 0 by A61, A64, SCMPDS_2: 59;

      (n + 7) <> (n + 5);

      hence (( Comput (P,s,7)) . ( intpos (n + 7))) = (x mod y) by A61, A65, A70, AMI_3: 10, SCMPDS_2: 59;

      (n + 6) <> (n + 5);

      hence (( Comput (P,s,7)) . ( intpos (n + 6))) = y by A61, A66, A70, AMI_3: 10, SCMPDS_2: 59;

      (n + 4) <> (n + 5);

      hence (( Comput (P,s,7)) . ( intpos (n + 4))) = n by A61, A67, A70, AMI_3: 10, SCMPDS_2: 59;

      thus thesis by A59, A61, A70, SCMPDS_2: 59;

    end;

    

     Lm5: GCD-Algorithm c= P & ( IC s) = 5 & n = (s . SBP ) & (s . GBP ) = 0 & (s . ( DataLoc ((s . SBP ),3))) > 0 & 1 < m & m <= (n + 1) implies (( Comput (P,s,7)) . ( intpos m)) = (s . ( intpos m))

    proof

      assume

       A1: GCD-Algorithm c= P;

      assume

       A2: ( IC s) = 5;

      assume

       A3: n = (s . SBP );

      assume

       A4: (s . GBP ) = 0 ;

      assume

       A5: (s . ( DataLoc ((s . SBP ),3))) > 0 ;

      assume

       A6: 1 < m;

      assume

       A7: m <= (n + 1);

      

       A8: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

      

       A9: (P /. ( IC ( Comput (P,s,1)))) = (P . ( IC ( Comput (P,s,1)))) by PBOOLE: 143;

      

       A10: ( Comput (P,s,(1 + 0 ))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

      .= ( Following (P,s)) by EXTPRO_1: 2

      .= ( Exec (i05,s)) by A2, A8, Lm1, A1;

      

      then

       A11: ( IC ( Comput (P,s,1))) = (( IC s) + 1) by A5, SCMPDS_2: 56

      .= (5 + 1) by A2;

      

      then

       A12: ( CurInstr (P,( Comput (P,s,1)))) = (P . 6) by A9

      .= i06 by Lm1, A1;

      

       A13: ( Comput (P,s,(1 + 1))) = ( Following (P,( Comput (P,s,1)))) by EXTPRO_1: 3

      .= ( Exec (i06,( Comput (P,s,1)))) by A12;

      

       A14: (( Comput (P,s,1)) . SBP ) = n by A3, A10, SCMPDS_2: 56;

      

       A15: (( Comput (P,s,1)) . GBP ) = 0 by A4, A10, SCMPDS_2: 56;

      

       A16: (( Comput (P,s,1)) . ( intpos m)) = (s . ( intpos m)) by A10, SCMPDS_2: 56;

      

       A17: (P /. ( IC ( Comput (P,s,2)))) = (P . ( IC ( Comput (P,s,2)))) by PBOOLE: 143;

      

       A18: ( IC ( Comput (P,s,2))) = (( IC ( Comput (P,s,1))) + 1) by A13, SCMPDS_2: 47

      .= (6 + 1) by A11;

      

      then

       A19: ( CurInstr (P,( Comput (P,s,2)))) = (P . 7) by A17

      .= i07 by Lm1, A1;

      

       A20: ( Comput (P,s,(2 + 1))) = ( Following (P,( Comput (P,s,2)))) by EXTPRO_1: 3

      .= ( Exec (i07,( Comput (P,s,2)))) by A19;

      

       A21: ( DataLoc ((( Comput (P,s,1)) . SBP ),6)) = ( intpos (n + 6)) by A14, Th1;

      then

       A22: (( Comput (P,s,2)) . SBP ) = n by A13, A14, Lm3, SCMPDS_2: 47;

      

       A23: (( Comput (P,s,2)) . GBP ) = 0 by A13, A15, A21, Lm2, SCMPDS_2: 47;

      (n + 1) < (n + 6) by XREAL_1: 6;

      then

       A24: (( Comput (P,s,2)) . ( intpos m)) = (s . ( intpos m)) by A7, A13, A16, A21, AMI_3: 10, SCMPDS_2: 47;

      

       A25: (P /. ( IC ( Comput (P,s,3)))) = (P . ( IC ( Comput (P,s,3)))) by PBOOLE: 143;

      

       A26: ( IC ( Comput (P,s,3))) = (( IC ( Comput (P,s,2))) + 1) by A20, SCMPDS_2: 52

      .= (7 + 1) by A18;

      

      then

       A27: ( CurInstr (P,( Comput (P,s,3)))) = (P . 8) by A25

      .= i08 by Lm1, A1;

      

       A28: ( Comput (P,s,(3 + 1))) = ( Following (P,( Comput (P,s,3)))) by EXTPRO_1: 3

      .= ( Exec (i08,( Comput (P,s,3)))) by A27;

      

       A29: ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) = ( intpos (n + 2)) by A22, Th1;

      then

       A30: SBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) by Lm3;

      

       A31: ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) = ( intpos (n + 3)) by A22, Th1;

      then SBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) by Lm3;

      then

       A32: (( Comput (P,s,3)) . SBP ) = n by A20, A22, A30, SCMPDS_2: 52;

      

       A33: GBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) by A29, Lm2;

       GBP <> ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) by A31, Lm2;

      then

       A34: (( Comput (P,s,3)) . GBP ) = 0 by A20, A23, A33, SCMPDS_2: 52;

      (n + 1) < (n + 2) by XREAL_1: 6;

      then

       A35: ( intpos m) <> ( DataLoc ((( Comput (P,s,2)) . SBP ),2)) by A7, A29, AMI_3: 10;

      (n + 1) < (n + 3) by XREAL_1: 6;

      then ( intpos m) <> ( DataLoc ((( Comput (P,s,2)) . SBP ),3)) by A7, A31, AMI_3: 10;

      then

       A36: (( Comput (P,s,3)) . ( intpos m)) = (s . ( intpos m)) by A20, A24, A35, SCMPDS_2: 52;

      

       A37: (P /. ( IC ( Comput (P,s,4)))) = (P . ( IC ( Comput (P,s,4)))) by PBOOLE: 143;

      

       A38: ( IC ( Comput (P,s,4))) = (( IC ( Comput (P,s,3))) + 1) by A28, SCMPDS_2: 47

      .= (8 + 1) by A26;

      

      then

       A39: ( CurInstr (P,( Comput (P,s,4)))) = (P . 9) by A37

      .= i09 by Lm1, A1;

      

       A40: ( Comput (P,s,(4 + 1))) = ( Following (P,( Comput (P,s,4)))) by EXTPRO_1: 3

      .= ( Exec (i09,( Comput (P,s,4)))) by A39;

      

       A41: ( DataLoc ((( Comput (P,s,3)) . SBP ),7)) = ( intpos (n + 7)) by A32, Th1;

      then

       A42: (( Comput (P,s,4)) . SBP ) = n by A28, A32, Lm3, SCMPDS_2: 47;

      

       A43: (( Comput (P,s,4)) . GBP ) = 0 by A28, A34, A41, Lm2, SCMPDS_2: 47;

      (n + 1) < (n + 7) by XREAL_1: 6;

      then

       A44: (( Comput (P,s,4)) . ( intpos m)) = (s . ( intpos m)) by A7, A28, A36, A41, AMI_3: 10, SCMPDS_2: 47;

      

       A45: (P /. ( IC ( Comput (P,s,5)))) = (P . ( IC ( Comput (P,s,5)))) by PBOOLE: 143;

      

       A46: ( IC ( Comput (P,s,5))) = (( IC ( Comput (P,s,4))) + 1) by A40, SCMPDS_2: 47

      .= (9 + 1) by A38;

      

      then

       A47: ( CurInstr (P,( Comput (P,s,5)))) = (P . 10) by A45

      .= i10 by Lm1, A1;

      

       A48: ( Comput (P,s,(5 + 1))) = ( Following (P,( Comput (P,s,5)))) by EXTPRO_1: 3

      .= ( Exec (i10,( Comput (P,s,5)))) by A47;

      

       A49: ( DataLoc ((( Comput (P,s,4)) . SBP ),(4 + RetSP ))) = ( intpos (n + (4 + 0 ))) by A42, Th1, SCMPDS_I:def 13;

      then

       A50: (( Comput (P,s,5)) . SBP ) = n by A40, A42, Lm3, SCMPDS_2: 47;

      

       A51: (( Comput (P,s,5)) . GBP ) = 0 by A40, A43, A49, Lm2, SCMPDS_2: 47;

      (n + 1) < (n + 4) by XREAL_1: 6;

      then

       A52: (( Comput (P,s,5)) . ( intpos m)) = (s . ( intpos m)) by A7, A40, A44, A49, AMI_3: 10, SCMPDS_2: 47;

      

       A53: (P /. ( IC ( Comput (P,s,6)))) = (P . ( IC ( Comput (P,s,6)))) by PBOOLE: 143;

      ( IC ( Comput (P,s,6))) = (( IC ( Comput (P,s,5))) + 1) by A48, SCMPDS_2: 48

      .= (10 + 1) by A46;

      

      then

       A54: ( CurInstr (P,( Comput (P,s,6)))) = (P . 11) by A53

      .= i11 by Lm1, A1;

      

       A55: ( Comput (P,s,(6 + 1))) = ( Following (P,( Comput (P,s,6)))) by EXTPRO_1: 3

      .= ( Exec (i11,( Comput (P,s,6)))) by A54;

      

       A56: ( DataLoc ((( Comput (P,s,5)) . GBP ),1)) = ( intpos ( 0 + 1)) by A51, Th1;

      then

       A57: (( Comput (P,s,6)) . SBP ) = (n + 4) by A48, A50, SCMPDS_2: 48;

      

       A58: (( Comput (P,s,6)) . ( intpos m)) = (s . ( intpos m)) by A6, A48, A52, A56, AMI_3: 10, SCMPDS_2: 48;

      

       A59: ( DataLoc ((( Comput (P,s,6)) . SBP ), RetIC )) = ( intpos ((n + 4) + 1)) by A57, Th1, SCMPDS_I:def 14

      .= ( intpos (n + (4 + 1)));

      (n + 1) < (n + 5) by XREAL_1: 6;

      hence thesis by A7, A55, A58, A59, AMI_3: 10, SCMPDS_2: 59;

    end;

    theorem :: SCMP_GCD:12

    

     Th12: for s be State of SCMPDS st GCD-Algorithm c= P & ( IC s) = 5 & (s . SBP ) > 0 & (s . GBP ) = 0 & (s . ( DataLoc ((s . SBP ),3))) >= 0 & (s . ( DataLoc ((s . SBP ),2))) >= (s . ( DataLoc ((s . SBP ),3))) holds ex n st ( CurInstr (P,( Comput (P,s,n)))) = ( return SBP ) & (s . SBP ) = (( Comput (P,s,n)) . SBP ) & (( Comput (P,s,n)) . ( DataLoc ((s . SBP ),2))) = ((s . ( DataLoc ((s . SBP ),2))) gcd (s . ( DataLoc ((s . SBP ),3)))) & for j be Nat st 1 < j & j <= ((s . SBP ) + 1) holds (s . ( intpos j)) = (( Comput (P,s,n)) . ( intpos j))

    proof

      set GA = GCD-Algorithm ;

      defpred P[ Nat] means for s be State of SCMPDS st GA c= P & ( IC s) = 5 & (s . SBP ) > 0 & (s . GBP ) = 0 & (s . ( DataLoc ((s . SBP ),3))) <= $1 & (s . ( DataLoc ((s . SBP ),3))) >= 0 & (s . ( DataLoc ((s . SBP ),2))) >= (s . ( DataLoc ((s . SBP ),3))) holds ex n st ( CurInstr (P,( Comput (P,s,n)))) = ( return SBP ) & (s . SBP ) = (( Comput (P,s,n)) . SBP ) & (( Comput (P,s,n)) . ( DataLoc ((s . SBP ),2))) = ((s . ( DataLoc ((s . SBP ),2))) gcd (s . ( DataLoc ((s . SBP ),3)))) & (for j be Nat st 1 < j & j <= ((s . SBP ) + 1) holds (s . ( intpos j)) = (( Comput (P,s,n)) . ( intpos j)));

      now

        let s be State of SCMPDS ;

        set x = (s . ( DataLoc ((s . SBP ),2))), y = (s . ( DataLoc ((s . SBP ),3)));

        assume

         A1: GA c= P;

        assume

         A2: ( IC s) = 5;

        assume (s . SBP ) > 0 ;

        assume (s . GBP ) = 0 ;

        assume

         A3: y <= 0 ;

        assume

         A4: y >= 0 ;

        assume

         A5: x >= y;

        

         A6: (P /. ( IC s)) = (P . ( IC s)) by PBOOLE: 143;

        

         A7: (P /. ( IC ( Comput (P,s,1)))) = (P . ( IC ( Comput (P,s,1)))) by PBOOLE: 143;

        

         A8: ( Comput (P,s,(1 + 0 ))) = ( Following (P,( Comput (P,s, 0 )))) by EXTPRO_1: 3

        .= ( Following (P,s)) by EXTPRO_1: 2

        .= ( Exec (i05,s)) by A2, A6, Lm1, A1;

        

        then

         A9: ( IC ( Comput (P,s,1))) = ( ICplusConst (s,9)) by A3, SCMPDS_2: 56

        .= (5 + 9) by A2, SCMPDS_6: 12;

        reconsider n = 1 as Nat;

        take n;

        

        thus ( CurInstr (P,( Comput (P,s,n)))) = (P . 14) by A9, A7

        .= i14 by Lm1, A1;

        thus (( Comput (P,s,n)) . SBP ) = (s . SBP ) by A8, SCMPDS_2: 56;

        

         A10: y = 0 by A3, A4;

        then

         A11: |.y.| = 0 by ABSVALUE:def 1;

        

        thus (( Comput (P,s,n)) . ( DataLoc ((s . SBP ),2))) = x by A8, SCMPDS_2: 56

        .= |.x.| by A5, A10, ABSVALUE:def 1

        .= ( |.x.| gcd |.y.|) by A11, NEWTON: 52

        .= (x gcd y) by INT_2: 34;

        thus for j be Nat st 1 < j & j <= ((s . SBP ) + 1) holds (s . ( intpos j)) = (( Comput (P,s,n)) . ( intpos j)) by A8, SCMPDS_2: 56;

      end;

      then

       A12: P[ 0 ];

       A13:

      now

        let k be Nat;

        assume

         A14: P[k];

        now

          let s be State of SCMPDS ;

          set x = (s . ( DataLoc ((s . SBP ),2))), y = (s . ( DataLoc ((s . SBP ),3))), yy = y;

          assume

           A15: GA c= P;

          assume

           A16: ( IC s) = 5;

          assume

           A17: (s . SBP ) > 0 ;

          assume

           A18: (s . GBP ) = 0 ;

          assume

           A19: y <= (k + 1);

          assume

           A20: y >= 0 ;

          assume

           A21: x >= y;

          then

           A22: x >= 0 by A20;

          reconsider y as Element of NAT by A20, INT_1: 3;

          per cases by A19, NAT_1: 8;

            suppose y <= k;

            hence ex n st ( CurInstr (P,( Comput (P,s,n)))) = ( return SBP ) & (s . SBP ) = (( Comput (P,s,n)) . SBP ) & (( Comput (P,s,n)) . ( DataLoc ((s . SBP ),2))) = (x gcd yy) & for j be Nat st 1 < j & j <= ((s . SBP ) + 1) holds (s . ( intpos j)) = (( Comput (P,s,n)) . ( intpos j)) by A14, A16, A17, A18, A21, A15;

          end;

            suppose

             A23: y = (k + 1);

            then

             A24: y > 0 ;

            reconsider pn = (s . SBP ) as Element of NAT by A17, INT_1: 3;

            

             A25: pn = (s . SBP );

            then

             A26: ( IC ( Comput (P,s,7))) = (5 + 7) by A16, A18, A24, Lm4, A15;

            

             A27: ( Comput (P,s,8)) = ( Exec (i12,( Comput (P,s,7)))) by A16, A18, A24, A25, Lm4, A15;

            

             A28: (( Comput (P,s,7)) . SBP ) = (pn + 4) by A16, A18, A24, Lm4, A15;

            

             A29: (( Comput (P,s,7)) . GBP ) = 0 by A16, A18, A24, A25, Lm4, A15;

            

             A30: (( Comput (P,s,7)) . ( intpos (pn + 7))) = (x mod y) by A16, A18, A24, Lm4, A15;

            

             A31: (( Comput (P,s,7)) . ( intpos (pn + 6))) = y by A16, A18, A24, Lm4, A15;

            

             A32: (( Comput (P,s,7)) . ( intpos (pn + 4))) = pn by A16, A18, A24, Lm4, A15;

            

             A33: (( Comput (P,s,7)) . ( intpos (pn + 5))) = 11 by A16, A18, A24, Lm4, A15;

            set s8 = ( Comput (P,s,8)), P8 = P;

            

             A34: ( IC s8) = ( ICplusConst (( Comput (P,s,7)),( - 7))) by A27, SCMPDS_2: 54

            .= 5 by A26, Th2;

            

             A35: GA c= P8 by A15;

            

             A36: (s8 . SBP ) = (pn + 4) by A27, A28, SCMPDS_2: 54;

            

             A37: 4 <= (pn + 4) by NAT_1: 11;

            

             A38: (s8 . SBP ) > 0 by A36;

            

             A39: (s8 . GBP ) = 0 by A27, A29, SCMPDS_2: 54;

            set x1 = (s8 . ( DataLoc ((s8 . SBP ),2))), y1 = (s8 . ( DataLoc ((s8 . SBP ),3)));

            

             A40: x1 = (s8 . ( intpos ((pn + 4) + 2))) by A36, Th1

            .= y by A27, A31, SCMPDS_2: 54;

            

             A41: y1 = (s8 . ( intpos ((pn + 4) + 3))) by A36, Th1

            .= (x mod y) by A27, A30, SCMPDS_2: 54;

            then

             A42: y1 < y by A23, NEWTON: 65;

            then y1 <= k by A23, INT_1: 7;

            then

            consider m such that

             A43: ( CurInstr (P,( Comput (P,s8,m)))) = ( return SBP ) and

             A44: (s8 . SBP ) = (( Comput (P,s8,m)) . SBP ) and

             A45: (( Comput (P,s8,m)) . ( DataLoc ((s8 . SBP ),2))) = (x1 gcd y1) and

             A46: for j be Nat st 1 < j & j <= ((s8 . SBP ) + 1) holds (s8 . ( intpos j)) = (( Comput (P,s8,m)) . ( intpos j)) by A14, A34, A35, A38, A39, A40, A41, A42, NEWTON: 64;

            set s9 = ( Comput (P,s,(m + 8)));

            

             A47: (s8 . SBP ) = (s9 . SBP ) by A44, EXTPRO_1: 4;

            

             A48: ( Comput (P,s,(m + 8))) = ( Comput (P,( Comput (P,s,8)),m)) by EXTPRO_1: 4;

            

             A49: ( Comput (P,s,(m + (8 + 1)))) = ( Comput (P,s,((m + 8) + 1)))

            .= ( Following (P,s9)) by EXTPRO_1: 3

            .= ( Exec (( CurInstr (P,s9)),s9))

            .= ( Exec (( CurInstr (P,( Comput (P,s8,m)))),s9)) by A48

            .= ( Exec (( return SBP ),s9)) by A43;

            

             A50: 1 < (pn + 4) by A37, XXREAL_0: 2;

            (pn + 4) < ((s8 . SBP ) + 1) by A36, XREAL_1: 29;

            

            then

             A51: (s8 . ( intpos (pn + 4))) = (( Comput (P,s8,m)) . ( intpos (pn + 4))) by A46, A50

            .= (s9 . ( intpos (pn + 4))) by EXTPRO_1: 4;

            5 <= (pn + 5) by NAT_1: 11;

            then

             A52: 1 < (pn + 5) by XXREAL_0: 2;

            

             A53: 11 = (s8 . ( intpos (pn + 5))) by A27, A33, SCMPDS_2: 54

            .= (( Comput (P,s8,m)) . ( intpos (pn + 5))) by A36, A46, A52

            .= (s9 . ( intpos ((pn + 4) + 1))) by EXTPRO_1: 4

            .= (s9 . ( DataLoc ((s9 . SBP ), RetIC ))) by A36, A47, Th1, SCMPDS_I:def 14;

            

             A54: (P /. ( IC ( Comput (P,s,(m + 9))))) = (P . ( IC ( Comput (P,s,(m + 9))))) by PBOOLE: 143;

            

             A55: ( IC ( Comput (P,s,(m + 9)))) = ( |.(s9 . ( DataLoc ((s9 . SBP ), RetIC ))).| + 2) by A49, SCMPDS_2: 58

            .= (11 + 2) by A53, ABSVALUE: 29;

            

            then

             A56: ( CurInstr (P,( Comput (P,s,(m + 9))))) = (P . 13) by A54

            .= i13 by Lm1, A15;

            

             A57: ( Comput (P,s,(m + (9 + 1)))) = ( Comput (P,s,((m + 9) + 1)))

            .= ( Following (P,( Comput (P,s,(m + 9))))) by EXTPRO_1: 3

            .= ( Exec (i13,( Comput (P,s,(m + 9))))) by A56;

            

             A58: (( Comput (P,s,(m + 9))) . SBP ) = (s9 . ( DataLoc ((pn + 4), RetSP ))) by A36, A47, A49, SCMPDS_2: 58

            .= (s9 . ( intpos ((pn + 4) + 0 ))) by Th1, SCMPDS_I:def 13

            .= pn by A27, A32, A51, SCMPDS_2: 54;

            

             A59: (( Comput (P,s,(m + 9))) . ( intpos (pn + 6))) = (s9 . ( intpos ((pn + 4) + 2))) by A49, Lm3, SCMPDS_2: 58

            .= (s9 . ( DataLoc ((s8 . SBP ),2))) by A36, Th1

            .= (x1 gcd y1) by A45, EXTPRO_1: 4;

            

             A60: (P /. ( IC ( Comput (P,s,(m + 10))))) = (P . ( IC ( Comput (P,s,(m + 10))))) by PBOOLE: 143;

            ( IC ( Comput (P,s,(m + 10)))) = (( IC ( Comput (P,s,(m + 9)))) + 1) by A57, SCMPDS_2: 47

            .= (13 + 1) by A55;

            

            then

             A61: ( CurInstr (P,( Comput (P,s,(m + 10))))) = (P . 14) by A60

            .= i14 by Lm1, A15;

            hereby

              reconsider n = (m + 10) as Nat;

              take n;

              thus ( CurInstr (P,( Comput (P,s,n)))) = ( return SBP ) by A61;

              

               A62: ( DataLoc ((( Comput (P,s,(m + 9))) . SBP ),2)) = ( intpos (pn + 2)) by A58, Th1;

              hence (( Comput (P,s,n)) . SBP ) = (s . SBP ) by A57, A58, Lm3, SCMPDS_2: 47;

              

              thus (( Comput (P,s,n)) . ( DataLoc ((s . SBP ),2))) = (( Comput (P,s,(m + 9))) . ( DataLoc (pn,6))) by A57, A58, SCMPDS_2: 47

              .= (yy gcd (x mod yy)) by A40, A41, A59, Th1

              .= (x gcd yy) by A22, A23, NAT_D: 30;

              hereby

                let j be Nat;

                assume that

                 A63: 1 < j and

                 A64: j <= ((s . SBP ) + 1);

                (s . SBP ) <= (s8 . SBP ) by A36, NAT_1: 11;

                then ((s . SBP ) + 1) <= ((s8 . SBP ) + 1) by XREAL_1: 6;

                then

                 A65: j <= ((s8 . SBP ) + 1) by A64, XXREAL_0: 2;

                

                 A66: (( Comput (P,s,(m + 9))) . ( intpos j)) = (s9 . ( intpos j)) by A49, A63, AMI_3: 10, SCMPDS_2: 58

                .= (( Comput (P,s8,m)) . ( intpos j)) by EXTPRO_1: 4

                .= (s8 . ( intpos j)) by A46, A63, A65;

                

                 A67: (pn + 1) < (pn + 2) by XREAL_1: 6;

                (( Comput (P,s,7)) . ( intpos j)) = (s . ( intpos j)) by A16, A18, A23, A25, A63, A64, Lm5, A15;

                

                hence (s . ( intpos j)) = (s8 . ( intpos j)) by A27, SCMPDS_2: 54

                .= (( Comput (P,s,n)) . ( intpos j)) by A57, A62, A64, A66, A67, AMI_3: 10, SCMPDS_2: 47;

              end;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

      

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

      let s be State of SCMPDS ;

      assume that

       A69: GA c= P and

       A70: ( IC s) = 5 and

       A71: (s . SBP ) > 0 and

       A72: (s . GBP ) = 0 and

       A73: (s . ( DataLoc ((s . SBP ),3))) >= 0 and

       A74: (s . ( DataLoc ((s . SBP ),2))) >= (s . ( DataLoc ((s . SBP ),3)));

      reconsider m = (s . ( DataLoc ((s . SBP ),3))) as Element of NAT by A73, INT_1: 3;

       P[m] by A68;

      hence thesis by A70, A71, A72, A74, A69;

    end;

    theorem :: SCMP_GCD:13

    

     Th13: for s be State of SCMPDS st GCD-Algorithm c= P & ( IC s) = 5 & (s . SBP ) > 0 & (s . GBP ) = 0 & (s . ( DataLoc ((s . SBP ),3))) >= 0 & (s . ( DataLoc ((s . SBP ),2))) >= 0 holds ex n st ( CurInstr (P,( Comput (P,s,n)))) = ( return SBP ) & (s . SBP ) = (( Comput (P,s,n)) . SBP ) & (( Comput (P,s,n)) . ( DataLoc ((s . SBP ),2))) = ((s . ( DataLoc ((s . SBP ),2))) gcd (s . ( DataLoc ((s . SBP ),3)))) & for j be Nat st 1 < j & j <= ((s . SBP ) + 1) holds (s . ( intpos j)) = (( Comput (P,s,n)) . ( intpos j))

    proof

      let s be State of SCMPDS ;

      set GA = GCD-Algorithm , x = (s . ( DataLoc ((s . SBP ),2))), y = (s . ( DataLoc ((s . SBP ),3))), yy = y;

      assume that

       A1: GA c= P and

       A2: ( IC s) = 5 and

       A3: (s . SBP ) > 0 and

       A4: (s . GBP ) = 0 and

       A5: y >= 0 and

       A6: x >= 0 ;

      per cases ;

        suppose x >= y;

        hence thesis by A2, A3, A4, A5, Th12, A1;

      end;

        suppose x < y;

        then

         A7: y > 0 by A6;

        reconsider y as Element of NAT by A5, INT_1: 3;

        reconsider pn = (s . SBP ) as Element of NAT by A3, INT_1: 3;

        

         A8: pn = (s . SBP );

        then

         A9: ( IC ( Comput (P,s,7))) = (5 + 7) by A2, A4, A7, Lm4, A1;

        

         A10: ( Comput (P,s,8)) = ( Exec (i12,( Comput (P,s,7)))) by A2, A4, A7, A8, Lm4, A1;

        

         A11: (( Comput (P,s,7)) . SBP ) = (pn + 4) by A2, A4, A7, Lm4, A1;

        

         A12: (( Comput (P,s,7)) . GBP ) = 0 by A2, A4, A7, A8, Lm4, A1;

        

         A13: (( Comput (P,s,7)) . ( intpos (pn + 7))) = (x mod y) by A2, A4, A7, Lm4, A1;

        

         A14: (( Comput (P,s,7)) . ( intpos (pn + 6))) = y by A2, A4, A7, Lm4, A1;

        

         A15: (( Comput (P,s,7)) . ( intpos (pn + 4))) = pn by A2, A4, A7, Lm4, A1;

        

         A16: (( Comput (P,s,7)) . ( intpos (pn + 5))) = 11 by A2, A4, A7, Lm4, A1;

        set s8 = ( Comput (P,s,8));

        

         A17: ( IC s8) = ( ICplusConst (( Comput (P,s,7)),( - 7))) by A10, SCMPDS_2: 54

        .= 5 by A9, Th2;

        

         A18: (s8 . SBP ) = (pn + 4) by A10, A11, SCMPDS_2: 54;

        

         A19: 4 <= (pn + 4) by NAT_1: 11;

        

         A20: (s8 . SBP ) > 0 by A18;

        

         A21: (s8 . GBP ) = 0 by A10, A12, SCMPDS_2: 54;

        set x1 = (s8 . ( DataLoc ((s8 . SBP ),2))), y1 = (s8 . ( DataLoc ((s8 . SBP ),3)));

        

         A22: x1 = (s8 . ( intpos ((pn + 4) + 2))) by A18, Th1

        .= y by A10, A14, SCMPDS_2: 54;

        

         A23: y1 = (s8 . ( intpos ((pn + 4) + 3))) by A18, Th1

        .= (x mod y) by A10, A13, SCMPDS_2: 54;

        then y1 < y by A7, NEWTON: 65;

        then

        consider m such that

         A24: ( CurInstr (P,( Comput (P,s8,m)))) = ( return SBP ) and

         A25: (s8 . SBP ) = (( Comput (P,s8,m)) . SBP ) and

         A26: (( Comput (P,s8,m)) . ( DataLoc ((s8 . SBP ),2))) = (x1 gcd y1) and

         A27: for j be Nat st 1 < j & j <= ((s8 . SBP ) + 1) holds (s8 . ( intpos j)) = (( Comput (P,s8,m)) . ( intpos j)) by A17, A20, A21, A22, A23, Th12, A1, NEWTON: 64;

        set s9 = ( Comput (P,s,(m + 8)));

        

         A28: (s8 . SBP ) = (s9 . SBP ) by A25, EXTPRO_1: 4;

        

         A29: ( Comput (P,s,(m + 8))) = ( Comput (P,( Comput (P,s,8)),m)) by EXTPRO_1: 4;

        

         A30: ( Comput (P,s,(m + (8 + 1)))) = ( Comput (P,s,((m + 8) + 1)))

        .= ( Following (P,s9)) by EXTPRO_1: 3

        .= ( Exec (( return SBP ),s9)) by A24, A29;

        

         A31: 1 < (pn + 4) by A19, XXREAL_0: 2;

        (pn + 4) < ((s8 . SBP ) + 1) by A18, XREAL_1: 29;

        

        then

         A32: (s8 . ( intpos (pn + 4))) = (( Comput (P,s8,m)) . ( intpos (pn + 4))) by A27, A31

        .= (s9 . ( intpos (pn + 4))) by EXTPRO_1: 4;

        5 <= (pn + 5) by NAT_1: 11;

        then

         A33: 1 < (pn + 5) by XXREAL_0: 2;

        

         A34: 11 = (s8 . ( intpos (pn + 5))) by A10, A16, SCMPDS_2: 54

        .= (( Comput (P,s8,m)) . ( intpos (pn + 5))) by A18, A27, A33

        .= (s9 . ( intpos ((pn + 4) + 1))) by EXTPRO_1: 4

        .= (s9 . ( DataLoc ((s9 . SBP ), RetIC ))) by A18, A28, Th1, SCMPDS_I:def 14;

        

         A35: (P /. ( IC ( Comput (P,s,(m + 9))))) = (P . ( IC ( Comput (P,s,(m + 9))))) by PBOOLE: 143;

        

         A36: ( IC ( Comput (P,s,(m + 9)))) = ( |.(s9 . ( DataLoc ((s9 . SBP ), RetIC ))).| + 2) by A30, SCMPDS_2: 58

        .= (11 + 2) by A34, ABSVALUE: 29;

        

        then

         A37: ( CurInstr (P,( Comput (P,s,(m + 9))))) = (P . 13) by A35

        .= i13 by Lm1, A1;

        

         A38: ( Comput (P,s,(m + (9 + 1)))) = ( Comput (P,s,((m + 9) + 1)))

        .= ( Following (P,( Comput (P,s,(m + 9))))) by EXTPRO_1: 3

        .= ( Exec (i13,( Comput (P,s,(m + 9))))) by A37;

        

         A39: (( Comput (P,s,(m + 9))) . SBP ) = (s9 . ( DataLoc ((pn + 4), RetSP ))) by A18, A28, A30, SCMPDS_2: 58

        .= (s9 . ( intpos ((pn + 4) + 0 ))) by Th1, SCMPDS_I:def 13

        .= pn by A10, A15, A32, SCMPDS_2: 54;

        

         A40: (( Comput (P,s,(m + 9))) . ( intpos (pn + 6))) = (s9 . ( intpos ((pn + 4) + 2))) by A30, Lm3, SCMPDS_2: 58

        .= (s9 . ( DataLoc ((s8 . SBP ),2))) by A18, Th1

        .= (x1 gcd y1) by A26, EXTPRO_1: 4;

        

         A41: (P /. ( IC ( Comput (P,s,(m + 10))))) = (P . ( IC ( Comput (P,s,(m + 10))))) by PBOOLE: 143;

        ( IC ( Comput (P,s,(m + 10)))) = (( IC ( Comput (P,s,(m + 9)))) + 1) by A38, SCMPDS_2: 47

        .= (13 + 1) by A36;

        

        then

         A42: ( CurInstr (P,( Comput (P,s,(m + 10))))) = (P . 14) by A41

        .= i14 by Lm1, A1;

        hereby

          reconsider n = (m + 10) as Nat;

          take n;

          thus ( CurInstr (P,( Comput (P,s,n)))) = ( return SBP ) by A42;

          

           A43: ( DataLoc ((( Comput (P,s,(m + 9))) . SBP ),2)) = ( intpos (pn + 2)) by A39, Th1;

          hence (( Comput (P,s,n)) . SBP ) = (s . SBP ) by A38, A39, Lm3, SCMPDS_2: 47;

          

          thus (( Comput (P,s,n)) . ( DataLoc ((s . SBP ),2))) = (( Comput (P,s,(m + 9))) . ( DataLoc (pn,6))) by A38, A39, SCMPDS_2: 47

          .= (yy gcd (x mod yy)) by A22, A23, A40, Th1

          .= (x gcd yy) by A6, A7, NAT_D: 30;

          hereby

            let j be Nat;

            assume that

             A44: 1 < j and

             A45: j <= ((s . SBP ) + 1);

            (s . SBP ) <= (s8 . SBP ) by A18, NAT_1: 11;

            then ((s . SBP ) + 1) <= ((s8 . SBP ) + 1) by XREAL_1: 6;

            then

             A46: j <= ((s8 . SBP ) + 1) by A45, XXREAL_0: 2;

            

             A47: (( Comput (P,s,(m + 9))) . ( intpos j)) = (s9 . ( intpos j)) by A30, A44, AMI_3: 10, SCMPDS_2: 58

            .= (( Comput (P,s8,m)) . ( intpos j)) by EXTPRO_1: 4

            .= (s8 . ( intpos j)) by A27, A44, A46;

            

             A48: (pn + 1) < (pn + 2) by XREAL_1: 6;

            (( Comput (P,s,7)) . ( intpos j)) = (s . ( intpos j)) by A2, A4, A7, A8, A44, A45, Lm5, A1;

            

            hence (s . ( intpos j)) = (s8 . ( intpos j)) by A10, SCMPDS_2: 54

            .= (( Comput (P,s,n)) . ( intpos j)) by A38, A43, A45, A47, A48, AMI_3: 10, SCMPDS_2: 47;

          end;

        end;

      end;

    end;

    begin

    theorem :: SCMP_GCD:14

    for s be 0 -started State of SCMPDS st GCD-Algorithm c= P holds for x,y be Integer st (s . ( intpos 9)) = x & (s . ( intpos 10)) = y & x >= 0 & y >= 0 holds (( Result (P,s)) . ( intpos 9)) = (x gcd y)

    proof

      let s be 0 -started State of SCMPDS ;

      set GA = GCD-Algorithm ;

      assume

       A1: GA c= P;

      let x,y be Integer;

      assume that

       A2: (s . ( intpos 9)) = x and

       A3: (s . ( intpos 10)) = y and

       A4: x >= 0 and

       A5: y >= 0 ;

      set s4 = ( Comput (P,s,4));

      

       A6: ( IC s4) = 5 by Th11, A1;

      

       A7: (s4 . GBP ) = 0 by Th11, A1;

      

       A8: (s4 . SBP ) = 7 by Th11, A1;

      

       A9: (s4 . ( intpos (7 + RetIC ))) = 2 by Th11, A1;

      

       A10: (s4 . ( intpos 9)) = (s . ( intpos 9)) by Th11, A1;

      

       A11: (s4 . ( DataLoc ((s4 . SBP ),3))) = (s4 . ( intpos (7 + 3))) by A8, Th1

      .= y by A3, Th11, A1;

      

       A12: ( DataLoc ((s4 . SBP ),2)) = ( intpos (7 + 2)) by A8, Th1;

      then

       A13: (s4 . ( DataLoc ((s4 . SBP ),2))) = x by A2, Th11, A1;

      consider n such that

       A14: ( CurInstr (P,( Comput (P,s4,n)))) = ( return SBP ) and

       A15: (s4 . SBP ) = (( Comput (P,s4,n)) . SBP ) and

       A16: (( Comput (P,s4,n)) . ( DataLoc ((s4 . SBP ),2))) = ((s4 . ( DataLoc ((s4 . SBP ),2))) gcd (s4 . ( DataLoc ((s4 . SBP ),3)))) and

       A17: for j be Nat st 1 < j & j <= ((s4 . SBP ) + 1) holds (s4 . ( intpos j)) = (( Comput (P,s4,n)) . ( intpos j)) by A2, A4, A5, A6, A7, A8, A10, A11, A12, Th13, A1;

      

       A18: ( DataLoc ((( Comput (P,s4,n)) . SBP ), RetIC )) = ( intpos (7 + 1)) by A8, A15, Th1, SCMPDS_I:def 14;

      

       A19: ( Comput (P,s4,(n + 1))) = ( Following (P,( Comput (P,s4,n)))) by EXTPRO_1: 3

      .= ( Exec (i14,( Comput (P,s4,n)))) by A14;

      

       A20: for m be Nat st m = (( Comput (P,s4,n)) . ( DataLoc ((( Comput (P,s4,n)) . SBP ), RetIC ))) holds m = |.(( Comput (P,s4,n)) . ( DataLoc ((( Comput (P,s4,n)) . SBP ), RetIC ))).| by ABSVALUE: 29;

      

       A21: ( IC ( Comput (P,s,(4 + (n + 1))))) = (( Comput (P,s4,(n + 1))) . ( IC SCMPDS )) by EXTPRO_1: 4

      .= ( |.(( Comput (P,s4,n)) . ( DataLoc ((( Comput (P,s4,n)) . SBP ), RetIC ))).| + 2) by A19, SCMPDS_2: 58

      .= (2 + 2) by A8, A9, A17, A18, A20, SCMPDS_I:def 14;

      (P . ( IC ( Comput (P,s,(4 + (n + 1)))))) = (P . ( IC ( Comput (P,s,(4 + (n + 1))))))

      .= i04 by Lm1, A21, A1;

      

      then ( Result (P,s)) = ( Comput (P,s,(4 + (n + 1)))) by EXTPRO_1: 7

      .= ( Comput (P,s4,(n + 1))) by EXTPRO_1: 4;

      hence thesis by A11, A12, A13, A16, A19, AMI_3: 10, SCMPDS_2: 58;

    end;

    

     Lm6: GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & ( IC s1) = 5 & n = (s1 . SBP ) & (s1 . GBP ) = 0 & (s1 . ( DataLoc ((s1 . SBP ),3))) > 0 & ( IC s2) = ( IC s1) & (s2 . SBP ) = (s1 . SBP ) & (s2 . GBP ) = 0 & (s2 . ( DataLoc ((s1 . SBP ),2))) = (s1 . ( DataLoc ((s1 . SBP ),2))) & (s2 . ( DataLoc ((s1 . SBP ),3))) = (s1 . ( DataLoc ((s1 . SBP ),3))) implies ( IC ( Comput (P1,s1,7))) = (5 + 7) & ( Comput (P1,s1,8)) = ( Exec (i12,( Comput (P1,s1,7)))) & (( Comput (P1,s1,7)) . SBP ) = (n + 4) & (( Comput (P1,s1,7)) . GBP ) = 0 & (( Comput (P1,s1,7)) . ( intpos (n + 7))) = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) & (( Comput (P1,s1,7)) . ( intpos (n + 6))) = (s1 . ( intpos (n + 3))) & ( IC ( Comput (P2,s2,7))) = (5 + 7) & ( Comput (P2,s2,8)) = ( Exec (i12,( Comput (P2,s2,7)))) & (( Comput (P2,s2,7)) . SBP ) = (n + 4) & (( Comput (P2,s2,7)) . GBP ) = 0 & (( Comput (P2,s2,7)) . ( intpos (n + 7))) = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) & (( Comput (P2,s2,7)) . ( intpos (n + 6))) = (s1 . ( intpos (n + 3))) & (( Comput (P1,s1,7)) . ( intpos (n + 4))) = n & (( Comput (P1,s1,7)) . ( intpos (n + 5))) = 11 & (( Comput (P2,s2,7)) . ( intpos (n + 4))) = n & (( Comput (P2,s2,7)) . ( intpos (n + 5))) = 11

    proof

      set GA = GCD-Algorithm ;

      assume that

       A1: GA c= P1 and

       A2: GA c= P2;

      assume

       A3: ( IC s1) = 5;

      assume

       A4: n = (s1 . SBP );

      assume

       A5: (s1 . GBP ) = 0 ;

      assume

       A6: (s1 . ( DataLoc ((s1 . SBP ),3))) > 0 ;

      assume that

       A7: ( IC s2) = ( IC s1) and

       A8: (s2 . SBP ) = (s1 . SBP ) and

       A9: (s2 . GBP ) = 0 ;

      assume that

       A10: (s2 . ( DataLoc ((s1 . SBP ),2))) = (s1 . ( DataLoc ((s1 . SBP ),2))) and

       A11: (s2 . ( DataLoc ((s1 . SBP ),3))) = (s1 . ( DataLoc ((s1 . SBP ),3)));

      

       A12: ( DataLoc ((s1 . SBP ),2)) = ( intpos (n + 2)) by A4, Th1;

      

       A13: ( DataLoc ((s1 . SBP ),3)) = ( intpos (n + 3)) by A4, Th1;

      thus ( IC ( Comput (P1,s1,7))) = (5 + 7) & ( Comput (P1,s1,8)) = ( Exec (i12,( Comput (P1,s1,7)))) & (( Comput (P1,s1,7)) . SBP ) = (n + 4) & (( Comput (P1,s1,7)) . GBP ) = 0 by A3, A4, A5, A6, Lm4, A1;

      thus (( Comput (P1,s1,7)) . ( intpos (n + 7))) = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) by A3, A4, A5, A6, A12, A13, Lm4, A1;

      thus (( Comput (P1,s1,7)) . ( intpos (n + 6))) = (s1 . ( intpos (n + 3))) by A3, A4, A5, A6, A13, Lm4, A1;

      thus ( IC ( Comput (P2,s2,7))) = (5 + 7) & ( Comput (P2,s2,8)) = ( Exec (i12,( Comput (P2,s2,7)))) & (( Comput (P2,s2,7)) . SBP ) = (n + 4) & (( Comput (P2,s2,7)) . GBP ) = 0 by A3, A4, A6, A7, A8, A9, A11, Lm4, A2;

      thus (( Comput (P2,s2,7)) . ( intpos (n + 7))) = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) by A3, A4, A6, A7, A8, A9, A10, A11, A12, A13, Lm4, A2;

      thus (( Comput (P2,s2,7)) . ( intpos (n + 6))) = (s1 . ( intpos (n + 3))) by A3, A4, A6, A7, A8, A9, A11, A13, Lm4, A2;

      thus (( Comput (P1,s1,7)) . ( intpos (n + 4))) = n & (( Comput (P1,s1,7)) . ( intpos (n + 5))) = 11 by A3, A4, A5, A6, Lm4, A1;

      thus thesis by A3, A4, A6, A7, A8, A9, A11, Lm4, A2;

    end;

    

     Lm7: GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & ( IC s1) = 5 & n = (s1 . SBP ) & (s1 . GBP ) = 0 & (s1 . ( DataLoc ((s1 . SBP ),3))) > 0 & ( IC s2) = ( IC s1) & (s2 . SBP ) = (s1 . SBP ) & (s2 . GBP ) = 0 & (s2 . ( DataLoc ((s1 . SBP ),2))) = (s1 . ( DataLoc ((s1 . SBP ),2))) & (s2 . ( DataLoc ((s1 . SBP ),3))) = (s1 . ( DataLoc ((s1 . SBP ),3))) implies for k be Nat, a be Int_position st k <= 7 & (s1 . a) = (s2 . a) holds ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) & (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a)

    proof

      set GA = GCD-Algorithm ;

      assume that

       A1: GA c= P1 and

       A2: GA c= P2;

      assume

       A3: ( IC s1) = 5;

      assume

       A4: n = (s1 . SBP );

      assume

       A5: (s1 . GBP ) = 0 ;

      assume

       A6: (s1 . ( DataLoc ((s1 . SBP ),3))) > 0 ;

      assume that

       A7: ( IC s2) = ( IC s1) and

       A8: (s2 . SBP ) = (s1 . SBP ) and

       A9: (s2 . GBP ) = 0 ;

      assume that

       A10: (s2 . ( DataLoc ((s1 . SBP ),2))) = (s1 . ( DataLoc ((s1 . SBP ),2))) and

       A11: (s2 . ( DataLoc ((s1 . SBP ),3))) = (s1 . ( DataLoc ((s1 . SBP ),3)));

      

       A12: (P1 /. ( IC s1)) = (P1 . ( IC s1)) by PBOOLE: 143;

      

       A13: ( Comput (P1,s1,(1 + 0 ))) = ( Following (P1,( Comput (P1,s1, 0 )))) by EXTPRO_1: 3

      .= ( Following (P1,s1)) by EXTPRO_1: 2

      .= ( Exec (i05,s1)) by A12, A3, Lm1, A1;

      

       A14: (P2 /. ( IC s2)) = (P2 . ( IC s2)) by PBOOLE: 143;

      

       A15: ( Comput (P2,s2,(1 + 0 ))) = ( Following (P2,( Comput (P2,s2, 0 )))) by EXTPRO_1: 3

      .= ( Following (P2,s2)) by EXTPRO_1: 2

      .= ( Exec (i05,s2)) by A3, A7, Lm1, A14, A2;

      

       A16: (P1 /. ( IC ( Comput (P1,s1,1)))) = (P1 . ( IC ( Comput (P1,s1,1)))) by PBOOLE: 143;

      

       A17: ( IC ( Comput (P1,s1,1))) = (( IC s1) + 1) by A6, A13, SCMPDS_2: 56

      .= (5 + 1) by A3;

      

      then

       A18: ( CurInstr (P1,( Comput (P1,s1,1)))) = (P1 . 6) by A16

      .= i06 by Lm1, A1;

      

       A19: ( Comput (P1,s1,(1 + 1))) = ( Following (P1,( Comput (P1,s1,1)))) by EXTPRO_1: 3

      .= ( Exec (i06,( Comput (P1,s1,1)))) by A18;

      

       A20: (( Comput (P1,s1,1)) . SBP ) = n by A4, A13, SCMPDS_2: 56;

      

       A21: (( Comput (P1,s1,1)) . GBP ) = 0 by A5, A13, SCMPDS_2: 56;

      

       A22: (P2 /. ( IC ( Comput (P2,s2,1)))) = (P2 . ( IC ( Comput (P2,s2,1)))) by PBOOLE: 143;

      

       A23: ( IC ( Comput (P2,s2,1))) = (( IC s2) + 1) by A6, A8, A11, A15, SCMPDS_2: 56

      .= (5 + 1) by A3, A7;

      

      then

       A24: ( CurInstr (P2,( Comput (P2,s2,1)))) = (P2 . 6) by A22

      .= i06 by Lm1, A2;

      

       A25: ( Comput (P2,s2,(1 + 1))) = ( Following (P2,( Comput (P2,s2,1)))) by EXTPRO_1: 3

      .= ( Exec (i06,( Comput (P2,s2,1)))) by A24;

      

       A26: (P1 /. ( IC ( Comput (P1,s1,2)))) = (P1 . ( IC ( Comput (P1,s1,2)))) by PBOOLE: 143;

      

       A27: ( IC ( Comput (P1,s1,2))) = (( IC ( Comput (P1,s1,1))) + 1) by A19, SCMPDS_2: 47

      .= (6 + 1) by A17;

      

      then

       A28: ( CurInstr (P1,( Comput (P1,s1,2)))) = (P1 . 7) by A26

      .= i07 by Lm1, A1;

      

       A29: ( Comput (P1,s1,(2 + 1))) = ( Following (P1,( Comput (P1,s1,2)))) by EXTPRO_1: 3

      .= ( Exec (i07,( Comput (P1,s1,2)))) by A28;

      

       A30: ( DataLoc ((( Comput (P1,s1,1)) . SBP ),6)) = ( intpos (n + 6)) by A20, Th1;

      then

       A31: (( Comput (P1,s1,2)) . SBP ) = n by A19, A20, Lm3, SCMPDS_2: 47;

      

       A32: (( Comput (P1,s1,2)) . GBP ) = 0 by A19, A21, A30, Lm2, SCMPDS_2: 47;

      

       A33: (P2 /. ( IC ( Comput (P2,s2,2)))) = (P2 . ( IC ( Comput (P2,s2,2)))) by PBOOLE: 143;

      

       A34: ( IC ( Comput (P2,s2,2))) = (( IC ( Comput (P2,s2,1))) + 1) by A25, SCMPDS_2: 47

      .= (6 + 1) by A23;

      

      then

       A35: ( CurInstr (P2,( Comput (P2,s2,2)))) = (P2 . 7) by A33

      .= i07 by Lm1, A2;

      

       A36: ( Comput (P2,s2,(2 + 1))) = ( Following (P2,( Comput (P2,s2,2)))) by EXTPRO_1: 3

      .= ( Exec (i07,( Comput (P2,s2,2)))) by A35;

      

       A37: (P1 /. ( IC ( Comput (P1,s1,3)))) = (P1 . ( IC ( Comput (P1,s1,3)))) by PBOOLE: 143;

      

       A38: ( IC ( Comput (P1,s1,3))) = (( IC ( Comput (P1,s1,2))) + 1) by A29, SCMPDS_2: 52

      .= (7 + 1) by A27;

      

      then

       A39: ( CurInstr (P1,( Comput (P1,s1,3)))) = (P1 . 8) by A37

      .= i08 by Lm1, A1;

      

       A40: ( Comput (P1,s1,(3 + 1))) = ( Following (P1,( Comput (P1,s1,3)))) by EXTPRO_1: 3

      .= ( Exec (i08,( Comput (P1,s1,3)))) by A39;

      

       A41: ( DataLoc ((( Comput (P1,s1,2)) . SBP ),2)) = ( intpos (n + 2)) by A31, Th1;

      then

       A42: SBP <> ( DataLoc ((( Comput (P1,s1,2)) . SBP ),2)) by Lm3;

      

       A43: ( DataLoc ((( Comput (P1,s1,2)) . SBP ),3)) = ( intpos (n + 3)) by A31, Th1;

      then SBP <> ( DataLoc ((( Comput (P1,s1,2)) . SBP ),3)) by Lm3;

      then

       A44: (( Comput (P1,s1,3)) . SBP ) = n by A29, A31, A42, SCMPDS_2: 52;

      

       A45: GBP <> ( DataLoc ((( Comput (P1,s1,2)) . SBP ),2)) by A41, Lm2;

       GBP <> ( DataLoc ((( Comput (P1,s1,2)) . SBP ),3)) by A43, Lm2;

      then

       A46: (( Comput (P1,s1,3)) . GBP ) = 0 by A29, A32, A45, SCMPDS_2: 52;

      

       A47: (P2 /. ( IC ( Comput (P2,s2,3)))) = (P2 . ( IC ( Comput (P2,s2,3)))) by PBOOLE: 143;

      

       A48: ( IC ( Comput (P2,s2,3))) = (( IC ( Comput (P2,s2,2))) + 1) by A36, SCMPDS_2: 52

      .= (7 + 1) by A34;

      

      then

       A49: ( CurInstr (P2,( Comput (P2,s2,3)))) = (P2 . 8) by A47

      .= i08 by Lm1, A2;

      

       A50: ( Comput (P2,s2,(3 + 1))) = ( Following (P2,( Comput (P2,s2,3)))) by EXTPRO_1: 3

      .= ( Exec (i08,( Comput (P2,s2,3)))) by A49;

      

       A51: (P1 /. ( IC ( Comput (P1,s1,4)))) = (P1 . ( IC ( Comput (P1,s1,4)))) by PBOOLE: 143;

      

       A52: ( IC ( Comput (P1,s1,4))) = (( IC ( Comput (P1,s1,3))) + 1) by A40, SCMPDS_2: 47

      .= (8 + 1) by A38;

      

      then

       A53: ( CurInstr (P1,( Comput (P1,s1,4)))) = (P1 . 9) by A51

      .= i09 by Lm1, A1;

      

       A54: ( Comput (P1,s1,(4 + 1))) = ( Following (P1,( Comput (P1,s1,4)))) by EXTPRO_1: 3

      .= ( Exec (i09,( Comput (P1,s1,4)))) by A53;

      

       A55: ( DataLoc ((( Comput (P1,s1,3)) . SBP ),7)) = ( intpos (n + 7)) by A44, Th1;

      then

       A56: (( Comput (P1,s1,4)) . SBP ) = n by A40, A44, Lm3, SCMPDS_2: 47;

      

       A57: (( Comput (P1,s1,4)) . GBP ) = 0 by A40, A46, A55, Lm2, SCMPDS_2: 47;

      

       A58: (P2 /. ( IC ( Comput (P2,s2,4)))) = (P2 . ( IC ( Comput (P2,s2,4)))) by PBOOLE: 143;

      

       A59: ( IC ( Comput (P2,s2,4))) = (( IC ( Comput (P2,s2,3))) + 1) by A50, SCMPDS_2: 47

      .= (8 + 1) by A48;

      

      then

       A60: ( CurInstr (P2,( Comput (P2,s2,4)))) = (P2 . 9) by A58

      .= i09 by Lm1, A2;

      

       A61: ( Comput (P2,s2,(4 + 1))) = ( Following (P2,( Comput (P2,s2,4)))) by EXTPRO_1: 3

      .= ( Exec (i09,( Comput (P2,s2,4)))) by A60;

      

       A62: (P1 /. ( IC ( Comput (P1,s1,5)))) = (P1 . ( IC ( Comput (P1,s1,5)))) by PBOOLE: 143;

      

       A63: ( IC ( Comput (P1,s1,5))) = (( IC ( Comput (P1,s1,4))) + 1) by A54, SCMPDS_2: 47

      .= (9 + 1) by A52;

      

      then

       A64: ( CurInstr (P1,( Comput (P1,s1,5)))) = (P1 . 10) by A62

      .= i10 by Lm1, A1;

      

       A65: ( Comput (P1,s1,(5 + 1))) = ( Following (P1,( Comput (P1,s1,5)))) by EXTPRO_1: 3

      .= ( Exec (i10,( Comput (P1,s1,5)))) by A64;

      ( DataLoc ((( Comput (P1,s1,4)) . SBP ),(4 + RetSP ))) = ( intpos (n + (4 + 0 ))) by A56, Th1, SCMPDS_I:def 13;

      then

       A66: (( Comput (P1,s1,5)) . GBP ) = 0 by A54, A57, Lm2, SCMPDS_2: 47;

      

       A67: (P2 /. ( IC ( Comput (P2,s2,5)))) = (P2 . ( IC ( Comput (P2,s2,5)))) by PBOOLE: 143;

      

       A68: ( IC ( Comput (P2,s2,5))) = (( IC ( Comput (P2,s2,4))) + 1) by A61, SCMPDS_2: 47

      .= (9 + 1) by A59;

      

      then

       A69: ( CurInstr (P2,( Comput (P2,s2,5)))) = (P2 . 10) by A67

      .= i10 by Lm1, A2;

      

       A70: ( Comput (P2,s2,(5 + 1))) = ( Following (P2,( Comput (P2,s2,5)))) by EXTPRO_1: 3

      .= ( Exec (i10,( Comput (P2,s2,5)))) by A69;

      

       A71: (P1 /. ( IC ( Comput (P1,s1,6)))) = (P1 . ( IC ( Comput (P1,s1,6)))) by PBOOLE: 143;

      

       A72: ( IC ( Comput (P1,s1,6))) = (( IC ( Comput (P1,s1,5))) + 1) by A65, SCMPDS_2: 48

      .= (10 + 1) by A63;

      

      then

       A73: ( CurInstr (P1,( Comput (P1,s1,6)))) = (P1 . 11) by A71

      .= i11 by Lm1, A1;

      

       A74: ( Comput (P1,s1,(6 + 1))) = ( Following (P1,( Comput (P1,s1,6)))) by EXTPRO_1: 3

      .= ( Exec (i11,( Comput (P1,s1,6)))) by A73;

      

       A75: (P2 /. ( IC ( Comput (P2,s2,6)))) = (P2 . ( IC ( Comput (P2,s2,6)))) by PBOOLE: 143;

      

       A76: ( IC ( Comput (P2,s2,6))) = (( IC ( Comput (P2,s2,5))) + 1) by A70, SCMPDS_2: 48

      .= (10 + 1) by A68;

      

      then

       A77: ( CurInstr (P2,( Comput (P2,s2,6)))) = (P2 . 11) by A75

      .= i11 by Lm1, A2;

      

       A78: ( Comput (P2,s2,(6 + 1))) = ( Following (P2,( Comput (P2,s2,6)))) by EXTPRO_1: 3

      .= ( Exec (i11,( Comput (P2,s2,6)))) by A77;

       A79:

      now

        let b;

        assume (s1 . b) = (s2 . b);

        

        hence (( Comput (P1,s1,1)) . b) = (s2 . b) by A13, SCMPDS_2: 56

        .= (( Comput (P2,s2,1)) . b) by A15, SCMPDS_2: 56;

      end;

      

       A80: (s1 . b) = (s2 . b) implies (( Comput (P1,s1,2)) . b) = (( Comput (P2,s2,2)) . b)

      proof

        assume

         A81: (s1 . b) = (s2 . b);

        per cases ;

          suppose

           A82: b = ( DataLoc ((( Comput (P1,s1,1)) . SBP ),6));

          then

           A83: b = ( DataLoc ((( Comput (P2,s2,1)) . SBP ),6)) by A8, A79;

          

          thus (( Comput (P1,s1,2)) . b) = (( Comput (P1,s1,1)) . ( DataLoc ((s1 . SBP ),3))) by A4, A19, A20, A82, SCMPDS_2: 47

          .= (( Comput (P2,s2,1)) . ( DataLoc ((( Comput (P1,s1,1)) . SBP ),3))) by A4, A11, A20, A79

          .= (( Comput (P2,s2,1)) . ( DataLoc ((( Comput (P2,s2,1)) . SBP ),3))) by A8, A79

          .= (( Comput (P2,s2,2)) . b) by A25, A83, SCMPDS_2: 47;

        end;

          suppose

           A84: b <> ( DataLoc ((( Comput (P1,s1,1)) . SBP ),6));

          then

           A85: b <> ( DataLoc ((( Comput (P2,s2,1)) . SBP ),6)) by A8, A79;

          

          thus (( Comput (P1,s1,2)) . b) = (( Comput (P1,s1,1)) . b) by A19, A84, SCMPDS_2: 47

          .= (( Comput (P2,s2,1)) . b) by A79, A81

          .= (( Comput (P2,s2,2)) . b) by A25, A85, SCMPDS_2: 47;

        end;

      end;

       A86:

      now

        let b;

        assume

         A87: (s1 . b) = (s2 . b);

        set x1 = ( DataLoc ((( Comput (P1,s1,2)) . SBP ),2)), x2 = ( DataLoc ((( Comput (P1,s1,2)) . SBP ),3)), y1 = ( DataLoc ((( Comput (P2,s2,2)) . SBP ),2)), y2 = ( DataLoc ((( Comput (P2,s2,2)) . SBP ),3));

        

         A88: x1 = y1 by A8, A80;

        

         A89: x2 = y2 by A8, A80;

        per cases ;

          suppose

           A90: b <> x1 & b <> x2;

          

          hence (( Comput (P1,s1,3)) . b) = (( Comput (P1,s1,2)) . b) by A29, SCMPDS_2: 52

          .= (( Comput (P2,s2,2)) . b) by A80, A87

          .= (( Comput (P2,s2,3)) . b) by A36, A88, A89, A90, SCMPDS_2: 52;

        end;

          suppose

           A91: b = x1;

          

           A92: (n + 2) <> (n + 3);

          then

           A93: x1 <> x2 by A41, A43, AMI_3: 10;

          

           A94: y1 <> y2 by A41, A43, A88, A89, A92, AMI_3: 10;

          

          thus (( Comput (P1,s1,3)) . b) = ((( Comput (P1,s1,2)) . x1) div (( Comput (P1,s1,2)) . x2)) by A29, A91, A93, SCMPDS_2: 52

          .= ((( Comput (P2,s2,2)) . x1) div (( Comput (P1,s1,2)) . x2)) by A4, A10, A31, A80

          .= ((( Comput (P2,s2,2)) . x1) div (( Comput (P2,s2,2)) . x2)) by A4, A11, A31, A80

          .= (( Comput (P2,s2,3)) . b) by A36, A88, A89, A91, A94, SCMPDS_2: 52;

        end;

          suppose

           A95: b = x2;

          

          hence (( Comput (P1,s1,3)) . b) = ((( Comput (P1,s1,2)) . x1) mod (( Comput (P1,s1,2)) . x2)) by A29, SCMPDS_2: 52

          .= ((( Comput (P2,s2,2)) . x1) mod (( Comput (P1,s1,2)) . x2)) by A4, A10, A31, A80

          .= ((( Comput (P2,s2,2)) . x1) mod (( Comput (P2,s2,2)) . x2)) by A4, A11, A31, A80

          .= (( Comput (P2,s2,3)) . b) by A36, A88, A89, A95, SCMPDS_2: 52;

        end;

      end;

       A96:

      now

        let b;

        assume

         A97: (s1 . b) = (s2 . b);

        per cases ;

          suppose

           A98: b = ( DataLoc ((( Comput (P1,s1,3)) . SBP ),7));

          then

           A99: b = ( DataLoc ((( Comput (P2,s2,3)) . SBP ),7)) by A8, A86;

          

          thus (( Comput (P1,s1,4)) . b) = (( Comput (P1,s1,3)) . ( DataLoc ((( Comput (P1,s1,3)) . SBP ),3))) by A40, A98, SCMPDS_2: 47

          .= (( Comput (P2,s2,3)) . ( DataLoc ((( Comput (P1,s1,3)) . SBP ),3))) by A4, A11, A44, A86

          .= (( Comput (P2,s2,3)) . ( DataLoc ((( Comput (P2,s2,3)) . SBP ),3))) by A8, A86

          .= (( Comput (P2,s2,4)) . b) by A50, A99, SCMPDS_2: 47;

        end;

          suppose

           A100: b <> ( DataLoc ((( Comput (P1,s1,3)) . SBP ),7));

          then

           A101: b <> ( DataLoc ((( Comput (P2,s2,3)) . SBP ),7)) by A8, A86;

          

          thus (( Comput (P1,s1,4)) . b) = (( Comput (P1,s1,3)) . b) by A40, A100, SCMPDS_2: 47

          .= (( Comput (P2,s2,3)) . b) by A86, A97

          .= (( Comput (P2,s2,4)) . b) by A50, A101, SCMPDS_2: 47;

        end;

      end;

       A102:

      now

        let b;

        assume

         A103: (s1 . b) = (s2 . b);

        

         A104: (s1 . ( DataLoc ((( Comput (P1,s1,4)) . GBP ),1))) = (s2 . ( intpos ( 0 + 1))) by A8, A57, Th1

        .= (s2 . ( DataLoc ((( Comput (P1,s1,4)) . GBP ),1))) by A57, Th1;

        per cases ;

          suppose

           A105: b = ( DataLoc ((( Comput (P1,s1,4)) . SBP ),(4 + RetSP )));

          then

           A106: b = ( DataLoc ((( Comput (P2,s2,4)) . SBP ),(4 + RetSP ))) by A8, A96;

          

          thus (( Comput (P1,s1,5)) . b) = (( Comput (P1,s1,4)) . ( DataLoc ((( Comput (P1,s1,4)) . GBP ),1))) by A54, A105, SCMPDS_2: 47

          .= (( Comput (P2,s2,4)) . ( DataLoc ((( Comput (P1,s1,4)) . GBP ),1))) by A96, A104

          .= (( Comput (P2,s2,4)) . ( DataLoc ((( Comput (P2,s2,4)) . GBP ),1))) by A5, A9, A96

          .= (( Comput (P2,s2,5)) . b) by A61, A106, SCMPDS_2: 47;

        end;

          suppose

           A107: b <> ( DataLoc ((( Comput (P1,s1,4)) . SBP ),(4 + RetSP )));

          then

           A108: b <> ( DataLoc ((( Comput (P2,s2,4)) . SBP ),(4 + RetSP ))) by A8, A96;

          

          thus (( Comput (P1,s1,5)) . b) = (( Comput (P1,s1,4)) . b) by A54, A107, SCMPDS_2: 47

          .= (( Comput (P2,s2,4)) . b) by A96, A103

          .= (( Comput (P2,s2,5)) . b) by A61, A108, SCMPDS_2: 47;

        end;

      end;

       A109:

      now

        let b;

        assume

         A110: (s1 . b) = (s2 . b);

        

         A111: (s1 . ( DataLoc ((( Comput (P1,s1,5)) . GBP ),1))) = (s2 . ( intpos ( 0 + 1))) by A8, A66, Th1

        .= (s2 . ( DataLoc ((( Comput (P1,s1,5)) . GBP ),1))) by A66, Th1;

        per cases ;

          suppose

           A112: b = ( DataLoc ((( Comput (P1,s1,5)) . GBP ),1));

          then

           A113: b = ( DataLoc ((( Comput (P2,s2,5)) . GBP ),1)) by A5, A9, A102;

          

          thus (( Comput (P1,s1,6)) . b) = ((( Comput (P1,s1,5)) . ( DataLoc ((( Comput (P1,s1,5)) . GBP ),1))) + 4) by A65, A112, SCMPDS_2: 48

          .= ((( Comput (P2,s2,5)) . ( DataLoc ((( Comput (P1,s1,5)) . GBP ),1))) + 4) by A102, A111

          .= ((( Comput (P2,s2,5)) . ( DataLoc ((( Comput (P2,s2,5)) . GBP ),1))) + 4) by A5, A9, A102

          .= (( Comput (P2,s2,6)) . b) by A70, A113, SCMPDS_2: 48;

        end;

          suppose

           A114: b <> ( DataLoc ((( Comput (P1,s1,5)) . GBP ),1));

          then

           A115: b <> ( DataLoc ((( Comput (P2,s2,5)) . GBP ),1)) by A5, A9, A102;

          

          thus (( Comput (P1,s1,6)) . b) = (( Comput (P1,s1,5)) . b) by A65, A114, SCMPDS_2: 48

          .= (( Comput (P2,s2,5)) . b) by A102, A110

          .= (( Comput (P2,s2,6)) . b) by A70, A115, SCMPDS_2: 48;

        end;

      end;

       A116:

      now

        let b;

        assume

         A117: (s1 . b) = (s2 . b);

        per cases ;

          suppose

           A118: b = ( DataLoc ((( Comput (P1,s1,6)) . SBP ), RetIC ));

          then

           A119: b = ( DataLoc ((( Comput (P2,s2,6)) . SBP ), RetIC )) by A8, A109;

          

          thus (( Comput (P1,s1,7)) . b) = ( IC ( Comput (P1,s1,6))) by A74, A118, SCMPDS_2: 59

          .= (( Comput (P2,s2,7)) . b) by A72, A76, A78, A119, SCMPDS_2: 59;

        end;

          suppose

           A120: b <> ( DataLoc ((( Comput (P1,s1,6)) . SBP ), RetIC ));

          then

           A121: b <> ( DataLoc ((( Comput (P2,s2,6)) . SBP ), RetIC )) by A8, A109;

          

          thus (( Comput (P1,s1,7)) . b) = (( Comput (P1,s1,6)) . b) by A74, A120, SCMPDS_2: 59

          .= (( Comput (P2,s2,6)) . b) by A109, A117

          .= (( Comput (P2,s2,7)) . b) by A78, A121, SCMPDS_2: 59;

        end;

      end;

      hereby

        let k be Nat, a be Int_position;

        assume that

         A122: k <= 7 and

         A123: (s1 . a) = (s2 . a);

        k = 0 or ... or k = 7 by A122;

        per cases ;

          suppose

           A124: k = 0 ;

          

          hence ( IC ( Comput (P1,s1,k))) = ( IC s1) by EXTPRO_1: 2

          .= ( IC ( Comput (P2,s2,k))) by A7, A124, EXTPRO_1: 2;

          

          thus (( Comput (P1,s1,k)) . a) = (s1 . a) by A124, EXTPRO_1: 2

          .= (( Comput (P2,s2,k)) . a) by A123, A124, EXTPRO_1: 2;

        end;

          suppose

           A125: k = 1;

          hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A17, A23;

          thus (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A79, A123, A125;

        end;

          suppose

           A126: k = 2;

          hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A27, A34;

          thus (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A80, A123, A126;

        end;

          suppose

           A127: k = 3;

          hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A38, A48;

          thus (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A86, A123, A127;

        end;

          suppose

           A128: k = 4;

          hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A52, A59;

          thus (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A96, A123, A128;

        end;

          suppose

           A129: k = 5;

          hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A63, A68;

          thus (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A102, A123, A129;

        end;

          suppose

           A130: k = 6;

          hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A72, A76;

          thus (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A109, A123, A130;

        end;

          suppose

           A131: k = 7;

          

          hence ( IC ( Comput (P1,s1,k))) = (( IC ( Comput (P2,s2,6))) + 1) by A72, A74, A76, SCMPDS_2: 59

          .= ( IC ( Comput (P2,s2,k))) by A78, A131, SCMPDS_2: 59;

          thus (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A116, A123, A131;

        end;

      end;

    end;

    

     Lm8: for s1,s2 be State of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & ( IC s1) = 5 & (s1 . SBP ) > 0 & (s1 . GBP ) = 0 & (s1 . ( DataLoc ((s1 . SBP ),3))) >= 0 & (s1 . ( DataLoc ((s1 . SBP ),2))) >= (s1 . ( DataLoc ((s1 . SBP ),3))) & ( IC s2) = ( IC s1) & (s2 . SBP ) = (s1 . SBP ) & (s2 . GBP ) = 0 & (s2 . ( DataLoc ((s1 . SBP ),2))) = (s1 . ( DataLoc ((s1 . SBP ),2))) & (s2 . ( DataLoc ((s1 . SBP ),3))) = (s1 . ( DataLoc ((s1 . SBP ),3))) holds ex n st ( CurInstr (P1,( Comput (P1,s1,n)))) = ( return SBP ) & (s1 . SBP ) = (( Comput (P1,s1,n)) . SBP ) & ( CurInstr (P2,( Comput (P2,s2,n)))) = ( return SBP ) & (s2 . SBP ) = (( Comput (P2,s2,n)) . SBP ) & (for j be Nat st 1 < j & j <= ((s1 . SBP ) + 1) holds (s1 . ( intpos j)) = (( Comput (P1,s1,n)) . ( intpos j)) & (s2 . ( intpos j)) = (( Comput (P2,s2,n)) . ( intpos j))) & for k be Nat, a be Int_position st k <= n & (s1 . a) = (s2 . a) holds ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) & (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a)

    proof

      set GA = GCD-Algorithm ;

      defpred P[ Nat] means for s1,s2 be State of SCMPDS st GA c= P1 & GA c= P2 & ( IC s1) = 5 & (s1 . SBP ) > 0 & (s1 . GBP ) = 0 & (s1 . ( DataLoc ((s1 . SBP ),3))) <= $1 & (s1 . ( DataLoc ((s1 . SBP ),3))) >= 0 & (s1 . ( DataLoc ((s1 . SBP ),2))) >= (s1 . ( DataLoc ((s1 . SBP ),3))) & ( IC s2) = ( IC s1) & (s2 . SBP ) = (s1 . SBP ) & (s2 . GBP ) = 0 & (s2 . ( DataLoc ((s1 . SBP ),2))) = (s1 . ( DataLoc ((s1 . SBP ),2))) & (s2 . ( DataLoc ((s1 . SBP ),3))) = (s1 . ( DataLoc ((s1 . SBP ),3))) holds ex n st ( CurInstr (P1,( Comput (P1,s1,n)))) = ( return SBP ) & (s1 . SBP ) = (( Comput (P1,s1,n)) . SBP ) & ( CurInstr (P2,( Comput (P2,s2,n)))) = ( return SBP ) & (s2 . SBP ) = (( Comput (P2,s2,n)) . SBP ) & (for j be Nat st 1 < j & j <= ((s1 . SBP ) + 1) holds (s1 . ( intpos j)) = (( Comput (P1,s1,n)) . ( intpos j)) & (s2 . ( intpos j)) = (( Comput (P2,s2,n)) . ( intpos j))) & (for k be Nat, a be Int_position st k <= n & (s1 . a) = (s2 . a) holds ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) & (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a));

      

       A1: P[ 0 ]

      proof

        let s1,s2 be State of SCMPDS ;

        set x = (s1 . ( DataLoc ((s1 . SBP ),2))), y = (s1 . ( DataLoc ((s1 . SBP ),3))), y2 = (s2 . ( DataLoc ((s1 . SBP ),3)));

        assume that

         A2: GA c= P1 and

         A3: GA c= P2;

        assume

         A4: ( IC s1) = 5;

        assume that (s1 . SBP ) > 0 and (s1 . GBP ) = 0 ;

        assume

         A5: y <= 0 ;

        assume y >= 0 ;

        assume x >= y;

        assume that

         A6: ( IC s2) = ( IC s1) and

         A7: (s2 . SBP ) = (s1 . SBP ) and (s2 . GBP ) = 0 ;

        assume that (s2 . ( DataLoc ((s1 . SBP ),2))) = x and

         A8: y2 = y;

        

         A9: (P1 /. ( IC s1)) = (P1 . ( IC s1)) by PBOOLE: 143;

        

         A10: ( Comput (P1,s1,(1 + 0 ))) = ( Following (P1,( Comput (P1,s1, 0 )))) by EXTPRO_1: 3

        .= ( Following (P1,s1)) by EXTPRO_1: 2

        .= ( Exec (i05,s1)) by A4, A9, Lm1, A2;

        

         A11: (P2 /. ( IC s2)) = (P2 . ( IC s2)) by PBOOLE: 143;

        

         A12: ( Comput (P2,s2,(1 + 0 ))) = ( Following (P2,( Comput (P2,s2, 0 )))) by EXTPRO_1: 3

        .= ( Following (P2,s2)) by EXTPRO_1: 2

        .= ( Exec (i05,s2)) by A4, A6, A11, Lm1, A3;

        

         A13: ( IC ( Comput (P1,s1,1))) = ( ICplusConst (s1,9)) by A5, A10, SCMPDS_2: 56

        .= (5 + 9) by A4, SCMPDS_6: 12;

        

         A14: ( IC ( Comput (P2,s2,1))) = ( ICplusConst (s2,9)) by A5, A7, A8, A12, SCMPDS_2: 56

        .= (5 + 9) by A4, A6, SCMPDS_6: 12;

        take n = 1;

        

         A15: (P1 /. ( IC ( Comput (P1,s1,n)))) = (P1 . ( IC ( Comput (P1,s1,n)))) by PBOOLE: 143;

        

        thus ( CurInstr (P1,( Comput (P1,s1,n)))) = (P1 . 14) by A13, A15

        .= i14 by Lm1, A2;

        thus (( Comput (P1,s1,n)) . SBP ) = (s1 . SBP ) by A10, SCMPDS_2: 56;

        

         A16: (P2 /. ( IC ( Comput (P2,s2,n)))) = (P2 . ( IC ( Comput (P2,s2,n)))) by PBOOLE: 143;

        

        thus ( CurInstr (P2,( Comput (P2,s2,n)))) = (P2 . 14) by A14, A16

        .= i14 by Lm1, A3;

        thus (( Comput (P2,s2,n)) . SBP ) = (s2 . SBP ) by A12, SCMPDS_2: 56;

        thus for j be Nat st 1 < j & j <= ((s1 . SBP ) + 1) holds (s1 . ( intpos j)) = (( Comput (P1,s1,n)) . ( intpos j)) & (s2 . ( intpos j)) = (( Comput (P2,s2,n)) . ( intpos j)) by A10, A12, SCMPDS_2: 56;

        hereby

          let k be Nat, a;

          assume that

           A17: k <= n and

           A18: (s1 . a) = (s2 . a);

          per cases by A17, NAT_1: 25;

            suppose

             A19: k = 0 ;

            

            hence ( IC ( Comput (P1,s1,k))) = ( IC s2) by A6, EXTPRO_1: 2

            .= ( IC ( Comput (P2,s2,k))) by A19, EXTPRO_1: 2;

            

            thus (( Comput (P1,s1,k)) . a) = (s1 . a) by A19, EXTPRO_1: 2

            .= (( Comput (P2,s2,k)) . a) by A18, A19, EXTPRO_1: 2;

          end;

            suppose

             A20: k = 1;

            hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A13, A14;

            

            thus (( Comput (P1,s1,k)) . a) = (s1 . a) by A10, A20, SCMPDS_2: 56

            .= (( Comput (P2,s2,k)) . a) by A12, A18, A20, SCMPDS_2: 56;

          end;

        end;

      end;

       A21:

      now

        let k be Nat;

        assume

         A22: P[k];

        thus P[(k + 1)]

        proof

          let s1,s2 be State of SCMPDS ;

          set x = (s1 . ( DataLoc ((s1 . SBP ),2))), y = (s1 . ( DataLoc ((s1 . SBP ),3)));

          assume that

           A23: GA c= P1 and

           A24: GA c= P2;

          assume

           A25: ( IC s1) = 5;

          assume that

           A26: (s1 . SBP ) > 0 and

           A27: (s1 . GBP ) = 0 ;

          assume

           A28: y <= (k + 1);

          assume

           A29: y >= 0 ;

          assume

           A30: x >= y;

          assume that

           A31: ( IC s2) = ( IC s1) and

           A32: (s2 . SBP ) = (s1 . SBP ) and

           A33: (s2 . GBP ) = 0 ;

          assume that

           A34: (s2 . ( DataLoc ((s1 . SBP ),2))) = x and

           A35: (s2 . ( DataLoc ((s1 . SBP ),3))) = y;

          reconsider y as Element of NAT by A29, INT_1: 3;

          per cases by A28, NAT_1: 8;

            suppose y <= k;

            hence ex n st ( CurInstr (P1,( Comput (P1,s1,n)))) = ( return SBP ) & (s1 . SBP ) = (( Comput (P1,s1,n)) . SBP ) & ( CurInstr (P2,( Comput (P2,s2,n)))) = ( return SBP ) & (s2 . SBP ) = (( Comput (P2,s2,n)) . SBP ) & (for j be Nat st 1 < j & j <= ((s1 . SBP ) + 1) holds (s1 . ( intpos j)) = (( Comput (P1,s1,n)) . ( intpos j)) & (s2 . ( intpos j)) = (( Comput (P2,s2,n)) . ( intpos j))) & for k be Nat, a st k <= n & (s1 . a) = (s2 . a) holds ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) & (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A22, A25, A26, A27, A30, A31, A32, A33, A34, A35, A23, A24;

          end;

            suppose

             A36: y = (k + 1);

            then

             A37: y > 0 ;

            reconsider n = (s1 . SBP ) as Element of NAT by A26, INT_1: 3;

            

             A38: n = (s1 . SBP );

            set s8 = ( Comput (P1,s1,8)), t8 = ( Comput (P2,s2,8));

            

             A39: ( IC ( Comput (P1,s1,7))) = (5 + 7) by A25, A27, A34, A37, A38, Lm6, A23;

            

             A40: s8 = ( Exec (i12,( Comput (P1,s1,7)))) by A25, A27, A34, A37, A38, Lm6, A23;

            

             A41: (( Comput (P1,s1,7)) . SBP ) = (n + 4) by A25, A27, A34, A37, Lm6, A23;

            

             A42: (( Comput (P1,s1,7)) . GBP ) = 0 by A25, A27, A34, A37, A38, Lm6, A23;

            

             A43: (( Comput (P1,s1,7)) . ( intpos (n + 7))) = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) by A25, A27, A34, A37, Lm6, A23;

            

             A44: (( Comput (P1,s1,7)) . ( intpos (n + 6))) = (s1 . ( intpos (n + 3))) by A25, A27, A34, A37, Lm6, A23;

            

             A45: ( IC ( Comput (P2,s2,7))) = (5 + 7) by A25, A31, A32, A33, A34, A35, A37, A38, Lm6, A24;

            

             A46: t8 = ( Exec (i12,( Comput (P2,s2,7)))) by A25, A31, A32, A33, A34, A35, A37, A38, Lm6, A24;

            

             A47: (( Comput (P2,s2,7)) . SBP ) = (n + 4) by A25, A31, A32, A33, A34, A35, A37, Lm6, A24;

            

             A48: (( Comput (P2,s2,7)) . GBP ) = 0 by A25, A31, A32, A33, A34, A35, A37, A38, Lm6, A24;

            

             A49: (( Comput (P2,s2,7)) . ( intpos (n + 7))) = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) by A25, A27, A31, A32, A33, A34, A35, A37, Lm6, A24;

            

             A50: (( Comput (P2,s2,7)) . ( intpos (n + 6))) = (s1 . ( intpos (n + 3))) by A25, A27, A31, A32, A33, A34, A35, A37, Lm6, A24;

            

             A51: (( Comput (P1,s1,7)) . ( intpos (n + 4))) = n by A25, A27, A34, A37, Lm6, A23;

            

             A52: (( Comput (P1,s1,7)) . ( intpos (n + 5))) = 11 by A25, A27, A34, A37, Lm6, A23;

            

             A53: (( Comput (P2,s2,7)) . ( intpos (n + 4))) = n by A25, A31, A32, A33, A34, A35, A37, Lm6, A24;

            

             A54: (( Comput (P2,s2,7)) . ( intpos (n + 5))) = 11 by A25, A31, A32, A33, A34, A35, A37, Lm6, A24;

            

             A55: ( DataLoc ((n + 4),2)) = ( intpos ((n + 4) + 2)) by Th1

            .= ( intpos (n + (4 + 2)));

            

             A56: ( DataLoc ((n + 4),3)) = ( intpos ((n + 4) + 3)) by Th1

            .= ( intpos (n + (4 + 3)));

            

             A57: ( IC s8) = ( ICplusConst (( Comput (P1,s1,7)),( - 7))) by A40, SCMPDS_2: 54

            .= 5 by A39, Th2;

            

             A58: (s8 . SBP ) = (n + 4) by A40, A41, SCMPDS_2: 54;

            

             A59: 4 <= (n + 4) by NAT_1: 11;

            

             A60: (s8 . SBP ) > 0 by A58;

            

             A61: (s8 . GBP ) = 0 by A40, A42, SCMPDS_2: 54;

            set x1 = (s8 . ( DataLoc ((s8 . SBP ),2))), y1 = (s8 . ( DataLoc ((s8 . SBP ),3)));

            

             A62: x1 = (s1 . ( intpos (n + 3))) by A40, A44, A55, A58, SCMPDS_2: 54

            .= y by Th1;

            

             A63: y1 = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) by A40, A43, A56, A58, SCMPDS_2: 54

            .= ((s1 . ( intpos (n + 2))) mod y) by Th1;

            then

             A64: y1 < y by A36, NEWTON: 65;

            then

             A65: y1 <= k by A36, INT_1: 7;

            

             A66: ( IC t8) = ( ICplusConst (( Comput (P2,s2,7)),( - 7))) by A46, SCMPDS_2: 54

            .= ( IC s8) by A45, A57, Th2;

            

             A67: (t8 . SBP ) = (s8 . SBP ) by A46, A47, A58, SCMPDS_2: 54;

            

             A68: (t8 . GBP ) = 0 by A46, A48, SCMPDS_2: 54;

            set x3 = (t8 . ( DataLoc ((s8 . SBP ),2)));

            

             A69: x3 = (s1 . ( intpos (n + 3))) by A46, A50, A55, A58, SCMPDS_2: 54

            .= x1 by A62, Th1;

            (t8 . ( DataLoc ((s8 . SBP ),3))) = ((s1 . ( intpos (n + 2))) mod (s1 . ( intpos (n + 3)))) by A46, A49, A56, A58, SCMPDS_2: 54

            .= y1 by A63, Th1;

            then

            consider m such that

             A70: ( CurInstr (P1,( Comput (P1,s8,m)))) = ( return SBP ) and

             A71: (s8 . SBP ) = (( Comput (P1,s8,m)) . SBP ) and

             A72: ( CurInstr (P2,( Comput (P2,t8,m)))) = ( return SBP ) and

             A73: (t8 . SBP ) = (( Comput (P2,t8,m)) . SBP ) and

             A74: for j be Nat st 1 < j & j <= ((s8 . SBP ) + 1) holds (s8 . ( intpos j)) = (( Comput (P1,s8,m)) . ( intpos j)) & (t8 . ( intpos j)) = (( Comput (P2,t8,m)) . ( intpos j)) and

             A75: for k be Nat, a be Int_position st k <= m & (s8 . a) = (t8 . a) holds ( IC ( Comput (P1,s8,k))) = ( IC ( Comput (P2,t8,k))) & (( Comput (P1,s8,k)) . a) = (( Comput (P2,t8,k)) . a) by A22, A57, A60, A61, A62, A63, A64, A65, A66, A67, A68, A69, A23, A24, NEWTON: 64;

            set s9 = ( Comput (P1,s1,(m + 8))), t9 = ( Comput (P2,s2,(m + 8)));

            

             A76: (s8 . SBP ) = (s9 . SBP ) by A71, EXTPRO_1: 4;

            

             A77: ( Comput (P1,s1,(m + 8))) = ( Comput (P1,( Comput (P1,s1,8)),m)) by EXTPRO_1: 4;

            

             A78: ( Comput (P1,s1,(m + (8 + 1)))) = ( Comput (P1,s1,((m + 8) + 1)))

            .= ( Following (P1,s9)) by EXTPRO_1: 3

            .= ( Exec (( return SBP ),s9)) by A70, A77;

            

             A79: 1 < (n + 4) by A59, XXREAL_0: 2;

            

             A80: (n + 4) < ((s8 . SBP ) + 1) by A58, XREAL_1: 29;

            

            then

             A81: (s8 . ( intpos (n + 4))) = (( Comput (P1,s8,m)) . ( intpos (n + 4))) by A74, A79

            .= (s9 . ( intpos (n + 4))) by EXTPRO_1: 4;

            5 <= (n + 5) by NAT_1: 11;

            then

             A82: 1 < (n + 5) by XXREAL_0: 2;

            

             A83: ( intpos (n + (4 + 1))) = ( intpos ((n + 4) + 1))

            .= ( DataLoc ((n + 4),1)) by Th1;

            

             A84: 11 = (s8 . ( intpos (n + 5))) by A40, A52, SCMPDS_2: 54

            .= (( Comput (P1,s8,m)) . ( intpos (n + 5))) by A58, A74, A82

            .= (s9 . ( DataLoc ((s9 . SBP ), RetIC ))) by A58, A76, A83, EXTPRO_1: 4, SCMPDS_I:def 14;

            

             A85: (t9 . SBP ) = (n + 4) by A58, A67, A73, EXTPRO_1: 4;

            

             A86: ( Comput (P2,s2,(m + 8))) = ( Comput (P2,( Comput (P2,s2,8)),m)) by EXTPRO_1: 4;

            

             A87: ( Comput (P2,s2,(m + (8 + 1)))) = ( Comput (P2,s2,((m + 8) + 1)))

            .= ( Following (P2,t9)) by EXTPRO_1: 3

            .= ( Exec (( return SBP ),t9)) by A72, A86;

            

             A88: (t8 . ( intpos (n + 4))) = (( Comput (P2,t8,m)) . ( intpos (n + 4))) by A74, A79, A80

            .= (t9 . ( intpos (n + 4))) by EXTPRO_1: 4;

            

             A89: 11 = (t8 . ( intpos (n + 5))) by A46, A54, SCMPDS_2: 54

            .= (( Comput (P2,t8,m)) . ( intpos (n + 5))) by A58, A74, A82

            .= (t9 . ( DataLoc ((t9 . SBP ), RetIC ))) by A83, A85, EXTPRO_1: 4, SCMPDS_I:def 14;

            

             A90: (P1 /. ( IC ( Comput (P1,s1,(m + 9))))) = (P1 . ( IC ( Comput (P1,s1,(m + 9))))) by PBOOLE: 143;

            

             A91: ( IC ( Comput (P1,s1,(m + 9)))) = ( |.(s9 . ( DataLoc ((s9 . SBP ), RetIC ))).| + 2) by A78, SCMPDS_2: 58

            .= (11 + 2) by A84, ABSVALUE: 29;

            

            then

             A92: ( CurInstr (P1,( Comput (P1,s1,(m + 9))))) = (P1 . 13) by A90

            .= i13 by Lm1, A23;

            

             A93: ( Comput (P1,s1,(m + (9 + 1)))) = ( Comput (P1,s1,((m + 9) + 1)))

            .= ( Following (P1,( Comput (P1,s1,(m + 9))))) by EXTPRO_1: 3

            .= ( Exec (i13,( Comput (P1,s1,(m + 9))))) by A92;

            

             A94: (( Comput (P1,s1,(m + 9))) . SBP ) = (s9 . ( DataLoc ((n + 4), RetSP ))) by A58, A76, A78, SCMPDS_2: 58

            .= (s9 . ( intpos ((n + 4) + 0 ))) by Th1, SCMPDS_I:def 13

            .= n by A40, A51, A81, SCMPDS_2: 54;

            

             A95: (P2 /. ( IC ( Comput (P2,s2,(m + 9))))) = (P2 . ( IC ( Comput (P2,s2,(m + 9))))) by PBOOLE: 143;

            

             A96: ( IC ( Comput (P2,s2,(m + 9)))) = ( |.(t9 . ( DataLoc ((t9 . SBP ), RetIC ))).| + 2) by A87, SCMPDS_2: 58

            .= (11 + 2) by A89, ABSVALUE: 29;

            

            then

             A97: ( CurInstr (P2,( Comput (P2,s2,(m + 9))))) = (P2 . 13) by A95

            .= i13 by Lm1, A24;

            

             A98: ( Comput (P2,s2,(m + (9 + 1)))) = ( Comput (P2,s2,((m + 9) + 1)))

            .= ( Following (P2,( Comput (P2,s2,(m + 9))))) by EXTPRO_1: 3

            .= ( Exec (i13,( Comput (P2,s2,(m + 9))))) by A97;

            

             A99: (( Comput (P2,s2,(m + 9))) . SBP ) = (t9 . ( DataLoc ((n + 4), RetSP ))) by A85, A87, SCMPDS_2: 58

            .= (t9 . ( intpos ((n + 4) + 0 ))) by Th1, SCMPDS_I:def 13

            .= n by A46, A53, A88, SCMPDS_2: 54;

            

             A100: ( IC ( Comput (P1,s1,(m + 10)))) = (( IC ( Comput (P1,s1,(m + 9)))) + 1) by A93, SCMPDS_2: 47

            .= (13 + 1) by A91;

            

             A101: ( IC ( Comput (P2,s2,(m + 10)))) = (( IC ( Comput (P2,s2,(m + 9)))) + 1) by A98, SCMPDS_2: 47

            .= (13 + 1) by A96;

            hereby

              reconsider nn = (m + 10) as Nat;

              take nn;

              

               A102: (P1 /. ( IC ( Comput (P1,s1,nn)))) = (P1 . ( IC ( Comput (P1,s1,nn)))) by PBOOLE: 143;

              

              thus ( CurInstr (P1,( Comput (P1,s1,nn)))) = (P1 . 14) by A100, A102

              .= ( return SBP ) by Lm1, A23;

              

               A103: (P2 /. ( IC ( Comput (P2,s2,nn)))) = (P2 . ( IC ( Comput (P2,s2,nn)))) by PBOOLE: 143;

              

               A104: ( DataLoc ((( Comput (P1,s1,(m + 9))) . SBP ),2)) = ( intpos (n + 2)) by A94, Th1;

              hence (( Comput (P1,s1,nn)) . SBP ) = (s1 . SBP ) by A93, A94, Lm3, SCMPDS_2: 47;

              

              thus ( CurInstr (P2,( Comput (P2,s2,nn)))) = (P2 . 14) by A101, A103

              .= ( return SBP ) by Lm1, A24;

              

               A105: ( DataLoc ((( Comput (P2,s2,(m + 9))) . SBP ),2)) = ( intpos (n + 2)) by A99, Th1;

              hence (( Comput (P2,s2,nn)) . SBP ) = (s2 . SBP ) by A32, A98, A99, Lm3, SCMPDS_2: 47;

              hereby

                let j be Nat;

                assume that

                 A106: 1 < j and

                 A107: j <= ((s1 . SBP ) + 1);

                (s1 . SBP ) <= (s8 . SBP ) by A58, NAT_1: 11;

                then ((s1 . SBP ) + 1) <= ((s8 . SBP ) + 1) by XREAL_1: 6;

                then

                 A108: j <= ((s8 . SBP ) + 1) by A107, XXREAL_0: 2;

                

                 A109: (( Comput (P1,s1,(m + 9))) . ( intpos j)) = (s9 . ( intpos j)) by A78, A106, AMI_3: 10, SCMPDS_2: 58

                .= (( Comput (P1,s8,m)) . ( intpos j)) by EXTPRO_1: 4

                .= (s8 . ( intpos j)) by A74, A106, A108;

                

                 A110: (n + 1) < (n + 2) by XREAL_1: 6;

                (( Comput (P1,s1,7)) . ( intpos j)) = (s1 . ( intpos j)) by A25, A27, A36, A38, A106, A107, Lm5, A23;

                

                hence (s1 . ( intpos j)) = (s8 . ( intpos j)) by A40, SCMPDS_2: 54

                .= (( Comput (P1,s1,nn)) . ( intpos j)) by A93, A104, A107, A109, A110, AMI_3: 10, SCMPDS_2: 47;

                

                 A111: (( Comput (P2,s2,(m + 9))) . ( intpos j)) = (t9 . ( intpos j)) by A87, A106, AMI_3: 10, SCMPDS_2: 58

                .= (( Comput (P2,t8,m)) . ( intpos j)) by EXTPRO_1: 4

                .= (t8 . ( intpos j)) by A74, A106, A108;

                j <= (n + 1) by A107;

                then (( Comput (P2,s2,7)) . ( intpos j)) = (s2 . ( intpos j)) by A25, A31, A32, A33, A35, A36, A106, Lm5, A24;

                

                hence (s2 . ( intpos j)) = (t8 . ( intpos j)) by A46, SCMPDS_2: 54

                .= (( Comput (P2,s2,nn)) . ( intpos j)) by A98, A105, A107, A110, A111, AMI_3: 10, SCMPDS_2: 47;

              end;

              hereby

                let j be Nat, a;

                assume that

                 A112: j <= nn and

                 A113: (s1 . a) = (s2 . a);

                nn = ((m + 9) + 1);

                then

                 A114: j <= (m + 9) or j = nn by A112, NAT_1: 8;

                

                 A115: (m + (8 + 1)) = ((m + 8) + 1);

                 A116:

                now

                  assume

                   A117: j <= (m + 8);

                  per cases ;

                    suppose j < (7 + 1);

                    hence j <= 7 or j >= 8 & j <= (m + 8) by NAT_1: 13;

                  end;

                    suppose j >= 8;

                    hence j <= 7 or j >= 8 & j <= (m + 8) by A117;

                  end;

                end;

                

                 A118: (s8 . a) = (( Comput (P1,s1,7)) . a) by A40, SCMPDS_2: 54

                .= (( Comput (P2,s2,7)) . a) by A25, A27, A31, A32, A33, A23, A24, A34, A35, A37, A38, A113, Lm7

                .= (t8 . a) by A46, SCMPDS_2: 54;

                 A119:

                now

                  let b;

                  assume

                   A120: (s8 . b) = (t8 . b);

                  per cases ;

                    suppose b = SBP ;

                    hence (( Comput (P1,s1,(m + 9))) . b) = (( Comput (P2,s2,(m + 9))) . b) by A94, A99;

                  end;

                    suppose

                     A121: b <> SBP ;

                    

                    hence (( Comput (P1,s1,(m + 9))) . b) = (s9 . b) by A78, SCMPDS_2: 58

                    .= (( Comput (P1,s8,m)) . b) by EXTPRO_1: 4

                    .= (( Comput (P2,t8,m)) . b) by A75, A120

                    .= (t9 . b) by EXTPRO_1: 4

                    .= (( Comput (P2,s2,(m + 9))) . b) by A87, A121, SCMPDS_2: 58;

                  end;

                end;

                

                 A122: (s8 . ( DataLoc ((( Comput (P1,s1,(m + 9))) . SBP ),6))) = x1 by A55, A58, A94, Th1

                .= (t8 . ( DataLoc ((( Comput (P1,s1,(m + 9))) . SBP ),6))) by A55, A58, A69, A94, Th1;

                 A123:

                now

                  per cases ;

                    suppose

                     A124: a <> ( DataLoc ((( Comput (P2,s2,(m + 9))) . SBP ),2));

                    

                    hence (( Comput (P1,s1,nn)) . a) = (( Comput (P1,s1,(m + 9))) . a) by A93, A94, A99, SCMPDS_2: 47

                    .= (( Comput (P2,s2,(m + 9))) . a) by A118, A119

                    .= (( Comput (P2,s2,nn)) . a) by A98, A124, SCMPDS_2: 47;

                  end;

                    suppose

                     A125: a = ( DataLoc ((( Comput (P2,s2,(m + 9))) . SBP ),2));

                    

                    hence (( Comput (P1,s1,nn)) . a) = (( Comput (P1,s1,(m + 9))) . ( DataLoc ((( Comput (P1,s1,(m + 9))) . SBP ),6))) by A93, A94, A99, SCMPDS_2: 47

                    .= (( Comput (P2,s2,(m + 9))) . ( DataLoc ((( Comput (P2,s2,(m + 9))) . SBP ),6))) by A94, A99, A119, A122

                    .= (( Comput (P2,s2,nn)) . a) by A98, A125, SCMPDS_2: 47;

                  end;

                end;

                per cases by A114, A115, A116, NAT_1: 8;

                  suppose j <= 7;

                  hence ( IC ( Comput (P1,s1,j))) = ( IC ( Comput (P2,s2,j))) & (( Comput (P1,s1,j)) . a) = (( Comput (P2,s2,j)) . a) by A25, A27, A31, A32, A33, A34, A35, A37, A38, A113, Lm7, A23, A24;

                end;

                  suppose

                   A126: j >= 8 & j <= (m + 8);

                  then

                  consider j1 be Nat such that

                   A127: j = (8 + j1) by NAT_1: 10;

                  reconsider j1 as Nat;

                  

                   A128: j1 <= m by A126, A127, XREAL_1: 6;

                  

                  thus ( IC ( Comput (P1,s1,j))) = ( IC ( Comput (P1,s8,j1))) by A127, EXTPRO_1: 4

                  .= ( IC ( Comput (P2,t8,j1))) by A75, A118, A128

                  .= ( IC ( Comput (P2,s2,j))) by A127, EXTPRO_1: 4;

                  

                  thus (( Comput (P1,s1,j)) . a) = (( Comput (P1,s8,j1)) . a) by A127, EXTPRO_1: 4

                  .= (( Comput (P2,t8,j1)) . a) by A75, A118, A128

                  .= (( Comput (P2,s2,j)) . a) by A127, EXTPRO_1: 4;

                end;

                  suppose

                   A129: j = (m + 9);

                  hence ( IC ( Comput (P1,s1,j))) = ( IC ( Comput (P2,s2,j))) by A91, A96;

                  thus (( Comput (P1,s1,j)) . a) = (( Comput (P2,s2,j)) . a) by A118, A119, A129;

                end;

                  suppose

                   A130: j = nn;

                  hence ( IC ( Comput (P1,s1,j))) = ( IC ( Comput (P2,s2,j))) by A100, A101;

                  thus (( Comput (P1,s1,j)) . a) = (( Comput (P2,s2,j)) . a) by A123, A130;

                end;

              end;

            end;

          end;

        end;

      end;

      

       A131: for n holds P[n] from NAT_1:sch 2( A1, A21);

      let s1,s2 be State of SCMPDS ;

      assume that

       A132: GA c= P1 and

       A133: GA c= P2 and

       A134: ( IC s1) = 5 and

       A135: (s1 . SBP ) > 0 and

       A136: (s1 . GBP ) = 0 and

       A137: (s1 . ( DataLoc ((s1 . SBP ),3))) >= 0 and

       A138: (s1 . ( DataLoc ((s1 . SBP ),2))) >= (s1 . ( DataLoc ((s1 . SBP ),3))) and

       A139: ( IC s2) = ( IC s1) and

       A140: (s2 . SBP ) = (s1 . SBP ) and

       A141: (s2 . GBP ) = 0 and

       A142: (s2 . ( DataLoc ((s1 . SBP ),2))) = (s1 . ( DataLoc ((s1 . SBP ),2))) and

       A143: (s2 . ( DataLoc ((s1 . SBP ),3))) = (s1 . ( DataLoc ((s1 . SBP ),3)));

      reconsider m = (s1 . ( DataLoc ((s1 . SBP ),3))) as Element of NAT by A137, INT_1: 3;

       P[m] by A131;

      hence thesis by A134, A135, A136, A138, A139, A140, A141, A142, A143, A132, A133;

    end;

    

     Lm9: for s1,s2 be State of SCMPDS , a be Int_position, k be Nat st ( Start-At ( 0 , SCMPDS )) c= s1 & ( Start-At ( 0 , SCMPDS )) c= s2 & GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & (s1 . a) = (s2 . a) & k <= 4 holds ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) & (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a)

    proof

      let s1,s2 be State of SCMPDS , a be Int_position, k be Nat;

      set GA = GCD-Algorithm ;

      assume that

       A1: ( Start-At ( 0 , SCMPDS )) c= s1 and

       A2: ( Start-At ( 0 , SCMPDS )) c= s2 and

       A3: GA c= P1 and

       A4: GA c= P2;

      assume that

       A5: (s1 . a) = (s2 . a) and

       A6: k <= 4;

      

       A7: ( IC s1) = 0 by A1, MEMSTR_0: 39;

      

       A8: (P1 /. ( IC s1)) = (P1 . ( IC s1)) by PBOOLE: 143;

      

       A9: ( Comput (P1,s1,( 0 + 1))) = ( Following (P1,( Comput (P1,s1, 0 )))) by EXTPRO_1: 3

      .= ( Following (P1,s1)) by EXTPRO_1: 2

      .= ( Exec (i00,s1)) by A7, Lm1, A8, A3;

      

       A10: ( IC s2) = 0 by A2, MEMSTR_0: 39;

      

       A11: (P2 /. ( IC s2)) = (P2 . ( IC s2)) by PBOOLE: 143;

      

       A12: ( Comput (P2,s2,( 0 + 1))) = ( Following (P2,( Comput (P2,s2, 0 )))) by EXTPRO_1: 3

      .= ( Following (P2,s2)) by EXTPRO_1: 2

      .= ( Exec (i00,s2)) by A10, Lm1, A11, A4;

      

       A13: (P1 /. ( IC ( Comput (P1,s1,1)))) = (P1 . ( IC ( Comput (P1,s1,1)))) by PBOOLE: 143;

      

       A14: ( IC ( Comput (P1,s1,1))) = (( IC s1) + 1) by A9, SCMPDS_2: 45

      .= ( 0 + 1) by A7;

      

      then

       A15: ( CurInstr (P1,( Comput (P1,s1,1)))) = (P1 . 1) by A13

      .= i01 by Lm1, A3;

      

       A16: ( Comput (P1,s1,(1 + 1))) = ( Following (P1,( Comput (P1,s1,1)))) by EXTPRO_1: 3

      .= ( Exec (i01,( Comput (P1,s1,1)))) by A15;

      

       A17: (P2 /. ( IC ( Comput (P2,s2,1)))) = (P2 . ( IC ( Comput (P2,s2,1)))) by PBOOLE: 143;

      

       A18: ( IC ( Comput (P2,s2,1))) = (( IC s2) + 1) by A12, SCMPDS_2: 45

      .= ( 0 + 1) by A10;

      

      then

       A19: ( CurInstr (P2,( Comput (P2,s2,1)))) = (P2 . 1) by A17

      .= i01 by Lm1, A4;

      

       A20: ( Comput (P2,s2,(1 + 1))) = ( Following (P2,( Comput (P2,s2,1)))) by EXTPRO_1: 3

      .= ( Exec (i01,( Comput (P2,s2,1)))) by A19;

      

       A21: (P1 /. ( IC ( Comput (P1,s1,2)))) = (P1 . ( IC ( Comput (P1,s1,2)))) by PBOOLE: 143;

      

       A22: ( IC ( Comput (P1,s1,2))) = (( IC ( Comput (P1,s1,1))) + 1) by A16, SCMPDS_2: 45

      .= (1 + 1) by A14;

      

      then

       A23: ( CurInstr (P1,( Comput (P1,s1,2)))) = (P1 . 2) by A21

      .= i02 by Lm1, A3;

      

       A24: ( Comput (P1,s1,(2 + 1))) = ( Following (P1,( Comput (P1,s1,2)))) by EXTPRO_1: 3

      .= ( Exec (i02,( Comput (P1,s1,2)))) by A23;

      

       A25: (( Comput (P1,s1,2)) . SBP ) = 7 by A16, SCMPDS_2: 45;

      

       A26: (P2 /. ( IC ( Comput (P2,s2,2)))) = (P2 . ( IC ( Comput (P2,s2,2)))) by PBOOLE: 143;

      

       A27: ( IC ( Comput (P2,s2,2))) = (( IC ( Comput (P2,s2,1))) + 1) by A20, SCMPDS_2: 45

      .= (1 + 1) by A18;

      

      then

       A28: ( CurInstr (P2,( Comput (P2,s2,2)))) = (P2 . 2) by A26

      .= i02 by Lm1, A4;

      

       A29: ( Comput (P2,s2,(2 + 1))) = ( Following (P2,( Comput (P2,s2,2)))) by EXTPRO_1: 3

      .= ( Exec (i02,( Comput (P2,s2,2)))) by A28;

      

       A30: (( Comput (P2,s2,2)) . SBP ) = 7 by A20, SCMPDS_2: 45;

      

       A31: (P1 /. ( IC ( Comput (P1,s1,3)))) = (P1 . ( IC ( Comput (P1,s1,3)))) by PBOOLE: 143;

      

       A32: ( IC ( Comput (P1,s1,3))) = (( IC ( Comput (P1,s1,2))) + 1) by A24, SCMPDS_2: 59

      .= (2 + 1) by A22;

      

      then

       A33: ( CurInstr (P1,( Comput (P1,s1,3)))) = (P1 . 3) by A31

      .= i03 by Lm1, A3;

      

       A34: ( Comput (P1,s1,(3 + 1))) = ( Following (P1,( Comput (P1,s1,3)))) by EXTPRO_1: 3

      .= ( Exec (i03,( Comput (P1,s1,3)))) by A33;

      

       A35: (P2 /. ( IC ( Comput (P2,s2,3)))) = (P2 . ( IC ( Comput (P2,s2,3)))) by PBOOLE: 143;

      

       A36: ( IC ( Comput (P2,s2,3))) = (( IC ( Comput (P2,s2,2))) + 1) by A29, SCMPDS_2: 59

      .= (2 + 1) by A27;

      

      then

       A37: ( CurInstr (P2,( Comput (P2,s2,3)))) = (P2 . 3) by A35

      .= i03 by Lm1, A4;

      

       A38: ( Comput (P2,s2,(3 + 1))) = ( Following (P2,( Comput (P2,s2,3)))) by EXTPRO_1: 3

      .= ( Exec (i03,( Comput (P2,s2,3)))) by A37;

       A39:

      now

        let b;

        assume

         A40: (s1 . b) = (s2 . b);

        per cases ;

          suppose

           A41: b = GBP ;

          

          hence (( Comput (P1,s1,1)) . b) = 0 by A9, SCMPDS_2: 45

          .= (( Comput (P2,s2,1)) . b) by A12, A41, SCMPDS_2: 45;

        end;

          suppose

           A42: b <> GBP ;

          

          hence (( Comput (P1,s1,1)) . b) = (s1 . b) by A9, SCMPDS_2: 45

          .= (( Comput (P2,s2,1)) . b) by A12, A40, A42, SCMPDS_2: 45;

        end;

      end;

       A43:

      now

        let b;

        assume

         A44: (s1 . b) = (s2 . b);

        per cases ;

          suppose

           A45: b = SBP ;

          

          hence (( Comput (P1,s1,2)) . b) = 7 by A16, SCMPDS_2: 45

          .= (( Comput (P2,s2,2)) . b) by A20, A45, SCMPDS_2: 45;

        end;

          suppose

           A46: b <> SBP ;

          

          hence (( Comput (P1,s1,2)) . b) = (( Comput (P1,s1,1)) . b) by A16, SCMPDS_2: 45

          .= (( Comput (P2,s2,1)) . b) by A39, A44

          .= (( Comput (P2,s2,2)) . b) by A20, A46, SCMPDS_2: 45;

        end;

      end;

       A47:

      now

        let b;

        assume

         A48: (s1 . b) = (s2 . b);

        per cases ;

          suppose

           A49: b = ( DataLoc ((( Comput (P1,s1,2)) . SBP ), RetIC ));

          

          hence (( Comput (P1,s1,3)) . b) = ( IC ( Comput (P1,s1,2))) by A24, SCMPDS_2: 59

          .= (( Comput (P2,s2,3)) . b) by A22, A25, A27, A29, A30, A49, SCMPDS_2: 59;

        end;

          suppose

           A50: b <> ( DataLoc ((( Comput (P1,s1,2)) . SBP ), RetIC ));

          

          hence (( Comput (P1,s1,3)) . b) = (( Comput (P1,s1,2)) . b) by A24, SCMPDS_2: 59

          .= (( Comput (P2,s2,2)) . b) by A43, A48

          .= (( Comput (P2,s2,3)) . b) by A25, A29, A30, A50, SCMPDS_2: 59;

        end;

      end;

      k = 0 or ... or k = 4 by A6;

      per cases ;

        suppose

         A51: k = 0 ;

        

        hence ( IC ( Comput (P1,s1,k))) = ( IC s1) by EXTPRO_1: 2

        .= ( IC ( Comput (P2,s2,k))) by A7, A10, A51, EXTPRO_1: 2;

        

        thus (( Comput (P1,s1,k)) . a) = (s1 . a) by A51, EXTPRO_1: 2

        .= (( Comput (P2,s2,k)) . a) by A5, A51, EXTPRO_1: 2;

      end;

        suppose

         A52: k = 1;

        hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A14, A18;

        thus thesis by A5, A39, A52;

      end;

        suppose

         A53: k = 2;

        hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A22, A27;

        thus thesis by A5, A43, A53;

      end;

        suppose

         A54: k = 3;

        hence ( IC ( Comput (P1,s1,k))) = ( IC ( Comput (P2,s2,k))) by A32, A36;

        thus thesis by A5, A47, A54;

      end;

        suppose

         A55: k = 4;

        

        hence ( IC ( Comput (P1,s1,k))) = ( ICplusConst (( Comput (P1,s1,3)),2)) by A34, SCMPDS_2: 54

        .= (3 + 2) by A32, SCMPDS_6: 12

        .= ( ICplusConst (( Comput (P2,s2,3)),2)) by A36, SCMPDS_6: 12

        .= ( IC ( Comput (P2,s2,k))) by A38, A55, SCMPDS_2: 54;

        

        thus (( Comput (P1,s1,k)) . a) = (( Comput (P1,s1,3)) . a) by A34, A55, SCMPDS_2: 54

        .= (( Comput (P2,s2,3)) . a) by A5, A47

        .= (( Comput (P2,s2,k)) . a) by A38, A55, SCMPDS_2: 54;

      end;

    end;

    begin

    theorem :: SCMP_GCD:15

    for p be FinPartState of SCMPDS , x,y be Integer st y >= 0 & x >= y & p = ((( intpos 9),( intpos 10)) --> (x,y)) holds ( Initialize p) is GCD-Algorithm -autonomic

    proof

      let p be FinPartState of SCMPDS , x,y be Integer;

      set GA = GCD-Algorithm , a = ( intpos 9), b = ( intpos 10);

      assume that

       A1: y >= 0 and

       A2: x >= y and

       A3: p = ((a,b) --> (x,y));

      

       A4: ( dom p) = {a, b} by A3, FUNCT_4: 62;

      a in SCM-Data-Loc & b in SCM-Data-Loc by AMI_2:def 16;

      then a in ( Data-Locations SCMPDS ) & b in ( Data-Locations SCMPDS ) by SCMPDS_2: 84;

      then

       A5: ( dom p) c= ( Data-Locations SCMPDS ) by A4, ZFMISC_1: 32;

       not ( IC SCMPDS ) in ( Data-Locations SCMPDS ) by STRUCT_0: 3;

      then {( IC SCMPDS )} misses ( Data-Locations SCMPDS ) by ZFMISC_1: 50;

      then ( Data-Locations SCMPDS ) misses {( IC SCMPDS )};

      then ( dom p) misses {( IC SCMPDS )} by A5, XBOOLE_1: 63;

      then

       A6: p is data-only;

      a in ( dom p) by A4, TARSKI:def 2;

      then

       A7: a in ( dom p);

      b in ( dom p) by A4, TARSKI:def 2;

      then

       A8: b in ( dom p);

      

       A9: ( dom ( Start-At ( 0 , SCMPDS ))) = {( IC SCMPDS )} by FUNCOP_1: 13;

      

       A10: for t be State of SCMPDS st ( Initialize p) c= t holds (t . a) = x & (t . b) = y

      proof

        let t be State of SCMPDS such that

         A11: ( Initialize p) c= t;

        p = ( DataPart p) by A6, MEMSTR_0: 7;

        then ( dom p) misses ( dom ( Start-At ( 0 , SCMPDS ))) by A9, MEMSTR_0: 4;

        then p c= ( Initialize p) by FUNCT_4: 32;

        then p c= ( Initialize p);

        then

         A12: p c= t by A11, XBOOLE_1: 1;

        

        hence (t . a) = (p . a) by A7, GRFUNC_1: 2

        .= (p . a)

        .= x by A3, AMI_3: 10, FUNCT_4: 63;

        

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

        .= (p . b)

        .= y by A3, FUNCT_4: 63;

      end;

      let P1,P2 be Instruction-Sequence of SCMPDS such that

       A13: GA c= P1 & GA c= P2;

      let s1,s2 be State of SCMPDS such that

       A14: ( Initialize p) c= s1 and

       A15: ( Initialize p) c= s2;

      ( Initialize p) c= s1 by A14;

      then

       A16: ( Start-At ( 0 , SCMPDS )) c= s1 by MEMSTR_0: 50;

      then

       A17: s1 is 0 -started by MEMSTR_0: 29;

      

       A18: GA c= P1 by A13;

      ( Initialize p) c= s2 by A15;

      then

       A19: ( Start-At ( 0 , SCMPDS )) c= s2 by MEMSTR_0: 50;

      then

       A20: s2 is 0 -started by MEMSTR_0: 29;

      

       A21: GA c= P2 by A13;

      

       A22: (s1 . a) = x by A10, A14;

      

       A23: (s1 . b) = y by A10, A14;

      

       A24: (s2 . a) = x by A10, A15;

      

       A25: (s2 . b) = y by A10, A15;

      set s4 = ( Comput (P1,s1,4)), t4 = ( Comput (P2,s2,4));

      

       A26: ( IC s4) = 5 by Th11, A18, A17;

      

       A27: (s4 . GBP ) = 0 by Th11, A18, A17;

      

       A28: (s4 . SBP ) = 7 by Th11, A18, A17;

      

       A29: (s4 . ( intpos (7 + RetIC ))) = 2 by Th11, A18, A17;

      

       A30: (s4 . ( intpos 9)) = (s1 . ( intpos 9)) by Th11, A18, A17;

      

       A31: (s4 . ( intpos 10)) = (s1 . ( intpos 10)) by Th11, A18, A17;

      

       A32: (s4 . ( DataLoc ((s4 . SBP ),3))) = (s4 . ( intpos (7 + 3))) by A28, Th1

      .= y by A10, A14, A31;

      

       A33: ( DataLoc ((s4 . SBP ),2)) = ( intpos (7 + 2)) by A28, Th1;

      

       A34: ( IC t4) = 5 by Th11, A21, A20;

      

       A35: (t4 . GBP ) = 0 by Th11, A21, A20;

      

       A36: (t4 . SBP ) = 7 by Th11, A21, A20;

      

       A37: (t4 . ( intpos (7 + RetIC ))) = 2 by Th11, A21, A20;

      

       A38: (t4 . ( intpos 9)) = (s2 . ( intpos 9)) by Th11, A21, A20;

      

       A39: (t4 . ( intpos 10)) = (s2 . ( intpos 10)) by Th11, A21, A20;

      (t4 . ( DataLoc ((t4 . SBP ),3))) = (t4 . ( intpos (7 + 3))) by A36, Th1

      .= (s4 . ( DataLoc ((s4 . SBP ),3))) by A10, A15, A32, A39;

      then

      consider n such that

       A40: ( CurInstr (P1,( Comput (P1,s4,n)))) = ( return SBP ) and

       A41: (s4 . SBP ) = (( Comput (P1,s4,n)) . SBP ) and

       A42: ( CurInstr (P2,( Comput (P2,t4,n)))) = ( return SBP ) and

       A43: (t4 . SBP ) = (( Comput (P2,t4,n)) . SBP ) and

       A44: for j be Nat st 1 < j & j <= ((s4 . SBP ) + 1) holds (s4 . ( intpos j)) = (( Comput (P1,s4,n)) . ( intpos j)) & (t4 . ( intpos j)) = (( Comput (P2,t4,n)) . ( intpos j)) and

       A45: for k be Nat, c be Int_position st k <= n & (s4 . c) = (t4 . c) holds ( IC ( Comput (P1,s4,k))) = ( IC ( Comput (P2,t4,k))) & (( Comput (P1,s4,k)) . c) = (( Comput (P2,t4,k)) . c) by A1, A2, A10, A15, A22, A26, A27, A28, A30, A32, A33, A34, A35, A36, A38, Lm8, A18, A21;

      

       A46: (( Comput (P1,s4,n)) . ( DataLoc ((( Comput (P1,s4,n)) . SBP ), RetIC ))) = (( Comput (P1,s4,n)) . ( intpos (7 + 1))) by A28, A41, Th1, SCMPDS_I:def 14

      .= 2 by A28, A29, A44, SCMPDS_I:def 14;

      

       A47: (( Comput (P2,t4,n)) . ( DataLoc ((( Comput (P2,t4,n)) . SBP ), RetIC ))) = (( Comput (P2,t4,n)) . ( intpos (7 + 1))) by A36, A43, Th1, SCMPDS_I:def 14

      .= 2 by A28, A37, A44, SCMPDS_I:def 14;

      

       A48: (P1 /. ( IC ( Comput (P1,s4,(n + 1))))) = (P1 . ( IC ( Comput (P1,s4,(n + 1))))) by PBOOLE: 143;

      

       A49: ( Comput (P1,s4,(n + 1))) = ( Following (P1,( Comput (P1,s4,n)))) by EXTPRO_1: 3

      .= ( Exec (i14,( Comput (P1,s4,n)))) by A40;

      

      then

       A50: ( IC ( Comput (P1,s4,(n + 1)))) = ( |.(( Comput (P1,s4,n)) . ( DataLoc ((( Comput (P1,s4,n)) . SBP ), RetIC ))).| + 2) by SCMPDS_2: 58

      .= (2 + 2) by A46, ABSVALUE: 29;

      

      then

       A51: ( CurInstr (P1,( Comput (P1,s4,(n + 1))))) = (P1 . 4) by A48

      .= (P1 . 4)

      .= i04 by Lm1, A18;

      

       A52: (P2 /. ( IC ( Comput (P2,t4,(n + 1))))) = (P2 . ( IC ( Comput (P2,t4,(n + 1))))) by PBOOLE: 143;

      

       A53: ( Comput (P2,t4,(n + 1))) = ( Following (P2,( Comput (P2,t4,n)))) by EXTPRO_1: 3

      .= ( Exec (i14,( Comput (P2,t4,n)))) by A42;

      

      then

       A54: ( IC ( Comput (P2,t4,(n + 1)))) = ( |.(( Comput (P2,t4,n)) . ( DataLoc ((( Comput (P2,t4,n)) . SBP ), RetIC ))).| + 2) by SCMPDS_2: 58

      .= (2 + 2) by A47, ABSVALUE: 29;

      

      then

       A55: ( CurInstr (P2,( Comput (P2,t4,(n + 1))))) = (P2 . 4) by A52

      .= (P2 . 4)

      .= i04 by Lm1, A21;

      

       A56: (s4 . a) = (t4 . a) by A19, A22, A24, Lm9, A18, A16, A21;

      

       A57: (s4 . b) = (t4 . b) by A19, A23, A25, Lm9, A18, A16, A21;

      

       A58: (( Comput (P1,s4,(n + 1))) . a) = (( Comput (P1,s4,n)) . a) by A49, AMI_3: 10, SCMPDS_2: 58

      .= (( Comput (P2,t4,n)) . a) by A45, A56

      .= (( Comput (P2,t4,(n + 1))) . a) by A53, AMI_3: 10, SCMPDS_2: 58;

      

       A59: (( Comput (P1,s4,(n + 1))) . b) = (( Comput (P1,s4,n)) . b) by A49, AMI_3: 10, SCMPDS_2: 58

      .= (( Comput (P2,t4,n)) . b) by A45, A57

      .= (( Comput (P2,t4,(n + 1))) . b) by A53, AMI_3: 10, SCMPDS_2: 58;

       A60:

      now

        let j be Nat;

        

         A61: j < ((n + 4) + 1) or j >= (n + 5);

         A62:

        now

          assume

           A63: j <= (n + 4);

          

           A64: j < (3 + 1) or j >= 4;

          per cases by A64, NAT_1: 13;

            case j <= 3;

            hence j <= 3;

          end;

            case j >= 4;

            hence j >= 4 & j <= (n + 4) by A63;

          end;

        end;

        per cases by A61, A62, NAT_1: 13;

          suppose j <= 3;

          then

           A65: j <= 4 by XXREAL_0: 2;

          hence ( IC ( Comput (P1,s1,j))) = ( IC ( Comput (P2,s2,j))) by A19, A22, A24, Lm9, A18, A16, A21;

          thus (( Comput (P1,s1,j)) . a) = (( Comput (P2,s2,j)) . a) by A19, A22, A24, A65, Lm9, A18, A16, A21;

          thus (( Comput (P1,s1,j)) . b) = (( Comput (P2,s2,j)) . b) by A19, A23, A25, A65, Lm9, A18, A16, A21;

        end;

          suppose

           A66: j >= 4 & j <= (n + 4);

          then

          consider j1 be Nat such that

           A67: j = (4 + j1) by NAT_1: 10;

          reconsider j1 as Nat;

          

           A68: j1 <= n by A66, A67, XREAL_1: 6;

          

          thus ( IC ( Comput (P1,s1,j))) = ( IC ( Comput (P1,s4,j1))) by A67, EXTPRO_1: 4

          .= ( IC ( Comput (P2,t4,j1))) by A45, A56, A68

          .= ( IC ( Comput (P2,s2,j))) by A67, EXTPRO_1: 4;

          

          thus (( Comput (P1,s1,j)) . a) = (( Comput (P1,s4,j1)) . a) by A67, EXTPRO_1: 4

          .= (( Comput (P2,t4,j1)) . a) by A45, A56, A68

          .= (( Comput (P2,s2,j)) . a) by A67, EXTPRO_1: 4;

          

          thus (( Comput (P1,s1,j)) . b) = (( Comput (P1,s4,j1)) . b) by A67, EXTPRO_1: 4

          .= (( Comput (P2,t4,j1)) . b) by A45, A57, A68

          .= (( Comput (P2,s2,j)) . b) by A67, EXTPRO_1: 4;

        end;

          suppose j >= (n + 5);

          then

          consider j1 be Nat such that

           A69: j = ((n + (1 + 4)) + j1) by NAT_1: 10;

          reconsider j1 as Nat;

          

           A70: j = (((n + 1) + j1) + 4) by A69;

          

          hence ( IC ( Comput (P1,s1,j))) = ( IC ( Comput (P1,s4,((n + 1) + j1)))) by EXTPRO_1: 4

          .= ( IC ( Comput (P2,t4,(n + 1)))) by A50, A51, A54, EXTPRO_1: 5, NAT_1: 11

          .= ( IC ( Comput (P2,t4,((n + 1) + j1)))) by A55, EXTPRO_1: 5, NAT_1: 11

          .= ( IC ( Comput (P2,s2,j))) by A70, EXTPRO_1: 4;

          

          thus (( Comput (P1,s1,j)) . a) = (( Comput (P1,s4,((n + 1) + j1))) . a) by A70, EXTPRO_1: 4

          .= (( Comput (P2,t4,(n + 1))) . a) by A51, A58, EXTPRO_1: 5, NAT_1: 11

          .= (( Comput (P2,t4,((n + 1) + j1))) . a) by A55, EXTPRO_1: 5, NAT_1: 11

          .= (( Comput (P2,s2,j)) . a) by A70, EXTPRO_1: 4;

          

          thus (( Comput (P1,s1,j)) . b) = (( Comput (P1,s4,((n + 1) + j1))) . b) by A70, EXTPRO_1: 4

          .= (( Comput (P2,t4,(n + 1))) . b) by A51, A59, EXTPRO_1: 5, NAT_1: 11

          .= (( Comput (P2,t4,((n + 1) + j1))) . b) by A55, EXTPRO_1: 5, NAT_1: 11

          .= (( Comput (P2,s2,j)) . b) by A70, EXTPRO_1: 4;

        end;

      end;

      set A = {( IC SCMPDS ), a, b};

      

       A71: ( IC SCMPDS ) in ( dom ( Initialize p)) by MEMSTR_0: 48;

      ( dom ( DataPart ( Initialize p))) = ( dom ( DataPart p)) by MEMSTR_0: 45

      .= ( dom ( DataPart p))

      .= {a, b} by A6, A4, MEMSTR_0: 7;

      

      then

       A72: ( dom ( Initialize p)) = ( {( IC SCMPDS )} \/ {a, b}) by A71, MEMSTR_0: 24

      .= A by ENUMSET1: 2;

      let k be Nat;

      

       A73: (( Comput (P1,s1,k)) . ( IC SCMPDS )) = ( IC ( Comput (P1,s1,k)))

      .= ( IC ( Comput (P2,s2,k))) by A60

      .= (( Comput (P2,s2,k)) . ( IC SCMPDS ));

      

       A74: (( Comput (P1,s1,k)) . a) = (( Comput (P2,s2,k)) . a) by A60;

      

       A75: (( Comput (P1,s1,k)) . b) = (( Comput (P2,s2,k)) . b) by A60;

      ( dom ( Comput (P1,s1,k))) = the carrier of SCMPDS by PARTFUN1:def 2

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

      then (( Comput (P1,s1,k)) | A) = (( Comput (P2,s2,k)) | A) by A73, A74, A75, GRFUNC_1: 31;

      hence thesis by A72;

    end;