scmpds_4.miz



    begin

    reserve l,m,n for Nat,

i,j,k for Instruction of SCMPDS ,

I,J,K for Program of SCMPDS ,

p,q,r for PartState of SCMPDS ;

    reserve a,b,c for Int_position,

s,s1,s2 for State of SCMPDS ,

k1,k2 for Integer;

    theorem :: SCMPDS_4:1

    

     Th1: ( InsCode i) in { 0 , 1, 4, 5, 6, 14} or (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1)

    proof

      assume

       A1: not ( InsCode i) in { 0 , 1, 4, 5, 6, 14};

      

       A2: ( InsCode i) = 0 or ... or ( InsCode i) = 14 by SCMPDS_2: 6;

      per cases by A2, A1, ENUMSET1:def 4;

        suppose ( InsCode i) = 2;

        then ex a, k1 st i = (a := k1) by SCMPDS_2: 28;

        hence thesis by SCMPDS_2: 45;

      end;

        suppose ( InsCode i) = 3;

        then ex a, k1 st i = ( saveIC (a,k1)) by SCMPDS_2: 29;

        hence thesis by SCMPDS_2: 59;

      end;

        suppose ( InsCode i) = 7;

        then ex a, k1, k2 st i = ((a,k1) := k2) by SCMPDS_2: 33;

        hence thesis by SCMPDS_2: 46;

      end;

        suppose ( InsCode i) = 8;

        then ex a, k1, k2 st i = ( AddTo (a,k1,k2)) by SCMPDS_2: 34;

        hence thesis by SCMPDS_2: 48;

      end;

        suppose ( InsCode i) = 9;

        then ex a, b, k1, k2 st i = ( AddTo (a,k1,b,k2)) by SCMPDS_2: 35;

        hence thesis by SCMPDS_2: 49;

      end;

        suppose ( InsCode i) = 10;

        then ex a, b, k1, k2 st i = ( SubFrom (a,k1,b,k2)) by SCMPDS_2: 36;

        hence thesis by SCMPDS_2: 50;

      end;

        suppose ( InsCode i) = 11;

        then ex a, b, k1, k2 st i = ( MultBy (a,k1,b,k2)) by SCMPDS_2: 37;

        hence thesis by SCMPDS_2: 51;

      end;

        suppose ( InsCode i) = 12;

        then ex a, b, k1, k2 st i = ( Divide (a,k1,b,k2)) by SCMPDS_2: 38;

        hence thesis by SCMPDS_2: 52;

      end;

        suppose ( InsCode i) = 13;

        then ex a, b, k1, k2 st i = ((a,k1) := (b,k2)) by SCMPDS_2: 39;

        hence thesis by SCMPDS_2: 47;

      end;

    end;

    theorem :: SCMPDS_4:2

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

    proof

      let s1,s2 be State of SCMPDS such that

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

       A2: for a be Int_position holds (s1 . a) = (s2 . a);

      

       A3: the carrier of SCMPDS = ( {( IC SCMPDS )} \/ SCM-Data-Loc ) by SCMPDS_2: 84, STRUCT_0: 4

      .= ( {( IC SCMPDS )} \/ SCM-Data-Loc );

      

       A4: ( dom (s2 | ( dom s2))) = (( dom s2) /\ ( dom s2)) by RELAT_1: 61

      .= ( dom s2)

      .= ( {( IC SCMPDS )} \/ SCM-Data-Loc ) by A3, PARTFUN1:def 2;

      

       A5: ( dom (s1 | ( dom s1))) = (( dom s1) /\ ( dom s1)) by RELAT_1: 61

      .= ( dom s1)

      .= ( {( IC SCMPDS )} \/ SCM-Data-Loc ) by A3, PARTFUN1:def 2;

      

       A6: (s1 | ( dom s1)) = s1 & (s2 | ( dom s2)) = s2 by RELAT_1: 69;

      now

        let x be object;

        assume

         A7: x in ( {( IC SCMPDS )} \/ SCM-Data-Loc );

        per cases by A7, XBOOLE_0:def 3;

          suppose x in {( IC SCMPDS )};

          then

           A8: x = ( IC SCMPDS ) by TARSKI:def 1;

          

          hence ((s1 | ( dom s1)) . x) = ( IC s1) by A5, A7, FUNCT_1: 47

          .= ((s2 | ( dom s2)) . x) by A1, A4, A7, A8, FUNCT_1: 47;

        end;

          suppose x in SCM-Data-Loc ;

          then

           A9: x is Int_position by AMI_2:def 16;

          

          thus ((s1 | ( dom s1)) . x) = (s1 . x) by A5, A7, FUNCT_1: 47

          .= (s2 . x) by A2, A9

          .= ((s2 | ( dom s2)) . x) by A4, A7, FUNCT_1: 47;

        end;

      end;

      hence s1 = s2 by A6, A5, A4, FUNCT_1: 2;

    end;

    theorem :: SCMPDS_4:3

    

     Th3: for k1,k2 be Nat st k1 <> k2 holds ( DataLoc (k1, 0 )) <> ( DataLoc (k2, 0 ))

    proof

      let k1,k2 be Nat;

      assume

       A1: k1 <> k2;

      assume ( DataLoc (k1, 0 )) = ( DataLoc (k2, 0 ));

      then |.(k1 + 0 ).| = |.(k2 + 0 ).| by XTUPLE_0: 1;

      then k1 = |.k2.| by ABSVALUE:def 1;

      hence contradiction by A1, ABSVALUE:def 1;

    end;

    theorem :: SCMPDS_4:4

    

     Th4: for dl be Int_position holds ex i be Nat st dl = ( DataLoc (i, 0 ))

    proof

      let dl be Int_position;

      consider i be Nat such that

       A1: dl = [1, i] by AMI_2: 23, AMI_2:def 16;

      take i;

      thus thesis by A1, ABSVALUE:def 1;

    end;

    scheme :: SCMPDS_4:sch1

    SCMPDSEx { G( set) -> Integer , I() -> Element of NAT } :

