scmpds_3.miz



    begin

    reserve j,k,m,n for Nat,

a,b for Int_position,

k1,k2 for Integer;

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

    theorem :: SCMPDS_3:1

    for k1 be Integer, s1,s2 be State of SCMPDS st ( IC s1) = ( IC s2) holds ( ICplusConst (s1,k1)) = ( ICplusConst (s2,k1))

    proof

      let k1 be Integer, s1,s2 be State of SCMPDS ;

      

       A1: ex i be Element of NAT st i = ( IC s1) & ( ICplusConst (s1,k1)) = |.(i + k1).| by SCMPDS_2:def 18;

      assume ( IC s1) = ( IC s2);

      hence thesis by A1, SCMPDS_2:def 18;

    end;

    theorem :: SCMPDS_3:2

    for k1 be Integer, a be Int_position, s1,s2 be State of SCMPDS st ( DataPart s1) = ( DataPart s2) holds (s1 . ( DataLoc ((s1 . a),k1))) = (s2 . ( DataLoc ((s2 . a),k1)))

    proof

      let k1 be Integer, a be Int_position, s1,s2 be State of SCMPDS ;

      assume

       A1: ( DataPart s1) = ( DataPart s2);

      

       A2: a in SCM-Data-Loc by AMI_2:def 16;

      

      then

       A3: (s1 . a) = (( DataPart s1) . a) by FUNCT_1: 49, SCMPDS_2: 84

      .= (s2 . a) by A1, A2, FUNCT_1: 49, SCMPDS_2: 84;

      

       A4: ( DataLoc ((s1 . a),k1)) in SCM-Data-Loc by AMI_2:def 16;

      

      hence (s1 . ( DataLoc ((s1 . a),k1))) = (( DataPart s1) . ( DataLoc ((s1 . a),k1))) by FUNCT_1: 49, SCMPDS_2: 84

      .= (s2 . ( DataLoc ((s2 . a),k1))) by A1, A4, A3, FUNCT_1: 49, SCMPDS_2: 84;

    end;

    theorem :: SCMPDS_3:3

    for a be Int_position, s1,s2 be State of SCMPDS st ( DataPart s1) = ( DataPart s2) holds (s1 . a) = (s2 . a)

    proof

      let a be Int_position, s1,s2 be State of SCMPDS ;

      assume

       A1: ( DataPart s1) = ( DataPart s2);

      

       A2: a in SCM-Data-Loc by AMI_2:def 16;

      

      hence (s1 . a) = (( DataPart s1) . a) by FUNCT_1: 49, SCMPDS_2: 84

      .= (s2 . a) by A1, A2, FUNCT_1: 49, SCMPDS_2: 84;

    end;

    theorem :: SCMPDS_3:4

     not ( IC SCMPDS ) in SCM-Data-Loc

    proof

      assume ( IC SCMPDS ) in SCM-Data-Loc ;

      then ( IC SCMPDS ) is Int_position by AMI_2:def 16;

      then ( Values ( IC SCMPDS )) = INT by SCMPDS_2: 5;

      hence contradiction by MEMSTR_0:def 6, NUMBERS: 7;

    end;

    begin

    ::$Canceled

    theorem :: SCMPDS_3:6

    for s be State of SCMPDS , iloc be Nat, a be Int_position holds (s . a) = ((s +* ( Start-At (iloc, SCMPDS ))) . a)

    proof

      let s be State of SCMPDS , iloc be Nat, a be Int_position;

      a in the carrier of SCMPDS ;

      then a in ( dom s) by PARTFUN1:def 2;

      then

       A1: ( dom ( Start-At (iloc, SCMPDS ))) = {( IC SCMPDS )} & a in (( dom s) \/ ( dom ( Start-At (iloc, SCMPDS )))) by XBOOLE_0:def 3;

      a <> ( IC SCMPDS ) by SCMPDS_2: 43;

      then not a in {( IC SCMPDS )} by TARSKI:def 1;

      hence thesis by A1, FUNCT_4:def 1;

    end;

    theorem :: SCMPDS_3:7

    for s,t be State of SCMPDS holds (s +* (t | SCM-Data-Loc )) is State of SCMPDS ;

    begin

    definition

      let la be Int_position;

      let a be Integer;

      :: original: .-->

      redefine

      func la .--> a -> FinPartState of SCMPDS ;

      coherence

      proof

        a is Element of INT & ( Values la) = INT by INT_1:def 2, SCMPDS_2: 5;

        hence thesis;

      end;

    end

    registration

      cluster SCMPDS -> IC-recognized;

      coherence

      proof

        let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

        let p be q -autonomic FinPartState of SCMPDS such that

         A1: p is non empty;

        assume

         A2: not ( IC SCMPDS ) in ( dom p);

         not ( IC SCMPDS ) in ( dom p) by A2;

        then

         A3: ( dom p) misses {( IC SCMPDS )} by ZFMISC_1: 50;

        ( dom p) c= ( {( IC SCMPDS )} \/ ( dom ( DataPart p))) by MEMSTR_0: 32;

        then

         A4: ( dom p) c= ( dom ( DataPart p)) by A3, XBOOLE_1: 73;

        

         A5: ( dom ( DataPart p)) <> {} by A1, A4, XBOOLE_1: 3;

        ( DataPart p) c= p by MEMSTR_0: 12;

        then

         A6: ( dom ( DataPart p)) c= ( dom p) by RELAT_1: 11;

         not p is q -autonomic

        proof

          set il = the Element of ( NAT \ ( dom q));

          set d1 = the Element of ( dom ( DataPart p));

          

           A7: d1 in ( dom ( DataPart p)) by A5;

          ( dom ( DataPart p)) c= the carrier of SCMPDS by RELAT_1:def 18;

          then

          reconsider d1 as Element of SCMPDS by A7;

           not NAT c= ( dom q);

          then

           A8: ( NAT \ ( dom q)) <> {} by XBOOLE_1: 37;

          then

          reconsider il as Element of NAT by XBOOLE_0:def 5;

          

           A9: not il in ( dom q) by A8, XBOOLE_0:def 5;

          ( dom ( DataPart p)) c= SCM-Data-Loc by RELAT_1: 58, SCMPDS_2: 84;

          then

          reconsider d1 as Int_position by A7, AMI_2:def 16;

          

           A10: ( IC SCMPDS ) in ( dom ( Start-At (il, SCMPDS ))) by TARSKI:def 1;

          

           A11: ( dom p) misses {( IC SCMPDS )} by A2, ZFMISC_1: 50;

          set p2 = (p +* ( Start-At (il, SCMPDS )));

          set p1 = (p +* ( Start-At (il, SCMPDS )));

          set q2 = (q +* (il .--> (d1 := 1)));

          set q1 = (q +* (il .--> (d1 := 0 )));

          

           A13: ( dom q) misses ( dom (il .--> (d1 := 1))) by A9, ZFMISC_1: 50;

          

           A14: ( dom q) misses ( dom (il .--> (d1 := 0 ))) by A9, ZFMISC_1: 50;

          consider s1 be State of SCMPDS such that

           A15: p1 c= s1 by PBOOLE: 141;

          consider S1 be Instruction-Sequence of SCMPDS such that

           A16: q1 c= S1 by PBOOLE: 145;

          consider s2 be State of SCMPDS such that

           A17: p2 c= s2 by PBOOLE: 141;

          consider S2 be Instruction-Sequence of SCMPDS such that

           A18: q2 c= S2 by PBOOLE: 145;

          take P1 = S1, P2 = S2;

          (( dom p) /\ ( dom ( Start-At (il, SCMPDS )))) = (( dom p) /\ {( IC SCMPDS )})

          .= {} by A11, XBOOLE_0:def 7

          .= {} ;

          then ( dom p) misses ( dom ( Start-At (il, SCMPDS ))) by XBOOLE_0:def 7;

          then p c= p1 by FUNCT_4: 32;

          then

           A19: p c= s1 by A15, XBOOLE_1: 1;

          q c= q1 by A14, FUNCT_4: 32;

          hence q c= P1 by A16, XBOOLE_1: 1;

          (( dom p) /\ ( dom ( Start-At (il, SCMPDS )))) = (( dom p) /\ {( IC SCMPDS )})

          .= {} by A11, XBOOLE_0:def 7

          .= {} ;

          then ( dom p) misses ( dom ( Start-At (il, SCMPDS ))) by XBOOLE_0:def 7;

          then p c= p2 by FUNCT_4: 32;

          then

           A20: p c= s2 by A17, XBOOLE_1: 1;

          q c= q2 by A13, FUNCT_4: 32;

          hence q c= P2 by A18, XBOOLE_1: 1;

          take s1, s2;

          p c= s1 by A19;

          hence p c= s1;

          thus p c= s2 by A20;

          take 1;

          

           A21: ( dom p2) = (( dom p) \/ ( dom ( Start-At (il, SCMPDS )))) by FUNCT_4:def 1;

          

           A22: ( dom q2) = (( dom q) \/ ( dom (il .--> (d1 := 1)))) by FUNCT_4:def 1;

          

           A23: ( IC SCMPDS ) in ( dom ( Start-At (il, SCMPDS ))) by A10;

          then ( IC SCMPDS ) in ( dom p2) by A21, XBOOLE_0:def 3;

          

          then

           A24: ( IC s2) = (p2 . ( IC SCMPDS )) by A17, GRFUNC_1: 2

          .= (( Start-At (il, SCMPDS )) . ( IC SCMPDS )) by A23, FUNCT_4: 13

          .= (( Start-At (il, SCMPDS )) . ( IC SCMPDS ))

          .= il by FUNCOP_1: 72;

          il in ( dom (il .--> (d1 := 1))) by TARSKI:def 1;

          then

           A25: il in ( dom (il .--> (d1 := 1)));

          then il in ( dom q2) by A22, XBOOLE_0:def 3;

          

          then

           A26: (S2 . il) = (q2 . il) by A18, GRFUNC_1: 2

          .= ((il .--> (d1 := 1)) . il) by A25, FUNCT_4: 13

          .= ((il .--> (d1 := 1)) . il)

          .= (d1 := 1) by FUNCOP_1: 72;

          

           A27: (S2 /. ( IC s2)) = (S2 . ( IC s2)) by PBOOLE: 143;

          

           A28: (( Comput (S2,s2,( 0 + 1))) . d1) = (( Following (S2,( Comput (S2,s2, 0 )))) . d1) by EXTPRO_1: 3

          .= (( Following (S2,s2)) . d1)

          .= 1 by A24, A26, A27, SCMPDS_2: 45;

          

           A29: ( dom p) c= the carrier of SCMPDS by RELAT_1:def 18;

          ( dom ( Comput (S1,s1,1))) = the carrier of SCMPDS by PARTFUN1:def 2;

          then

           A30: ( dom (( Comput (S1,s1,1)) | ( dom p))) = ( dom p) by A29, RELAT_1: 62;

          

           A31: ( dom p1) = (( dom p) \/ ( dom ( Start-At (il, SCMPDS )))) by FUNCT_4:def 1;

          

           A32: ( dom q1) = (( dom q) \/ ( dom (il .--> (d1 := 0 )))) by FUNCT_4:def 1;

          

           A33: ( IC SCMPDS ) in ( dom ( Start-At (il, SCMPDS ))) by A10;

          then ( IC SCMPDS ) in ( dom p1) by A31, XBOOLE_0:def 3;

          

          then

           A34: ( IC s1) = (p1 . ( IC SCMPDS )) by A15, GRFUNC_1: 2

          .= (( Start-At (il, SCMPDS )) . ( IC SCMPDS )) by A33, FUNCT_4: 13

          .= (( Start-At (il, SCMPDS )) . ( IC SCMPDS ))

          .= il by FUNCOP_1: 72;

          il in ( dom (il .--> (d1 := 0 ))) by TARSKI:def 1;

          then

           A36: il in ( dom (il .--> (d1 := 0 )));

          then il in ( dom q1) by A32, XBOOLE_0:def 3;

          

          then

           A37: (S1 . il) = (q1 . il) by A16, GRFUNC_1: 2

          .= ((il .--> (d1 := 0 )) . il) by A36, FUNCT_4: 13

          .= ((il .--> (d1 := 0 )) . il)

          .= (d1 := 0 ) by FUNCOP_1: 72;

          

           A38: (S1 /. ( IC s1)) = (S1 . ( IC s1)) by PBOOLE: 143;

          

           A39: ( dom ( Comput (S2,s2,1))) = the carrier of SCMPDS by PARTFUN1:def 2;

          

           A40: ( dom (( Comput (S2,s2,1)) | ( dom p))) = ( dom p) by A29, A39, RELAT_1: 62;

          (( Comput (S1,s1,( 0 + 1))) . d1) = (( Following (S1,( Comput (S1,s1, 0 )))) . d1) by EXTPRO_1: 3

          .= (( Following (S1,s1)) . d1)

          .= 0 by A34, A37, A38, SCMPDS_2: 45;

          then ((( Comput (S1,s1,1)) | ( dom p)) . d1) = 0 by A7, A30, A6, FUNCT_1: 47;

          hence thesis by A28, A7, A40, A6, FUNCT_1: 47;

        end;

        hence contradiction;

      end;

    end

    theorem :: SCMPDS_3:8

    

     Th7: for s1,s2 be State of SCMPDS , k1,k2,m be Integer st ( IC s1) = ( IC s2) & k1 <> k2 & m = ( IC s1) & (m + k1) >= 0 & (m + k2) >= 0 holds ( ICplusConst (s1,k1)) <> ( ICplusConst (s2,k2))

    proof

      let s1,s2 be State of SCMPDS , k1,k2,m be Integer;

      assume that

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

       A2: k1 <> k2 and

       A3: m = ( IC s1) and

       A4: (m + k1) >= 0 and

       A5: (m + k2) >= 0 ;

      ex i be Element of NAT st i = ( IC s1) & ( ICplusConst (s1,k1)) = |.(i + k1).| by SCMPDS_2:def 18;

      then

       A6: ( ICplusConst (s1,k1)) = (m + k1) by A3, A4, ABSVALUE:def 1;

      assume

       A7: ( ICplusConst (s1,k1)) = ( ICplusConst (s2,k2));

      ex j be Element of NAT st j = ( IC s2) & ( ICplusConst (s2,k2)) = |.(j + k2).| by SCMPDS_2:def 18;

      then ( ICplusConst (s2,k2)) = (m + k2) by A1, A3, A5, ABSVALUE:def 1;

      hence contradiction by A2, A7, A6;

    end;

    theorem :: SCMPDS_3:9

    for s1,s2 be State of SCMPDS , k1,k2 be Nat st ( IC s1) = ( IC s2) & k1 <> k2 holds ( ICplusConst (s1,k1)) <> ( ICplusConst (s2,k2))

    proof

      let s1,s2 be State of SCMPDS , k1,k2 be Nat;

      reconsider m = ( IC s1) as Element of NAT ;

      set mm = (m + 2);

      

       A1: ((mm - 2) + k1) >= 0 ;

      

       A2: ((mm - 2) + k2) >= 0 ;

      assume ( IC s1) = ( IC s2) & k1 <> k2;

      hence thesis by A1, A2, Th7;

    end;

    theorem :: SCMPDS_3:10

    

     Th9: for s be State of SCMPDS holds (( IC s) + 1) = ( ICplusConst (s,1))

    proof

      let s be State of SCMPDS ;

      consider j be Element of NAT such that

       A1: j = ( IC s) and

       A2: ( ICplusConst (s,1)) = |.(j + 1).| by SCMPDS_2:def 18;

      reconsider mj = ( IC s) as Element of NAT ;

      

       A3: (j * 1) >= 0 ;

      (( IC s) + 1) = ( |.mj.| + 1) by ABSVALUE:def 1

      .= ( |.mj.| + |.1.|) by ABSVALUE:def 1

      .= |.(mj + 1).| by A1, A3, ABSVALUE: 11;

      hence thesis by A1, A2;

    end;

    registration

      cluster SCMPDS -> CurIns-recognized;

      coherence

      proof

        let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

        let p be q -autonomic non empty FinPartState of SCMPDS , s be State of SCMPDS such that

         A1: p c= s;

        let P be Instruction-Sequence of SCMPDS such that

         A2: q c= P;

        let i be Nat;

        set Csi = ( Comput (P,s,i));

        set loc = ( IC Csi);

        set loc1 = (loc + 1);

        assume not ( IC ( Comput (P,s,i))) in ( dom q);

        then

         A3: not loc in ( dom q);

        set I = ( the Int_position := 0 );

        set q1 = (q +* (loc .--> I));

        set q2 = (q +* (loc .--> ( halt SCMPDS )));

        reconsider P1 = (P +* (loc .--> I)) as Instruction-Sequence of SCMPDS ;

        reconsider P2 = (P +* (loc .--> ( halt SCMPDS ))) as Instruction-Sequence of SCMPDS ;

        

         A5: loc in ( dom (loc .--> ( halt SCMPDS ))) by TARSKI:def 1;

        

         A7: loc in ( dom (loc .--> I)) by TARSKI:def 1;

        

         A8: ( dom q) misses ( dom (loc .--> ( halt SCMPDS ))) by A3, ZFMISC_1: 50;

        

         A9: ( dom q) misses ( dom (loc .--> I)) by A3, ZFMISC_1: 50;

        

         A10: q1 c= P1 by A2, FUNCT_4: 123;

        

         A11: q2 c= P2 by A2, FUNCT_4: 123;

        set Cs2i = ( Comput (P2,s,i)), Cs1i = ( Comput (P1,s,i));

         not p is q -autonomic

        proof

          ((loc .--> ( halt SCMPDS )) . loc) = ( halt SCMPDS ) by FUNCOP_1: 72;

          then

           A12: (P2 . loc) = ( halt SCMPDS ) by A5, FUNCT_4: 13;

          ((loc .--> I) . loc) = I by FUNCOP_1: 72;

          then

           A13: (P1 . loc) = I by A7, FUNCT_4: 13;

          take P1, P2;

          q c= q1 by A9, FUNCT_4: 32;

          hence

           A14: q c= P1 by A10, XBOOLE_1: 1;

          q c= q2 by A8, FUNCT_4: 32;

          hence

           A15: q c= P2 by A11, XBOOLE_1: 1;

          take s, s;

          thus p c= s by A1;

          

           A16: (Cs1i | ( dom p)) = (Csi | ( dom p)) by A14, A2, A1, EXTPRO_1:def 10;

          thus p c= s by A1;

          

           A17: (Cs1i | ( dom p)) = (Cs2i | ( dom p)) by A14, A15, A1, EXTPRO_1:def 10;

          take k = (i + 1);

          set Cs1k = ( Comput (P1,s,k));

          

           A18: ( IC SCMPDS ) in ( dom p) by AMISTD_5: 6;

          ( IC Csi) = ( IC (Csi | ( dom p))) by A18, FUNCT_1: 49;

          then ( IC Cs1i) = loc by A16, A18, FUNCT_1: 49;

          

          then

           A19: ( CurInstr (P1,Cs1i)) = (P1 . loc) by PBOOLE: 143

          .= I by A13;

          

           A20: Cs1k = ( Following (P1,Cs1i)) by EXTPRO_1: 3

          .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i))

          .= ( Exec (I,Cs1i)) by A19;

          

           A21: ( IC ( Exec (I,Cs1i))) = (( IC Cs1i) + 1) by SCMPDS_2: 45;

          

           A22: ( IC SCMPDS ) in ( dom p) by AMISTD_5: 6;

          

           A23: ( IC Csi) = ( IC (Csi | ( dom p))) by A22, FUNCT_1: 49;

          then ( IC Cs1i) = loc by A16, A22, FUNCT_1: 49;

          

          then

           A24: ( IC Cs1k) = (loc + 1) by A20, A21

          .= loc1;

          set Cs2k = ( Comput (P2,s,k));

          

           A25: Cs2k = ( Following (P2,Cs2i)) by EXTPRO_1: 3

          .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

          

           A26: (P2 /. ( IC Cs2i)) = (P2 . ( IC Cs2i)) by PBOOLE: 143;

          ( IC Cs2i) = loc by A16, A23, A17, A22, FUNCT_1: 49;

          then

           A27: ( IC Cs2k) = loc by A25, A12, A26, EXTPRO_1:def 3;

          ( IC (Cs1k | ( dom p))) = ( IC Cs1k) & ( IC (Cs2k | ( dom p))) = ( IC Cs2k) by A22, FUNCT_1: 49;

          hence thesis by A24, A27;

        end;

        hence contradiction;

      end;

    end

    theorem :: SCMPDS_3:11

    for q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds for i be Nat, k1,k2 be Integer, a,b be Int_position st ( CurInstr (P1,( Comput (P1,s1,i)))) = ((a,k1) := (b,k2)) & a in ( dom p) & ( DataLoc ((( Comput (P1,s1,i)) . a),k1)) in ( dom p) holds (( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . b),k2))) = (( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . b),k2)))

    proof

      let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS such that

       A1: p c= s1 & p c= s2 and

       A2: q c= P1 & q c= P2;

      

       A3: p c= s1 & p c= s2 by A1;

      let i be Nat, k1,k2 be Integer, a,b be Int_position;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      assume that

       A4: I = ((a,k1) := (b,k2)) and

       A5: a in ( dom p) and

       A6: ( DataLoc ((Cs1i . a),k1)) in ( dom p);

      a in ( dom p) implies ((Cs1i | ( dom p)) . a) = (Cs1i . a) & ((Cs2i | ( dom p)) . a) = (Cs2i . a) by FUNCT_1: 49;

      then

       A7: (Cs1i . a) = (Cs2i . a) by A5, A2, A3, EXTPRO_1:def 10;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A8: (Cs1i1 . ( DataLoc ((Cs1i . a),k1))) = (Cs1i . ( DataLoc ((Cs1i . b),k2))) by A4, SCMPDS_2: 47;

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A9: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      

       A10: ( DataLoc ((Cs1i . a),k1)) in ( dom p) implies ((Cs1i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs1i1 . ( DataLoc ((Cs1i . a),k1))) & ((Cs2i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs2i1 . ( DataLoc ((Cs1i . a),k1))) by FUNCT_1: 49;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then (Cs2i1 . ( DataLoc ((Cs2i . a),k1))) = (Cs2i . ( DataLoc ((Cs2i . b),k2))) by A9, A4, SCMPDS_2: 47;

      hence thesis by A10, A6, A7, A8, A2, A3, EXTPRO_1:def 10;

    end;

    theorem :: SCMPDS_3:12

    for q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds for i be Nat, k1,k2 be Integer, a,b be Int_position st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( AddTo (a,k1,b,k2)) & a in ( dom p) & ( DataLoc ((( Comput (P1,s1,i)) . a),k1)) in ( dom p) holds (( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . b),k2))) = (( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . b),k2)))

    proof

      let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS such that

       A1: p c= s1 & p c= s2 and

       A2: q c= P1 & q c= P2;

      

       A3: p c= s1 & p c= s2 by A1;

      let i be Nat, k1,k2 be Integer, a,b be Int_position;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      assume that

       A4: I = ( AddTo (a,k1,b,k2)) and

       A5: a in ( dom p) and

       A6: ( DataLoc ((Cs1i . a),k1)) in ( dom p);

      a in ( dom p) implies ((Cs1i | ( dom p)) . a) = (Cs1i . a) & ((Cs2i | ( dom p)) . a) = (Cs2i . a) by FUNCT_1: 49;

      then

       A7: (Cs1i . a) = (Cs2i . a) by A5, A2, A3, EXTPRO_1:def 10;

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set D11 = (Cs1i1 . ( DataLoc ((Cs1i . a),k1))), D21 = (Cs2i1 . ( DataLoc ((Cs2i . a),k1))), C11 = (Cs1i . ( DataLoc ((Cs1i . a),k1))), C12 = (Cs1i . ( DataLoc ((Cs1i . b),k2))), C21 = (Cs2i . ( DataLoc ((Cs2i . a),k1))), C22 = (Cs2i . ( DataLoc ((Cs2i . b),k2)));

      

       A8: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      ( DataLoc ((Cs1i . a),k1)) in ( dom p) implies ((Cs1i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs1i1 . ( DataLoc ((Cs1i . a),k1))) & ((Cs2i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs2i1 . ( DataLoc ((Cs1i . a),k1))) by FUNCT_1: 49;

      then

       A9: D11 = D21 by A6, A7, A2, A3, EXTPRO_1:def 10;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A10: D11 = (C11 + C12) by A4, SCMPDS_2: 49;

      ( DataLoc ((Cs1i . a),k1)) in ( dom p) implies ((Cs1i | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs1i . ( DataLoc ((Cs1i . a),k1))) & ((Cs2i | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs2i . ( DataLoc ((Cs1i . a),k1))) by FUNCT_1: 49;

      then

       A11: C11 = C21 by A6, A7, A2, A3, EXTPRO_1:def 10;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then D21 = (C21 + C22) by A8, A4, SCMPDS_2: 49;

      hence thesis by A11, A9, A10;

    end;

    theorem :: SCMPDS_3:13

    for q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds for i be Nat, k1,k2 be Integer, a,b be Int_position st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( SubFrom (a,k1,b,k2)) & a in ( dom p) & ( DataLoc ((( Comput (P1,s1,i)) . a),k1)) in ( dom p) holds (( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . b),k2))) = (( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . b),k2)))

    proof

      let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS such that

       A1: p c= s1 & p c= s2 and

       A2: q c= P1 & q c= P2;

      

       A3: p c= s1 & p c= s2 by A1;

      let i be Nat, k1,k2 be Integer, a,b be Int_position;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      assume that

       A4: I = ( SubFrom (a,k1,b,k2)) and

       A5: a in ( dom p) and

       A6: ( DataLoc ((Cs1i . a),k1)) in ( dom p);

      a in ( dom p) implies ((Cs1i | ( dom p)) . a) = (Cs1i . a) & ((Cs2i | ( dom p)) . a) = (Cs2i . a) by FUNCT_1: 49;

      then

       A7: (Cs1i . a) = (Cs2i . a) by A5, A2, A3, EXTPRO_1:def 10;

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set D11 = (Cs1i1 . ( DataLoc ((Cs1i . a),k1))), D21 = (Cs2i1 . ( DataLoc ((Cs2i . a),k1))), C11 = (Cs1i . ( DataLoc ((Cs1i . a),k1))), C12 = (Cs1i . ( DataLoc ((Cs1i . b),k2))), C21 = (Cs2i . ( DataLoc ((Cs2i . a),k1))), C22 = (Cs2i . ( DataLoc ((Cs2i . b),k2)));

      

       A8: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      ( DataLoc ((Cs1i . a),k1)) in ( dom p) implies ((Cs1i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs1i1 . ( DataLoc ((Cs1i . a),k1))) & ((Cs2i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs2i1 . ( DataLoc ((Cs1i . a),k1))) by FUNCT_1: 49;

      then

       A9: D11 = D21 by A6, A7, A2, A3, EXTPRO_1:def 10;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A10: D11 = (C11 - C12) by A4, SCMPDS_2: 50;

      ( DataLoc ((Cs1i . a),k1)) in ( dom p) implies ((Cs1i | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs1i . ( DataLoc ((Cs1i . a),k1))) & ((Cs2i | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs2i . ( DataLoc ((Cs1i . a),k1))) by FUNCT_1: 49;

      then

       A11: C11 = C21 by A6, A7, A2, A3, EXTPRO_1:def 10;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then D21 = (C21 - C22) by A8, A4, SCMPDS_2: 50;

      hence thesis by A11, A9, A10;

    end;

    theorem :: SCMPDS_3:14

    for q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds for i be Nat, k1,k2 be Integer, a,b be Int_position st ( CurInstr (P1,( Comput (P1,s1,i)))) = ( MultBy (a,k1,b,k2)) & a in ( dom p) & ( DataLoc ((( Comput (P1,s1,i)) . a),k1)) in ( dom p) holds ((( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . a),k1))) * (( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . b),k2)))) = ((( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . a),k1))) * (( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . b),k2))))

    proof

      let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS such that

       A1: p c= s1 & p c= s2 and

       A2: q c= P1 & q c= P2;

      

       A3: p c= s1 & p c= s2 by A1;

      let i be Nat, k1,k2 be Integer, a,b be Int_position;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      assume that

       A4: I = ( MultBy (a,k1,b,k2)) and

       A5: a in ( dom p) and

       A6: ( DataLoc ((Cs1i . a),k1)) in ( dom p);

      a in ( dom p) implies ((Cs1i | ( dom p)) . a) = (Cs1i . a) & ((Cs2i | ( dom p)) . a) = (Cs2i . a) by FUNCT_1: 49;

      then

       A7: (Cs1i . a) = (Cs2i . a) by A5, A2, A3, EXTPRO_1:def 10;

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set D11 = (Cs1i1 . ( DataLoc ((Cs1i . a),k1))), D21 = (Cs2i1 . ( DataLoc ((Cs2i . a),k1)));

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then

       A8: D11 = ((Cs1i . ( DataLoc ((Cs1i . a),k1))) * (Cs1i . ( DataLoc ((Cs1i . b),k2)))) by A4, SCMPDS_2: 51;

      

       A9: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      

       A10: ( DataLoc ((Cs1i . a),k1)) in ( dom p) implies ((Cs1i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs1i1 . ( DataLoc ((Cs1i . a),k1))) & ((Cs2i1 | ( dom p)) . ( DataLoc ((Cs1i . a),k1))) = (Cs2i1 . ( DataLoc ((Cs1i . a),k1))) by FUNCT_1: 49;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

      then D21 = ((Cs2i . ( DataLoc ((Cs2i . a),k1))) * (Cs2i . ( DataLoc ((Cs2i . b),k2)))) by A9, A4, SCMPDS_2: 51;

      hence thesis by A10, A6, A7, A8, A2, A3, EXTPRO_1:def 10;

    end;

    theorem :: SCMPDS_3:15

    for q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds for i,m be Nat, a be Int_position, k1,k2 be Integer st ( CurInstr (P1,( Comput (P1,s1,i)))) = ((a,k1) <>0_goto k2) & m = ( IC ( Comput (P1,s1,i))) & (m + k2) >= 0 & k2 <> 1 holds ((( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . a),k1))) = 0 iff (( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . a),k1))) = 0 )

    proof

      let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS such that

       A1: p c= s1 & p c= s2 and

       A2: q c= P1 & q c= P2;

      let i,m be Nat, a be Int_position, k1,k2 be Integer;

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: ( IC Cs1i) = ( IC Cs2i) & (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, AMISTD_5: 7, EXTPRO_1:def 10;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: (m + 1) >= 0 ;

      ( IC SCMPDS ) in ( dom p) by AMISTD_5: 6;

      then ( IC SCMPDS ) in ( dom p);

      then

       A6: ((Cs1i1 | ( dom p)) . ( IC SCMPDS )) = (Cs1i1 . ( IC SCMPDS )) & ((Cs2i1 | ( dom p)) . ( IC SCMPDS )) = (Cs2i1 . ( IC SCMPDS )) by FUNCT_1: 49;

      

       A7: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A8: I = ((a,k1) <>0_goto k2) and

       A9: m = ( IC Cs1i) & (m + k2) >= 0 & k2 <> 1;

      

       A10: I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

       A11:

      now

        assume that

         A12: (( Comput (P2,s2,i)) . ( DataLoc ((Cs2i . a),k1))) = 0 and

         A13: (( Comput (P1,s1,i)) . ( DataLoc ((Cs1i . a),k1))) <> 0 ;

        

         A14: (Cs1i1 . ( IC SCMPDS )) = ( ICplusConst (Cs1i,k2)) by A4, A8, A13, SCMPDS_2: 55;

        (Cs2i1 . ( IC SCMPDS )) = (( IC Cs2i) + 1) by A10, A7, A8, A12, SCMPDS_2: 55

        .= ( ICplusConst (Cs2i,1)) by Th9;

        hence contradiction by A6, A3, A9, A5, A14, Th7;

      end;

      now

        assume that

         A15: (( Comput (P1,s1,i)) . ( DataLoc ((Cs1i . a),k1))) = 0 and

         A16: (( Comput (P2,s2,i)) . ( DataLoc ((Cs2i . a),k1))) <> 0 ;

        

         A17: (Cs2i1 . ( IC SCMPDS )) = ( ICplusConst (Cs2i,k2)) by A10, A7, A8, A16, SCMPDS_2: 55;

        (Cs1i1 . ( IC SCMPDS )) = (( IC Cs1i) + 1) by A4, A8, A15, SCMPDS_2: 55

        .= ( ICplusConst (Cs1i,1)) by Th9;

        hence contradiction by A6, A3, A9, A5, A17, Th7;

      end;

      hence thesis by A11;

    end;

    theorem :: SCMPDS_3:16

    for q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds for i,m be Nat, a be Int_position, k1,k2 be Integer st ( CurInstr (P1,( Comput (P1,s1,i)))) = ((a,k1) <=0_goto k2) & m = ( IC ( Comput (P1,s1,i))) & (m + k2) >= 0 & k2 <> 1 holds ((( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . a),k1))) > 0 iff (( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . a),k1))) > 0 )

    proof

      let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS such that

       A1: p c= s1 & p c= s2 and

       A2: q c= P1 & q c= P2;

      let i,m be Nat, a be Int_position, k1,k2 be Integer;

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: ( IC Cs1i) = ( IC Cs2i) & (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, AMISTD_5: 7, EXTPRO_1:def 10;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: (m + 1) >= 0 ;

      ( IC SCMPDS ) in ( dom p) by AMISTD_5: 6;

      then ( IC SCMPDS ) in ( dom p);

      then

       A6: ((Cs1i1 | ( dom p)) . ( IC SCMPDS )) = (Cs1i1 . ( IC SCMPDS )) & ((Cs2i1 | ( dom p)) . ( IC SCMPDS )) = (Cs2i1 . ( IC SCMPDS )) by FUNCT_1: 49;

      

       A7: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A8: I = ((a,k1) <=0_goto k2) and

       A9: m = ( IC Cs1i) & (m + k2) >= 0 & k2 <> 1;

      

       A10: I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

       A11:

      now

        assume that

         A12: (( Comput (P2,s2,i)) . ( DataLoc ((Cs2i . a),k1))) > 0 and

         A13: (( Comput (P1,s1,i)) . ( DataLoc ((Cs1i . a),k1))) <= 0 ;

        

         A14: (Cs1i1 . ( IC SCMPDS )) = ( ICplusConst (Cs1i,k2)) by A4, A8, A13, SCMPDS_2: 56;

        (Cs2i1 . ( IC SCMPDS )) = (( IC Cs2i) + 1) by A10, A7, A8, A12, SCMPDS_2: 56

        .= ( ICplusConst (Cs2i,1)) by Th9;

        hence contradiction by A6, A3, A9, A5, A14, Th7;

      end;

      now

        assume that

         A15: (( Comput (P1,s1,i)) . ( DataLoc ((Cs1i . a),k1))) > 0 and

         A16: (( Comput (P2,s2,i)) . ( DataLoc ((Cs2i . a),k1))) <= 0 ;

        

         A17: (Cs2i1 . ( IC SCMPDS )) = ( ICplusConst (Cs2i,k2)) by A10, A7, A8, A16, SCMPDS_2: 56;

        (Cs1i1 . ( IC SCMPDS )) = (( IC Cs1i) + 1) by A4, A8, A15, SCMPDS_2: 56

        .= ( ICplusConst (Cs1i,1)) by Th9;

        hence contradiction by A6, A3, A9, A5, A17, Th7;

      end;

      hence thesis by A11;

    end;

    theorem :: SCMPDS_3:17

    for q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS st p c= s1 & p c= s2 & q c= P1 & q c= P2 holds for i,m be Nat, a be Int_position, k1,k2 be Integer st ( CurInstr (P1,( Comput (P1,s1,i)))) = ((a,k1) >=0_goto k2) & m = ( IC ( Comput (P1,s1,i))) & (m + k2) >= 0 & k2 <> 1 holds ((( Comput (P1,s1,i)) . ( DataLoc ((( Comput (P1,s1,i)) . a),k1))) < 0 iff (( Comput (P2,s2,i)) . ( DataLoc ((( Comput (P2,s2,i)) . a),k1))) < 0 )

    proof

      let q be non halt-free finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCMPDS , s1,s2 be State of SCMPDS such that

       A1: p c= s1 & p c= s2 and

       A2: q c= P1 & q c= P2;

      let i,m be Nat, a be Int_position, k1,k2 be Integer;

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      

       A3: ( IC Cs1i) = ( IC Cs2i) & (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A1, A2, AMISTD_5: 7, EXTPRO_1:def 10;

      set I = ( CurInstr (P1,( Comput (P1,s1,i))));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: (m + 1) >= 0 ;

      ( IC SCMPDS ) in ( dom p) by AMISTD_5: 6;

      then ( IC SCMPDS ) in ( dom p);

      then

       A6: ((Cs1i1 | ( dom p)) . ( IC SCMPDS )) = (Cs1i1 . ( IC SCMPDS )) & ((Cs2i1 | ( dom p)) . ( IC SCMPDS )) = (Cs2i1 . ( IC SCMPDS )) by FUNCT_1: 49;

      

       A7: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A8: I = ((a,k1) >=0_goto k2) and

       A9: m = ( IC Cs1i) & (m + k2) >= 0 & k2 <> 1;

      

       A10: I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A1, A2, AMISTD_5: 7;

       A11:

      now

        assume that

         A12: (( Comput (P2,s2,i)) . ( DataLoc ((Cs2i . a),k1))) < 0 and

         A13: (( Comput (P1,s1,i)) . ( DataLoc ((Cs1i . a),k1))) >= 0 ;

        

         A14: (Cs1i1 . ( IC SCMPDS )) = ( ICplusConst (Cs1i,k2)) by A4, A8, A13, SCMPDS_2: 57;

        (Cs2i1 . ( IC SCMPDS )) = (( IC Cs2i) + 1) by A10, A7, A8, A12, SCMPDS_2: 57

        .= ( ICplusConst (Cs2i,1)) by Th9;

        hence contradiction by A6, A3, A9, A5, A14, Th7;

      end;

      now

        assume that

         A15: (( Comput (P1,s1,i)) . ( DataLoc ((Cs1i . a),k1))) < 0 and

         A16: (( Comput (P2,s2,i)) . ( DataLoc ((Cs2i . a),k1))) >= 0 ;

        

         A17: (Cs2i1 . ( IC SCMPDS )) = ( ICplusConst (Cs2i,k2)) by A10, A7, A8, A16, SCMPDS_2: 57;

        (Cs1i1 . ( IC SCMPDS )) = (( IC Cs1i) + 1) by A4, A8, A15, SCMPDS_2: 57

        .= ( ICplusConst (Cs1i,1)) by Th9;

        hence contradiction by A6, A3, A9, A5, A17, Th7;

      end;

      hence thesis by A11;

    end;