scmpds_5.miz



    begin

    reserve x for set,

m,n for Nat,

a,b,c for Int_position,

i for Instruction of SCMPDS ,

s,s1,s2 for State of SCMPDS ,

k1,k2 for Integer,

loc,l1 for Nat,

I,J for Program of SCMPDS ,

N for with_non-empty_elements set;

    

     Lm1: ( card ( Stop SCMPDS )) = 1 by AFINSQ_1: 34;

    ::$Canceled

    theorem :: SCMPDS_5:12

    

     Th1: for I,J be Program of SCMPDS holds I c= ( stop (I ';' J))

    proof

      let I,J be Program of SCMPDS ;

      set IS = (I ';' (J ';' ( Stop SCMPDS ))), Ip = ( stop (I ';' J));

      

       A1: I c= IS by AFINSQ_1: 74;

      thus thesis by A1, AFINSQ_1: 27;

    end;

    theorem :: SCMPDS_5:13

    

     Th2: ( dom ( stop I)) c= ( dom ( stop (I ';' J)))

    proof

      set sI = ( stop I), sIJ = ( stop (I ';' J));

      

       A1: ( card sIJ) = (( card (I ';' J)) + 1) by Lm1, AFINSQ_1: 17

      .= ((( card I) + ( card J)) + 1) by AFINSQ_1: 17

      .= ((( card I) + 1) + ( card J));

      ( card sI) = (( card I) + 1) by Lm1, AFINSQ_1: 17;

      then

       A2: ( card sI) <= ( card sIJ) by A1, NAT_1: 11;

      set A = NAT ;

      let x be object;

      assume

       A3: x in ( dom sI);

      ( dom sI) c= A by RELAT_1:def 18;

      then

      reconsider l = x as Nat by A3;

      reconsider n = l as Nat;

      n < ( card sI) by A3, AFINSQ_1: 66;

      then n < ( card sIJ) by A2, XXREAL_0: 2;

      hence x in ( dom sIJ) by AFINSQ_1: 66;

    end;

    theorem :: SCMPDS_5:14

    

     Th3: for I,J be Program of SCMPDS holds (( stop I) +* ( stop (I ';' J))) = ( stop (I ';' J))

    proof

      let I,J be Program of SCMPDS ;

      set sI = ( stop I), IsI = sI, sIJ = ( stop (I ';' J)), IsIJ = sIJ;

      ( dom sI) c= ( dom sIJ) by Th2;

      hence thesis by FUNCT_4: 19;

    end;

    set SA0 = ( Start-At ( 0 , SCMPDS ));

    theorem :: SCMPDS_5:15

    

     Th4: (( Initialize s) . a) = (s . a)

    proof

       not a in ( dom SA0) by SCMPDS_4: 18;

      hence (( Initialize s) . a) = (s . a) by FUNCT_4: 11;

    end;

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

    theorem :: SCMPDS_5:16

    

     Th5: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS st ( stop I) c= P1 & ( stop I) c= P2 holds for k be Nat holds ( Comput (P1,s,k)) = ( Comput (P2,s,k)) & ( CurInstr (P1,( Comput (P1,s,k)))) = ( CurInstr (P2,( Comput (P2,s,k))))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS ;

      set SI = ( stop I);

      assume that

       A1: SI c= P1 and

       A2: SI c= P2;

      let k be Nat;

      

       A3: ( IC ( Comput (P1,s,k))) in ( dom SI) by A1, SCMPDS_4:def 6;

      

       A4: ( IC ( Comput (P2,s,k))) in ( dom SI) by A2, SCMPDS_4:def 6;

      for m be Nat st m < k holds ( IC ( Comput (P2,s,m))) in ( dom SI) by A2, SCMPDS_4:def 6;

      hence

       A5: ( Comput (P1,s,k)) = ( Comput (P2,s,k)) by A1, A2, SCMPDS_4: 21;

      

      thus ( CurInstr (P2,( Comput (P2,s,k)))) = (P2 . ( IC ( Comput (P2,s,k)))) by PBOOLE: 143

      .= (SI . ( IC ( Comput (P2,s,k)))) by A2, A4, GRFUNC_1: 2

      .= (P1 . ( IC ( Comput (P1,s,k)))) by A1, A5, A3, GRFUNC_1: 2

      .= ( CurInstr (P1,( Comput (P1,s,k)))) by PBOOLE: 143;

    end;

    theorem :: SCMPDS_5:17

    

     Th6: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS st ( stop I) c= P1 & ( stop I) c= P2 holds ( LifeSpan (P1,s)) = ( LifeSpan (P2,s)) & ( Result (P1,s)) = ( Result (P2,s))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS ;

      set SI = ( stop I);

      assume that

       A1: SI c= P1 and

       A2: SI c= P2;

      

       A3: P2 halts_on s by A2, SCMPDS_4:def 7;

      

       A4: P1 halts_on s by A1, SCMPDS_4:def 7;

       A5:

      now

        let l be Nat;

        assume

         A6: ( CurInstr (P2,( Comput (P2,s,l)))) = ( halt SCMPDS );

        ( CurInstr (P1,( Comput (P1,s,l)))) = ( CurInstr (P2,( Comput (P2,s,l)))) by A1, A2, Th5;

        hence ( LifeSpan (P1,s)) <= l by A4, A6, EXTPRO_1:def 15;

      end;

      ( CurInstr (P2,( Comput (P2,s,( LifeSpan (P1,s)))))) = ( CurInstr (P1,( Comput (P1,s,( LifeSpan (P1,s)))))) by A1, A2, Th5

      .= ( halt SCMPDS ) by A4, EXTPRO_1:def 15;

      hence

       A7: ( LifeSpan (P1,s)) = ( LifeSpan (P2,s)) by A5, A3, EXTPRO_1:def 15;

      P2 halts_on s by A2, SCMPDS_4:def 7;

      then

       A8: ( Result (P2,s)) = ( Comput (P2,s,( LifeSpan (P1,s)))) by A7, EXTPRO_1: 23;

      P1 halts_on s by A1, SCMPDS_4:def 7;

      then ( Result (P1,s)) = ( Comput (P1,s,( LifeSpan (P1,s)))) by EXTPRO_1: 23;

      hence thesis by A1, A2, A8, Th5;

    end;

    ::$Canceled

    theorem :: SCMPDS_5:19

    

     Th7: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS , J be Program of SCMPDS st ( stop I) c= P holds for m st m <= ( LifeSpan (P,s)) holds ( Comput (P,s,m)) = ( Comput ((P +* (I ';' J)),s,m))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS , J be Program of SCMPDS ;

      set SI = ( stop I);

      defpred X[ Nat] means $1 <= ( LifeSpan (P,s)) implies ( Comput (P,s,$1)) = ( Comput ((P +* (I ';' J)),s,$1));

      assume

       A1: SI c= P;

      then

       A2: P halts_on s by SCMPDS_4:def 7;

      

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

      proof

        ( dom (I ';' J)) = (( dom I) \/ ( dom ( Shift (J,( card I))))) by FUNCT_4:def 1;

        then

         A4: ( dom I) c= ( dom (I ';' J)) by XBOOLE_1: 7;

        let m;

        assume

         A5: m <= ( LifeSpan (P,s)) implies ( Comput (P,s,m)) = ( Comput ((P +* (I ';' J)),s,m));

        assume

         A6: (m + 1) <= ( LifeSpan (P,s));

        

         A7: ( Comput ((P +* (I ';' J)),s,(m + 1))) = ( Following ((P +* (I ';' J)),( Comput ((P +* (I ';' J)),s,m)))) by EXTPRO_1: 3;

        

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

        

         A9: (I ';' J) c= (P +* (I ';' J)) by FUNCT_4: 25;

        

         A10: ( IC ( Comput (P,s,m))) in ( dom SI) by A1, SCMPDS_4:def 6;

        

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

        

         A12: ( CurInstr (P,( Comput (P,s,m)))) = (SI . ( IC ( Comput (P,s,m)))) by A10, A11, A1, GRFUNC_1: 2;

        

         A13: ((P +* (I ';' J)) /. ( IC ( Comput ((P +* (I ';' J)),s,m)))) = ((P +* (I ';' J)) . ( IC ( Comput ((P +* (I ';' J)),s,m)))) by PBOOLE: 143;

        m < ( LifeSpan (P,s)) by A6, NAT_1: 13;

        then (SI . ( IC ( Comput (P,s,m)))) <> ( halt SCMPDS ) by A2, A12, EXTPRO_1:def 15;

        then

         A14: ( IC ( Comput (P,s,m))) in ( dom I) by A10, COMPOS_1: 51;

        ( CurInstr (P,( Comput (P,s,m)))) = (I . ( IC ( Comput (P,s,m)))) by A12, A14, AFINSQ_1:def 3

        .= ((I ';' J) . ( IC ( Comput (P,s,m)))) by A14, AFINSQ_1:def 3

        .= ( CurInstr ((P +* (I ';' J)),( Comput ((P +* (I ';' J)),s,m)))) by A6, A9, A14, A4, A13, A5, GRFUNC_1: 2, NAT_1: 13;

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

      end;

      

       A15: X[ 0 ];

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

    end;

    theorem :: SCMPDS_5:20

    

     Th8: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS , J be Program of SCMPDS st ( stop I) c= P holds for m st m <= ( LifeSpan (P,s)) holds ( Comput (P,s,m)) = ( Comput ((P +* ( stop (I ';' J))),s,m))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS , J be Program of SCMPDS ;

      assume

       A1: ( stop I) c= P;

      set sIJ = ( stop (I ';' J)), SS = ( Stop SCMPDS );

      let m;

      assume

       A2: m <= ( LifeSpan (P,s));

      (P +* sIJ) = (P +* (I ';' (J ';' SS))) by AFINSQ_1: 27;

      hence thesis by A1, A2, Th7;

    end;

    

     Lm2: ( Load (( DataLoc ( 0 , 0 )) := 0 )) is parahalting

    proof

      set ii = (( DataLoc ( 0 , 0 )) := 0 ), m0 = ( stop ( Load ii));

      let s be 0 -started State of SCMPDS ;

      let P such that

       A1: m0 c= P;

      

       A2: m0 = ( Macro ii);

      take 1;

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

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

      

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

      then

       A4: ( IC ( Exec (ii,s))) = ( 0 + 1) by SCMPDS_2: 45;

      1 in ( dom m0) by A2, COMPOS_1: 57;

      then (m0 . 1) = (P . 1) by A1, GRFUNC_1: 2;

      then

       A5: (P . 1) = ( halt SCMPDS ) by A2, COMPOS_1: 59;

       0 in ( dom m0) by A2, COMPOS_1: 57;

      then

       A6: (m0 . 0 ) = (P . 0 ) by A1, GRFUNC_1: 2;

      

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

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

      .= ( Following (P,s))

      .= ( Exec (ii,s)) by A3, A6, A7, A2, COMPOS_1: 58;

      hence thesis by A5, A4, PBOOLE: 143;

    end;

    begin

    definition

      ::$Canceled

      let i be Instruction of SCMPDS ;

      :: SCMPDS_5:def2

      attr i is parahalting means

      : Def1: ( Load i) is parahalting;

    end

    registration

      cluster No-StopCode shiftable parahalting for Instruction of SCMPDS ;

      existence

      proof

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

        ( InsCode i) = 2 by SCMPDS_2: 14;

        then i <> ( halt SCMPDS );

        hence i is No-StopCode;

        thus thesis by Lm2;

      end;

    end

    theorem :: SCMPDS_5:21

    ( goto k1) is No-StopCode

    proof

      

       A1: ( InsCode ( goto k1)) = 14 by SCMPDS_2: 12;

      thus ( goto k1) <> ( halt the InstructionsF of SCMPDS ) by A1;

    end;

    registration

      let a;

      cluster ( return a) -> No-StopCode;

      coherence

      proof

        set i = ( return a);

        ( InsCode i) = 1 by SCMPDS_2: 13;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

    end

    registration

      let a, k1;

      cluster (a := k1) -> No-StopCode;

      coherence

      proof

        set i = (a := k1);

        ( InsCode i) = 2 by SCMPDS_2: 14;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

      cluster ( saveIC (a,k1)) -> No-StopCode;

      coherence

      proof

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

        ( InsCode i) = 3 by SCMPDS_2: 15;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

    end

    registration

      let a, k1, k2;

      cluster ((a,k1) <>0_goto k2) -> No-StopCode;

      coherence

      proof

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

        ( InsCode i) = 4 by SCMPDS_2: 16;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

      cluster ((a,k1) <=0_goto k2) -> No-StopCode;

      coherence

      proof

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

        ( InsCode i) = 5 by SCMPDS_2: 17;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

      cluster ((a,k1) >=0_goto k2) -> No-StopCode;

      coherence

      proof

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

        ( InsCode i) = 6 by SCMPDS_2: 18;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

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

      coherence

      proof

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

        ( InsCode i) = 7 by SCMPDS_2: 19;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

    end

    registration

      let a, k1, k2;

      cluster ( AddTo (a,k1,k2)) -> No-StopCode;

      coherence

      proof

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

        ( InsCode i) = 8 by SCMPDS_2: 20;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

    end

    registration

      let a, b, k1, k2;

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

      coherence

      proof

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

        ( InsCode i) = 9 by SCMPDS_2: 21;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

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

      coherence

      proof

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

        ( InsCode i) = 10 by SCMPDS_2: 22;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

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

      coherence

      proof

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

        ( InsCode i) = 11 by SCMPDS_2: 23;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

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

      coherence

      proof

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

        ( InsCode i) = 12 by SCMPDS_2: 24;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

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

      coherence

      proof

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

        ( InsCode i) = 13 by SCMPDS_2: 25;

        then i <> ( halt SCMPDS );

        hence thesis;

      end;

    end

    registration

      cluster ( halt SCMPDS ) -> parahalting;

      coherence

      proof

        ( Stop SCMPDS ) = ( Load ( halt SCMPDS ));

        hence thesis;

      end;

    end

    registration

      let i be parahalting Instruction of SCMPDS ;

      cluster ( Load i) -> parahalting;

      coherence by Def1;

    end

    

     Lm3: (for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1)) implies ( Load i) is parahalting

    proof

      assume

       A1: for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1);

      set m0 = ( stop ( Load i));

      let t be 0 -started State of SCMPDS ;

      

       A2: m0 = ( Macro i);

      let Q such that

       A3: m0 c= Q;

      take 1;

      ( IC ( Comput (Q,t,1))) in NAT ;

      hence ( IC ( Comput (Q,t,1))) in ( dom Q) by PARTFUN1:def 2;

      

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

      then

       A5: ( IC ( Exec (i,t))) = ( 0 + 1) by A1;

      1 in ( dom m0) by A2, COMPOS_1: 57;

      then (m0 . 1) = (Q . 1) by A3, GRFUNC_1: 2;

      then

       A6: (Q . 1) = ( halt SCMPDS ) by A2, COMPOS_1: 59;

       0 in ( dom m0) by A2, COMPOS_1: 57;

      then

       A7: (m0 . 0 ) = (Q . 0 ) by A3, GRFUNC_1: 2;

      

       A8: (Q /. ( IC t)) = (Q . ( IC t)) by PBOOLE: 143;

      ( Comput (Q,t,( 0 + 1))) = ( Following (Q,( Comput (Q,t, 0 )))) by EXTPRO_1: 3

      .= ( Following (Q,t))

      .= ( Exec (i,t)) by A4, A7, A8, A2, COMPOS_1: 58;

      hence thesis by A5, A6, PBOOLE: 143;

    end;

    registration

      let a, k1;

      cluster (a := k1) -> parahalting;

      coherence

      proof

        set i = (a := k1);

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 45;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

    end

    registration

      let a, k1, k2;

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

      coherence

      proof

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

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 46;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

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

      coherence

      proof

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

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 48;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

    end

    registration

      let a, b, k1, k2;

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

      coherence

      proof

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

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 49;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

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

      coherence

      proof

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

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 50;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

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

      coherence

      proof

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

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 51;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

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

      coherence

      proof

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

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 52;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

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

      coherence

      proof

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

        for s holds (( Exec (i,s)) . ( IC SCMPDS )) = (( IC s) + 1) by SCMPDS_2: 47;

        then ( Load i) is parahalting by Lm3;

        hence thesis;

      end;

    end

    theorem :: SCMPDS_5:22

    

     Th10: ( InsCode i) = 1 implies not i is parahalting

    proof

      consider s such that

       A1: for a holds (s . a) = 2 by SCMPDS_2: 61;

      set P = the Instruction-Sequence of SCMPDS ;

      assume ( InsCode i) = 1;

      then

      consider a such that

       A2: i = ( return a) by SCMPDS_2: 27;

      assume i is parahalting;

      then

      reconsider Li = ( Load i) as parahalting Program of SCMPDS ;

      set pi = ( Macro i);

      set s1 = ( Initialize s), P1 = (P +* pi);

      (s1 . ( DataLoc ((s1 . a), RetIC ))) = (s . ( DataLoc ((s1 . a), RetIC ))) by Th4

      .= 2 by A1;

      

      then

       A3: (( Exec (i,s1)) . ( IC SCMPDS )) = ( |.2.| + 2) by A2, SCMPDS_2: 58

      .= (2 + 2) by ABSVALUE:def 1

      .= 4;

      set C1 = ( Comput (P1,s1,1));

      ( stop Li) c= P1 by FUNCT_4: 25;

      then

       A4: ( IC C1) in ( dom pi) by SCMPDS_4:def 6;

       0 in ( dom pi) by COMPOS_1: 57;

      

      then

       A5: (P1 . 0 ) = (pi . 0 ) by FUNCT_4: 13

      .= i by COMPOS_1: 58;

      

       A6: ( card pi) = 2 by COMPOS_1: 56;

      

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

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

      .= ( Following (P1,s1))

      .= ( Exec (i,s1)) by A5, A7, MEMSTR_0: 47;

      hence contradiction by A3, A4, A6, AFINSQ_1: 66;

    end;

    registration

      cluster parahalting shiftable halt-free for Program of SCMPDS ;

      existence

      proof

        set ii = (( DataLoc ( 0 , 0 )) := 0 );

        take II = ( Load ii);

        now

          let x be Nat;

          assume x in ( dom II);

          then x in { 0 } by FUNCOP_1: 13;

          then x = 0 by TARSKI:def 1;

          then

           A1: (II . x) = ii;

          ( InsCode ii) = 2 by SCMPDS_2: 14;

          hence (II . x) <> ( halt SCMPDS ) by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let I,J be halt-free Program of SCMPDS ;

      cluster (I ';' J) -> halt-free;

      coherence

      proof

        set IJ = (I ';' J);

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

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

        then

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

        let x be Nat such that

         A2: x in ( dom IJ);

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

          suppose

           A3: x in ( dom I);

          then (I . x) = (IJ . x) by AFINSQ_1:def 3;

          hence (IJ . x) <> ( halt SCMPDS ) by A3, COMPOS_1:def 27;

        end;

          suppose x in D;

          then

          consider n be Nat such that

           A4: x = (n + ( card I)) and

           A5: n in ( dom J);

          (J . n) = (IJ . x) by A4, A5, AFINSQ_1:def 3;

          hence (IJ . x) <> ( halt SCMPDS ) by A5, COMPOS_1:def 27;

        end;

      end;

    end

    registration

      let i be No-StopCode Instruction of SCMPDS ;

      cluster ( Load i) -> halt-free;

      coherence

      proof

        set p = ( Load i);

        now

          let x be Nat;

          assume x in ( dom p);

          then x = 0 by COMPOS_1: 50;

          then (p . x) = i;

          hence (p . x) <> ( halt SCMPDS ) by COMPOS_0:def 12;

        end;

        hence thesis;

      end;

    end

    registration

      let i be No-StopCode Instruction of SCMPDS , J be halt-free Program of SCMPDS ;

      cluster (i ';' J) -> halt-free;

      coherence ;

    end

    registration

      let I be halt-free Program of SCMPDS , j be No-StopCode Instruction of SCMPDS ;

      cluster (I ';' j) -> halt-free;

      coherence ;

    end

    registration

      let i,j be No-StopCode Instruction of SCMPDS ;

      cluster (i ';' j) -> halt-free;

      coherence ;

    end

    theorem :: SCMPDS_5:23

    

     Th11: for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS st ( stop I) c= P holds ( IC ( Comput (P,s,( LifeSpan ((P +* ( stop I)),s))))) = ( card I)

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS ;

      set Css = ( Comput (P,s,( LifeSpan (P,s))));

      reconsider n = ( IC Css) as Nat;

      assume

       A1: ( stop I) c= P;

      then

       A2: P halts_on s by SCMPDS_4:def 7;

      

       A3: (P +* ( stop I)) = P by A1, FUNCT_4: 98;

      I c= ( stop I) by AFINSQ_1: 74;

      then

       A4: I c= P by A1;

      now

        assume

         A5: ( IC Css) in ( dom I);

        

        then (I . ( IC Css)) = (P . ( IC Css)) by A4, GRFUNC_1: 2

        .= ( CurInstr (P,Css)) by PBOOLE: 143

        .= ( halt SCMPDS ) by A2, EXTPRO_1:def 15;

        hence contradiction by A5, COMPOS_1:def 27;

      end;

      then

       A6: n >= ( card I) by AFINSQ_1: 66;

      

       A7: ( card ( stop I)) = (( card I) + 1) by Lm1, AFINSQ_1: 17;

      ( IC Css) in ( dom ( stop I)) by A1, SCMPDS_4:def 6;

      then n < (( card I) + 1) by A7, AFINSQ_1: 66;

      then n <= ( card I) by NAT_1: 13;

      hence thesis by A3, A6, XXREAL_0: 1;

    end;

    theorem :: SCMPDS_5:24

    

     Th12: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS , k be Nat st k < ( LifeSpan ((P +* ( stop I)),s)) holds ( IC ( Comput ((P +* ( stop I)),s,k))) in ( dom I)

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS , k be Nat;

      set ss = s, PP = (P +* ( stop I)), m = ( LifeSpan (PP,ss));

      set Sk = ( Comput (PP,ss,k)), Ik = ( IC Sk);

      

       A1: ( stop I) c= PP by FUNCT_4: 25;

      then

       A2: PP halts_on ss by SCMPDS_4:def 7;

      reconsider n = Ik as Nat;

      

       A3: Ik in ( dom ( stop I)) by A1, SCMPDS_4:def 6;

      

       A4: ( stop I) c= PP by FUNCT_4: 25;

      assume

       A5: k < m;

       A6:

      now

        assume

         A7: n = ( card I);

        

         A8: 0 in ( dom ( Stop SCMPDS )) by COMPOS_1: 3;

        

         A9: (( Stop SCMPDS ) . 0 ) = ( halt SCMPDS );

        ( CurInstr (PP,Sk)) = (PP . Ik) by PBOOLE: 143

        .= (( stop I) . ( 0 + n)) by A3, A4, GRFUNC_1: 2

        .= ( halt SCMPDS ) by A7, A9, A8, AFINSQ_1:def 3;

        hence contradiction by A5, A2, EXTPRO_1:def 15;

      end;

      ( card ( stop I)) = (( card I) + 1) by Lm1, AFINSQ_1: 17;

      then n < (( card I) + 1) by A3, AFINSQ_1: 66;

      then n <= ( card I) by INT_1: 7;

      then n < ( card I) by A6, XXREAL_0: 1;

      hence thesis by AFINSQ_1: 66;

    end;

    theorem :: SCMPDS_5:25

    

     Th13: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS , k be Nat st I c= P & k <= ( LifeSpan ((P +* ( stop I)),s)) holds ( Comput (P,s,k)) = ( Comput ((P +* ( stop I)),s,k))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS , k be Nat;

      set m = ( LifeSpan ((P +* ( stop I)),s));

      assume that

       A1: I c= P and

       A2: k <= m;

      set s2 = s, P2 = (P +* ( stop I));

      defpred P[ Nat] means $1 <= m implies ( Comput (P,s,$1)) = ( Comput (P2,s2,$1));

      

       A3: P = (P +* I) by A1, FUNCT_4: 98;

       A4:

      now

        let k be Nat;

        assume

         A5: P[k];

        now

          

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

          

           A7: ( Comput (P,s,(k + 1))) = ( Following (P,( Comput (P,s,k)))) by EXTPRO_1: 3;

          

           A8: k < (k + 1) by XREAL_1: 29;

          assume

           A9: (k + 1) <= m;

          then

           A10: k < m by A8, XXREAL_0: 2;

          then ( IC ( Comput (P2,s2,k))) in ( dom I) by Th12;

          then

           A11: ( IC ( Comput (P2,s2,k))) in ( dom ( stop I)) by FUNCT_4: 12;

          

           A12: ( IC ( Comput (P2,s2,k))) in ( dom I) by A10, Th12;

          ( CurInstr (P,( Comput (P,s,k)))) = (P . ( IC ( Comput (P2,s2,k)))) by A5, A9, A8, PBOOLE: 143, XXREAL_0: 2

          .= (I . ( IC ( Comput (P2,s2,k)))) by A3, A10, Th12, FUNCT_4: 13

          .= (( stop I) . ( IC ( Comput (P2,s2,k)))) by A12, AFINSQ_1:def 3

          .= ((P +* ( stop I)) . ( IC ( Comput (P2,s2,k)))) by A11, FUNCT_4: 13

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

          hence ( Comput (P,s,(k + 1))) = ( Comput (P2,s2,(k + 1))) by A5, A9, A8, A7, A6, XXREAL_0: 2;

        end;

        hence P[(k + 1)];

      end;

      

       A13: P[ 0 ];

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

      hence thesis by A2;

    end;

    theorem :: SCMPDS_5:26

    

     Th14: for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS st I c= P holds ( IC ( Comput (P,s,( LifeSpan ((P +* ( stop I)),s))))) = ( card I)

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS ;

      set PP = (P +* ( stop I)), m = ( LifeSpan (PP,s));

      

       A1: ( stop I) c= PP by FUNCT_4: 25;

      

       A2: (( stop I) +* PP) = PP & (PP +* ( stop I)) = PP by A1, FUNCT_4: 97;

      assume I c= P;

      

      hence ( IC ( Comput (P,s,m))) = ( IC ( Comput (PP,s,m))) by Th13

      .= ( card I) by Th11, A2, FUNCT_4: 25;

    end;

    theorem :: SCMPDS_5:27

    

     Th15: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS st I c= P holds ( CurInstr (P,( Comput (P,s,( LifeSpan ((P +* ( stop I)),s)))))) = ( halt SCMPDS ) or ( IC ( Comput (P,s,( LifeSpan ((P +* ( stop I)),s))))) = ( card I)

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS ;

      set PP = (P +* ( stop I)), m = ( LifeSpan (PP,s));

      set s1 = ( Comput (P,s,m)), s2 = ( Comput (PP,s,( LifeSpan ((PP +* ( stop I)),( Initialize s))))), Ik = ( IC s2);

      

       A1: ( stop I) c= PP by FUNCT_4: 25;

      then

       A2: PP halts_on s by SCMPDS_4:def 7;

      reconsider n = Ik as Nat;

      

       A3: Ik in ( dom ( stop I)) by A1, SCMPDS_4:def 6;

      

       A4: ( Initialize s) = s by MEMSTR_0: 44;

      ( card ( stop I)) = (( card I) + 1) by Lm1, AFINSQ_1: 17;

      then n < (( card I) + 1) by A3, AFINSQ_1: 66;

      then

       A5: n <= ( card I) by INT_1: 7;

      

       A6: ( stop I) c= PP by FUNCT_4: 25;

      assume

       A7: I c= P;

      then

       A8: ( IC s1) = Ik by Th13, A4;

      now

        per cases by A5, XXREAL_0: 1;

          case n < ( card I);

          then

           A9: n in ( dom I) by AFINSQ_1: 66;

          

          thus ( halt SCMPDS ) = ( CurInstr (PP,s2)) by A2, A4, EXTPRO_1:def 15

          .= (PP . Ik) by PBOOLE: 143

          .= (( stop I) . Ik) by A3, A6, GRFUNC_1: 2

          .= (I . Ik) by A9, AFINSQ_1:def 3

          .= (P . ( IC s1)) by A7, A8, A9, GRFUNC_1: 2

          .= ( CurInstr (P,s1)) by PBOOLE: 143;

        end;

          case n = ( card I);

          hence ( IC s1) = ( card I) by A7, Th13, A4;

        end;

      end;

      hence thesis;

    end;

    theorem :: SCMPDS_5:28

    

     Th16: for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS , k be Nat st I c= P & k < ( LifeSpan ((P +* ( stop I)),s)) holds ( CurInstr (P,( Comput (P,s,k)))) <> ( halt SCMPDS )

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS , k be Nat;

      set PI = (P +* ( stop I)), s1 = ( Comput (P,s,k)), s2 = ( Comput (PI,s,k));

      assume that

       A1: I c= P and

       A2: k < ( LifeSpan (PI,s));

      

       A3: ( IC s2) in ( dom I) by A2, Th12;

      

       A4: (P /. ( IC s1)) = (P . ( IC s1)) by PBOOLE: 143;

      ( CurInstr (P,s1)) = (P . ( IC s2)) by A4, A1, A2, Th13

      .= (I . ( IC s2)) by A1, A3, GRFUNC_1: 2;

      hence thesis by A3, COMPOS_1:def 27;

    end;

    theorem :: SCMPDS_5:29

    

     Th17: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS , J be Program of SCMPDS , k be Nat st k <= ( LifeSpan ((P +* ( stop I)),s)) holds ( Comput ((P +* ( stop I)),s,k)) = ( Comput ((P +* (I ';' J)),s,k))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS , J be Program of SCMPDS , k be Nat;

      set spI = ( stop I), P1 = (P +* spI), P2 = (P +* (I ';' J));

      set n = ( LifeSpan (P1,s));

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

      

       A1: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let m be Nat;

        assume

         A2: m <= n implies ( Comput (P1,s,m)) = ( Comput (P2,s,m));

        

         A3: ( Comput (P2,s,(m + 1))) = ( Following (P2,( Comput (P2,s,m)))) by EXTPRO_1: 3;

        spI c= P1 by FUNCT_4: 25;

        then

         A4: ( IC ( Comput (P1,s,m))) in ( dom spI) by SCMPDS_4:def 6;

        

         A5: ( Comput (P1,s,(m + 1))) = ( Following (P1,( Comput (P1,s,m)))) by EXTPRO_1: 3;

        assume

         A6: (m + 1) <= n;

        

         A7: m < n by A6, NAT_1: 13;

        then ( IC ( Comput (P1,s,m))) in ( dom I) by Th12;

        then

         A8: ( IC ( Comput (P1,s,m))) in ( dom (I ';' J)) by FUNCT_4: 12;

        

         A9: ( IC ( Comput (P1,s,m))) in ( dom I) by A7, Th12;

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

        .= (spI . ( IC ( Comput (P1,s,m)))) by A4, FUNCT_4: 13

        .= (I . ( IC ( Comput (P1,s,m)))) by A9, AFINSQ_1:def 3

        .= ((I ';' J) . ( IC ( Comput (P1,s,m)))) by A9, AFINSQ_1:def 3

        .= (P2 . ( IC ( Comput (P1,s,m)))) by A8, FUNCT_4: 13

        .= ( CurInstr (P2,( Comput (P2,s,m)))) by A6, A2, NAT_1: 13, PBOOLE: 143;

        hence thesis by A2, A6, A5, A3, NAT_1: 13;

      end;

      

       A10: X[ 0 ];

      for k be Nat holds X[k] from NAT_1:sch 2( A10, A1);

      hence thesis;

    end;

    theorem :: SCMPDS_5:30

    

     Th18: for s be 0 -started State of SCMPDS holds for I be parahalting Program of SCMPDS , J be Program of SCMPDS , k be Nat st k <= ( LifeSpan ((P +* ( stop I)),s)) holds ( Comput ((P +* ( stop I)),s,k)) = ( Comput ((P +* ( stop (I ';' J))),s,k))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting Program of SCMPDS , J be Program of SCMPDS , k be Nat;

      

       A1: ( stop (I ';' J)) = (I ';' (J ';' ( Stop SCMPDS ))) by AFINSQ_1: 27;

      thus thesis by A1, Th17;

    end;

    registration

      let I be parahalting Program of SCMPDS , J be parahalting shiftable Program of SCMPDS ;

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

      coherence

      proof

        let p be Program of SCMPDS such that

         A1: p = (I ';' J);

        let s be 0 -started State of SCMPDS ;

        let P;

        set sIJ = ( stop p);

        set spJ = ( stop J), s1 = ( Initialize s), P1 = (P +* ( stop I)), m1 = ( LifeSpan (P1,s1)), s3 = ( Initialize ( Comput (P1,s1,m1))), P3 = (P1 +* spJ), m3 = ( LifeSpan (P3,s3)), D = SCM-Data-Loc ;

        

         A2: spJ c= P3 by FUNCT_4: 25;

        then

         A3: P3 halts_on s3 by SCMPDS_4:def 7;

        

         A4: ( DataPart ( Comput (P1,s1,m1))) = ( DataPart s3) by MEMSTR_0: 45;

        

         A5: I c= sIJ by A1, Th1;

        set s4 = ( Comput (P,s,m1)), P4 = P;

        assume

         A6: sIJ c= P;

        

         A7: p c= sIJ by AFINSQ_1: 74;

        

         A8: s = ( Initialize s) by MEMSTR_0: 44;

        (P +* (I ';' J)) = P by A7, A1, A6, FUNCT_4: 98, XBOOLE_1: 1;

        then

         A9: ( DataPart s4) = ( DataPart s3) by A4, A8, Th17;

        per cases by A6, A5, Th15, A8, XBOOLE_1: 1;

          suppose

           A10: ( CurInstr (P,s4)) = ( halt SCMPDS );

          take m1;

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

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

          thus thesis by A10;

        end;

          suppose

           A11: ( IC s4) = ( card I);

          reconsider m = (m1 + m3) as Nat;

          take m;

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

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

          

           A12: ( Comput (P,s,(m1 + m3))) = ( Comput (P,( Comput (P,s,m1)),m3)) by EXTPRO_1: 4;

          sIJ = (I ';' (J ';' ( Stop SCMPDS ))) by A1, AFINSQ_1: 27

          .= (I +* ( Shift (spJ,( card I))));

          then ( Shift (spJ,( card I))) c= sIJ by FUNCT_4: 25;

          then

           A13: ( Shift (spJ,( card I))) c= P4 by A6;

          ( CurInstr (P3,( Comput (P3,s3,m3)))) = ( CurInstr (P,( Comput (P,s,(m1 + m3))))) by A12, A2, A9, A11, A13, SCMPDS_4: 29;

          hence thesis by A3, EXTPRO_1:def 15;

        end;

      end;

    end

    registration

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

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

      coherence ;

    end

    registration

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

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

      coherence ;

    end

    registration

      let i be parahalting Instruction of SCMPDS , j be parahalting shiftable Instruction of SCMPDS ;

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

      coherence ;

    end

    theorem :: SCMPDS_5:31

    

     Th19: for s be State of SCMPDS , s1 be 0 -started State of SCMPDS , J be parahalting shiftable Program of SCMPDS st ( stop J) c= P & s = ( Comput ((P1 +* ( stop J)),s1,m)) holds ( Exec (( CurInstr (P,s)),( IncIC (s,n)))) = ( IncIC (( Following (P,s)),n))

    proof

      let s be State of SCMPDS , s1 be 0 -started State of SCMPDS , J be parahalting shiftable Program of SCMPDS ;

      set pJ = ( stop J), s2 = s1, P2 = (P1 +* pJ);

      set i = ( CurInstr (P,s)), ss = (s +* ( Start-At ((( IC s) + n), SCMPDS )));

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

      reconsider Nl = (( IC s) + 1) as Element of NAT ;

      

       A1: (( IC ss) + 1) = ((k + n) + 1) by FUNCT_4: 113

      .= ( IC (( Exec (i,s)) +* ( Start-At ((Nl + n), SCMPDS )))) by FUNCT_4: 113;

      assume

       A2: pJ c= P;

      assume

       A3: s = ( Comput (P2,s2,m));

      pJ c= P2 by FUNCT_4: 25;

      then

       A4: ( IC s) in ( dom pJ) by A3, SCMPDS_4:def 6;

      reconsider n1 = ( IC s) as Nat;

      set IEn = (( IC ( Exec (i,s))) + n);

      

       A5: ( IC ss) = (( IC s) + n) by FUNCT_4: 113;

      

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

      

       A7: i = (pJ . n1) by A4, A6, A2, GRFUNC_1: 2;

      then

       A8: ( InsCode i) <> 1 by A4, SCMPDS_4:def 9;

      

       A9: i valid_at n1 by A4, A7, SCMPDS_4:def 9;

      

       A10: ( InsCode i) <> 3 by A4, A7, SCMPDS_4:def 9;

      ( InsCode i) <= 14 by SCMPDS_2: 6;

      then ( InsCode i) = 0 or ... or ( InsCode i) = 14;

      per cases by A8, A10;

        suppose

         A11: ( InsCode i) = 0 ;

        

         A12: ( Following (P,s)) = s by A11, SCMPDS_2: 86;

        

        thus ( Exec (( CurInstr (P,s)),( IncIC (s,n)))) = ( IncIC (s,n)) by A11, SCMPDS_2: 86

        .= ( IncIC (( Following (P,s)),n)) by A12;

      end;

        suppose ( InsCode i) = 14;

        then

        consider k1 such that

         A13: i = ( goto k1) and

         A14: (n1 + k1) >= 0 by A9;

        

         A15: ( IC ( Exec (i,s))) = ( ICplusConst (s,k1)) by A13, SCMPDS_2: 54;

         A16:

        now

          let b;

          

          thus (( Exec (i,ss)) . b) = (ss . b) by A13, SCMPDS_2: 54

          .= (s . b) by SCMPDS_3: 6

          .= (( Exec (i,s)) . b) by A13, SCMPDS_2: 54

          .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

        end;

        ( IC ( Exec (i,ss))) = ( ICplusConst (ss,k1)) by A13, SCMPDS_2: 54

        .= IEn by A5, A14, A15, SCMPDS_4: 27

        .= ( IC ( IncIC (( Exec (i,s)),n))) by FUNCT_4: 113;

        hence thesis by A16, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 2;

        then

        consider a, k1 such that

         A17: i = (a := k1) by SCMPDS_2: 28;

         A18:

        now

          let b;

          per cases ;

            suppose

             A19: a = b;

            

            hence (( Exec (i,ss)) . b) = k1 by A17, SCMPDS_2: 45

            .= (( Exec (i,s)) . b) by A17, A19, SCMPDS_2: 45

            .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

          end;

            suppose

             A20: a <> b;

            

            hence (( Exec (i,ss)) . b) = (ss . b) by A17, SCMPDS_2: 45

            .= (s . b) by SCMPDS_3: 6

            .= (( Exec (i,s)) . b) by A17, A20, SCMPDS_2: 45

            .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A17, SCMPDS_2: 45;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A17, SCMPDS_2: 45;

        hence thesis by A18, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 4;

        then

        consider a, k1, k2 such that

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

         A22: (n1 + k2) >= 0 by A9;

         A23:

        now

          per cases ;

            suppose

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

            then

             A25: ( IC ( Exec (i,s))) = ( ICplusConst (s,k2)) by A21, SCMPDS_2: 55;

            (ss . ( DataLoc ((s . a),k1))) <> 0 by A24, SCMPDS_3: 6;

            then (ss . ( DataLoc ((ss . a),k1))) <> 0 by SCMPDS_3: 6;

            

            hence ( IC ( Exec (i,ss))) = ( ICplusConst (ss,k2)) by A21, SCMPDS_2: 55

            .= IEn by A5, A22, A25, SCMPDS_4: 27

            .= ( IC ( IncIC (( Exec (i,s)),n))) by FUNCT_4: 113;

          end;

            suppose

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

            then (ss . ( DataLoc ((s . a),k1))) = 0 by SCMPDS_3: 6;

            then

             A27: (ss . ( DataLoc ((ss . a),k1))) = 0 by SCMPDS_3: 6;

            ( IC ( Exec (i,s))) = Nl by A21, A26, SCMPDS_2: 55;

            hence ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A21, A27, SCMPDS_2: 55;

          end;

        end;

        now

          let b;

          

          thus (( Exec (i,ss)) . b) = (ss . b) by A21, SCMPDS_2: 55

          .= (s . b) by SCMPDS_3: 6

          .= (( Exec (i,s)) . b) by A21, SCMPDS_2: 55

          .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

        end;

        hence thesis by A23, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 5;

        then

        consider a, k1, k2 such that

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

         A29: (n1 + k2) >= 0 by A9;

         A30:

        now

          per cases ;

            suppose

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

            then

             A32: ( IC ( Exec (i,s))) = ( ICplusConst (s,k2)) by A28, SCMPDS_2: 56;

            (ss . ( DataLoc ((s . a),k1))) <= 0 by A31, SCMPDS_3: 6;

            then (ss . ( DataLoc ((ss . a),k1))) <= 0 by SCMPDS_3: 6;

            

            hence ( IC ( Exec (i,ss))) = ( ICplusConst (ss,k2)) by A28, SCMPDS_2: 56

            .= IEn by A5, A29, A32, SCMPDS_4: 27

            .= ( IC ( IncIC (( Exec (i,s)),n))) by FUNCT_4: 113;

          end;

            suppose

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

            then (ss . ( DataLoc ((s . a),k1))) > 0 by SCMPDS_3: 6;

            then

             A34: (ss . ( DataLoc ((ss . a),k1))) > 0 by SCMPDS_3: 6;

            ( IC ( Exec (i,s))) = Nl by A28, A33, SCMPDS_2: 56;

            hence ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A28, A34, SCMPDS_2: 56;

          end;

        end;

        now

          let b;

          

          thus (( Exec (i,ss)) . b) = (ss . b) by A28, SCMPDS_2: 56

          .= (s . b) by SCMPDS_3: 6

          .= (( Exec (i,s)) . b) by A28, SCMPDS_2: 56

          .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

        end;

        hence thesis by A30, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 6;

        then

        consider a, k1, k2 such that

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

         A36: (n1 + k2) >= 0 by A9;

         A37:

        now

          per cases ;

            suppose

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

            then

             A39: ( IC ( Exec (i,s))) = ( ICplusConst (s,k2)) by A35, SCMPDS_2: 57;

            (ss . ( DataLoc ((s . a),k1))) >= 0 by A38, SCMPDS_3: 6;

            then (ss . ( DataLoc ((ss . a),k1))) >= 0 by SCMPDS_3: 6;

            

            hence ( IC ( Exec (i,ss))) = ( ICplusConst (ss,k2)) by A35, SCMPDS_2: 57

            .= IEn by A5, A36, A39, SCMPDS_4: 27

            .= ( IC ( IncIC (( Exec (i,s)),n))) by FUNCT_4: 113;

          end;

            suppose

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

            then (ss . ( DataLoc ((s . a),k1))) < 0 by SCMPDS_3: 6;

            then

             A41: (ss . ( DataLoc ((ss . a),k1))) < 0 by SCMPDS_3: 6;

            ( IC ( Exec (i,s))) = Nl by A35, A40, SCMPDS_2: 57;

            hence ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A35, A41, SCMPDS_2: 57;

          end;

        end;

        now

          let b;

          

          thus (( Exec (i,ss)) . b) = (ss . b) by A35, SCMPDS_2: 57

          .= (s . b) by SCMPDS_3: 6

          .= (( Exec (i,s)) . b) by A35, SCMPDS_2: 57

          .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

        end;

        hence thesis by A37, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 7;

        then

        consider a, k1, k2 such that

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

         A43:

        now

          let b;

          per cases ;

            suppose

             A44: ( DataLoc ((ss . a),k1)) = b;

            then

             A45: ( DataLoc ((s . a),k1)) = b by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . b) = k2 by A42, A44, SCMPDS_2: 46

            .= (( Exec (i,s)) . b) by A42, A45, SCMPDS_2: 46

            .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

          end;

            suppose

             A46: ( DataLoc ((ss . a),k1)) <> b;

            then

             A47: ( DataLoc ((s . a),k1)) <> b by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . b) = (ss . b) by A42, A46, SCMPDS_2: 46

            .= (s . b) by SCMPDS_3: 6

            .= (( Exec (i,s)) . b) by A42, A47, SCMPDS_2: 46

            .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A42, SCMPDS_2: 46;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A42, SCMPDS_2: 46;

        hence thesis by A43, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 8;

        then

        consider a, k1, k2 such that

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

         A49:

        now

          let b;

          per cases ;

            suppose

             A50: ( DataLoc ((ss . a),k1)) = b;

            then

             A51: ( DataLoc ((s . a),k1)) = b by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . b) = ((ss . b) + k2) by A48, A50, SCMPDS_2: 48

            .= ((s . b) + k2) by SCMPDS_3: 6

            .= (( Exec (i,s)) . b) by A48, A51, SCMPDS_2: 48

            .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

          end;

            suppose

             A52: ( DataLoc ((ss . a),k1)) <> b;

            then

             A53: ( DataLoc ((s . a),k1)) <> b by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . b) = (ss . b) by A48, A52, SCMPDS_2: 48

            .= (s . b) by SCMPDS_3: 6

            .= (( Exec (i,s)) . b) by A48, A53, SCMPDS_2: 48

            .= (( IncIC (( Exec (i,s)),n)) . b) by SCMPDS_3: 6;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A48, SCMPDS_2: 48;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A48, SCMPDS_2: 48;

        hence thesis by A49, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 9;

        then

        consider a, b, k1, k2 such that

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

         A55:

        now

          let c;

          per cases ;

            suppose

             A56: ( DataLoc ((ss . a),k1)) = c;

            then

             A57: ( DataLoc ((s . a),k1)) = c by SCMPDS_3: 6;

            

             A58: (ss . ( DataLoc ((ss . b),k2))) = (s . ( DataLoc ((ss . b),k2))) by SCMPDS_3: 6

            .= (s . ( DataLoc ((s . b),k2))) by SCMPDS_3: 6;

            (ss . ( DataLoc ((ss . a),k1))) = (s . ( DataLoc ((ss . a),k1))) by SCMPDS_3: 6

            .= (s . ( DataLoc ((s . a),k1))) by SCMPDS_3: 6;

            

            hence (( Exec (i,ss)) . c) = ((s . ( DataLoc ((s . a),k1))) + (s . ( DataLoc ((s . b),k2)))) by A54, A56, A58, SCMPDS_2: 49

            .= (( Exec (i,s)) . c) by A54, A57, SCMPDS_2: 49

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

            suppose

             A59: ( DataLoc ((ss . a),k1)) <> c;

            then

             A60: ( DataLoc ((s . a),k1)) <> c by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . c) = (ss . c) by A54, A59, SCMPDS_2: 49

            .= (s . c) by SCMPDS_3: 6

            .= (( Exec (i,s)) . c) by A54, A60, SCMPDS_2: 49

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A54, SCMPDS_2: 49;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A54, SCMPDS_2: 49;

        hence thesis by A55, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 10;

        then

        consider a, b, k1, k2 such that

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

         A62:

        now

          let c;

          per cases ;

            suppose

             A63: ( DataLoc ((ss . a),k1)) = c;

            then

             A64: ( DataLoc ((s . a),k1)) = c by SCMPDS_3: 6;

            

             A65: (ss . ( DataLoc ((ss . b),k2))) = (s . ( DataLoc ((ss . b),k2))) by SCMPDS_3: 6

            .= (s . ( DataLoc ((s . b),k2))) by SCMPDS_3: 6;

            (ss . ( DataLoc ((ss . a),k1))) = (s . ( DataLoc ((ss . a),k1))) by SCMPDS_3: 6

            .= (s . ( DataLoc ((s . a),k1))) by SCMPDS_3: 6;

            

            hence (( Exec (i,ss)) . c) = ((s . ( DataLoc ((s . a),k1))) - (s . ( DataLoc ((s . b),k2)))) by A61, A63, A65, SCMPDS_2: 50

            .= (( Exec (i,s)) . c) by A61, A64, SCMPDS_2: 50

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

            suppose

             A66: ( DataLoc ((ss . a),k1)) <> c;

            then

             A67: ( DataLoc ((s . a),k1)) <> c by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . c) = (ss . c) by A61, A66, SCMPDS_2: 50

            .= (s . c) by SCMPDS_3: 6

            .= (( Exec (i,s)) . c) by A61, A67, SCMPDS_2: 50

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A61, SCMPDS_2: 50;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A61, SCMPDS_2: 50;

        hence thesis by A62, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 11;

        then

        consider a, b, k1, k2 such that

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

         A69:

        now

          let c;

          per cases ;

            suppose

             A70: ( DataLoc ((ss . a),k1)) = c;

            then

             A71: ( DataLoc ((s . a),k1)) = c by SCMPDS_3: 6;

            

             A72: (ss . ( DataLoc ((ss . b),k2))) = (s . ( DataLoc ((ss . b),k2))) by SCMPDS_3: 6

            .= (s . ( DataLoc ((s . b),k2))) by SCMPDS_3: 6;

            (ss . ( DataLoc ((ss . a),k1))) = (s . ( DataLoc ((ss . a),k1))) by SCMPDS_3: 6

            .= (s . ( DataLoc ((s . a),k1))) by SCMPDS_3: 6;

            

            hence (( Exec (i,ss)) . c) = ((s . ( DataLoc ((s . a),k1))) * (s . ( DataLoc ((s . b),k2)))) by A68, A70, A72, SCMPDS_2: 51

            .= (( Exec (i,s)) . c) by A68, A71, SCMPDS_2: 51

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

            suppose

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

            then

             A74: ( DataLoc ((s . a),k1)) <> c by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . c) = (ss . c) by A68, A73, SCMPDS_2: 51

            .= (s . c) by SCMPDS_3: 6

            .= (( Exec (i,s)) . c) by A68, A74, SCMPDS_2: 51

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A68, SCMPDS_2: 51;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A68, SCMPDS_2: 51;

        hence thesis by A69, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 12;

        then

        consider a, b, k1, k2 such that

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

         A76:

        now

          let c;

          

           A77: (ss . ( DataLoc ((ss . a),k1))) = (s . ( DataLoc ((ss . a),k1))) by SCMPDS_3: 6

          .= (s . ( DataLoc ((s . a),k1))) by SCMPDS_3: 6;

          

           A78: (ss . ( DataLoc ((ss . b),k2))) = (s . ( DataLoc ((ss . b),k2))) by SCMPDS_3: 6

          .= (s . ( DataLoc ((s . b),k2))) by SCMPDS_3: 6;

          per cases ;

            suppose

             A79: ( DataLoc ((ss . b),k2)) = c;

            then

             A80: ( DataLoc ((s . b),k2)) = c by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . c) = ((s . ( DataLoc ((s . a),k1))) mod (s . ( DataLoc ((s . b),k2)))) by A75, A77, A78, A79, SCMPDS_2: 52

            .= (( Exec (i,s)) . c) by A75, A80, SCMPDS_2: 52

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

            suppose

             A81: ( DataLoc ((ss . b),k2)) <> c;

            then

             A82: ( DataLoc ((s . b),k2)) <> c by SCMPDS_3: 6;

            hereby

              per cases ;

                suppose

                 A83: ( DataLoc ((ss . a),k1)) <> c;

                then

                 A84: ( DataLoc ((s . a),k1)) <> c by SCMPDS_3: 6;

                

                thus (( Exec (i,ss)) . c) = (ss . c) by A75, A81, A83, SCMPDS_2: 52

                .= (s . c) by SCMPDS_3: 6

                .= (( Exec (i,s)) . c) by A75, A82, A84, SCMPDS_2: 52

                .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

              end;

                suppose

                 A85: ( DataLoc ((ss . a),k1)) = c;

                then

                 A86: ( DataLoc ((s . a),k1)) = c by SCMPDS_3: 6;

                

                thus (( Exec (i,ss)) . c) = ((s . ( DataLoc ((s . a),k1))) div (s . ( DataLoc ((s . b),k2)))) by A75, A77, A78, A81, A85, SCMPDS_2: 52

                .= (( Exec (i,s)) . c) by A75, A82, A86, SCMPDS_2: 52

                .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

              end;

            end;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A75, SCMPDS_2: 52;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A75, SCMPDS_2: 52;

        hence thesis by A76, SCMPDS_2: 44;

      end;

        suppose ( InsCode i) = 13;

        then

        consider a, b, k1, k2 such that

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

         A88:

        now

          let c;

          per cases ;

            suppose

             A89: ( DataLoc ((ss . a),k1)) = c;

            then

             A90: ( DataLoc ((s . a),k1)) = c by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . c) = (ss . ( DataLoc ((ss . b),k2))) by A87, A89, SCMPDS_2: 47

            .= (s . ( DataLoc ((ss . b),k2))) by SCMPDS_3: 6

            .= (s . ( DataLoc ((s . b),k2))) by SCMPDS_3: 6

            .= (( Exec (i,s)) . c) by A87, A90, SCMPDS_2: 47

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

            suppose

             A91: ( DataLoc ((ss . a),k1)) <> c;

            then

             A92: ( DataLoc ((s . a),k1)) <> c by SCMPDS_3: 6;

            

            thus (( Exec (i,ss)) . c) = (ss . c) by A87, A91, SCMPDS_2: 47

            .= (s . c) by SCMPDS_3: 6

            .= (( Exec (i,s)) . c) by A87, A92, SCMPDS_2: 47

            .= (( IncIC (( Exec (i,s)),n)) . c) by SCMPDS_3: 6;

          end;

        end;

        ( IC ( Exec (i,s))) = Nl by A87, SCMPDS_2: 47;

        then ( IC ( Exec (i,ss))) = ( IC ( IncIC (( Exec (i,s)),n))) by A1, A87, SCMPDS_2: 47;

        hence thesis by A88, SCMPDS_2: 44;

      end;

    end;

    begin

    theorem :: SCMPDS_5:32

    for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS , k be Nat st ( stop (I ';' J)) c= P holds ( IncIC (( Comput (((P +* ( stop I)) +* ( stop J)),( Initialize ( Result ((P +* ( stop I)),s))),k)),( card I))) = ( Comput ((P +* ( stop (I ';' J))),s,(( LifeSpan ((P +* ( stop I)),s)) + k)))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS , k be Nat;

      set sIsI = s, PIPI = (P +* ( stop I)), RI = ( Result (PIPI,sIsI)), pJ = ( stop J), RIJ = ( Initialize RI), PRIJ = (PIPI +* pJ), pIJ = ( stop (I ';' J)), sIsIJ = s, PIPIJ = (P +* pIJ);

      

       A1: pJ c= PRIJ by FUNCT_4: 25;

      ( stop I) c= PIPI by FUNCT_4: 25;

      then

       A2: PIPI halts_on sIsI by SCMPDS_4:def 7;

      set s2 = ( Comput (PIPIJ,sIsIJ,(( LifeSpan (PIPI,sIsI)) + 0 )));

      set s1 = (RIJ +* ( Start-At ((( IC RIJ) + ( card I)), SCMPDS )));

      set m1 = ( LifeSpan (PIPI,sIsI));

      

       A3: I c= pIJ by Th1;

      assume

       A4: pIJ c= P;

      

       A5: (P +* pIJ) = P by A4, FUNCT_4: 98;

       A6:

      now

        

        thus ( IC s1) = (( IC RIJ) + ( card I)) by FUNCT_4: 113

        .= ( 0 + ( card I)) by FUNCT_4: 113

        .= ( IC s2) by A4, A3, Th14, A5, XBOOLE_1: 1;

        hereby

          let a be Int_position;

          

           A7: not a in ( dom ( Start-At ( 0 , SCMPDS ))) by SCMPDS_4: 18;

           not a in ( dom ( Start-At ((( IC RIJ) + ( card I)), SCMPDS ))) by SCMPDS_4: 18;

          

          hence (s1 . a) = (RIJ . a) by FUNCT_4: 11

          .= (RI . a) by A7, FUNCT_4: 11

          .= (( Comput (PIPI,sIsI,m1)) . a) by A2, EXTPRO_1: 23

          .= (s2 . a) by Th18;

        end;

      end;

      defpred X[ Nat] means ( IncIC (( Comput (PRIJ,RIJ,$1)),( card I))) = ( Comput (PIPIJ,sIsIJ,(( LifeSpan (PIPI,sIsI)) + $1)));

      

       A8: pIJ c= PIPIJ by FUNCT_4: 25;

      

       A9: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        set k1 = (k + 1), CRk = ( Comput (PRIJ,RIJ,k)), PCRk = PRIJ, CRSk = ( IncIC (CRk,( card I))), CIJk = ( Comput (PIPIJ,sIsIJ,(( LifeSpan (PIPI,sIsI)) + k))), PCIJk = PIPIJ, CRk1 = ( Comput (PRIJ,RIJ,k1)), CRSk1 = (CRk1 +* ( Start-At ((( IC CRk1) + ( card I)), SCMPDS ))), CIJk1 = ( Comput (PIPIJ,sIsIJ,(( LifeSpan (PIPI,sIsI)) + k1)));

        assume

         A10: CRSk = CIJk;

        

         A11: ( CurInstr (PCRk,CRk)) = ( CurInstr (PCIJk,CIJk))

        proof

          

           A12: ( CurInstr (PCIJk,CIJk)) = (PCIJk . ( IC CRSk)) by A10, PBOOLE: 143

          .= (PCIJk . (( IC CRk) + ( card I))) by FUNCT_4: 113;

          reconsider n = ( IC CRk) as Nat;

          

           A13: pIJ = (I ';' pJ) by AFINSQ_1: 27;

          

           A14: ( IC CRk) in ( dom pJ) by A1, SCMPDS_4:def 6;

          then n < ( card pJ) by AFINSQ_1: 66;

          then (n + ( card I)) < (( card pJ) + ( card I)) by XREAL_1: 6;

          then (n + ( card I)) < ( card pIJ) by A13, AFINSQ_1: 17;

          then

           A15: (( IC CRk) + ( card I)) in ( dom pIJ) by AFINSQ_1: 66;

          

           A16: (PCRk /. ( IC CRk)) = (PCRk . ( IC CRk)) by PBOOLE: 143;

          pJ c= PCRk by FUNCT_4: 25;

          

          hence ( CurInstr (PCRk,CRk)) = (pJ . ( IC CRk)) by A14, A16, GRFUNC_1: 2

          .= (pIJ . (( IC CRk) + ( card I))) by A14, A13, AFINSQ_1:def 3

          .= ( CurInstr (PCIJk,CIJk)) by A12, A8, A15, GRFUNC_1: 2;

        end;

        

         A17: ( Exec (( CurInstr (PCIJk,CIJk)),CIJk)) = ( IncIC (( Following (PCRk,CRk)),( card I))) by A10, Th19, A11, FUNCT_4: 25;

        CIJk1 = ( Comput (PIPIJ,sIsIJ,((( LifeSpan (PIPI,sIsI)) + k) + 1)));

        then

         A18: CIJk1 = ( Following (PIPIJ,CIJk)) by EXTPRO_1: 3;

         A19:

        now

          let a be Int_position;

          

          thus (CRSk1 . a) = (CRk1 . a) by SCMPDS_3: 6

          .= (( Following (PRIJ,CRk)) . a) by EXTPRO_1: 3

          .= (CIJk1 . a) by A18, A17, SCMPDS_3: 6;

        end;

        ( IC CRSk1) = (( IC CRk1) + ( card I)) by FUNCT_4: 113

        .= (( IC ( Following (PRIJ,CRk))) + ( card I)) by EXTPRO_1: 3;

        then ( IC CRSk1) = ( IC CIJk1) by A18, A17, FUNCT_4: 113;

        hence thesis by A19, SCMPDS_4: 2;

      end;

      

       A20: X[ 0 ] by A6, SCMPDS_4: 2;

      for k be Nat holds X[k] from NAT_1:sch 2( A20, A9);

      hence thesis;

    end;

    

     Lm4: for I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS , s be 0 -started State of SCMPDS st ( stop (I ';' J)) c= P & P1 = (P +* ( stop I)) holds ( IC ( Comput (P,s,( LifeSpan (P1,s))))) = ( card I) & ( DataPart ( Comput (P,s,( LifeSpan (P1,s))))) = ( DataPart ( Initialize ( Comput (P1,s,( LifeSpan (P1,s)))))) & ( Shift (( stop J),( card I))) c= P & ( LifeSpan (P,s)) = (( LifeSpan (P1,s)) + ( LifeSpan ((P1 +* ( stop J)),( Initialize ( Result (P1,s))))))

    proof

      set D = SCM-Data-Loc ;

      let I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS , s be 0 -started State of SCMPDS ;

      set spJ = ( stop J), sIJ = ( stop (I ';' J)), m1 = ( LifeSpan (P1,s)), s3 = ( Initialize ( Comput (P1,s,m1))), P3 = (P1 +* spJ);

      set m3 = ( LifeSpan (P3,s3));

      assume that

       A1: sIJ c= P and

       A2: P1 = (P +* ( stop I));

      set s4 = ( Comput (P,s,m1)), P4 = P;

      

       A3: I c= sIJ by Th1;

      hence

       A4: ( IC s4) = ( card I) by A1, A2, Th14, XBOOLE_1: 1;

      reconsider m = (m1 + m3) as Nat;

      sIJ = (I ';' (J ';' ( Stop SCMPDS ))) by AFINSQ_1: 27

      .= (I +* ( Shift (spJ,( card I))));

      then

       A5: ( Shift (spJ,( card I))) c= sIJ by FUNCT_4: 25;

      

       A6: spJ c= P3 by FUNCT_4: 25;

      then

       A7: P3 halts_on s3 by SCMPDS_4:def 7;

      

       A8: ( DataPart ( Comput (P1,s,m1))) = ( DataPart s3) by MEMSTR_0: 45;

      (I ';' J) c= ( stop (I ';' J)) by AFINSQ_1: 74;

      then (P +* (I ';' J)) = P by A1, FUNCT_4: 98, XBOOLE_1: 1;

      hence

       A9: ( DataPart s4) = ( DataPart s3) by A8, A2, Th17;

      

       A10: ( Comput (P,s,(m1 + m3))) = ( Comput (P,( Comput (P,s,m1)),m3)) by EXTPRO_1: 4;

      thus

       A11: ( Shift (spJ,( card I))) c= P4 by A5, A1;

      then ( CurInstr (P3,( Comput (P3,s3,m3)))) = ( CurInstr (P,( Comput (P,s,(m1 + m3))))) by A10, A6, A4, A9, SCMPDS_4: 29;

      then

       A12: ( CurInstr (P,( Comput (P,s,m)))) = ( halt SCMPDS ) by A7, EXTPRO_1:def 15;

       A13:

      now

        let k be Nat;

        assume (m1 + k) < m;

        then

         A14: k < m3 by XREAL_1: 6;

        assume

         A15: ( CurInstr (P,( Comput (P,s,(m1 + k))))) = ( halt SCMPDS );

        

         A16: ( Comput (P,s,(m1 + k))) = ( Comput (P,( Comput (P,s,m1)),k)) by EXTPRO_1: 4;

        ( CurInstr (P3,( Comput (P3,s3,k)))) = ( halt SCMPDS ) by A15, A16, A6, A4, A9, A11, SCMPDS_4: 29;

        hence contradiction by A7, A14, EXTPRO_1:def 15;

      end;

      now

        let k be Nat;

        assume

         A17: k < m;

        per cases ;

          suppose k < m1;

          hence ( CurInstr (P,( Comput (P,s,k)))) <> ( halt SCMPDS ) by A2, Th16, A1, A3, XBOOLE_1: 1;

        end;

          suppose m1 <= k;

          then

          consider kk be Nat such that

           A18: (m1 + kk) = k by NAT_1: 10;

          thus ( CurInstr (P,( Comput (P,s,k)))) <> ( halt SCMPDS ) by A13, A17, A18;

        end;

      end;

      then

       A19: for k be Nat st ( CurInstr (P,( Comput (P,s,k)))) = ( halt SCMPDS ) holds m <= k;

      ( stop I) c= P1 by A2, FUNCT_4: 25;

      then P1 halts_on s by SCMPDS_4:def 7;

      then

       A20: ( Result (P1,s)) = ( Comput (P1,s,( LifeSpan (P1,s)))) by EXTPRO_1: 23;

      P halts_on s by A1, SCMPDS_4:def 7;

      hence thesis by A20, A12, A19, EXTPRO_1:def 15;

    end;

    theorem :: SCMPDS_5:33

    

     Th21: for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS holds ( LifeSpan ((P +* ( stop (I ';' J))),s)) = (( LifeSpan ((P +* ( stop I)),s)) + ( LifeSpan (((P +* ( stop I)) +* ( stop J)),( Initialize ( Result ((P +* ( stop I)),s))))))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS ;

      set sI = ( stop I), sIJ = ( stop (I ';' J)), s1 = s, s2 = s, P1 = (P +* sIJ), P2 = (P +* ( stop I));

      

       A1: sIJ c= P1 by FUNCT_4: 25;

      set s3 = ( Initialize ( Result ((P1 +* ( stop I)),s1))), P3 = ((P1 +* ( stop I)) +* ( stop J)), s4 = ( Initialize ( Result (P2,s2))), P4 = (P2 +* ( stop J));

      

       A2: ( stop I) c= P2 by FUNCT_4: 25;

      

       A3: ( stop J) c= P4 by FUNCT_4: 25;

      

       A4: ( stop J) c= P3 by FUNCT_4: 25;

      

       A5: ( stop I) c= (P1 +* ( stop I)) by FUNCT_4: 25;

      then s4 = s3 by A2, Th6;

      then

       A6: ( LifeSpan (P3,s3)) = ( LifeSpan (P4,s4)) by A4, A3, Th6;

      ( LifeSpan ((P1 +* ( stop I)),s1)) = ( LifeSpan (P2,s2)) by A5, A2, Th6;

      hence thesis by A1, A6, Lm4;

    end;

    theorem :: SCMPDS_5:34

    

     Th22: for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS holds ( IExec ((I ';' J),P,s)) = ( IncIC (( IExec (J,P,( Initialize ( IExec (I,P,s))))),( card I)))

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS ;

      set A = NAT , D = SCM-Data-Loc , sI = ( stop I), sIJ = ( stop (I ';' J)), P1 = (P +* ( stop I)), m1 = ( LifeSpan (P1,s)), P2 = (P +* ( stop (I ';' J))), s3 = ( Initialize ( Comput (P1,s,m1))), P3 = (P1 +* ( stop J)), m3 = ( LifeSpan (P3,s3));

      

       A1: ( stop J) c= P3 by FUNCT_4: 25;

      then

       A2: P3 halts_on s3 by SCMPDS_4:def 7;

      

       A3: ( stop J) c= (P +* ( stop J)) by FUNCT_4: 25;

      

       A4: ( stop I) c= P1 by FUNCT_4: 25;

      then P1 halts_on s by SCMPDS_4:def 7;

      then

       A5: ( Initialize ( Comput (P1,s,m1))) = ( Initialize ( IExec (I,P,s))) by EXTPRO_1: 23;

      

       A6: ( Result ((P +* ( stop J)),( Initialize ( IExec (I,P,s))))) = ( Result (P3,s3)) by A1, A3, Th6, A5;

      

       A7: ( stop I) c= (P2 +* ( stop I)) by FUNCT_4: 25;

      

       A8: ((P2 +* ( stop I)) +* sIJ) = (P2 +* (( stop I) +* sIJ)) by FUNCT_4: 14

      .= (P2 +* sIJ) by Th3;

      

       A9: ( LifeSpan ((P2 +* ( stop I)),s)) = m1 by A4, A7, Th6;

      set S1 = s, E1 = (P2 +* ( stop I));

      

       A10: ( Comput (P1,s,m1)) = ( Comput ((P1 +* ( stop (I ';' J))),s,m1)) by Th8, FUNCT_4: 25;

      

       A11: ((P +* ( stop I)) +* sIJ) = (P +* (( stop I) +* sIJ)) by FUNCT_4: 14

      .= (P +* (sIJ +* sIJ)) by Th3

      .= ((P2 +* ( stop I)) +* sIJ) by A8;

      

       A12: ( DataPart ( Comput ((P2 +* ( stop I)),s,m1))) = ( DataPart ( Comput (P1,s,m1))) by A11, A10, A9, Th8, FUNCT_4: 25;

      

       A13: sIJ c= P2 by FUNCT_4: 25;

      

      then

       A14: ( DataPart ( Comput (P2,s,m1))) = ( DataPart ( Initialize ( Comput ((P2 +* ( stop I)),s,m1)))) by A9, Lm4

      .= ( DataPart ( Comput ((P2 +* ( stop I)),s,m1))) by MEMSTR_0: 45;

      

       A15: ( Shift (( stop J),( card I))) c= P2 by A13, A7, Lm4;

      

       A16: ( IC ( Comput (P2,s,m1))) = ( card I) by A13, A9, Lm4;

      

       A17: ( DataPart ( Initialize ( Comput (P1,s,m1)))) = ( DataPart ( Comput (P2,s,m1))) by A12, A14, MEMSTR_0: 45;

      then

       A18: ( IC ( Comput (P2,( Comput (P2,s,m1)),m3))) = (( IC ( Comput (P3,s3,m3))) + ( card I)) by A15, A1, A16, SCMPDS_4: 29;

      

       A19: ( DataPart ( Comput (P2,( Comput (P2,s,m1)),m3))) = ( DataPart ( Comput (P3,s3,m3))) by A16, A15, A1, A17, SCMPDS_4: 29;

      

       A20: P1 halts_on s by A4, SCMPDS_4:def 7;

      then

       A21: s3 = ( Initialize ( Result (P1,s))) by EXTPRO_1: 23;

      set SS1 = (( Initialize ( Result (P1,s))) +* ( stop J)), SS2 = (( Initialize ( IExec (I,P,s))) +* ( stop J));

      

       A22: ( IC ( Result ((P1 +* ( stop J)),( Initialize ( Result (P1,s)))))) = ( IC ( Result ((P +* ( stop J)),( Initialize ( IExec (I,P,s)))))) by Th6, A1, A3;

      

       A23: P2 halts_on s by A13, SCMPDS_4:def 7;

      

       A24: ( IC ( IExec ((I ';' J),P,s))) = ( IC ( Comput (P2,s,( LifeSpan (P2,s))))) by A23, EXTPRO_1: 23

      .= ( IC ( Comput (P2,s,(m1 + m3)))) by A21, Th21

      .= (( IC ( Comput (P3,s3,m3))) + ( card I)) by A18, EXTPRO_1: 4

      .= (( IC ( Result (P3,s3))) + ( card I)) by A2, EXTPRO_1: 23

      .= (( IC ( IExec (J,P,( Initialize ( IExec (I,P,s)))))) + ( card I)) by A22, A20, EXTPRO_1: 23;

      ( IExec ((I ';' J),P,s)) = ( Comput (P2,s,( LifeSpan (P2,s)))) by A23, EXTPRO_1: 23

      .= ( Comput (P2,s,(m1 + m3))) by A21, Th21;

      

      then

       A25: ( DataPart ( IExec ((I ';' J),P,s))) = ( DataPart ( Comput (P3,s3,m3))) by A19, EXTPRO_1: 4

      .= ( DataPart ( IExec (J,P,( Initialize ( IExec (I,P,s)))))) by A6, A2, EXTPRO_1: 23;

      hereby

        reconsider l = (( IC ( IExec (J,P,( Initialize ( IExec (I,P,s)))))) + ( card I)) as Nat;

        

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

         A27:

        now

          let x be object;

          assume

           A28: x in ( dom ( IExec ((I ';' J),P,s)));

          per cases by A28, SCMPDS_4: 6;

            suppose

             A29: x is Int_position;

            then x <> ( IC SCMPDS ) by SCMPDS_2: 43;

            then

             A30: not x in ( dom ( Start-At (l, SCMPDS ))) by A26, TARSKI:def 1;

            (( IExec ((I ';' J),P,s)) . x) = (( IExec (J,P,( Initialize ( IExec (I,P,s))))) . x) by A25, A29, SCMPDS_4: 8;

            hence (( IExec ((I ';' J),P,s)) . x) = (( IncIC (( IExec (J,P,( Initialize ( IExec (I,P,s))))),( card I))) . x) by A30, FUNCT_4: 11;

          end;

            suppose

             A31: x = ( IC SCMPDS );

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

            then

             A32: x in ( dom ( Start-At (l, SCMPDS ))) by FUNCOP_1: 13;

            

            thus (( IExec ((I ';' J),P,s)) . x) = (( Start-At (l, SCMPDS )) . ( IC SCMPDS )) by A24, A31, FUNCOP_1: 72

            .= (( IncIC (( IExec (J,P,( Initialize ( IExec (I,P,s))))),( card I))) . x) by A31, A32, FUNCT_4: 13;

          end;

        end;

        ( dom ( IExec ((I ';' J),P,s))) = the carrier of SCMPDS by PARTFUN1:def 2

        .= ( dom ( IncIC (( IExec (J,P,( Initialize ( IExec (I,P,s))))),( card I)))) by PARTFUN1:def 2;

        hence thesis by A27, FUNCT_1: 2;

      end;

    end;

    theorem :: SCMPDS_5:35

    for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS holds (( IExec ((I ';' J),P,s)) . a) = (( IExec (J,P,( Initialize ( IExec (I,P,s))))) . a)

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS , J be parahalting shiftable Program of SCMPDS ;

      

       A1: not a in ( dom ( Start-At ((( IC ( IExec (J,P,( Initialize ( IExec (I,P,s)))))) + ( card I)), SCMPDS ))) by SCMPDS_4: 18;

      ( IExec ((I ';' J),P,s)) = ( IncIC (( IExec (J,P,( Initialize ( IExec (I,P,s))))),( card I))) by Th22;

      hence thesis by A1, FUNCT_4: 11;

    end;

    begin

    ::$Canceled

    theorem :: SCMPDS_5:37

    (s1 | ( SCM-Data-Loc \/ {( IC SCMPDS )})) = (s2 | ( SCM-Data-Loc \/ {( IC SCMPDS )})) implies s1 = s2

    proof

      set Y = NAT ;

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

      

       A1: s1 = (s1 | (( Data-Locations SCMPDS ) \/ {( IC SCMPDS )})) & s2 = (s2 | (( Data-Locations SCMPDS ) \/ {( IC SCMPDS )})) by MEMSTR_0: 33;

      thus thesis by A1, SCMPDS_2: 84;

    end;

    theorem :: SCMPDS_5:38

    

     Th25: ( DataPart s1) = ( DataPart s2) & ( InsCode i) <> 3 implies ( DataPart ( Exec (i,s1))) = ( DataPart ( Exec (i,s2)))

    proof

      assume that

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

       A2: ( InsCode i) <> 3;

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

      per cases by A2;

        suppose ( InsCode i) = 0 ;

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

        hence thesis by A1;

      end;

        suppose ( InsCode i) = 14;

        then

         A3: ex k1 st i = ( goto k1) by SCMPDS_2: 26;

        now

          let a;

          

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

          .= (s2 . a) by A1, SCMPDS_4: 8

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

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 1;

        then

        consider a such that

         A4: i = ( return a) by SCMPDS_2: 27;

        now

          let b;

          per cases ;

            suppose

             A5: a = b;

            

            hence (( Exec (i,s1)) . b) = (s1 . ( DataLoc ((s1 . a), RetSP ))) by A4, SCMPDS_2: 58

            .= (s2 . ( DataLoc ((s2 . a), RetSP ))) by A1, SCMPDS_3: 2

            .= (( Exec (i,s2)) . b) by A4, A5, SCMPDS_2: 58;

          end;

            suppose

             A6: a <> b;

            

            hence (( Exec (i,s1)) . b) = (s1 . b) by A4, SCMPDS_2: 58

            .= (s2 . b) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . b) by A4, A6, SCMPDS_2: 58;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 2;

        then

        consider a, k1 such that

         A7: i = (a := k1) by SCMPDS_2: 28;

        now

          let b;

          per cases ;

            suppose

             A8: a = b;

            

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

            .= (( Exec (i,s2)) . b) by A7, A8, SCMPDS_2: 45;

          end;

            suppose

             A9: a <> b;

            

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

            .= (s2 . b) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . b) by A7, A9, SCMPDS_2: 45;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 4;

        then

         A10: ex a, k1, k2 st i = ((a,k1) <>0_goto k2) by SCMPDS_2: 30;

        now

          let a;

          

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

          .= (s2 . a) by A1, SCMPDS_4: 8

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

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 5;

        then

         A11: ex a, k1, k2 st i = ((a,k1) <=0_goto k2) by SCMPDS_2: 31;

        now

          let a;

          

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

          .= (s2 . a) by A1, SCMPDS_4: 8

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

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 6;

        then

         A12: ex a, k1, k2 st i = ((a,k1) >=0_goto k2) by SCMPDS_2: 32;

        now

          let a;

          

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

          .= (s2 . a) by A1, SCMPDS_4: 8

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

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 7;

        then

        consider a, k1, k2 such that

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

        now

          let b;

          per cases ;

            suppose

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

            then

             A15: ( DataLoc ((s2 . a),k1)) = b by A1, SCMPDS_4: 8;

            

            thus (( Exec (i,s1)) . b) = k2 by A13, A14, SCMPDS_2: 46

            .= (( Exec (i,s2)) . b) by A13, A15, SCMPDS_2: 46;

          end;

            suppose

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

            then

             A17: ( DataLoc ((s2 . a),k1)) <> b by A1, SCMPDS_4: 8;

            

            thus (( Exec (i,s1)) . b) = (s1 . b) by A13, A16, SCMPDS_2: 46

            .= (s2 . b) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . b) by A13, A17, SCMPDS_2: 46;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 8;

        then

        consider a, k1, k2 such that

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

        now

          let b;

          per cases ;

            suppose

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

            then

             A20: ( DataLoc ((s2 . a),k1)) = b by A1, SCMPDS_4: 8;

            

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

            .= ((s2 . ( DataLoc ((s2 . a),k1))) + k2) by A1, SCMPDS_3: 2

            .= (( Exec (i,s2)) . b) by A18, A20, SCMPDS_2: 48;

          end;

            suppose

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

            then

             A22: ( DataLoc ((s2 . a),k1)) <> b by A1, SCMPDS_4: 8;

            

            thus (( Exec (i,s1)) . b) = (s1 . b) by A18, A21, SCMPDS_2: 48

            .= (s2 . b) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . b) by A18, A22, SCMPDS_2: 48;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 9;

        then

        consider a, b, k1, k2 such that

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

        now

          let c;

          per cases ;

            suppose

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

            then

             A25: ( DataLoc ((s2 . a),k1)) = c by A1, SCMPDS_4: 8;

            

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

            .= ((s2 . ( DataLoc ((s2 . a),k1))) + (s1 . ( DataLoc ((s1 . b),k2)))) by A1, SCMPDS_3: 2

            .= ((s2 . ( DataLoc ((s2 . a),k1))) + (s2 . ( DataLoc ((s2 . b),k2)))) by A1, SCMPDS_3: 2

            .= (( Exec (i,s2)) . c) by A23, A25, SCMPDS_2: 49;

          end;

            suppose

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

            then

             A27: ( DataLoc ((s2 . a),k1)) <> c by A1, SCMPDS_4: 8;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A23, A26, SCMPDS_2: 49

            .= (s2 . c) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . c) by A23, A27, SCMPDS_2: 49;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 10;

        then

        consider a, b, k1, k2 such that

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

        now

          let c;

          per cases ;

            suppose

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

            then

             A30: ( DataLoc ((s2 . a),k1)) = c by A1, SCMPDS_4: 8;

            

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

            .= ((s2 . ( DataLoc ((s2 . a),k1))) - (s1 . ( DataLoc ((s1 . b),k2)))) by A1, SCMPDS_3: 2

            .= ((s2 . ( DataLoc ((s2 . a),k1))) - (s2 . ( DataLoc ((s2 . b),k2)))) by A1, SCMPDS_3: 2

            .= (( Exec (i,s2)) . c) by A28, A30, SCMPDS_2: 50;

          end;

            suppose

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

            then

             A32: ( DataLoc ((s2 . a),k1)) <> c by A1, SCMPDS_4: 8;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A28, A31, SCMPDS_2: 50

            .= (s2 . c) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . c) by A28, A32, SCMPDS_2: 50;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 11;

        then

        consider a, b, k1, k2 such that

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

        now

          let c;

          per cases ;

            suppose

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

            then

             A35: ( DataLoc ((s2 . a),k1)) = c by A1, SCMPDS_4: 8;

            

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

            .= ((s2 . ( DataLoc ((s2 . a),k1))) * (s1 . ( DataLoc ((s1 . b),k2)))) by A1, SCMPDS_3: 2

            .= ((s2 . ( DataLoc ((s2 . a),k1))) * (s2 . ( DataLoc ((s2 . b),k2)))) by A1, SCMPDS_3: 2

            .= (( Exec (i,s2)) . c) by A33, A35, SCMPDS_2: 51;

          end;

            suppose

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

            then

             A37: ( DataLoc ((s2 . a),k1)) <> c by A1, SCMPDS_4: 8;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A33, A36, SCMPDS_2: 51

            .= (s2 . c) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . c) by A33, A37, SCMPDS_2: 51;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 12;

        then

        consider a, b, k1, k2 such that

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

        now

          let c;

          per cases ;

            suppose

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

            then

             A40: ( DataLoc ((s2 . b),k2)) = c by A1, SCMPDS_4: 8;

            

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

            .= ((s2 . ( DataLoc ((s2 . a),k1))) mod (s1 . ( DataLoc ((s1 . b),k2)))) by A1, SCMPDS_3: 2

            .= ((s2 . ( DataLoc ((s2 . a),k1))) mod (s2 . ( DataLoc ((s2 . b),k2)))) by A1, SCMPDS_3: 2

            .= (( Exec (i,s2)) . c) by A38, A40, SCMPDS_2: 52;

          end;

            suppose

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

            then

             A42: ( DataLoc ((s2 . b),k2)) <> c by A1, SCMPDS_4: 8;

            hereby

              per cases ;

                suppose

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

                then

                 A44: ( DataLoc ((s2 . a),k1)) <> c by A1, SCMPDS_4: 8;

                

                thus (( Exec (i,s1)) . c) = (s1 . c) by A38, A41, A43, SCMPDS_2: 52

                .= (s2 . c) by A1, SCMPDS_4: 8

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

              end;

                suppose

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

                then

                 A46: ( DataLoc ((s2 . a),k1)) = c by A1, SCMPDS_4: 8;

                

                thus (( Exec (i,s1)) . c) = ((s1 . ( DataLoc ((s1 . a),k1))) div (s1 . ( DataLoc ((s1 . b),k2)))) by A38, A41, A45, SCMPDS_2: 52

                .= ((s2 . ( DataLoc ((s2 . a),k1))) div (s1 . ( DataLoc ((s1 . b),k2)))) by A1, SCMPDS_3: 2

                .= ((s2 . ( DataLoc ((s2 . a),k1))) div (s2 . ( DataLoc ((s2 . b),k2)))) by A1, SCMPDS_3: 2

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

              end;

            end;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

        suppose ( InsCode i) = 13;

        then

        consider a, b, k1, k2 such that

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

        now

          let c;

          per cases ;

            suppose

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

            then

             A49: ( DataLoc ((s2 . a),k1)) = c by A1, SCMPDS_4: 8;

            

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

            .= (s2 . ( DataLoc ((s2 . b),k2))) by A1, SCMPDS_3: 2

            .= (( Exec (i,s2)) . c) by A47, A49, SCMPDS_2: 47;

          end;

            suppose

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

            then

             A51: ( DataLoc ((s2 . a),k1)) <> c by A1, SCMPDS_4: 8;

            

            thus (( Exec (i,s1)) . c) = (s1 . c) by A47, A50, SCMPDS_2: 47

            .= (s2 . c) by A1, SCMPDS_4: 8

            .= (( Exec (i,s2)) . c) by A47, A51, SCMPDS_2: 47;

          end;

        end;

        hence thesis by SCMPDS_4: 8;

      end;

    end;

    theorem :: SCMPDS_5:39

    

     Th26: for i be shiftable Instruction of SCMPDS holds (( DataPart s1) = ( DataPart s2) implies ( DataPart ( Exec (i,s1))) = ( DataPart ( Exec (i,s2))))

    proof

      let i be shiftable Instruction of SCMPDS ;

      ( InsCode i) <> 3 by SCMPDS_4:def 10;

      hence thesis by Th25;

    end;

    theorem :: SCMPDS_5:40

    

     Th27: for s be 0 -started State of SCMPDS holds for i be parahalting Instruction of SCMPDS holds ( Exec (i,s)) = ( IExec (( Load i),P,s))

    proof

      let s be 0 -started State of SCMPDS ;

      let i be parahalting Instruction of SCMPDS ;

      set Li = ( Load i), Mi = ( Macro i);

      set PI = (P +* Mi);

      set IC1 = ( IC ( Comput (PI,s,1)));

      

       A1: ( Initialize s) = s by MEMSTR_0: 44;

      Mi c= PI by FUNCT_4: 25;

      then

       A2: PI halts_on s by SCMPDS_4:def 7;

      

       A3: 1 in ( dom Mi) by COMPOS_1: 57;

      

       A4: 0 in ( dom Mi) by COMPOS_1: 57;

      

       A5: (Mi . 1) = ( halt SCMPDS ) by COMPOS_1: 59;

      

       A6: (Mi . 0 ) = i by COMPOS_1: 58;

      

       A7: Mi c= PI by FUNCT_4: 25;

      then

       A8: IC1 in ( dom Mi) by SCMPDS_4:def 6;

      

       A9: (PI /. ( IC s)) = (PI . ( IC s)) by PBOOLE: 143;

      

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

      .= ( Following (PI,s))

      .= ( Exec ((PI . 0 ),s)) by A9, A1, MEMSTR_0: 47

      .= ( Exec (i,s)) by A4, A6, A7, GRFUNC_1: 2;

      per cases by A8, COMPOS_1: 60;

        suppose

         A11: IC1 = 0 ;

        set Ni = ( InsCode i);

        (( IC s) + 1) = ( 0 + 1) by A1, MEMSTR_0: 47;

        then

         A12: Ni in { 0 , 1, 4, 5, 6, 14} by A10, A11, SCMPDS_4: 1;

        

         A13: ( CurInstr (PI,( Comput (PI,s,1)))) = (PI . 0 ) by A11, PBOOLE: 143

        .= i by A4, A6, A7, GRFUNC_1: 2;

        

         A14: Ni <> 1 by Th10;

        hereby

          per cases ;

            suppose i = ( halt SCMPDS );

            hence thesis by A2, A10, A13, EXTPRO_1:def 9;

          end;

            suppose

             A15: i <> ( halt SCMPDS );

             A16:

            now

              let b;

              per cases by A12, A14, ENUMSET1:def 4;

                suppose ( InsCode i) = 0 ;

                hence (s . b) = (( Exec (i,s)) . b) by SCMPDS_2: 86;

              end;

                suppose ( InsCode i) = 14;

                then ex k1 st i = ( goto k1) by SCMPDS_2: 26;

                hence (s . b) = (( Exec (i,s)) . b) by SCMPDS_2: 54;

              end;

                suppose ( InsCode i) = 4;

                then ex a, k1, k2 st i = ((a,k1) <>0_goto k2) by SCMPDS_2: 30;

                hence (s . b) = (( Exec (i,s)) . b) by SCMPDS_2: 55;

              end;

                suppose ( InsCode i) = 5;

                then ex a, k1, k2 st i = ((a,k1) <=0_goto k2) by SCMPDS_2: 31;

                hence (s . b) = (( Exec (i,s)) . b) by SCMPDS_2: 56;

              end;

                suppose ( InsCode i) = 6;

                then ex a, k1, k2 st i = ((a,k1) >=0_goto k2) by SCMPDS_2: 32;

                hence (s . b) = (( Exec (i,s)) . b) by SCMPDS_2: 57;

              end;

            end;

            

             A17: ( Following (PI,s)) = ( Following (PI,( Comput (PI,s, 0 ))))

            .= ( Exec (i,s)) by A10, EXTPRO_1: 3;

            

             A18: ( IC s) = ( IC ( Exec (i,s))) by A10, A11, A1, MEMSTR_0: 47;

            then

             A19: s = ( Exec (i,s)) by A16, SCMPDS_2: 44;

            now

              let n;

              ( Comput (PI,s,n)) = s by A18, A16, A17, EXTPRO_1: 27, SCMPDS_2: 44

              .= ( Following (PI,( Comput (PI,s, 0 )))) by A19, A17

              .= ( Comput (PI,s,( 0 + 1))) by EXTPRO_1: 3;

              hence ( CurInstr (PI,( Comput (PI,s,n)))) <> ( halt SCMPDS ) by A13, A15;

            end;

            then not PI halts_on s;

            hence thesis by A7, SCMPDS_4:def 7;

          end;

        end;

      end;

        suppose

         A20: IC1 = 1;

        ( CurInstr (PI,( Comput (PI,s,1)))) = (PI . 1) by A20, PBOOLE: 143

        .= ( halt SCMPDS ) by A3, A5, A7, GRFUNC_1: 2;

        hence thesis by A2, A10, EXTPRO_1:def 9;

      end;

    end;

    theorem :: SCMPDS_5:41

    

     Th28: for s be 0 -started State of SCMPDS holds for I be parahalting halt-free Program of SCMPDS , j be parahalting shiftable Instruction of SCMPDS holds (( IExec ((I ';' j),P,s)) . a) = (( Exec (j,( IExec (I,P,s)))) . a)

    proof

      let s be 0 -started State of SCMPDS ;

      let I be parahalting halt-free Program of SCMPDS , j be parahalting shiftable Instruction of SCMPDS ;

      set Mj = ( Load j);

      set SA = ( Start-At ((( IC ( IExec (Mj,P,( Initialize ( IExec (I,P,s)))))) + ( card I)), SCMPDS ));

      

       A1: not a in ( dom SA) by SCMPDS_4: 18;

      

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

      for a holds (( Initialize ( IExec (I,P,s))) . a) = (( IExec (I,P,s)) . a) by Th4;

      then

       A3: ( DataPart ( Initialize ( IExec (I,P,s)))) = ( DataPart ( IExec (I,P,s))) by SCMPDS_4: 8;

      

      thus (( IExec ((I ';' j),P,s)) . a) = (( IncIC (( IExec (Mj,P,( Initialize ( IExec (I,P,s))))),( card I))) . a) by Th22

      .= (( IExec (Mj,P,( Initialize ( IExec (I,P,s))))) . a) by A1, FUNCT_4: 11

      .= (( Exec (j,( Initialize ( IExec (I,P,s))))) . a) by Th27

      .= (( DataPart ( Exec (j,( Initialize ( IExec (I,P,s)))))) . a) by A2, FUNCT_1: 49, SCMPDS_2: 84

      .= (( DataPart ( Exec (j,( IExec (I,P,s))))) . a) by A3, Th26

      .= (( Exec (j,( IExec (I,P,s)))) . a) by A2, FUNCT_1: 49, SCMPDS_2: 84;

    end;

    theorem :: SCMPDS_5:42

    for s be 0 -started State of SCMPDS holds for i be No-StopCode parahalting Instruction of SCMPDS , j be shiftable parahalting Instruction of SCMPDS holds (( IExec ((i ';' j),P,s)) . a) = (( Exec (j,( Exec (i,s)))) . a)

    proof

      let s be 0 -started State of SCMPDS ;

      let i be No-StopCode parahalting Instruction of SCMPDS , j be shiftable parahalting Instruction of SCMPDS ;

      set Mi = ( Load i);

      

      thus (( IExec ((i ';' j),P,s)) . a) = (( IExec ((Mi ';' j),P,s)) . a)

      .= (( Exec (j,( IExec (Mi,P,s)))) . a) by Th28

      .= (( Exec (j,( Exec (i,s)))) . a) by Th27;

    end;