ex S be State of SCMPDS st ( IC S) = I() & for i be Nat holds (S . ( DataLoc (i, 0 ))) = G(i);

      set S1 = {( IC SCMPDS )}, S2 = SCM-Data-Loc , S3 = NAT ;

      defpred P[ object, object] means ex m st $1 = ( IC SCMPDS ) & $2 = I() or $1 = ( DataLoc (m, 0 )) & $2 = G(m);

      

       A1: for e be object st e in the carrier of SCMPDS holds ex u be object st P[e, u]

      proof

        let e be object;

        assume e in the carrier of SCMPDS ;

        then

         A2: e in (S1 \/ S2) by SCMPDS_2: 84, STRUCT_0: 4;

        now

          per cases by A2, XBOOLE_0:def 3;

            case e in S1;

            hence e = ( IC SCMPDS ) by TARSKI:def 1;

          end;

            case e in S2;

            then e is Int_position by AMI_2:def 16;

            hence ex m st e = ( DataLoc (m, 0 )) by Th4;

          end;

        end;

        then

        consider m such that

         A3: e = ( IC SCMPDS ) or e = ( DataLoc (m, 0 ));

        per cases by A3;

          suppose

           A4: e = ( IC SCMPDS );

          take u = I();

          thus thesis by A4;

        end;

          suppose

           A5: e = ( DataLoc (m, 0 ));

          take u = G(m);

          thus thesis by A5;

        end;

      end;

      consider f be Function such that

       A6: ( dom f) = the carrier of SCMPDS and

       A7: for e be object st e in the carrier of SCMPDS holds P[e, (f . e)] from CLASSES1:sch 1( A1);

      

       A8: ( dom the Object-Kind of SCMPDS ) = the carrier of SCMPDS by FUNCT_2:def 1;

      now

        let x be object;

        assume

         A9: x in ( dom the Object-Kind of SCMPDS );

        then

         A10: x in (S1 \/ S2) by A8, SCMPDS_2: 84, STRUCT_0: 4;

        consider m such that

         A11: x = ( IC SCMPDS ) & (f . x) = I() or x = ( DataLoc (m, 0 )) & (f . x) = G(m) by A7, A8, A9;

        per cases by A10, XBOOLE_0:def 3;

          suppose x in S2;

          then x is Int_position by AMI_2:def 16;

          

          then (( the_Values_of SCMPDS ) . x) = ( Values ( DataLoc (m, 0 ))) by A11, SCMPDS_2: 43

          .= INT by SCMPDS_2: 5;

          hence (f . x) in (( the_Values_of SCMPDS ) . x) by A11, INT_1:def 2;

        end;

          suppose

           A12: x in S1;

          (( the_Values_of SCMPDS ) . x) = ( Values ( IC SCMPDS )) by TARSKI:def 1, A12

          .= NAT by MEMSTR_0:def 6;

          hence (f . x) in (( the_Values_of SCMPDS ) . x) by A11, A12, SCMPDS_2: 2, TARSKI:def 1;

        end;

      end;

      then

      reconsider f as State of SCMPDS by A6, A8, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

      consider m such that

       A13: ( IC SCMPDS ) = ( IC SCMPDS ) & (f . ( IC SCMPDS )) = I() or ( IC SCMPDS ) = ( DataLoc (m, 0 )) & (f . ( IC SCMPDS )) = G(m) by A7;

      take f;

      thus ( IC f) = I() by A13, SCMPDS_2: 43;

      let i be Nat;

      ex m st (( DataLoc (i, 0 )) = ( IC SCMPDS ) & (f . ( DataLoc (i, 0 ))) = I() or ( DataLoc (i, 0 )) = ( DataLoc (m, 0 )) & (f . ( DataLoc (i, 0 ))) = G(m)) by A7;

      hence thesis by Th3, SCMPDS_2: 43;

    end;

    theorem :: SCMPDS_4:5

    for s be State of SCMPDS holds ( dom s) = ( {( IC SCMPDS )} \/ SCM-Data-Loc )

    proof

      let s be State of SCMPDS ;

      ( dom s) = the carrier of SCMPDS by PARTFUN1:def 2;

      hence thesis by SCMPDS_2: 84, STRUCT_0: 4;

    end;

    theorem :: SCMPDS_4:6

    for s be State of SCMPDS , x be set st x in ( dom s) holds x is Int_position or x = ( IC SCMPDS )

    proof

      set S1 = {( IC SCMPDS )}, S2 = SCM-Data-Loc , S3 = NAT ;

      let s be State of SCMPDS ;

      let x be set;

      assume

       A1: x in ( dom s);

      ( dom s) = the carrier of SCMPDS by PARTFUN1:def 2;

      then x in (S1 \/ S2) by A1, SCMPDS_2: 84, STRUCT_0: 4;

      then x in S1 or x in S2 by XBOOLE_0:def 3;

      hence thesis by AMI_2:def 16, TARSKI:def 1;

    end;

    ::$Canceled

    theorem :: SCMPDS_4:8

    

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

    proof

      set T1 = {( IC SCMPDS )}, T2 = SCM-Data-Loc , T3 = NAT ;

      let s1,s2 be State of SCMPDS ;

       A1:

      now

        assume

         A2: for a be Int_position holds (s1 . a) = (s2 . a);

        hereby

          let x be set;

          assume x in SCM-Data-Loc ;

          then x is Int_position by AMI_2:def 16;

          hence (s1 . x) = (s2 . x) by A2;

        end;

      end;

      

       A3: (for x be set st x in SCM-Data-Loc holds (s1 . x) = (s2 . x)) implies for a be Int_position holds (s1 . a) = (s2 . a) by AMI_2:def 16;

      

       A4: ( dom s2) = the carrier of SCMPDS by PARTFUN1:def 2;

      ( dom s1) = the carrier of SCMPDS by PARTFUN1:def 2;

      hence thesis by A4, A1, A3, FUNCT_1: 95, SCMPDS_2: 84;

    end;

    reserve x for set;

    begin

    notation

      let I,J be Program of SCMPDS ;

      synonym I ';' J for I ^ J;

    end

    definition

      let I,J be Program of SCMPDS ;

      :: original: ';'

      redefine

      :: SCMPDS_4:def1

      func I ';' J -> Program of SCMPDS equals (I +* ( Shift (J,( card I))));

      compatibility by AFINSQ_1: 77;

      coherence ;

    end

    begin

    definition

      let i, J;

      :: SCMPDS_4:def2

      func i ';' J -> Program of SCMPDS equals (( Load i) ';' J);

      correctness ;

    end

    definition

      let I, j;

      :: SCMPDS_4:def3

      func I ';' j -> Program of SCMPDS equals (I ';' ( Load j));

      correctness ;

    end

    definition

      let i, j;

      :: SCMPDS_4:def4

      func i ';' j -> Program of SCMPDS equals (( Load i) ';' ( Load j));

      correctness ;

    end

    theorem :: SCMPDS_4:9

    (i ';' j) = (( Load i) ';' j);

    theorem :: SCMPDS_4:10

    (i ';' j) = (i ';' ( Load j));

    theorem :: SCMPDS_4:11

    ((I ';' J) ';' k) = (I ';' (J ';' k)) by AFINSQ_1: 27;

    theorem :: SCMPDS_4:12

    ((I ';' j) ';' K) = (I ';' (j ';' K)) by AFINSQ_1: 27;

    theorem :: SCMPDS_4:13

    ((I ';' j) ';' k) = (I ';' (j ';' k)) by AFINSQ_1: 27;

    theorem :: SCMPDS_4:14

    ((i ';' J) ';' K) = (i ';' (J ';' K)) by AFINSQ_1: 27;

    theorem :: SCMPDS_4:15

    ((i ';' J) ';' k) = (i ';' (J ';' k)) by AFINSQ_1: 27;

    theorem :: SCMPDS_4:16

    ((i ';' j) ';' K) = (i ';' (j ';' K)) by AFINSQ_1: 27;

    theorem :: SCMPDS_4:17

    ((i ';' j) ';' k) = (i ';' (j ';' k)) by AFINSQ_1: 27;

    reserve l,l1,loc for Nat;

    theorem :: SCMPDS_4:18

     not a in ( dom ( Start-At (l, SCMPDS )))

    proof

      

       A1: ( dom ( Start-At (l, SCMPDS ))) = {( IC SCMPDS )} by FUNCOP_1: 13;

      assume a in ( dom ( Start-At (l, SCMPDS )));

      then a = ( IC SCMPDS ) by A1, TARSKI:def 1;

      hence contradiction by SCMPDS_2: 43;

    end;

    definition

      let s be State of SCMPDS , li be Int_position, k be Integer;

      :: original: +*

      redefine

      func s +* (li,k) -> PartState of SCMPDS ;

      coherence

      proof

        

         A1: ( dom s) = the carrier of SCMPDS by PARTFUN1:def 2;

        now

          let x be object;

          assume x in ( dom (s +* (li,k)));

          then

           A2: x in ( dom s) by A1, PARTFUN1:def 2;

          per cases ;

            suppose

             A3: x = li;

            

            then

             A4: (( the_Values_of SCMPDS ) . x) = ( Values li)

            .= INT by SCMPDS_2: 5;

            ((s +* (li,k)) . x) = k by A1, A3, FUNCT_7: 31;

            hence ((s +* (li,k)) . x) in (( the_Values_of SCMPDS ) . x) by A4, INT_1:def 2;

          end;

            suppose x <> li;

            then ((s +* (li,k)) . x) = (s . x) by FUNCT_7: 32;

            hence ((s +* (li,k)) . x) in (( the_Values_of SCMPDS ) . x) by A2, FUNCT_1:def 14;

          end;

        end;

        hence thesis by FUNCT_1:def 14;

      end;

    end

    begin

    definition

      let I be Program of SCMPDS , s be State of SCMPDS ;

      let P be Instruction-Sequence of SCMPDS ;

      :: SCMPDS_4:def5

      func IExec (I,P,s) -> State of SCMPDS equals ( Result ((P +* ( stop I)),s));

      coherence ;

    end

    definition

      let I be Program of SCMPDS ;

      :: SCMPDS_4:def6

      attr I is paraclosed means

      : Def6: for s be 0 -started State of SCMPDS , n be Nat, P be Instruction-Sequence of SCMPDS st ( stop I) c= P holds ( IC ( Comput (P,s,n))) in ( dom ( stop I));

      :: SCMPDS_4:def7

      attr I is parahalting means for s be 0 -started State of SCMPDS , P be Instruction-Sequence of SCMPDS st ( stop I) c= P holds P halts_on s;

    end

    

     Lm1: ( Load ( halt SCMPDS )) is parahalting

    proof

      let s be 0 -started State of SCMPDS , P be Instruction-Sequence of SCMPDS ;

      set m = ( Load ( halt SCMPDS )), m0 = ( stop m);

      assume

       A1: m0 c= P;

      

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

      take 0 ;

      ( IC ( Comput (P,s, 0 ))) in NAT ;

      hence ( IC ( Comput (P,s, 0 ))) in ( dom P) by PARTFUN1:def 2;

      

       A3: (m . 0 ) = ( halt SCMPDS );

      ( dom m) = { 0 } by FUNCOP_1: 13;

      then

       A4: 0 in ( dom m) by TARSKI:def 1;

      then

       A5: 0 in ( dom m0) by FUNCT_4: 12;

      

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

      ( CurInstr (P,( Comput (P,s, 0 )))) = (m0 . 0 ) by A1, A5, A2, A6, GRFUNC_1: 2

      .= ( halt SCMPDS ) by A3, A4, AFINSQ_1:def 3;

      hence thesis;

    end;

    registration

      cluster parahalting for Program of SCMPDS ;

      existence by Lm1;

    end

    ::$Canceled

    theorem :: SCMPDS_4:20

    

     Th18: for P,Q be Instruction-Sequence of SCMPDS st Q = (P +* ((( IC s),(( IC s) + 1)) --> (( goto 1),( goto ( - 1))))) holds not Q halts_on s

    proof

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

       A1: Q = (P +* ((( IC s),(( IC s) + 1)) --> (( goto 1),( goto ( - 1)))));

      set m = ((( IC s),(( IC s) + 1)) --> (( goto 1),( goto ( - 1))));

      

       A2: (m . (( IC s) + 1)) = ( goto ( - 1)) by FUNCT_4: 63;

      ( IC s) <> (( IC s) + 1);

      then

       A3: (m . ( IC s)) = ( goto 1) by FUNCT_4: 63;

      defpred X[ Nat] means ( IC ( Comput (Q,s,$1))) = ( IC s) or ( IC ( Comput (Q,s,$1))) = (( IC s) + 1);

      

       A4: ( dom m) = {( IC s), (( IC s) + 1)} by FUNCT_4: 62;

      then

       A5: (( IC s) + 1) in ( dom m) by TARSKI:def 2;

      

       A6: ( IC s) in ( dom m) by A4, TARSKI:def 2;

      now

        let n;

        set Cn = ( Comput (Q,s,n));

        assume

         A7: ( IC Cn) = ( IC s) or ( IC Cn) = (( IC s) + 1);

        per cases by A7;

          case

           A8: ( IC Cn) = ( IC s);

          

          then

           A9: ( CurInstr (Q,Cn)) = (Q . ( IC s)) by PBOOLE: 143

          .= ( goto 1) by A6, A3, A1, FUNCT_4: 13;

          

          thus ( IC ( Comput (Q,s,(n + 1)))) = ( IC ( Following (Q,Cn))) by EXTPRO_1: 3

          .= ( ICplusConst (Cn,1)) by A9, SCMPDS_2: 54

          .= (( IC s) + 1) by A8, SCMPDS_3: 10;

        end;

          case

           A10: ( IC Cn) = (( IC s) + 1);

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

          

           A11: ex j be Element of NAT st j = ( IC Cn) & ( ICplusConst (Cn,( - 1))) = |.(j + ( - 1)).| by SCMPDS_2:def 18;

          

           A12: ( CurInstr (Q,( Comput (Q,s,n)))) = (Q . (( IC s) + 1)) by A10, PBOOLE: 143

          .= ( goto ( - 1)) by A5, A2, A1, FUNCT_4: 13;

          

          thus ( IC ( Comput (Q,s,(n + 1)))) = ( IC ( Following (Q,Cn))) by EXTPRO_1: 3

          .= |.((i + 4) + ( - 4)).| by A10, A12, A11, SCMPDS_2: 54

          .= ( IC s) by ABSVALUE:def 1;

        end;

      end;

      then

       A13: for n st X[n] holds X[(n + 1)];

      let nn be Nat;

      reconsider n = nn as Nat;

      assume ( IC ( Comput (Q,s,nn))) in ( dom Q);

      

       A14: X[ 0 ];

      

       A15: for n holds X[n] from NAT_1:sch 2( A14, A13);

      per cases by A15;

        suppose ( IC ( Comput (Q,s,n))) = ( IC s);

        

        then ( CurInstr (Q,( Comput (Q,s,n)))) = (Q . ( IC s)) by PBOOLE: 143

        .= ( goto 1) by A6, A3, A1, FUNCT_4: 13;

        hence thesis by SCMPDS_2: 73;

      end;

        suppose ( IC ( Comput (Q,s,n))) = (( IC s) + 1);

        

        then ( CurInstr (Q,( Comput (Q,s,n)))) = (Q . (( IC s) + 1)) by PBOOLE: 143

        .= ( goto ( - 1)) by A5, A2, A1, FUNCT_4: 13;

        hence thesis by SCMPDS_2: 73;

      end;

    end;

    theorem :: SCMPDS_4:21

    

     Th19: for P1,P2 be Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & (for m st m < n holds ( IC ( Comput (P2,s2,m))) in ( dom I)) holds for m st m <= n holds ( Comput (P1,s1,m)) = ( Comput (P2,s2,m))

    proof

      let P1,P2 be Instruction-Sequence of SCMPDS ;

      assume that

       A1: s1 = s2 and

       A2: I c= P1 and

       A3: I c= P2 and

       A4: for m st m < n holds ( IC ( Comput (P2,s2,m))) in ( dom I);

      defpred X[ Nat] means $1 <= n implies ( Comput (P1,s1,$1)) = ( Comput (P2,s2,$1));

      

       A5: for m st X[m] holds X[(m + 1)]

      proof

        let m such that

         A6: m <= n implies ( Comput (P1,s1,m)) = ( Comput (P2,s2,m));

        

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

        .= ( Exec (( CurInstr (P2,( Comput (P2,s2,m)))),( Comput (P2,s2,m))));

        

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

        .= ( Exec (( CurInstr (P1,( Comput (P1,s1,m)))),( Comput (P1,s1,m))));

        assume

         A9: (m + 1) <= n;

        

         A10: ( IC ( Comput (P2,s2,m))) in ( dom I) by A4, A9, NAT_1: 13;

        ( CurInstr (P1,( Comput (P1,s1,m)))) = (P1 . ( IC ( Comput (P1,s1,m)))) by PBOOLE: 143

        .= (I . ( IC ( Comput (P1,s1,m)))) by A2, A10, A9, A6, GRFUNC_1: 2, NAT_1: 13

        .= (P2 . ( IC ( Comput (P2,s2,m)))) by A3, A10, A9, A6, GRFUNC_1: 2, NAT_1: 13

        .= ( CurInstr (P2,( Comput (P2,s2,m)))) by PBOOLE: 143;

        hence thesis by A6, A8, A7, A9, NAT_1: 13;

      end;

      ( Comput (P1,s1, 0 )) = ( Comput (P2,s2, 0 )) by A1;

      then

       A11: X[ 0 ];

      thus for m holds X[m] from NAT_1:sch 2( A11, A5);

    end;

    reserve l1,l2 for Nat,

