scmpds_9.miz



    begin

    reserve a,b for Int_position,

i for Instruction of SCMPDS ,

l for Element of NAT ,

k,k1,k2 for Integer;

    definition

      let la,lb be Int_position, a,b be Integer;

      :: original: -->

      redefine

      func (la,lb) --> (a,b) -> PartState of SCMPDS ;

      coherence

      proof

        

         A1: ( Values la) = INT & ( Values lb) = INT by SCMPDS_2: 5;

        

         A2: a is Element of INT & b is Element of INT by INT_1:def 2;

        reconsider a as Element of ( Values la) by A1, A2;

        reconsider b as Element of ( Values lb) by A1, A2;

        ((la,lb) --> (a,b)) is PartState of SCMPDS ;

        hence thesis;

      end;

    end

    

     Lm1: ( JUMP ( goto k)) = {}

    proof

      set i = ( goto k);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      hereby

        set l2 = 0 ;

        set l1 = 1;

        let x be object;

        assume

         A1: x in ( JUMP i);

        ( NIC (i,l2)) in X;

        then x in ( NIC (i,l2)) by A1, SETFAM_1:def 1;

        then

        consider s2 be Element of ( product ( the_Values_of SCMPDS )) such that

         A2: x = ( IC ( Exec (i,s2))) and

         A3: ( IC s2) = l2;

        consider m2 be Element of NAT such that

         A4: m2 = ( IC s2) and

         A5: ( ICplusConst (s2,k)) = |.(m2 + k).| by SCMPDS_2:def 18;

        ( NIC (i,l1)) in X;

        then x in ( NIC (i,l1)) by A1, SETFAM_1:def 1;

        then

        consider s1 be Element of ( product ( the_Values_of SCMPDS )) such that

         A6: x = ( IC ( Exec (i,s1))) and

         A7: ( IC s1) = l1;

        consider m1 be Element of NAT such that

         A8: m1 = ( IC s1) and

         A9: ( ICplusConst (s1,k)) = |.(m1 + k).| by SCMPDS_2:def 18;

         |.(m2 + k).| = ( ICplusConst (s2,k)) by A5

        .= ( IC ( Exec (i,s2))) by SCMPDS_2: 54

        .= ( IC ( Exec (i,s1))) by A2, A6

        .= ( ICplusConst (s1,k)) by SCMPDS_2: 54

        .= |.(m1 + k).| by A9;

        per cases by A7, A8, A3, A4, ABSVALUE: 28;

          suppose ( 0 + k) = (1 + k);

          hence x in {} ;

        end;

          suppose ( 0 + k) = ( - (1 + k));

          then ( - ( - (1 / 2))) is integer;

          hence x in {} by NAT_D: 33;

        end;

      end;

      thus thesis;

    end;

    registration

      let k;

      cluster ( JUMP ( goto k)) -> empty;

      coherence by Lm1;

    end

    theorem :: SCMPDS_9:1

    

     Th1: (for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1)) implies ( NIC (i,l)) = {(l + 1)}

    proof

      reconsider I = i as Instruction of SCMPDS ;

      reconsider n = l as Element of NAT ;

      assume

       A1: for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1);

      hereby

        let x be object;

        assume x in ( NIC (i,l));

        then

        consider s be Element of ( product ( the_Values_of SCMPDS )) such that

         A2: x = ( IC ( Exec (i,s))) and

         A3: ( IC s) = l;

        x = (l + 1) by A1, A2, A3;

        hence x in {(l + 1)} by TARSKI:def 1;

      end;

      set t = the l -started State of SCMPDS ;

      reconsider t = the l -started State of SCMPDS as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

      

       A4: ( IC t) = l by MEMSTR_0:def 11;

      let x be object;

      assume x in {(l + 1)};

      then

       A5: x = (l + 1) by TARSKI:def 1;

      ( IC ( Exec (I,t))) = (l + 1) by A1, A4;

      hence thesis by A5, A4;

    end;

    theorem :: SCMPDS_9:2

    

     Th2: (for l be Element of NAT holds ( NIC (i,l)) = {(l + 1)}) implies ( JUMP i) is empty

    proof

      set p = 1, q = 2;

      assume

       A1: for l be Element of NAT holds ( NIC (i,l)) = {(l + 1)};

      set X = the set of all ( NIC (i,f)) where f be Nat;

      reconsider p, q as Element of NAT ;

      assume not thesis;

      then

      consider x be object such that

       A2: x in ( meet X);

      ( NIC (i,p)) = {(p + 1)} by A1;

      then {(p + 1)} in X;

      then x in {(p + 1)} by A2, SETFAM_1:def 1;

      then

       A3: x = (p + 1) by TARSKI:def 1;

      ( NIC (i,q)) = {(q + 1)} by A1;

      then {(q + 1)} in X;

      then x in {(q + 1)} by A2, SETFAM_1:def 1;

      hence contradiction by A3, TARSKI:def 1;

    end;

    theorem :: SCMPDS_9:3

    

     Th3: ( NIC (( goto k),l)) = { |.(k + l).|}

    proof

      set s = the State of SCMPDS ;

      set i = ( goto k);

      set t = |.(k + l).|;

      set I = i;

      reconsider n = l as Element of NAT ;

      hereby

        let x be object;

        assume x in ( NIC (i,l));

        then

        consider s be Element of ( product ( the_Values_of SCMPDS )) such that

         A1: x = ( IC ( Exec (i,s))) and

         A2: ( IC s) = l;

        

         A3: ex m1 be Element of NAT st m1 = ( IC s) & ( ICplusConst (s,k)) = |.(m1 + k).| by SCMPDS_2:def 18;

        x = t by A1, A2, A3, SCMPDS_2: 54;

        hence x in {t} by TARSKI:def 1;

      end;

      let x be object;

      reconsider u = the n -started State of SCMPDS as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

      

       A4: ( IC u) = n by MEMSTR_0:def 11;

      consider m1 be Element of NAT such that

       A5: m1 = ( IC u) and

       A6: ( ICplusConst (u,k)) = |.(m1 + k).| by SCMPDS_2:def 18;

      assume x in {t};

      

      then x = |.(m1 + k).| by A4, A5, TARSKI:def 1

      .= ( IC ( Exec (i,u))) by A6, SCMPDS_2: 54;

      hence thesis by A4;

    end;

    

     Lm2: for k be Nat st k > 1 holds (k - 2) is Element of NAT

    proof

      let k be Nat;

      assume k > 1;

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

      then (k - 2) >= (2 - 2) by XREAL_1: 9;

      hence thesis by INT_1: 3;

    end;

    theorem :: SCMPDS_9:4

    

     Th4: ( NIC (( return a),l)) = { k where k be Nat : k > 1 }

    proof

      set s = the State of SCMPDS ;

      set X = { k where k be Nat : k > 1 };

      set i = ( return a);

      hereby

        let x be object;

        assume x in ( NIC (i,l));

        then

        consider s be Element of ( product ( the_Values_of SCMPDS )) such that

         A1: x = ( IC ( Exec (i,s))) and ( IC s) = l;

        reconsider k = x as Element of NAT by A1;

        

         A2: ( |.(s . ( DataLoc ((s . a),1))).| + 2) >= ( 0 + 2) by XREAL_1: 6;

        k >= (1 + 1) by A2, A1, SCMPDS_2: 58, SCMPDS_I:def 14;

        then k > 1 by NAT_1: 13;

        hence x in X;

      end;

      let x be object;

      set I = i;

      reconsider n = l as Element of NAT ;

      assume x in X;

      then

      consider k be Nat such that

       A3: x = k and

       A4: k > 1;

      reconsider k2 = (k - 2) as Element of NAT by A4, Lm2;

      reconsider u = the n -started State of SCMPDS as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

      

       A5: ( IC u) = n by MEMSTR_0:def 11;

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

      then

      consider j be Nat such that

       A6: a = [1, j] by AMI_2: 23;

      set t = [1, (j + 1)];

      t in SCM-Data-Loc by AMI_2: 24;

      then

      reconsider t1 = t as Int_position by AMI_2:def 16;

      

       A7: ( DataLoc (j,1)) = [1, |.(j + 1).|]

      .= t by ABSVALUE:def 1;

      set g = ((a,t1) --> (j,k2));

      reconsider v = (u +* g) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

      

       A8: ( dom g) = {a, t} by FUNCT_4: 62;

      j <> (j + 1);

      then

       A9: a <> t by A6, XTUPLE_0: 1;

      then

       A10: (v . a) = j by FUNCT_4: 84;

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

      then

       A11: not ( IC SCMPDS ) in ( dom g) by A8, TARSKI:def 2;

      

       A12: ( IC v) = l by A5, A11, FUNCT_4: 11;

      

       A13: (v . t) = k2 by A9, FUNCT_4: 84;

      x = (k2 + 2) by A3

      .= ( |.(v . ( DataLoc (j,1))).| + 2) by A13, A7, ABSVALUE:def 1

      .= ( IC ( Exec (i,v))) by A10, SCMPDS_2: 58, SCMPDS_I:def 14;

      hence thesis by A12;

    end;

    theorem :: SCMPDS_9:5

    

     Th5: ( NIC (( saveIC (a,k1)),l)) = {(l + 1)}

    proof

      set i = ( saveIC (a,k1));

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 59;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:6

    

     Th6: ( NIC ((a := k1),l)) = {(l + 1)}

    proof

      set i = (a := k1);

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 45;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:7

    

     Th7: ( NIC (((a,k1) := k2),l)) = {(l + 1)}

    proof

      set i = ((a,k1) := k2);

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 46;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:8

    

     Th8: ( NIC (((a,k1) := (b,k2)),l)) = {(l + 1)}

    proof

      set i = ((a,k1) := (b,k2));

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 47;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:9

    

     Th9: ( NIC (( AddTo (a,k1,k2)),l)) = {(l + 1)}

    proof

      set i = ( AddTo (a,k1,k2));

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 48;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:10

    

     Th10: ( NIC (( AddTo (a,k1,b,k2)),l)) = {(l + 1)}

    proof

      set i = ( AddTo (a,k1,b,k2));

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 49;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:11

    

     Th11: ( NIC (( SubFrom (a,k1,b,k2)),l)) = {(l + 1)}

    proof

      set i = ( SubFrom (a,k1,b,k2));

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 50;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:12

    

     Th12: ( NIC (( MultBy (a,k1,b,k2)),l)) = {(l + 1)}

    proof

      set i = ( MultBy (a,k1,b,k2));

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 51;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:13

    

     Th13: ( NIC (( Divide (a,k1,b,k2)),l)) = {(l + 1)}

    proof

      set i = ( Divide (a,k1,b,k2));

      for s be State of SCMPDS st ( IC s) = l holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 52;

      hence thesis by Th1;

    end;

    theorem :: SCMPDS_9:14

    ( NIC (((a,k1) <>0_goto k2),l)) = {(l + 1), |.(k2 + l).|}

    proof

      set s = the State of SCMPDS ;

      set i = ((a,k1) <>0_goto k2);

      set t = |.(k2 + l).|;

      set I = i;

      reconsider n = l as Element of NAT ;

      reconsider u = the n -started State of SCMPDS as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

      hereby

        let x be object;

        assume x in ( NIC (i,l));

        then

        consider s be Element of ( product ( the_Values_of SCMPDS )) such that

         A1: x = ( IC ( Exec (i,s))) and

         A2: ( IC s) = l;

        

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

        per cases ;

          suppose

           A4: (s . ( DataLoc ((s . a),k1))) <> 0 ;

          x = t by A1, A2, A3, A4, SCMPDS_2: 55;

          hence x in {(l + 1), t} by TARSKI:def 2;

        end;

          suppose

           A5: (s . ( DataLoc ((s . a),k1))) = 0 ;

          x = (l + 1) by A1, A2, A5, SCMPDS_2: 55;

          hence x in {(l + 1), t} by TARSKI:def 2;

        end;

      end;

      let x be object;

      assume

       A6: x in {(l + 1), t};

      per cases by A6, TARSKI:def 2;

        suppose

         A7: x = (l + 1);

        reconsider u1 = (u +* (a .--> 0 )) as State of SCMPDS ;

        reconsider u2 = (u1 +* (( DataLoc ((u1 . a),k1)) .--> 0 )) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        

         A8: ( IC u2) = (u1 . ( IC SCMPDS )) by FUNCT_4: 83, SCMPDS_2: 43

        .= ( IC u) by FUNCT_4: 83, SCMPDS_2: 43

        .= n by MEMSTR_0:def 11;

        

         A9: (u2 . ( DataLoc ((u1 . a),k1))) = 0 by FUNCT_7: 94;

        (u2 . ( DataLoc ((u2 . a),k1))) = 0

        proof

          per cases ;

            suppose a = ( DataLoc ((u1 . a),k1));

            hence thesis by A9;

          end;

            suppose a <> ( DataLoc ((u1 . a),k1));

            then (u2 . a) = (u1 . a) by FUNCT_4: 83;

            hence thesis by FUNCT_7: 94;

          end;

        end;

        then x = ( IC ( Exec (i,u2))) by A7, A8, SCMPDS_2: 55;

        hence thesis by A8;

      end;

        suppose

         A10: x = t;

        reconsider u1 = (u +* (a .--> 1)) as State of SCMPDS ;

        reconsider u2 = (u1 +* (( DataLoc ((u1 . a),k1)) .--> 1)) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        

         A11: (u2 . ( DataLoc ((u1 . a),k1))) = 1 by FUNCT_7: 94;

        

         A12: (u2 . ( DataLoc ((u2 . a),k1))) <> 0

        proof

          per cases ;

            suppose a = ( DataLoc ((u1 . a),k1));

            hence thesis by A11;

          end;

            suppose a <> ( DataLoc ((u1 . a),k1));

            then (u2 . a) = (u1 . a) by FUNCT_4: 83;

            hence thesis by FUNCT_7: 94;

          end;

        end;

        

         A13: ( IC u2) = (u1 . ( IC SCMPDS )) by FUNCT_4: 83, SCMPDS_2: 43

        .= ( IC u) by FUNCT_4: 83, SCMPDS_2: 43

        .= n by MEMSTR_0:def 11;

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

        then x = ( IC ( Exec (i,u2))) by A10, A13, A12, SCMPDS_2: 55;

        hence thesis by A13;

      end;

    end;

    theorem :: SCMPDS_9:15

    ( NIC (((a,k1) <=0_goto k2),l)) = {(l + 1), |.(k2 + l).|}

    proof

      set s = the State of SCMPDS ;

      set i = ((a,k1) <=0_goto k2);

      set t = |.(k2 + l).|;

      set I = i;

      reconsider n = l as Element of NAT ;

      reconsider u = the n -started State of SCMPDS as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

      hereby

        let x be object;

        assume x in ( NIC (i,l));

        then

        consider s be Element of ( product ( the_Values_of SCMPDS )) such that

         A1: x = ( IC ( Exec (i,s))) and

         A2: ( IC s) = l;

        

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

        per cases ;

          suppose

           A4: (s . ( DataLoc ((s . a),k1))) <= 0 ;

          x = t by A1, A2, A3, A4, SCMPDS_2: 56;

          hence x in {(l + 1), t} by TARSKI:def 2;

        end;

          suppose

           A5: (s . ( DataLoc ((s . a),k1))) > 0 ;

          x = (l + 1) by A1, A2, A5, SCMPDS_2: 56;

          hence x in {(l + 1), t} by TARSKI:def 2;

        end;

      end;

      let x be object;

      assume

       A6: x in {(l + 1), t};

      per cases by A6, TARSKI:def 2;

        suppose

         A7: x = (l + 1);

        reconsider u1 = (u +* (a .--> 1)) as State of SCMPDS ;

        reconsider u2 = (u1 +* (( DataLoc ((u1 . a),k1)) .--> 1)) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        

         A8: ( IC u2) = (u1 . ( IC SCMPDS )) by FUNCT_4: 83, SCMPDS_2: 43

        .= ( IC u) by FUNCT_4: 83, SCMPDS_2: 43

        .= n by MEMSTR_0:def 11;

        

         A9: (u2 . ( DataLoc ((u1 . a),k1))) = 1 by FUNCT_7: 94;

        (u2 . ( DataLoc ((u2 . a),k1))) > 0

        proof

          per cases ;

            suppose a = ( DataLoc ((u1 . a),k1));

            hence thesis by A9;

          end;

            suppose a <> ( DataLoc ((u1 . a),k1));

            then (u2 . a) = (u1 . a) by FUNCT_4: 83;

            hence thesis by FUNCT_7: 94;

          end;

        end;

        then x = ( IC ( Exec (i,u2))) by A7, A8, SCMPDS_2: 56;

        hence thesis by A8;

      end;

        suppose

         A10: x = t;

        reconsider u1 = (u +* (a .--> 0 )) as State of SCMPDS ;

        reconsider u2 = (u1 +* (( DataLoc ((u1 . a),k1)) .--> 0 )) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        

         A11: (u2 . ( DataLoc ((u1 . a),k1))) = 0 by FUNCT_7: 94;

        

         A12: (u2 . ( DataLoc ((u2 . a),k1))) <= 0

        proof

          per cases ;

            suppose a = ( DataLoc ((u1 . a),k1));

            hence thesis by A11;

          end;

            suppose a <> ( DataLoc ((u1 . a),k1));

            then (u2 . a) = (u1 . a) by FUNCT_4: 83;

            hence thesis by FUNCT_7: 94;

          end;

        end;

        

         A13: ( IC u2) = (u1 . ( IC SCMPDS )) by FUNCT_4: 83, SCMPDS_2: 43

        .= ( IC u) by FUNCT_4: 83, SCMPDS_2: 43

        .= n by MEMSTR_0:def 11;

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

        then x = ( IC ( Exec (i,u2))) by A10, A13, A12, SCMPDS_2: 56;

        hence thesis by A13;

      end;

    end;

    theorem :: SCMPDS_9:16

    ( NIC (((a,k1) >=0_goto k2),l)) = {(l + 1), |.(k2 + l).|}

    proof

      set s = the State of SCMPDS ;

      set i = ((a,k1) >=0_goto k2);

      set t = |.(k2 + l).|;

      set I = i;

      reconsider n = l as Element of NAT ;

      reconsider u = the n -started State of SCMPDS as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

      hereby

        let x be object;

        assume x in ( NIC (i,l));

        then

        consider s be Element of ( product ( the_Values_of SCMPDS )) such that

         A1: x = ( IC ( Exec (i,s))) and

         A2: ( IC s) = l;

        

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

        per cases ;

          suppose

           A4: (s . ( DataLoc ((s . a),k1))) >= 0 ;

          x = t by A1, A2, A3, A4, SCMPDS_2: 57;

          hence x in {(l + 1), t} by TARSKI:def 2;

        end;

          suppose

           A5: (s . ( DataLoc ((s . a),k1))) < 0 ;

          x = (l + 1) by A1, A2, A5, SCMPDS_2: 57;

          hence x in {(l + 1), t} by TARSKI:def 2;

        end;

      end;

      let x be object;

      assume

       A6: x in {(l + 1), t};

      per cases by A6, TARSKI:def 2;

        suppose

         A7: x = (l + 1);

        

         A8: ( - 1) < 0 ;

        reconsider u1 = (u +* (a .--> ( - 1))) as State of SCMPDS ;

        reconsider u1 = (u +* (a .--> ( - 1))) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        reconsider u2 = (u1 +* (( DataLoc ((u1 . a),k1)) .--> ( - 1))) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        

         A9: ( IC u2) = (u1 . ( IC SCMPDS )) by FUNCT_4: 83, SCMPDS_2: 43

        .= ( IC u) by FUNCT_4: 83, SCMPDS_2: 43

        .= n by MEMSTR_0:def 11;

        

         A10: (u2 . ( DataLoc ((u1 . a),k1))) = ( - 1) by FUNCT_7: 94;

        (u2 . ( DataLoc ((u2 . a),k1))) < 0

        proof

          per cases ;

            suppose a = ( DataLoc ((u1 . a),k1));

            hence thesis by A10;

          end;

            suppose a <> ( DataLoc ((u1 . a),k1));

            then (u2 . a) = (u1 . a) by FUNCT_4: 83;

            hence thesis by A8, FUNCT_7: 94;

          end;

        end;

        then x = ( IC ( Exec (i,u2))) by A7, A9, SCMPDS_2: 57;

        hence thesis by A9;

      end;

        suppose

         A11: x = t;

        reconsider u1 = (u +* (a .--> ( - 1))) as State of SCMPDS ;

        reconsider u1 = (u +* (a .--> 0 )) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        reconsider u2 = (u1 +* (( DataLoc ((u1 . a),k1)) .--> 0 )) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        

         A12: (u2 . ( DataLoc ((u1 . a),k1))) = 0 by FUNCT_7: 94;

        

         A13: (u2 . ( DataLoc ((u2 . a),k1))) >= 0

        proof

          per cases ;

            suppose a = ( DataLoc ((u1 . a),k1));

            hence thesis by A12;

          end;

            suppose a <> ( DataLoc ((u1 . a),k1));

            then (u2 . a) = (u1 . a) by FUNCT_4: 83;

            hence thesis by FUNCT_7: 94;

          end;

        end;

        

         A14: ( IC u2) = (u1 . ( IC SCMPDS )) by FUNCT_4: 83, SCMPDS_2: 43

        .= ( IC u) by FUNCT_4: 83, SCMPDS_2: 43

        .= n by MEMSTR_0:def 11;

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

        then x = ( IC ( Exec (i,u2))) by A11, A14, A13, SCMPDS_2: 57;

        hence thesis by A14;

      end;

    end;

    theorem :: SCMPDS_9:17

    

     Th17: ( JUMP ( return a)) = { k where k be Nat : k > 1 }

    proof

      set A = { k where k be Nat : k > 1 };

      set i = ( return a);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      ( JUMP i) c= ( NIC (i, 0 )) by AMISTD_1: 19;

      hence ( JUMP i) c= A by Th4;

      let x be object;

      assume

       A1: x in A;

      now

        consider k be Nat such that

         A2: x = k and

         A3: k > 1 by A1;

        reconsider k2 = (k - 2) as Element of NAT by A3, Lm2;

        ( NIC (i, 0 )) in X;

        hence X <> {} ;

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

        then

        consider j be Nat such that

         A4: a = [1, j] by AMI_2: 23;

        set t = [1, (j + 1)];

        set s = the State of SCMPDS ;

        let y be set;

        

         A5: ( DataLoc (j,1)) = [1, |.(j + 1).|]

        .= t by ABSVALUE:def 1;

        t in SCM-Data-Loc by AMI_2: 24;

        then

        reconsider t1 = t as Int_position by AMI_2:def 16;

        assume y in X;

        then

        consider l be Nat such that

         A6: y = ( NIC (i,l));

        reconsider n = l as Element of NAT by ORDINAL1:def 12;

        set I = i;

        reconsider u = the n -started State of SCMPDS as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        

         A7: ( IC u) = n by MEMSTR_0:def 11;

        set g = ((a,t1) --> (j,k2));

        reconsider v = (u +* g) as Element of ( product ( the_Values_of SCMPDS )) by CARD_3: 107;

        j <> (j + 1);

        then

         A8: a <> t1 by A4, XTUPLE_0: 1;

        then

         A9: (v . a) = j by FUNCT_4: 84;

        

         A10: (v . t1) = k2 by A8, FUNCT_4: 84;

        

         A11: ( dom g) = {a, t1} by FUNCT_4: 62;

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

        then

         A12: not ( IC SCMPDS ) in ( dom g) by A11, TARSKI:def 2;

        

         A13: ( IC v) = l by A7, A12, FUNCT_4: 11;

        x = (k2 + 2) by A2

        .= ( |.(v . ( DataLoc (j,1))).| + 2) by A10, A5, ABSVALUE:def 1

        .= ( IC ( Exec (i,v))) by A9, SCMPDS_2: 58, SCMPDS_I:def 14;

        hence x in y by A6, A13;

      end;

      hence thesis by SETFAM_1:def 1;

    end;

    registration

      let a;

      cluster ( JUMP ( return a)) -> infinite;

      coherence

      proof

        { k where k be Nat : k > 1 } is infinite by PRE_CIRC: 23;

        hence thesis by Th17;

      end;

    end

    registration

      let a, k1;

      cluster ( JUMP ( saveIC (a,k1))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( saveIC (a,k1)),l)) = {(l + 1)} by Th5;

        hence thesis by Th2;

      end;

    end

    registration

      let a, k1;

      cluster ( JUMP (a := k1)) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC ((a := k1),l)) = {(l + 1)} by Th6;

        hence thesis by Th2;

      end;

    end

    registration

      let a, k1, k2;

      cluster ( JUMP ((a,k1) := k2)) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (((a,k1) := k2),l)) = {(l + 1)} by Th7;

        hence thesis by Th2;

      end;

    end

    registration

      let a, b, k1, k2;

      cluster ( JUMP ((a,k1) := (b,k2))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (((a,k1) := (b,k2)),l)) = {(l + 1)} by Th8;

        hence thesis by Th2;

      end;

    end

    registration

      let a, k1, k2;

      cluster ( JUMP ( AddTo (a,k1,k2))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( AddTo (a,k1,k2)),l)) = {(l + 1)} by Th9;

        hence thesis by Th2;

      end;

    end

    registration

      let a, b, k1, k2;

      cluster ( JUMP ( AddTo (a,k1,b,k2))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( AddTo (a,k1,b,k2)),l)) = {(l + 1)} by Th10;

        hence thesis by Th2;

      end;

      cluster ( JUMP ( SubFrom (a,k1,b,k2))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( SubFrom (a,k1,b,k2)),l)) = {(l + 1)} by Th11;

        hence thesis by Th2;

      end;

      cluster ( JUMP ( MultBy (a,k1,b,k2))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( MultBy (a,k1,b,k2)),l)) = {(l + 1)} by Th12;

        hence thesis by Th2;

      end;

      cluster ( JUMP ( Divide (a,k1,b,k2))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( Divide (a,k1,b,k2)),l)) = {(l + 1)} by Th13;

        hence thesis by Th2;

      end;

    end

    

     Lm3: not (5 / 3) is integer

    proof

       not 3 qua Integer divides 5

      proof

        assume not thesis;

        then

         A1: (5 mod 3) = 0 by PEPIN: 6;

        5 = ((3 * 1) + 2);

        hence contradiction by A1, NAT_D:def 2;

      end;

      hence thesis by WSIERP_1: 17;

    end;

    

     Lm4: for d be Real holds (((( |.d.| + ((( - d) + |.d.|) + 4)) + 2) - 2) + d) <> ( - ((((( |.d.| + ((( - d) + |.d.|) + 4)) + ((( - d) + |.d.|) + 4)) + 2) - 2) + d))

    proof

      let d be Real;

      set c = ((( - d) + |.d.|) + 4);

      set xx = ((c + c) + c);

      (( - d) + |.d.|) >= 0 by ABSVALUE: 27;

      then (( - 2) * xx) < (( - 2) * 0 ) by XREAL_1: 69;

      then

       A1: ((( - 2) * xx) / 4) < ( 0 / 4) by XREAL_1: 74;

      assume (((( |.d.| + c) + 2) - 2) + d) = ( - ((((( |.d.| + c) + ((( - d) + |.d.|) + 4)) + 2) - 2) + d));

      then (d + |.d.|) = ((( - 2) * xx) / 4);

      hence contradiction by A1, ABSVALUE: 26;

    end;

    

     Lm5: for b,d be Real holds (b + 1) <> (b + (((( - d) + |.d.|) + 4) + d))

    proof

      let b,d be Real;

      set c = ((( - d) + |.d.|) + 4);

       |.d.| >= 0 by COMPLEX1: 46;

      then

       A1: ( |.d.| + 3) >= ( 0 + 3) by XREAL_1: 7;

      assume (b + 1) = (b + (c + d));

      hence thesis by A1;

    end;

    

     Lm6: for c,d be Real st c > 0 holds (( |.d.| + c) + 1) <> ( - ((( |.d.| + c) + c) + d))

    proof

      let c,d be Real such that

       A1: c > 0 ;

      assume

       A2: (( |.d.| + c) + 1) = ( - ((( |.d.| + c) + c) + d));

      per cases ;

        suppose

         A3: d >= 0 ;

        then |.d.| = d by ABSVALUE:def 1;

        hence contradiction by A1, A2, A3;

      end;

        suppose

         A4: d < 0 ;

        then |.d.| = ( - d) by ABSVALUE:def 1;

        then ((( - d) + (3 * c)) + 1) = 0 by A2;

        hence contradiction by A1, A4;

      end;

    end;

    

     Lm7: for b be Real, d be Integer st d <> 5 holds ((b + ((( - d) + |.d.|) + 4)) + 1) <> (b + d)

    proof

      let b be Real, d be Integer;

      assume

       A1: d <> 5;

      assume

       A2: ((b + ((( - d) + |.d.|) + 4)) + 1) = (b + d);

      per cases ;

        suppose d >= 0 ;

        then |.d.| = d by ABSVALUE:def 1;

        hence thesis by A1, A2;

      end;

        suppose d < 0 ;

        then |.d.| = ( - d) by ABSVALUE:def 1;

        hence thesis by A2, Lm3;

      end;

    end;

    

     Lm8: for c,d be Real st c > 0 holds ((( |.d.| + c) + c) + 1) <> ( - (( |.d.| + c) + d))

    proof

      let c,d be Real;

      assume

       A1: c > 0 ;

      assume

       A2: ((( |.d.| + c) + c) + 1) = ( - (( |.d.| + c) + d));

      per cases ;

        suppose

         A3: d >= 0 ;

        then |.d.| = d by ABSVALUE:def 1;

        hence contradiction by A1, A2, A3;

      end;

        suppose

         A4: d < 0 ;

        then |.d.| = ( - d) by ABSVALUE:def 1;

        hence contradiction by A1, A2, A4;

      end;

    end;

    

     Lm9: ( JUMP ((a,k1) <>0_goto 5)) = {}

    proof

      set k2 = 5;

      set i = ((a,k1) <>0_goto k2);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      hereby

        set nl2 = 8;

        set nl1 = 5;

        let x be object;

        assume

         A1: x in ( JUMP i);

        set l2 = nl2;

        ( NIC (i,l2)) in X;

        then x in ( NIC (i,l2)) by A1, SETFAM_1:def 1;

        then

        consider s2 be Element of ( product ( the_Values_of SCMPDS )) such that

         A2: x = ( IC ( Exec (i,s2))) and

         A3: ( IC s2) = l2;

        set l1 = nl1;

        ( NIC (i,l1)) in X;

        then x in ( NIC (i,l1)) by A1, SETFAM_1:def 1;

        then

        consider s1 be Element of ( product ( the_Values_of SCMPDS )) such that

         A4: x = ( IC ( Exec (i,s1))) and

         A5: ( IC s1) = l1;

        consider m2 be Element of NAT such that

         A6: m2 = ( IC s2) and

         A7: ( ICplusConst (s2,k2)) = |.(m2 + k2).| by SCMPDS_2:def 18;

        consider m1 be Element of NAT such that

         A8: m1 = ( IC s1) and

         A9: ( ICplusConst (s1,k2)) = |.(m1 + k2).| by SCMPDS_2:def 18;

        per cases ;

          suppose that

           A10: (s1 . ( DataLoc ((s1 . a),k1))) <> 0 and

           A11: (s2 . ( DataLoc ((s2 . a),k1))) <> 0 ;

          

           A12: x = |.(m2 + k2).| by A2, A7, A11, SCMPDS_2: 55;

          x = |.(m1 + k2).| by A4, A9, A10, SCMPDS_2: 55;

          then (nl1 + k2) = (nl2 + k2) or (nl1 + k2) = ( - (nl2 + k2)) by A5, A8, A3, A6, A12, ABSVALUE: 28;

          hence x in {} ;

        end;

          suppose that

           A13: (s1 . ( DataLoc ((s1 . a),k1))) = 0 and

           A14: (s2 . ( DataLoc ((s2 . a),k1))) = 0 ;

          

           A15: x = (l2 + 1) by A2, A3, A14, SCMPDS_2: 55;

          x = (l1 + 1) by A4, A5, A13, SCMPDS_2: 55;

          hence x in {} by A15;

        end;

          suppose that

           A16: (s1 . ( DataLoc ((s1 . a),k1))) = 0 and

           A17: (s2 . ( DataLoc ((s2 . a),k1))) <> 0 ;

          reconsider n1 = l1 as Element of NAT ;

          set w1 = n1;

          

           A18: x = |.(m2 + k2).| by A2, A7, A17, SCMPDS_2: 55;

          x = (n1 + 1) by A4, A5, A16, SCMPDS_2: 55

          .= (n1 + 1);

          then (w1 + 1) = (m2 + k2) or (w1 + 1) = ( - (m2 + k2)) by A18, ABSVALUE: 1;

          hence x in {} by A3, A6;

        end;

          suppose that

           A19: (s1 . ( DataLoc ((s1 . a),k1))) <> 0 and

           A20: (s2 . ( DataLoc ((s2 . a),k1))) = 0 ;

          reconsider n2 = l2 as Element of NAT ;

          

           A21: x = (n2 + 1) by A2, A3, A20, SCMPDS_2: 55

          .= (n2 + 1);

          set w2 = n2;

          x = |.(m1 + k2).| by A4, A9, A19, SCMPDS_2: 55;

          then (w2 + 1) = (m1 + k2) or (w2 + 1) = ( - (m1 + k2)) by A21, ABSVALUE: 1;

          hence x in {} by A5, A8;

        end;

      end;

      thus thesis;

    end;

    

     Lm10: k2 <> 5 implies ( JUMP ((a,k1) <>0_goto k2)) = {}

    proof

      set i = ((a,k1) <>0_goto k2);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      assume

       A1: k2 <> 5;

      hereby

        set x1 = ((( - k2) + |.k2.|) + 4);

        let x be object;

        assume

         A2: x in ( JUMP i);

        

         A3: x1 > ((( - k2) + |.k2.|) + 0 ) by XREAL_1: 6;

        then

         A4: x1 > 0 by ABSVALUE: 27;

        then

        reconsider x1 as Element of NAT by INT_1: 3;

        set nl1 = ( |.k2.| + x1);

        set nl2 = (nl1 + x1);

        set l1 = nl1;

        set l2 = nl2;

        ( NIC (i,l1)) in X;

        then x in ( NIC (i,l1)) by A2, SETFAM_1:def 1;

        then

        consider s1 be Element of ( product ( the_Values_of SCMPDS )) such that

         A5: x = ( IC ( Exec (i,s1))) and

         A6: ( IC s1) = l1;

        consider m1 be Element of NAT such that

         A7: m1 = ( IC s1) and

         A8: ( ICplusConst (s1,k2)) = |.(m1 + k2).| by SCMPDS_2:def 18;

        ( NIC (i,l2)) in X;

        then x in ( NIC (i,l2)) by A2, SETFAM_1:def 1;

        then

        consider s2 be Element of ( product ( the_Values_of SCMPDS )) such that

         A9: x = ( IC ( Exec (i,s2))) and

         A10: ( IC s2) = l2;

        consider m2 be Element of NAT such that

         A11: m2 = ( IC s2) and

         A12: ( ICplusConst (s2,k2)) = |.(m2 + k2).| by SCMPDS_2:def 18;

        per cases ;

          suppose that

           A13: (s1 . ( DataLoc ((s1 . a),k1))) <> 0 and

           A14: (s2 . ( DataLoc ((s2 . a),k1))) <> 0 ;

          

           A15: x = |.(m2 + k2).| by A9, A12, A14, SCMPDS_2: 55;

          

           A16: x = |.(m1 + k2).| by A5, A8, A13, SCMPDS_2: 55;

          thus x in {}

          proof

            per cases by A6, A7, A10, A11, A16, A15, ABSVALUE: 28;

              suppose (((nl1 + 2) - 2) + k2) = (((nl2 + 2) - 2) + k2);

              hence thesis by A3, ABSVALUE: 27;

            end;

              suppose (((nl1 + 2) - 2) + k2) = ( - (((nl2 + 2) - 2) + k2));

              hence thesis by Lm4;

            end;

          end;

        end;

          suppose that

           A17: (s1 . ( DataLoc ((s1 . a),k1))) = 0 and

           A18: (s2 . ( DataLoc ((s2 . a),k1))) = 0 ;

          

           A19: x = (l2 + 1) by A9, A10, A18, SCMPDS_2: 55;

          x = (l1 + 1) by A5, A6, A17, SCMPDS_2: 55;

          hence x in {} by A3, A19, ABSVALUE: 27;

        end;

          suppose that

           A20: (s1 . ( DataLoc ((s1 . a),k1))) = 0 and

           A21: (s2 . ( DataLoc ((s2 . a),k1))) <> 0 ;

          reconsider n1 = l1 as Element of NAT ;

          set w1 = n1;

          

           A22: x = |.(m2 + k2).| by A9, A12, A21, SCMPDS_2: 55;

          

           A23: x = (n1 + 1) by A5, A6, A20, SCMPDS_2: 55

          .= (n1 + 1);

          thus x in {}

          proof

            per cases by A23, A22, ABSVALUE: 1;

              suppose (w1 + 1) = (m2 + k2);

              then (nl1 + 1) = (nl1 + (x1 + k2)) by A10, A11;

              hence thesis by Lm5;

            end;

              suppose (w1 + 1) = ( - (m2 + k2));

              hence thesis by A4, A10, A11, Lm6;

            end;

          end;

        end;

          suppose that

           A24: (s1 . ( DataLoc ((s1 . a),k1))) <> 0 and

           A25: (s2 . ( DataLoc ((s2 . a),k1))) = 0 ;

          reconsider n2 = l2 as Element of NAT ;

          

           A26: x = (n2 + 1) by A9, A10, A25, SCMPDS_2: 55

          .= (n2 + 1);

          set w2 = n2;

          

           A27: x = |.(m1 + k2).| by A5, A8, A24, SCMPDS_2: 55;

          thus x in {}

          proof

            per cases by A27, A26, ABSVALUE: 1;

              suppose (w2 + 1) = (m1 + k2);

              hence thesis by A1, A6, A7, Lm7;

            end;

              suppose (w2 + 1) = ( - (m1 + k2));

              hence thesis by A4, A6, A7, Lm8;

            end;

          end;

        end;

      end;

      thus thesis;

    end;

    

     Lm11: ( JUMP ((a,k1) <=0_goto 5)) = {}

    proof

      set k2 = 5;

      set i = ((a,k1) <=0_goto k2);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      hereby

        set nl2 = 8;

        set nl1 = 5;

        let x be object;

        assume

         A1: x in ( JUMP i);

        set l2 = nl2;

        ( NIC (i,l2)) in X;

        then x in ( NIC (i,l2)) by A1, SETFAM_1:def 1;

        then

        consider s2 be Element of ( product ( the_Values_of SCMPDS )) such that

         A2: x = ( IC ( Exec (i,s2))) and

         A3: ( IC s2) = l2;

        set l1 = nl1;

        ( NIC (i,l1)) in X;

        then x in ( NIC (i,l1)) by A1, SETFAM_1:def 1;

        then

        consider s1 be Element of ( product ( the_Values_of SCMPDS )) such that

         A4: x = ( IC ( Exec (i,s1))) and

         A5: ( IC s1) = l1;

        consider m2 be Element of NAT such that

         A6: m2 = ( IC s2) and

         A7: ( ICplusConst (s2,k2)) = |.(m2 + k2).| by SCMPDS_2:def 18;

        consider m1 be Element of NAT such that

         A8: m1 = ( IC s1) and

         A9: ( ICplusConst (s1,k2)) = |.(m1 + k2).| by SCMPDS_2:def 18;

        per cases ;

          suppose that

           A10: (s1 . ( DataLoc ((s1 . a),k1))) <= 0 and

           A11: (s2 . ( DataLoc ((s2 . a),k1))) <= 0 ;

          

           A12: x = |.(m2 + k2).| by A2, A7, A11, SCMPDS_2: 56;

          x = |.(m1 + k2).| by A4, A9, A10, SCMPDS_2: 56;

          then (nl1 + k2) = (nl2 + k2) or (nl1 + k2) = ( - (nl2 + k2)) by A5, A8, A3, A6, A12, ABSVALUE: 28;

          hence x in {} ;

        end;

          suppose that

           A13: (s1 . ( DataLoc ((s1 . a),k1))) > 0 and

           A14: (s2 . ( DataLoc ((s2 . a),k1))) > 0 ;

          

           A15: x = (l2 + 1) by A2, A3, A14, SCMPDS_2: 56;

          x = (l1 + 1) by A4, A5, A13, SCMPDS_2: 56;

          hence x in {} by A15;

        end;

          suppose that

           A16: (s1 . ( DataLoc ((s1 . a),k1))) > 0 and

           A17: (s2 . ( DataLoc ((s2 . a),k1))) <= 0 ;

          reconsider n1 = l1 as Element of NAT ;

          set w1 = n1;

          

           A18: x = |.(m2 + k2).| by A2, A7, A17, SCMPDS_2: 56;

          x = (n1 + 1) by A4, A5, A16, SCMPDS_2: 56

          .= (n1 + 1);

          then (w1 + 1) = (m2 + k2) or (w1 + 1) = ( - (m2 + k2)) by A18, ABSVALUE: 1;

          hence x in {} by A3, A6;

        end;

          suppose that

           A19: (s1 . ( DataLoc ((s1 . a),k1))) <= 0 and

           A20: (s2 . ( DataLoc ((s2 . a),k1))) > 0 ;

          reconsider n2 = l2 as Element of NAT ;

          

           A21: x = (n2 + 1) by A2, A3, A20, SCMPDS_2: 56

          .= (n2 + 1);

          set w2 = n2;

          x = |.(m1 + k2).| by A4, A9, A19, SCMPDS_2: 56;

          then (w2 + 1) = (m1 + k2) or (w2 + 1) = ( - (m1 + k2)) by A21, ABSVALUE: 1;

          hence x in {} by A5, A8;

        end;

      end;

      thus thesis;

    end;

    

     Lm12: k2 <> 5 implies ( JUMP ((a,k1) <=0_goto k2)) = {}

    proof

      set i = ((a,k1) <=0_goto k2);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      assume

       A1: k2 <> 5;

      hereby

        set x1 = ((( - k2) + |.k2.|) + 4);

        let x be object;

        assume

         A2: x in ( JUMP i);

        

         A3: x1 > ((( - k2) + |.k2.|) + 0 ) by XREAL_1: 6;

        then

         A4: x1 > 0 by ABSVALUE: 27;

        then

        reconsider x1 as Element of NAT by INT_1: 3;

        set nl1 = ( |.k2.| + x1);

        set nl2 = (nl1 + x1);

        set l1 = nl1;

        set l2 = nl2;

        ( NIC (i,l1)) in X;

        then x in ( NIC (i,l1)) by A2, SETFAM_1:def 1;

        then

        consider s1 be Element of ( product ( the_Values_of SCMPDS )) such that

         A5: x = ( IC ( Exec (i,s1))) and

         A6: ( IC s1) = l1;

        consider m1 be Element of NAT such that

         A7: m1 = ( IC s1) and

         A8: ( ICplusConst (s1,k2)) = |.(m1 + k2).| by SCMPDS_2:def 18;

        ( NIC (i,l2)) in X;

        then x in ( NIC (i,l2)) by A2, SETFAM_1:def 1;

        then

        consider s2 be Element of ( product ( the_Values_of SCMPDS )) such that

         A9: x = ( IC ( Exec (i,s2))) and

         A10: ( IC s2) = l2;

        consider m2 be Element of NAT such that

         A11: m2 = ( IC s2) and

         A12: ( ICplusConst (s2,k2)) = |.(m2 + k2).| by SCMPDS_2:def 18;

        per cases ;

          suppose that

           A13: (s1 . ( DataLoc ((s1 . a),k1))) <= 0 and

           A14: (s2 . ( DataLoc ((s2 . a),k1))) <= 0 ;

          

           A15: x = |.(m2 + k2).| by A9, A12, A14, SCMPDS_2: 56;

          

           A16: x = |.(m1 + k2).| by A5, A8, A13, SCMPDS_2: 56;

          thus x in {}

          proof

            per cases by A6, A7, A10, A11, A16, A15, ABSVALUE: 28;

              suppose (nl1 + k2) = (nl2 + k2);

              hence thesis by A3, ABSVALUE: 27;

            end;

              suppose (((nl1 + 2) - 2) + k2) = ( - (((nl2 + 2) - 2) + k2));

              hence thesis by Lm4;

            end;

          end;

        end;

          suppose that

           A17: (s1 . ( DataLoc ((s1 . a),k1))) > 0 and

           A18: (s2 . ( DataLoc ((s2 . a),k1))) > 0 ;

          

           A19: x = (l2 + 1) by A9, A10, A18, SCMPDS_2: 56;

          x = (l1 + 1) by A5, A6, A17, SCMPDS_2: 56;

          hence x in {} by A3, A19, ABSVALUE: 27;

        end;

          suppose that

           A20: (s1 . ( DataLoc ((s1 . a),k1))) > 0 and

           A21: (s2 . ( DataLoc ((s2 . a),k1))) <= 0 ;

          reconsider n1 = l1 as Element of NAT ;

          set w1 = n1;

          

           A22: x = |.(m2 + k2).| by A9, A12, A21, SCMPDS_2: 56;

          

           A23: x = (n1 + 1) by A5, A6, A20, SCMPDS_2: 56

          .= (n1 + 1);

          thus x in {}

          proof

            per cases by A23, A22, ABSVALUE: 1;

              suppose (w1 + 1) = (m2 + k2);

              then (nl1 + 1) = (nl1 + (x1 + k2)) by A10, A11;

              hence thesis by Lm5;

            end;

              suppose (w1 + 1) = ( - (m2 + k2));

              hence thesis by A4, A10, A11, Lm6;

            end;

          end;

        end;

          suppose that

           A24: (s1 . ( DataLoc ((s1 . a),k1))) <= 0 and

           A25: (s2 . ( DataLoc ((s2 . a),k1))) > 0 ;

          reconsider n2 = l2 as Element of NAT ;

          

           A26: x = (n2 + 1) by A9, A10, A25, SCMPDS_2: 56

          .= (n2 + 1);

          set w2 = n2;

          

           A27: x = |.(m1 + k2).| by A5, A8, A24, SCMPDS_2: 56;

          thus x in {}

          proof

            per cases by A27, A26, ABSVALUE: 1;

              suppose (w2 + 1) = (m1 + k2);

              hence thesis by A1, A6, A7, Lm7;

            end;

              suppose (w2 + 1) = ( - (m1 + k2));

              hence thesis by A4, A6, A7, Lm8;

            end;

          end;

        end;

      end;

      thus thesis;

    end;

    

     Lm13: ( JUMP ((a,k1) >=0_goto 5)) = {}

    proof

      set k2 = 5;

      set i = ((a,k1) >=0_goto k2);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      hereby

        set nl2 = 8;

        set nl1 = 5;

        let x be object;

        assume

         A1: x in ( JUMP i);

        set l2 = nl2;

        ( NIC (i,l2)) in X;

        then x in ( NIC (i,l2)) by A1, SETFAM_1:def 1;

        then

        consider s2 be Element of ( product ( the_Values_of SCMPDS )) such that

         A2: x = ( IC ( Exec (i,s2))) and

         A3: ( IC s2) = l2;

        set l1 = nl1;

        ( NIC (i,l1)) in X;

        then x in ( NIC (i,l1)) by A1, SETFAM_1:def 1;

        then

        consider s1 be Element of ( product ( the_Values_of SCMPDS )) such that

         A4: x = ( IC ( Exec (i,s1))) and

         A5: ( IC s1) = l1;

        consider m2 be Element of NAT such that

         A6: m2 = ( IC s2) and

         A7: ( ICplusConst (s2,k2)) = |.(m2 + k2).| by SCMPDS_2:def 18;

        consider m1 be Element of NAT such that

         A8: m1 = ( IC s1) and

         A9: ( ICplusConst (s1,k2)) = |.(m1 + k2).| by SCMPDS_2:def 18;

        per cases ;

          suppose that

           A10: (s1 . ( DataLoc ((s1 . a),k1))) >= 0 and

           A11: (s2 . ( DataLoc ((s2 . a),k1))) >= 0 ;

          

           A12: x = |.(m2 + k2).| by A2, A7, A11, SCMPDS_2: 57;

          x = |.(m1 + k2).| by A4, A9, A10, SCMPDS_2: 57;

          then (((nl1 + 2) - 2) + k2) = (((nl2 + 2) - 2) + k2) or (((nl1 + 2) - 2) + k2) = ( - (((nl2 + 2) - 2) + k2)) by A5, A8, A3, A6, A12, ABSVALUE: 28;

          hence x in {} ;

        end;

          suppose that

           A13: (s1 . ( DataLoc ((s1 . a),k1))) < 0 and

           A14: (s2 . ( DataLoc ((s2 . a),k1))) < 0 ;

          

           A15: x = (l2 + 1) by A2, A3, A14, SCMPDS_2: 57;

          x = (l1 + 1) by A4, A5, A13, SCMPDS_2: 57;

          hence x in {} by A15;

        end;

          suppose that

           A16: (s1 . ( DataLoc ((s1 . a),k1))) < 0 and

           A17: (s2 . ( DataLoc ((s2 . a),k1))) >= 0 ;

          reconsider n1 = l1 as Element of NAT ;

          set w1 = n1;

          

           A18: x = |.(m2 + k2).| by A2, A7, A17, SCMPDS_2: 57;

          x = (n1 + 1) by A4, A5, A16, SCMPDS_2: 57

          .= (n1 + 1);

          then (w1 + 1) = (m2 + k2) or (w1 + 1) = ( - (m2 + k2)) by A18, ABSVALUE: 1;

          hence x in {} by A3, A6;

        end;

          suppose that

           A19: (s1 . ( DataLoc ((s1 . a),k1))) >= 0 and

           A20: (s2 . ( DataLoc ((s2 . a),k1))) < 0 ;

          reconsider n2 = l2 as Element of NAT ;

          

           A21: x = (n2 + 1) by A2, A3, A20, SCMPDS_2: 57

          .= (n2 + 1);

          set w2 = n2;

          x = |.(m1 + k2).| by A4, A9, A19, SCMPDS_2: 57;

          then (w2 + 1) = (m1 + k2) or (w2 + 1) = ( - (m1 + k2)) by A21, ABSVALUE: 1;

          hence x in {} by A5, A8;

        end;

      end;

      thus thesis;

    end;

    

     Lm14: k2 <> 5 implies ( JUMP ((a,k1) >=0_goto k2)) = {}

    proof

      set i = ((a,k1) >=0_goto k2);

      set X = the set of all ( NIC (i,l)) where l be Nat;

      assume

       A1: k2 <> 5;

      hereby

        set x1 = ((( - k2) + |.k2.|) + 4);

        let x be object;

        assume

         A2: x in ( JUMP i);

        

         A3: x1 > ((( - k2) + |.k2.|) + 0 ) by XREAL_1: 6;

        then

         A4: x1 > 0 by ABSVALUE: 27;

        then

        reconsider x1 as Element of NAT by INT_1: 3;

        set nl1 = ( |.k2.| + x1);

        set nl2 = (nl1 + x1);

        set l1 = nl1;

        set l2 = nl2;

        ( NIC (i,l1)) in X;

        then x in ( NIC (i,l1)) by A2, SETFAM_1:def 1;

        then

        consider s1 be Element of ( product ( the_Values_of SCMPDS )) such that

         A5: x = ( IC ( Exec (i,s1))) and

         A6: ( IC s1) = l1;

        consider m1 be Element of NAT such that

         A7: m1 = ( IC s1) and

         A8: ( ICplusConst (s1,k2)) = |.(m1 + k2).| by SCMPDS_2:def 18;

        ( NIC (i,l2)) in X;

        then x in ( NIC (i,l2)) by A2, SETFAM_1:def 1;

        then

        consider s2 be Element of ( product ( the_Values_of SCMPDS )) such that

         A9: x = ( IC ( Exec (i,s2))) and

         A10: ( IC s2) = l2;

        consider m2 be Element of NAT such that

         A11: m2 = ( IC s2) and

         A12: ( ICplusConst (s2,k2)) = |.(m2 + k2).| by SCMPDS_2:def 18;

        per cases ;

          suppose that

           A13: (s1 . ( DataLoc ((s1 . a),k1))) >= 0 and

           A14: (s2 . ( DataLoc ((s2 . a),k1))) >= 0 ;

          

           A15: x = |.(m2 + k2).| by A9, A12, A14, SCMPDS_2: 57;

          

           A16: x = |.(m1 + k2).| by A5, A8, A13, SCMPDS_2: 57;

          thus x in {}

          proof

            per cases by A6, A7, A10, A11, A16, A15, ABSVALUE: 28;

              suppose (((nl1 + 2) - 2) + k2) = (((nl2 + 2) - 2) + k2);

              hence thesis by A3, ABSVALUE: 27;

            end;

              suppose (((nl1 + 2) - 2) + k2) = ( - (((nl2 + 2) - 2) + k2));

              hence thesis by Lm4;

            end;

          end;

        end;

          suppose that

           A17: (s1 . ( DataLoc ((s1 . a),k1))) < 0 and

           A18: (s2 . ( DataLoc ((s2 . a),k1))) < 0 ;

          

           A19: x = (l2 + 1) by A9, A10, A18, SCMPDS_2: 57;

          x = (l1 + 1) by A5, A6, A17, SCMPDS_2: 57;

          hence x in {} by A3, A19, ABSVALUE: 27;

        end;

          suppose that

           A20: (s1 . ( DataLoc ((s1 . a),k1))) < 0 and

           A21: (s2 . ( DataLoc ((s2 . a),k1))) >= 0 ;

          reconsider n1 = l1 as Element of NAT ;

          set w1 = n1;

          

           A22: x = |.(m2 + k2).| by A9, A12, A21, SCMPDS_2: 57;

          

           A23: x = (n1 + 1) by A5, A6, A20, SCMPDS_2: 57

          .= (n1 + 1);

          thus x in {}

          proof

            per cases by A23, A22, ABSVALUE: 1;

              suppose (w1 + 1) = (m2 + k2);

              then (nl1 + 1) = (nl1 + (x1 + k2)) by A10, A11;

              hence thesis by Lm5;

            end;

              suppose (w1 + 1) = ( - (m2 + k2));

              hence thesis by A4, A10, A11, Lm6;

            end;

          end;

        end;

          suppose that

           A24: (s1 . ( DataLoc ((s1 . a),k1))) >= 0 and

           A25: (s2 . ( DataLoc ((s2 . a),k1))) < 0 ;

          reconsider n2 = l2 as Element of NAT ;

          

           A26: x = (n2 + 1) by A9, A10, A25, SCMPDS_2: 57

          .= (n2 + 1);

          set w2 = n2;

          

           A27: x = |.(m1 + k2).| by A5, A8, A24, SCMPDS_2: 57;

          thus x in {}

          proof

            per cases by A27, A26, ABSVALUE: 1;

              suppose (w2 + 1) = (m1 + k2);

              hence thesis by A1, A6, A7, Lm7;

            end;

              suppose (w2 + 1) = ( - (m1 + k2));

              hence thesis by A4, A6, A7, Lm8;

            end;

          end;

        end;

      end;

      thus thesis;

    end;

    registration

      let a, k1, k2;

      cluster ( JUMP ((a,k1) <>0_goto k2)) -> empty;

      coherence

      proof

        k2 = 5 or k2 <> 5;

        hence thesis by Lm9, Lm10;

      end;

      cluster ( JUMP ((a,k1) <=0_goto k2)) -> empty;

      coherence

      proof

        k2 = 5 or k2 <> 5;

        hence thesis by Lm11, Lm12;

      end;

      cluster ( JUMP ((a,k1) >=0_goto k2)) -> empty;

      coherence

      proof

        k2 = 5 or k2 <> 5;

        hence thesis by Lm13, Lm14;

      end;

    end

    theorem :: SCMPDS_9:18

    

     Th18: ( SUCC (l, SCMPDS )) = NAT

    proof

      thus ( SUCC (l, SCMPDS )) c= NAT ;

      let x be object;

      set X = the set of all (( NIC (i,l)) \ ( JUMP i)) where i be Element of the InstructionsF of SCMPDS ;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      reconsider xx = x as Element of NAT ;

      set i = ( goto (xx - l));

      ( NIC (i,l)) = { |.((xx - l) + l).|} by Th3

      .= {x} by ABSVALUE:def 1;

      then

       A1: x in (( NIC (i,l)) \ ( JUMP i)) by TARSKI:def 1;

      (( NIC (i,l)) \ ( JUMP i)) in X;

      hence thesis by A1, TARSKI:def 4;

    end;

    registration

      cluster SCMPDS -> non InsLoc-antisymmetric;

      coherence

      proof

        ( SUCC (2, SCMPDS )) = NAT by Th18;

        then

         A1: 2 <= (1, SCMPDS ) by AMI_WSTD: 33;

        ( SUCC (1, SCMPDS )) = NAT by Th18;

        then

         A2: 1 <= (2, SCMPDS ) by AMI_WSTD: 33;

        assume SCMPDS is InsLoc-antisymmetric;

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

      end;

    end

    registration

      cluster SCMPDS -> non weakly_standard;

      coherence by AMI_WSTD: 10;

    end