i1,i2 for Instruction of SCMPDS ;

    registration

      cluster parahalting -> paraclosed for Program of SCMPDS ;

      coherence

      proof

        let I be Program of SCMPDS ;

        assume

         A1: I is parahalting;

        let s be 0 -started State of SCMPDS , n be Nat, P be Instruction-Sequence of SCMPDS ;

        defpred X[ Nat] means not ( IC ( Comput (P,s,$1))) in ( dom ( stop I));

        assume

         A2: ( stop I) c= P;

        assume not ( IC ( Comput (P,s,n))) in ( dom ( stop I));

        then

         A3: ex n be Nat st X[n];

        consider n be Nat such that

         A4: X[n] and

         A5: for m be Nat st X[m] holds n <= m from NAT_1:sch 5( A3);

        reconsider n as Nat;

        

         A6: for m st m < n holds ( IC ( Comput (P,s,m))) in ( dom ( stop I)) by A5;

        set s2 = ( Comput (P,s,n)), Ig = ((( IC s2),(( IC s2) + 1)) --> (( goto 1),( goto ( - 1))));

        reconsider P0 = (P +* Ig) as Instruction-Sequence of SCMPDS ;

        reconsider P3 = (P +* (( IC s2),( goto 1))) as Instruction-Sequence of SCMPDS ;

        reconsider P2 = (P3 +* ((( IC s) + 12),( goto ( - 1)))) as Instruction-Sequence of SCMPDS ;

        reconsider P4 = (P3 +* ((( IC s2) + 1),( goto ( - 1)))) as Instruction-Sequence of SCMPDS ;

        

         A7: P0 = P4 by FUNCT_7: 139;

        ( stop I) c= P3 by A2, A4, FUNCT_7: 89;

        then

         A8: ( stop I) c= P0 by A7, A4, AFINSQ_1: 73, FUNCT_7: 89;

        then

         A9: ( Comput (P0,s,n)) = s2 by A2, A6, Th19;

         not P0 halts_on s2 by Th18;

        hence contradiction by A1, A8, A9, EXTPRO_1: 22;

      end;

    end

    begin

    definition

      let i be Instruction of SCMPDS ;

      let n be Nat;

      :: SCMPDS_4:def8

      pred i valid_at n means (( InsCode i) = 14 implies ex k1 st i = ( goto k1) & (n + k1) >= 0 ) & (( InsCode i) = 4 implies ex a, k1, k2 st i = ((a,k1) <>0_goto k2) & (n + k2) >= 0 ) & (( InsCode i) = 5 implies ex a, k1, k2 st i = ((a,k1) <=0_goto k2) & (n + k2) >= 0 ) & (( InsCode i) = 6 implies ex a, k1, k2 st i = ((a,k1) >=0_goto k2) & (n + k2) >= 0 );

    end

    reserve l for Nat;

    definition

      let IT be finitethe InstructionsF of SCMPDS -valued NAT -defined Function;

      :: SCMPDS_4:def9

      attr IT is shiftable means

      : Def9: for n, i st n in ( dom IT) & i = (IT . n) holds ( InsCode i) <> 1 & ( InsCode i) <> 3 & i valid_at n;

    end

    

     Lm2: ( Load ( halt SCMPDS )) is shiftable

    proof

      set m = ( Load ( halt SCMPDS ));

      

       A1: ( dom m) = { 0 } by FUNCOP_1: 13;

      let n, i;

      assume that

       A2: n in ( dom m) and

       A3: i = (m . n);

      

       A4: n = 0 by A1, A2, TARSKI:def 1;

      i = [ 0 , {} , {} ] by A3, A4, SCMPDS_2: 80;

      then ( InsCode i) = 0 ;

      hence thesis;

    end;

    theorem :: SCMPDS_4:22

    

     Th20: for i be Instruction of SCMPDS , m,n be Nat st i valid_at m & m <= n holds i valid_at n

    proof

      let i be Instruction of SCMPDS , m,n be Nat;

      assume that

       A1: i valid_at m and

       A2: m <= n;

       A3:

      now

        assume ( InsCode i) = 4;

        then

        consider a, k1, k2 such that

         A4: i = ((a,k1) <>0_goto k2) and

         A5: (m + k2) >= 0 by A1;

        take a, k1, k2;

        thus i = ((a,k1) <>0_goto k2) by A4;

        thus (n + k2) >= 0 by A2, A5, XREAL_1: 6;

      end;

       A6:

      now

        assume ( InsCode i) = 6;

        then

        consider a, k1, k2 such that

         A7: i = ((a,k1) >=0_goto k2) and

         A8: (m + k2) >= 0 by A1;

        take a, k1, k2;

        thus i = ((a,k1) >=0_goto k2) by A7;

        thus (n + k2) >= 0 by A2, A8, XREAL_1: 6;

      end;

       A9:

      now

        assume ( InsCode i) = 5;

        then

        consider a, k1, k2 such that

         A10: i = ((a,k1) <=0_goto k2) and

         A11: (m + k2) >= 0 by A1;

        take a, k1, k2;

        thus i = ((a,k1) <=0_goto k2) by A10;

        thus (n + k2) >= 0 by A2, A11, XREAL_1: 6;

      end;

      now

        assume ( InsCode i) = 14;

        then

        consider k1 such that

         A12: i = ( goto k1) and

         A13: (m + k1) >= 0 by A1;

        take k1;

        thus i = ( goto k1) by A12;

        thus (n + k1) >= 0 by A2, A13, XREAL_1: 6;

      end;

      hence thesis by A3, A9, A6;

    end;

    registration

      cluster parahalting shiftable for Program of SCMPDS ;

      existence by Lm1, Lm2;

    end

    definition

      let i be Instruction of SCMPDS ;

      :: SCMPDS_4:def10

      attr i is shiftable means

      : Def10: ( InsCode i) = 2 or ( InsCode i) <> 14 & ( InsCode i) > 6;

    end

    registration

      cluster shiftable for Instruction of SCMPDS ;

      existence

      proof

        take i = (( DataLoc ( 0 , 0 )) := 1);

        thus thesis;

      end;

    end

    registration

      let a, k1;

      cluster (a := k1) -> shiftable;

      coherence ;

    end

    registration

      let a, k1, k2;

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

      coherence ;

    end

    registration

      let a, k1, k2;

      cluster ( AddTo (a,k1,k2)) -> shiftable;

      coherence ;

    end

    registration

      let a, b, k1, k2;

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

      coherence

      proof

        ( InsCode ( AddTo (a,k1,b,k2))) = 9 by SCMPDS_2: 21;

        hence thesis;

      end;

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

      coherence

      proof

        ( InsCode ( SubFrom (a,k1,b,k2))) = 10 by SCMPDS_2: 22;

        hence thesis;

      end;

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

      coherence

      proof

        ( InsCode ( MultBy (a,k1,b,k2))) = 11 by SCMPDS_2: 23;

        hence thesis;

      end;

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

      coherence

      proof

        ( InsCode ( Divide (a,k1,b,k2))) = 12 by SCMPDS_2: 24;

        hence thesis;

      end;

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

      coherence

      proof

        ( InsCode ((a,k1) := (b,k2))) = 13 by SCMPDS_2: 25;

        hence thesis;

      end;

    end

    registration

      let I,J be shiftable Program of SCMPDS ;

      cluster (I ';' J) -> shiftable;

      coherence

      proof

        set IJ = (I ';' J);

        now

          set D = { (l + ( card I)) where l be Nat : l in ( dom J) };

          let n, i such that

           A1: n in ( dom IJ) and

           A2: i = (IJ . n);

          ( dom ( Shift (J,( card I)))) = D by VALUED_1:def 12;

          then

           A3: ( dom IJ) = (( dom I) \/ D) by FUNCT_4:def 1;

          per cases by A1, A3, XBOOLE_0:def 3;

            suppose

             A4: n in ( dom I);

            then (I . n) = i by A2, AFINSQ_1:def 3;

            hence ( InsCode i) <> 1 & ( InsCode i) <> 3 & i valid_at n by A4, Def9;

          end;

            suppose n in D;

            then

            consider l be Nat such that

             A5: n = (l + ( card I)) and

             A6: l in ( dom J);

            

             A7: (J . l) = i by A2, A5, A6, AFINSQ_1:def 3;

            hence ( InsCode i) <> 1 & ( InsCode i) <> 3 by A6, Def9;

            i valid_at l by A6, A7, Def9;

            hence i valid_at n by A5, Th20, NAT_1: 11;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let i be shiftable Instruction of SCMPDS ;

      cluster ( Load i) -> shiftable;

      coherence

      proof

        let p be Program of SCMPDS such that

         A1: p = ( Load i);

        let n, j such that

         A2: n in ( dom p) and

         A3: j = (p . n);

        ( dom p) = { 0 } by A1, FUNCOP_1: 13;

        then n = 0 by A2, TARSKI:def 1;

        then

         A4: j = i by A3, A1;

        hence ( InsCode j) <> 1 by Def10;

        thus ( InsCode j) <> 3 by A4, Def10;

        ( InsCode j) <> 4 & ( InsCode j) <> 5 & ( InsCode j) <> 6 & ( InsCode j) <> 14 by A4, Def10;

        hence j valid_at n;

      end;

    end

    registration

      let i be shiftable Instruction of SCMPDS , J be shiftable Program of SCMPDS ;

      cluster (i ';' J) -> shiftable;

      coherence ;

    end

    registration

      let I be shiftable Program of SCMPDS , j be shiftable Instruction of SCMPDS ;

      cluster (I ';' j) -> shiftable;

      coherence ;

    end

    registration

      let i,j be shiftable Instruction of SCMPDS ;

      cluster (i ';' j) -> shiftable;

      coherence ;

    end

    registration

      cluster ( Stop SCMPDS ) -> parahalting shiftable;

      coherence by Lm1, Lm2;

    end

    registration

      let I be shiftable Program of SCMPDS ;

      cluster ( stop I) -> shiftable;

      coherence ;

    end

    theorem :: SCMPDS_4:23

    for I be shiftable Program of SCMPDS , k1 be Integer st (( card I) + k1) >= 0 holds (I ';' ( goto k1)) is shiftable

    proof

      let I be shiftable Program of SCMPDS , k1 be Integer;

      set J = ( Load ( goto k1));

      set Ig = (I ';' ( goto k1));

      assume

       A1: (( card I) + k1) >= 0 ;

      now

        set D = { (l + ( card I)) where l be Nat : l in ( dom J) };

        let n, i such that

         A2: n in ( dom Ig) and

         A3: i = (Ig . n);

        ( dom ( Shift (J,( card I)))) = D by VALUED_1:def 12;

        then

         A4: ( dom Ig) = (( dom I) \/ D) by FUNCT_4:def 1;

        per cases by A2, A4, XBOOLE_0:def 3;

          suppose

           A5: n in ( dom I);

          then (I . n) = i by A3, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3 & i valid_at n by A5, Def9;

        end;

          suppose n in D;

          then

          consider l be Nat such that

           A6: n = (l + ( card I)) and

           A7: l in ( dom J);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then

           A8: l = 0 by A7, TARSKI:def 1;

          

          then

           A9: ( goto k1) = (J . l)

          .= i by A3, A6, A7, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          thus i valid_at n by A1, A6, A8, A9;

        end;

      end;

      hence thesis;

    end;

    registration

      let n be Nat;

      cluster ( Load ( goto n)) -> shiftable;

      coherence

      proof

        set k1 = n;

        set J = ( Load ( goto k1));

        now

          let n, i such that

           A1: n in ( dom J) and

           A2: i = (J . n);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then n = 0 by A1, TARSKI:def 1;

          then

           A3: ( goto k1) = i by A2;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          

           A4: (n + k1) >= 0 & ( InsCode i) <> 6 by A3;

          thus i valid_at n by A3, A4;

        end;

        hence thesis;

      end;

    end

    theorem :: SCMPDS_4:24

    for I be shiftable Program of SCMPDS , k1,k2 be Integer, a be Int_position st (( card I) + k2) >= 0 holds (I ';' ((a,k1) <>0_goto k2)) is shiftable

    proof

      let I be shiftable Program of SCMPDS , k1,k2 be Integer, a be Int_position;

      set ii = ((a,k1) <>0_goto k2), J = ( Load ii);

      set Ig = (I ';' ii);

      assume

       A1: (( card I) + k2) >= 0 ;

      now

        set D = { (l + ( card I)) where l be Nat : l in ( dom J) };

        let n, i such that

         A2: n in ( dom Ig) and

         A3: i = (Ig . n);

        ( dom ( Shift (J,( card I)))) = D by VALUED_1:def 12;

        then

         A4: ( dom Ig) = (( dom I) \/ D) by FUNCT_4:def 1;

        per cases by A2, A4, XBOOLE_0:def 3;

          suppose

           A5: n in ( dom I);

          then (I . n) = i by A3, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3 & i valid_at n by A5, Def9;

        end;

          suppose n in D;

          then

          consider l be Nat such that

           A6: n = (l + ( card I)) and

           A7: l in ( dom J);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then

           A8: l = 0 by A7, TARSKI:def 1;

          

          then

           A9: ii = (J . l)

          .= i by A3, A6, A7, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          thus i valid_at n by A1, A6, A8, A9;

        end;

      end;

      hence thesis;

    end;

    registration

      let k1 be Integer, a be Int_position, n be Nat;

      cluster ( Load ((a,k1) <>0_goto n)) -> shiftable;

      coherence

      proof

        set k2 = n;

        set ii = ((a,k1) <>0_goto k2), J = ( Load ii);

        now

          let n, i such that

           A1: n in ( dom J) and

           A2: i = (J . n);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then n = 0 by A1, TARSKI:def 1;

          then

           A3: ii = i by A2;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          

           A4: (n + k2) >= 0 & ( InsCode i) <> 6 & ( InsCode i) <> 14 by A3;

          thus i valid_at n by A3, A4;

        end;

        hence thesis;

      end;

    end

    theorem :: SCMPDS_4:25

    for I be shiftable Program of SCMPDS , k1,k2 be Integer, a be Int_position st (( card I) + k2) >= 0 holds (I ';' ((a,k1) <=0_goto k2)) is shiftable

    proof

      let I be shiftable Program of SCMPDS , k1,k2 be Integer, a be Int_position;

      set ii = ((a,k1) <=0_goto k2), J = ( Load ii);

      set Ig = (I ';' ii);

      assume

       A1: (( card I) + k2) >= 0 ;

      now

        set D = { (l + ( card I)) where l be Nat : l in ( dom J) };

        let n, i such that

         A2: n in ( dom Ig) and

         A3: i = (Ig . n);

        ( dom ( Shift (J,( card I)))) = D by VALUED_1:def 12;

        then

         A4: ( dom Ig) = (( dom I) \/ D) by FUNCT_4:def 1;

        per cases by A2, A4, XBOOLE_0:def 3;

          suppose

           A5: n in ( dom I);

          then (I . n) = i by A3, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3 & i valid_at n by A5, Def9;

        end;

          suppose n in D;

          then

          consider l be Nat such that

           A6: n = (l + ( card I)) and

           A7: l in ( dom J);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then

           A8: l = 0 by A7, TARSKI:def 1;

          

          then

           A9: ii = (J . l)

          .= i by A3, A6, A7, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          thus i valid_at n by A1, A6, A8, A9;

        end;

      end;

      hence thesis;

    end;

    registration

      let k1 be Integer, a be Int_position, n be Nat;

      cluster ( Load ((a,k1) <=0_goto n)) -> shiftable;

      coherence

      proof

        set k2 = n;

        set ii = ((a,k1) <=0_goto k2), J = ( Load ii);

        now

          let n, i such that

           A1: n in ( dom J) and

           A2: i = (J . n);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then n = 0 by A1, TARSKI:def 1;

          then

           A3: ii = i by A2;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          

           A4: (n + k2) >= 0 & ( InsCode i) <> 6 & ( InsCode i) <> 14 by A3;

          thus i valid_at n by A3, A4;

        end;

        hence thesis;

      end;

    end

    theorem :: SCMPDS_4:26

    for I be shiftable Program of SCMPDS , k1,k2 be Integer, a be Int_position st (( card I) + k2) >= 0 holds (I ';' ((a,k1) >=0_goto k2)) is shiftable

    proof

      let I be shiftable Program of SCMPDS , k1,k2 be Integer, a be Int_position;

      set ii = ((a,k1) >=0_goto k2), J = ( Load ii);

      set Ig = (I ';' ii);

      assume

       A1: (( card I) + k2) >= 0 ;

      now

        set D = { (l + ( card I)) where l be Nat : l in ( dom J) };

        let n, i such that

         A2: n in ( dom Ig) and

         A3: i = (Ig . n);

        ( dom ( Shift (J,( card I)))) = D by VALUED_1:def 12;

        then

         A4: ( dom Ig) = (( dom I) \/ D) by FUNCT_4:def 1;

        per cases by A2, A4, XBOOLE_0:def 3;

          suppose

           A5: n in ( dom I);

          then (I . n) = i by A3, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3 & i valid_at n by A5, Def9;

        end;

          suppose n in D;

          then

          consider l be Nat such that

           A6: n = (l + ( card I)) and

           A7: l in ( dom J);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then

           A8: l = 0 by A7, TARSKI:def 1;

          

          then

           A9: ii = (J . l)

          .= i by A3, A6, A7, AFINSQ_1:def 3;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          thus i valid_at n by A1, A6, A8, A9;

        end;

      end;

      hence thesis;

    end;

    registration

      let k1 be Integer, a be Int_position, n be Nat;

      cluster ( Load ((a,k1) >=0_goto n)) -> shiftable;

      coherence

      proof

        set k2 = n;

        set ii = ((a,k1) >=0_goto k2), J = ( Load ii);

        now

          let n, i such that

           A1: n in ( dom J) and

           A2: i = (J . n);

          ( dom J) = { 0 } by FUNCOP_1: 13;

          then n = 0 by A1, TARSKI:def 1;

          then

           A3: ii = i by A2;

          hence ( InsCode i) <> 1 & ( InsCode i) <> 3;

          

           A4: (n + k2) >= 0 & ( InsCode i) <> 5 & ( InsCode i) <> 14 by A3;

          thus i valid_at n by A3, A4;

        end;

        hence thesis;

      end;

    end

    theorem :: SCMPDS_4:27

    

     Th25: for s1,s2 be State of SCMPDS , n,m be Nat, k1 be Integer st ( IC s1) = m & (m + k1) >= 0 & (( IC s1) + n) = ( IC s2) holds (( ICplusConst (s1,k1)) + n) = ( ICplusConst (s2,k1))

    proof

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

      assume that

       A1: ( IC s1) = m and

       A2: (m + k1) >= 0 and

       A3: (( IC s1) + n) = ( IC s2);

      reconsider nk = ( ICplusConst (s1,k1)) as Element of NAT ;

      reconsider mk = (m + k1) as Element of NAT by A2, INT_1: 3;

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

      then (ex n2 be Element of NAT st n2 = ( IC s2) & ( ICplusConst (s2,k1)) = |.(n2 + k1).|) & nk = mk by A1, ABSVALUE:def 1, SCMPDS_2:def 18;

      hence thesis by A1, A3, ABSVALUE:def 1;

    end;

    theorem :: SCMPDS_4:28

    

     Th26: for s1,s2 be State of SCMPDS , n,m be Nat, i be Instruction of SCMPDS holds ( IC s1) = m & i valid_at m & ( InsCode i) <> 1 & ( InsCode i) <> 3 & (( IC s1) + n) = ( IC s2) & ( DataPart s1) = ( DataPart s2) implies (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) & ( DataPart ( Exec (i,s1))) = ( DataPart ( Exec (i,s2)))

    proof

      let s1,s2 be State of SCMPDS , n,m be Nat;

      let i be Instruction of SCMPDS ;

      assume that

       A1: ( IC s1) = m and

       A2: i valid_at m and

       A3: ( InsCode i) <> 1 & ( InsCode i) <> 3 and

       A4: (( IC s1) + n) = ( IC s2) and

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

       A6:

      now

        let a, k1;

        

        thus (s1 . ( DataLoc ((s1 . a),k1))) = (s1 . ( DataLoc ((s2 . a),k1))) by A5, Th7

        .= (s2 . ( DataLoc ((s2 . a),k1))) by A5, Th7;

      end;

      reconsider k1 = ( IC s1) as Nat;

      set Ci = ( InsCode i);

      

       A7: ((( IC s1) + 1) + n) = (( IC s2) + 1) by A4;

       A8:

      now

        assume Ci <> 0 & Ci <> 14 & Ci <> 1 & Ci <> 4 & Ci <> 5 & Ci <> 6;

        then

         A9: not Ci in { 0 , 1, 4, 5, 6, 14} by ENUMSET1:def 4;

        then ( IC ( Exec (i,s1))) = (( IC s1) + 1) by Th1;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A7, A9, Th1;

      end;

      Ci = 0 or ... or Ci = 14 by SCMPDS_2: 6;

      per cases by A3;

        suppose Ci = 0 ;

        then

         A10: ( Exec (i,s1)) = s1 & ( Exec (i,s2)) = s2 by SCMPDS_2: 86;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A4;

        thus ( DataPart ( Exec (i,s1))) = ( DataPart ( Exec (i,s2))) by A5, A10;

      end;

        suppose Ci = 14;

        then

        consider k1 such that

         A11: i = ( goto k1) and

         A12: (m + k1) >= 0 by A2;

        ( IC ( Exec (i,s1))) = ( ICplusConst (s1,k1)) by A11, SCMPDS_2: 54;

        

        hence (( IC ( Exec (i,s1))) + n) = ( ICplusConst (s2,k1)) by A1, A4, A12, Th25

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

        now

          let a;

          

          thus (( Exec (i,s1)) . a) = (s1 . a) by A11, SCMPDS_2: 54

          .= (s2 . a) by A5, Th7

          .= (( Exec (i,s2)) . a) by A11, SCMPDS_2: 54;

        end;

        hence thesis by Th7;

      end;

        suppose

         A13: Ci = 2;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, k1 such that

         A14: i = (a := k1) by A13, SCMPDS_2: 28;

        now

          let b;

          per cases ;

            suppose

             A15: a = b;

            

            hence (( Exec (i,s1)) . b) = k1 by A14, SCMPDS_2: 45

            .= (( Exec (i,s2)) . b) by A14, A15, SCMPDS_2: 45;

          end;

            suppose

             A16: a <> b;

            

            hence (( Exec (i,s1)) . b) = (s1 . b) by A14, SCMPDS_2: 45

            .= (s2 . b) by A5, Th7

            .= (( Exec (i,s2)) . b) by A14, A16, SCMPDS_2: 45;

          end;

        end;

        hence thesis by Th7;

      end;

        suppose Ci = 4;

        then

        consider a, k1, k2 such that

         A17: i = ((a,k1) <>0_goto k2) and

         A18: (m + k2) >= 0 by A2;

        hereby

          per cases ;

            suppose

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

            then

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

            ( IC ( Exec (i,s1))) = ( ICplusConst (s1,k2)) by A17, A19, SCMPDS_2: 55;

            

            hence (( IC ( Exec (i,s1))) + n) = ( ICplusConst (s2,k2)) by A1, A4, A18, Th25

            .= ( IC ( Exec (i,s2))) by A17, A20, SCMPDS_2: 55;

          end;

            suppose (s1 . ( DataLoc ((s1 . a),k1))) = 0 ;

            then (s2 . ( DataLoc ((s2 . a),k1))) = 0 & ( IC ( Exec (i,s1))) = (( IC s1) + 1) by A6, A17, SCMPDS_2: 55;

            hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A7, A17, SCMPDS_2: 55;

          end;

        end;

        now

          let a;

          

          thus (( Exec (i,s1)) . a) = (s1 . a) by A17, SCMPDS_2: 55

          .= (s2 . a) by A5, Th7

          .= (( Exec (i,s2)) . a) by A17, SCMPDS_2: 55;

        end;

        hence thesis by Th7;

      end;

        suppose Ci = 5;

        then

        consider a, k1, k2 such that

         A21: i = ((a,k1) <=0_goto k2) and

         A22: (m + k2) >= 0 by A2;

        hereby

          per cases ;

            suppose

             A23: (s1 . ( DataLoc ((s1 . a),k1))) <= 0 ;

            then

             A24: (s2 . ( DataLoc ((s2 . a),k1))) <= 0 by A6;

            ( IC ( Exec (i,s1))) = ( ICplusConst (s1,k2)) by A21, A23, SCMPDS_2: 56;

            

            hence (( IC ( Exec (i,s1))) + n) = ( ICplusConst (s2,k2)) by A1, A4, A22, Th25

            .= ( IC ( Exec (i,s2))) by A21, A24, SCMPDS_2: 56;

          end;

            suppose (s1 . ( DataLoc ((s1 . a),k1))) > 0 ;

            then (s2 . ( DataLoc ((s2 . a),k1))) > 0 & ( IC ( Exec (i,s1))) = (( IC s1) + 1) by A6, A21, SCMPDS_2: 56;

            hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A7, A21, SCMPDS_2: 56;

          end;

        end;

        now

          let a;

          

          thus (( Exec (i,s1)) . a) = (s1 . a) by A21, SCMPDS_2: 56

          .= (s2 . a) by A5, Th7

          .= (( Exec (i,s2)) . a) by A21, SCMPDS_2: 56;

        end;

        hence thesis by Th7;

      end;

        suppose Ci = 6;

        then

        consider a, k1, k2 such that

         A25: i = ((a,k1) >=0_goto k2) and

         A26: (m + k2) >= 0 by A2;

        hereby

          per cases ;

            suppose

             A27: (s1 . ( DataLoc ((s1 . a),k1))) >= 0 ;

            then

             A28: (s2 . ( DataLoc ((s2 . a),k1))) >= 0 by A6;

            ( IC ( Exec (i,s1))) = ( ICplusConst (s1,k2)) by A25, A27, SCMPDS_2: 57;

            

            hence (( IC ( Exec (i,s1))) + n) = ( ICplusConst (s2,k2)) by A1, A4, A26, Th25

            .= ( IC ( Exec (i,s2))) by A25, A28, SCMPDS_2: 57;

          end;

            suppose (s1 . ( DataLoc ((s1 . a),k1))) < 0 ;

            then (s2 . ( DataLoc ((s2 . a),k1))) < 0 & ( IC ( Exec (i,s1))) = (( IC s1) + 1) by A6, A25, SCMPDS_2: 57;

            hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A7, A25, SCMPDS_2: 57;

          end;

        end;

        now

          let a;

          

          thus (( Exec (i,s1)) . a) = (s1 . a) by A25, SCMPDS_2: 57

          .= (s2 . a) by A5, Th7

          .= (( Exec (i,s2)) . a) by A25, SCMPDS_2: 57;

        end;

        hence thesis by Th7;

      end;

        suppose

         A29: Ci = 7;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, k1, k2 such that

         A30: i = ((a,k1) := k2) by A29, SCMPDS_2: 33;

        now

          let b;

          per cases ;

            suppose

             A31: ( DataLoc ((s1 . a),k1)) = b;

            then

             A32: ( DataLoc ((s2 . a),k1)) = b by A5, Th7;

            

            thus (( Exec (i,s1)) . b) = k2 by A30, A31, SCMPDS_2: 46

            .= (( Exec (i,s2)) . b) by A30, A32, SCMPDS_2: 46;

          end;

            suppose

             A33: ( DataLoc ((s1 . a),k1)) <> b;

            then

             A34: ( DataLoc ((s2 . a),k1)) <> b by A5, Th7;

            

            thus (( Exec (i,s1)) . b) = (s1 . b) by A30, A33, SCMPDS_2: 46

            .= (s2 . b) by A5, Th7

            .= (( Exec (i,s2)) . b) by A30, A34, SCMPDS_2: 46;

          end;

        end;

        hence thesis by Th7;

      end;

        suppose

         A35: Ci = 8;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, k1, k2 such that

         A36: i = ( AddTo (a,k1,k2)) by A35, SCMPDS_2: 34;

        now

          let b;

          per cases ;

            suppose

             A37: ( DataLoc ((s1 . a),k1)) = b;

            then

             A38: ( DataLoc ((s2 . a),k1)) = b by A5, Th7;

            

            thus (( Exec (i,s1)) . b) = ((s1 . ( DataLoc ((s1 . a),k1))) + k2) by A36, A37, SCMPDS_2: 48

            .= ((s2 . ( DataLoc ((s2 . a),k1))) + k2) by A6

            .= (( Exec (i,s2)) . b) by A36, A38, SCMPDS_2: 48;

          end;

            suppose

             A39: ( DataLoc ((s1 . a),k1)) <> b;

            then

             A40: ( DataLoc ((s2 . a),k1)) <> b by A5, Th7;

            

            thus (( Exec (i,s1)) . b) = (s1 . b) by A36, A39, SCMPDS_2: 48

            .= (s2 . b) by A5, Th7

            .= (( Exec (i,s2)) . b) by A36, A40, SCMPDS_2: 48;

          end;

        end;

        hence thesis by Th7;

      end;

        suppose

         A41: Ci = 9;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, b, k1, k2 such that

         A42: i = ( AddTo (a,k1,b,k2)) by A41, SCMPDS_2: 35;

        now

          let c;

          per cases ;

            suppose

             A43: ( DataLoc ((s1 . a),k1)) = c;

            then

             A44: ( DataLoc ((s2 . a),k1)) = c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = ((s1 . ( DataLoc ((s1 . a),k1))) + (s1 . ( DataLoc ((s1 . b),k2)))) by A42, A43, SCMPDS_2: 49

            .= ((s2 . ( DataLoc ((s2 . a),k1))) + (s1 . ( DataLoc ((s1 . b),k2)))) by A6

            .= ((s2 . ( DataLoc ((s2 . a),k1))) + (s2 . ( DataLoc ((s2 . b),k2)))) by A6

            .= (( Exec (i,s2)) . c) by A42, A44, SCMPDS_2: 49;

          end;

            suppose

             A45: ( DataLoc ((s1 . a),k1)) <> c;

            then

             A46: ( DataLoc ((s2 . a),k1)) <> c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A42, A45, SCMPDS_2: 49

            .= (s2 . c) by A5, Th7

            .= (( Exec (i,s2)) . c) by A42, A46, SCMPDS_2: 49;

          end;

        end;

        hence thesis by Th7;

      end;

        suppose

         A47: Ci = 10;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, b, k1, k2 such that

         A48: i = ( SubFrom (a,k1,b,k2)) by A47, SCMPDS_2: 36;

        now

          let c;

          per cases ;

            suppose

             A49: ( DataLoc ((s1 . a),k1)) = c;

            then

             A50: ( DataLoc ((s2 . a),k1)) = c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = ((s1 . ( DataLoc ((s1 . a),k1))) - (s1 . ( DataLoc ((s1 . b),k2)))) by A48, A49, SCMPDS_2: 50

            .= ((s2 . ( DataLoc ((s2 . a),k1))) - (s1 . ( DataLoc ((s1 . b),k2)))) by A6

            .= ((s2 . ( DataLoc ((s2 . a),k1))) - (s2 . ( DataLoc ((s2 . b),k2)))) by A6

            .= (( Exec (i,s2)) . c) by A48, A50, SCMPDS_2: 50;

          end;

            suppose

             A51: ( DataLoc ((s1 . a),k1)) <> c;

            then

             A52: ( DataLoc ((s2 . a),k1)) <> c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A48, A51, SCMPDS_2: 50

            .= (s2 . c) by A5, Th7

            .= (( Exec (i,s2)) . c) by A48, A52, SCMPDS_2: 50;

          end;

        end;

        hence thesis by Th7;

      end;

        suppose

         A53: Ci = 11;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, b, k1, k2 such that

         A54: i = ( MultBy (a,k1,b,k2)) by A53, SCMPDS_2: 37;

        now

          let c;

          per cases ;

            suppose

             A55: ( DataLoc ((s1 . a),k1)) = c;

            then

             A56: ( DataLoc ((s2 . a),k1)) = c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = ((s1 . ( DataLoc ((s1 . a),k1))) * (s1 . ( DataLoc ((s1 . b),k2)))) by A54, A55, SCMPDS_2: 51

            .= ((s2 . ( DataLoc ((s2 . a),k1))) * (s1 . ( DataLoc ((s1 . b),k2)))) by A6

            .= ((s2 . ( DataLoc ((s2 . a),k1))) * (s2 . ( DataLoc ((s2 . b),k2)))) by A6

            .= (( Exec (i,s2)) . c) by A54, A56, SCMPDS_2: 51;

          end;

            suppose

             A57: ( DataLoc ((s1 . a),k1)) <> c;

            then

             A58: ( DataLoc ((s2 . a),k1)) <> c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A54, A57, SCMPDS_2: 51

            .= (s2 . c) by A5, Th7

            .= (( Exec (i,s2)) . c) by A54, A58, SCMPDS_2: 51;

          end;

        end;

        hence thesis by Th7;

      end;

        suppose

         A59: Ci = 12;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, b, k1, k2 such that

         A60: i = ( Divide (a,k1,b,k2)) by A59, SCMPDS_2: 38;

        now

          let c;

          per cases ;

            suppose

             A61: ( DataLoc ((s1 . b),k2)) = c;

            then

             A62: ( DataLoc ((s2 . b),k2)) = c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = ((s1 . ( DataLoc ((s1 . a),k1))) mod (s1 . ( DataLoc ((s1 . b),k2)))) by A60, A61, SCMPDS_2: 52

            .= ((s2 . ( DataLoc ((s2 . a),k1))) mod (s1 . ( DataLoc ((s1 . b),k2)))) by A6

            .= ((s2 . ( DataLoc ((s2 . a),k1))) mod (s2 . ( DataLoc ((s2 . b),k2)))) by A6

            .= (( Exec (i,s2)) . c) by A60, A62, SCMPDS_2: 52;

          end;

            suppose

             A63: ( DataLoc ((s1 . b),k2)) <> c;

            then

             A64: ( DataLoc ((s2 . b),k2)) <> c by A5, Th7;

            hereby

              per cases ;

                suppose

                 A65: ( DataLoc ((s1 . a),k1)) <> c;

                then

                 A66: ( DataLoc ((s2 . a),k1)) <> c by A5, Th7;

                

                thus (( Exec (i,s1)) . c) = (s1 . c) by A60, A63, A65, SCMPDS_2: 52

                .= (s2 . c) by A5, Th7

                .= (( Exec (i,s2)) . c) by A60, A64, A66, SCMPDS_2: 52;

              end;

                suppose

                 A67: ( DataLoc ((s1 . a),k1)) = c;

                then

                 A68: ( DataLoc ((s2 . a),k1)) = c by A5, Th7;

                

                thus (( Exec (i,s1)) . c) = ((s1 . ( DataLoc ((s1 . a),k1))) div (s1 . ( DataLoc ((s1 . b),k2)))) by A60, A63, A67, SCMPDS_2: 52

                .= ((s2 . ( DataLoc ((s2 . a),k1))) div (s1 . ( DataLoc ((s1 . b),k2)))) by A6

                .= ((s2 . ( DataLoc ((s2 . a),k1))) div (s2 . ( DataLoc ((s2 . b),k2)))) by A6

                .= (( Exec (i,s2)) . c) by A60, A64, A68, SCMPDS_2: 52;

              end;

            end;

          end;

        end;

        hence thesis by Th7;

      end;

        suppose

         A69: Ci = 13;

        hence (( IC ( Exec (i,s1))) + n) = ( IC ( Exec (i,s2))) by A8;

        consider a, b, k1, k2 such that

         A70: i = ((a,k1) := (b,k2)) by A69, SCMPDS_2: 39;

        now

          let c;

          per cases ;

            suppose

             A71: ( DataLoc ((s1 . a),k1)) = c;

            then

             A72: ( DataLoc ((s2 . a),k1)) = c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = (s1 . ( DataLoc ((s1 . b),k2))) by A70, A71, SCMPDS_2: 47

            .= (s2 . ( DataLoc ((s2 . b),k2))) by A6

            .= (( Exec (i,s2)) . c) by A70, A72, SCMPDS_2: 47;

          end;

            suppose

             A73: ( DataLoc ((s1 . a),k1)) <> c;

            then

             A74: ( DataLoc ((s2 . a),k1)) <> c by A5, Th7;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A70, A73, SCMPDS_2: 47

            .= (s2 . c) by A5, Th7

            .= (( Exec (i,s2)) . c) by A70, A74, SCMPDS_2: 47;

          end;

        end;

        hence thesis by Th7;

      end;

    end;

    theorem :: SCMPDS_4:29

    for P1,P2 be Instruction-Sequence of SCMPDS holds for s1 be 0 -started State of SCMPDS holds for J be parahalting shiftable Program of SCMPDS st ( stop J) c= P1 holds for n be Nat st ( Shift (( stop J),n)) c= P2 & ( IC s2) = n & ( DataPart s1) = ( DataPart s2) holds for i be Nat holds (( IC ( Comput (P1,s1,i))) + n) = ( IC ( Comput (P2,s2,i))) & ( CurInstr (P1,( Comput (P1,s1,i)))) = ( CurInstr (P2,( Comput (P2,s2,i)))) & ( DataPart ( Comput (P1,s1,i))) = ( DataPart ( Comput (P2,s2,i)))

    proof

      let P1,P2 be Instruction-Sequence of SCMPDS ;

      let s1 be 0 -started State of SCMPDS ;

      let I be parahalting shiftable Program of SCMPDS ;

      set SI = ( stop I);

      assume

       A1: SI c= P1;

      let n be Nat;

      assume that

       A2: ( Shift (SI,n)) c= P2 and

       A3: ( IC s2) = n and

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

      

       A5: 0 in ( dom SI) by COMPOS_1: 36;

      then

       A6: ( 0 + n) in ( dom ( Shift (SI,n))) by VALUED_1: 24;

      defpred P[ Nat] means (( IC ( Comput (P1,s1,$1))) + n) = ( IC ( Comput (P2,s2,$1))) & ( CurInstr (P1,( Comput (P1,s1,$1)))) = ( CurInstr (P2,( Comput (P2,s2,$1)))) & ( DataPart ( Comput (P1,s1,$1))) = ( DataPart ( Comput (P2,s2,$1)));

      

       A7: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A8: P[k];

        reconsider m = ( IC ( Comput (P1,s1,k))) as Nat;

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

        

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

        .= ( Exec (( CurInstr (P1,( Comput (P1,s1,k)))),( Comput (P1,s1,k))));

        reconsider l = ( IC ( Comput (P1,s1,(k + 1)))) as Nat;

        

         A10: ( IC ( Comput (P1,s1,(k + 1)))) in ( dom SI) by A1, Def6;

        then

         A11: (l + n) in ( dom ( Shift (SI,n))) by VALUED_1: 24;

        

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

        .= ( Exec (( CurInstr (P2,( Comput (P2,s2,k)))),( Comput (P2,s2,k))));

        

         A13: ( IC ( Comput (P1,s1,k))) in ( dom SI) by A1, Def6;

        

         A14: i = (P1 . ( IC ( Comput (P1,s1,k)))) by PBOOLE: 143

        .= (SI . ( IC ( Comput (P1,s1,k)))) by A1, A13, GRFUNC_1: 2;

        then

         A15: ( InsCode i) <> 1 & ( InsCode i) <> 3 by A13, Def9;

        

         A16: i valid_at m by A13, A14, Def9;

        hence

         A17: (( IC ( Comput (P1,s1,(k + 1)))) + n) = ( IC ( Comput (P2,s2,(k + 1)))) by A8, A9, A12, A15, Th26;

        ( CurInstr (P1,( Comput (P1,s1,(k + 1))))) = (P1 . l) by PBOOLE: 143

        .= (SI . l) by A1, A10, GRFUNC_1: 2;

        

        hence ( CurInstr (P1,( Comput (P1,s1,(k + 1))))) = (( Shift (SI,n)) . ( IC ( Comput (P2,s2,(k + 1))))) by A17, A10, VALUED_1:def 12

        .= (P2 . ( IC ( Comput (P2,s2,(k + 1))))) by A2, A17, A11, GRFUNC_1: 2

        .= ( CurInstr (P2,( Comput (P2,s2,(k + 1))))) by PBOOLE: 143;

        thus thesis by A8, A9, A12, A15, A16, Th26;

      end;

      

       A18: (P1 . ( IC s1)) = (P1 . 0 ) by MEMSTR_0:def 11

      .= (SI . 0 ) by A1, A5, GRFUNC_1: 2;

      let i be Nat;

      

       A19: ( DataPart ( Comput (P1,s1, 0 ))) = ( DataPart s2) by A4

      .= ( DataPart ( Comput (P2,s2, 0 )));

      

       A20: ( IC ( Comput (P1,s1, 0 ))) = ( IC s1)

      .= 0 by MEMSTR_0:def 11;

      

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

      

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

      ( CurInstr (P1,( Comput (P1,s1, 0 )))) = ( CurInstr (P1,s1))

      .= (( Shift (SI,n)) . ( 0 + n)) by A5, A18, A22, VALUED_1:def 12

      .= ( CurInstr (P2,( Comput (P2,s2, 0 )))) by A2, A3, A6, A21, GRFUNC_1: 2;

      then

       A23: P[ 0 ] by A3, A20, A19;

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

      hence thesis;

    end;