scm_1.miz



    begin

    registration

      let i1 be Integer;

      cluster <%i1%> -> INT -valued;

      coherence ;

      let i2 be Integer;

      cluster <%i1, i2%> -> INT -valued;

      coherence ;

      let i3 be Integer;

      cluster <%i1, i2, i3%> -> INT -valued;

      coherence ;

      let i4 be Integer;

      cluster <%i1, i2, i3, i4%> -> INT -valued;

      coherence ;

    end

    definition

      let D be XFinSequence of INT ;

      :: SCM_1:def1

      mode State-consisting of D -> State of SCM means

      : Def1: for k be Element of NAT st k < ( len D) holds (it . ( dl. k)) = (D . k);

      existence

      proof

        defpred P[ object, object] means ex k be Element of NAT st $1 = ( dl. k) & $2 = (D . k);

        

         A1: for x,y be object st x in the carrier of SCM & P[x, y] holds y in INT by INT_1:def 2;

        

         A2: for x,y1,y2 be object st x in the carrier of SCM & P[x, y1] & P[x, y2] holds y1 = y2 by AMI_3: 10;

        consider p be PartFunc of SCM , INT such that

         A3: for x be object holds x in ( dom p) iff x in the carrier of SCM & ex y be object st P[x, y] and

         A4: for x be object st x in ( dom p) holds P[x, (p . x)] from PARTFUN1:sch 2( A1, A2);

        

         A5: p is the carrier of SCM -defined

        proof

          let e be object;

          thus thesis by A3;

        end;

        p is ( the_Values_of SCM ) -compatible

        proof

          let e be object;

          assume

           A6: e in ( dom p);

          then

           A7: ex y be object st P[e, y] by A3;

          reconsider o = e as Object of SCM by A6, A3;

          

           A8: ( Values o) = INT by A7, AMI_3: 11;

          consider k be Element of NAT such that

           A9: o = ( dl. k) & (p . o) = (D . k) by A4, A6;

          thus (p . e) in (( the_Values_of SCM ) . e) by A8, A9, INT_1:def 2;

        end;

        then

        reconsider p as PartState of SCM by A5;

        take s = ( the State of SCM +* p);

        let k be Element of NAT ;

        assume k < ( len D);

        ex i be Element of NAT st ( dl. k) = ( dl. i) & (D . k) = (D . i);

        then

         A10: ( dl. k) in ( dom p) by A3;

        then

        consider i be Element of NAT such that

         A11: ( dl. k) = ( dl. i) & (p . ( dl. k)) = (D . i) by A4;

        

         A12: k = i by A11, AMI_3: 10;

        p c= s by FUNCT_4: 25;

        hence (s . ( dl. k)) = (D . k) by A12, A11, A10, GRFUNC_1: 2;

      end;

    end

    registration

      let D be XFinSequence of INT , il be Element of NAT ;

      cluster il -started for State-consisting of D;

      existence

      proof

        set s = the State-consisting of D;

        set s1 = (s +* ( Start-At (il, SCM )));

        for k be Element of NAT st k < ( len D) holds (s1 . ( dl. k)) = (D . k)

        proof

          let k be Element of NAT ;

          assume

           A1: k < ( len D);

          

           A2: ( dom ( Start-At (il, SCM ))) = {( IC SCM )} by FUNCOP_1: 13;

          ( dl. k) <> ( IC SCM ) by AMI_3: 13;

          then not ( dl. k) in ( dom ( Start-At (il, SCM ))) by A2, TARSKI:def 1;

          

          hence (s1 . ( dl. k)) = (s . ( dl. k)) by FUNCT_4: 11

          .= (D . k) by A1, Def1;

        end;

        then

        reconsider s1 as State-consisting of D by Def1;

        take s1;

        thus ( IC s1) = il by MEMSTR_0: 16;

      end;

    end

    theorem :: SCM_1:1

    for i1,i2,i3,i4 be Integer, il be Element of NAT , s be il -started State-consisting of <%i1, i2, i3, i4%> holds (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2 & (s . ( dl. 2)) = i3 & (s . ( dl. 3)) = i4

    proof

      let i1,i2,i3,i4 be Integer, il be Element of NAT , s be il -started State-consisting of <%i1, i2, i3, i4%>;

      set D = <%i1, i2, i3, i4%>;

      

       A1: (D . 2) = i3 & (D . 3) = i4;

      

       A2: ( len D) = 4 & ( 0 + 0 ) = 0 by AFINSQ_1: 84;

      (D . 0 ) = i1 & (D . 1) = i2;

      hence thesis by A1, A2, Def1;

    end;

    theorem :: SCM_1:2

    

     Th2: for i1,i2 be Integer, il be Element of NAT , s be il -started State-consisting of <%i1, i2%> holds (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2

    proof

      let i1,i2 be Integer, il be Element of NAT , s be il -started State-consisting of <%i1, i2%>;

      set data = <%i1, i2%>;

      

       A1: ( len data) = 2 & (data . 0 ) = i1 by AFINSQ_1: 38;

      (data . 1) = i2;

      hence thesis by A1, Def1;

    end;

    theorem :: SCM_1:3

    

     Th3: for I1,I2 be Instruction of SCM holds for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%I1%> ^ <%I2%>) c= F holds (F . 0 ) = I1 & (F . 1) = I2

    proof

      let I1,I2 be Instruction of SCM ;

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%I1%> ^ <%I2%>) c= F;

      set ins = ( <%I1%> ^ <%I2%>);

      

       A2: ins = <%I1, I2%>;

      then

       A3: (ins . 1) = I2;

      

       A4: (ins . 0 ) = I1 by A2;

      ( len ins) = 2 by A2, AFINSQ_1: 38;

      then 0 in ( dom ins) & 1 in ( dom ins) by CARD_1: 50, TARSKI:def 2;

      hence thesis by A1, A3, A4, GRFUNC_1: 2;

    end;

    reserve F for total NAT -definedthe InstructionsF of SCM -valued Function;

    

     Lm1: for k be Nat, s be State of SCM holds ( Comput (F,s,(k + 1))) = ( Exec (( CurInstr (F,( Comput (F,s,k)))),( Comput (F,s,k))))

    proof

      let k be Nat, s be State of SCM ;

      

      thus ( Comput (F,s,(k + 1))) = ( Following (F,( Comput (F,s,k)))) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (F,( Comput (F,s,k)))),( Comput (F,s,k))));

    end;

     Lm2:

    now

      let F be total NAT -definedthe InstructionsF of SCM -valued Function;

      let k,n be Element of NAT , s be State of SCM , a,b be Data-Location;

      assume

       A1: ( IC ( Comput (F,s,k))) = n;

      set csk1 = ( Comput (F,s,(k + 1)));

      set csk = ( Comput (F,s,k));

      assume

       A2: (F . n) = (a := b) or (F . n) = ( AddTo (a,b)) or (F . n) = ( SubFrom (a,b)) or (F . n) = ( MultBy (a,b)) or a <> b & (F . n) = ( Divide (a,b));

      

       A3: ( dom F) = NAT by PARTFUN1:def 2;

      

      thus csk1 = ( Exec (( CurInstr (F,csk)),csk)) by Lm1

      .= ( Exec ((F . n),csk)) by A1, A3, PARTFUN1:def 6;

      

      hence ( IC csk1) = (( IC csk) + 1) by A2, AMI_3: 2, AMI_3: 3, AMI_3: 4, AMI_3: 5, AMI_3: 6

      .= (n + 1) by A1;

    end;

    theorem :: SCM_1:4

    

     Th4: for k,n be Element of NAT , s be State of SCM , a,b be Data-Location st ( IC ( Comput (F,s,k))) = n & (F . n) = (a := b) holds ( IC ( Comput (F,s,(k + 1)))) = (n + 1) & (( Comput (F,s,(k + 1))) . a) = (( Comput (F,s,k)) . b) & for d be Data-Location st d <> a holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Element of NAT , s be State of SCM , a,b be Data-Location;

      assume

       A1: ( IC ( Comput (F,s,k))) = n;

      assume (F . n) = (a := b);

      then ( Comput (F,s,(k + 1))) = ( Exec ((a := b),( Comput (F,s,k)))) by A1, Lm2;

      hence thesis by A1, AMI_3: 2;

    end;

    theorem :: SCM_1:5

    

     Th5: for k,n be Element of NAT , s be State of SCM , a,b be Data-Location st ( IC ( Comput (F,s,k))) = n & (F . n) = ( AddTo (a,b)) holds ( IC ( Comput (F,s,(k + 1)))) = (n + 1) & (( Comput (F,s,(k + 1))) . a) = ((( Comput (F,s,k)) . a) + (( Comput (F,s,k)) . b)) & for d be Data-Location st d <> a holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Element of NAT , s be State of SCM , a,b be Data-Location;

      assume

       A1: ( IC ( Comput (F,s,k))) = n;

      assume (F . n) = ( AddTo (a,b));

      then ( Comput (F,s,(k + 1))) = ( Exec (( AddTo (a,b)),( Comput (F,s,k)))) by A1, Lm2;

      hence thesis by A1, AMI_3: 3;

    end;

    theorem :: SCM_1:6

    

     Th6: for k,n be Element of NAT , s be State of SCM , a,b be Data-Location st ( IC ( Comput (F,s,k))) = n & (F . n) = ( SubFrom (a,b)) holds ( IC ( Comput (F,s,(k + 1)))) = (n + 1) & (( Comput (F,s,(k + 1))) . a) = ((( Comput (F,s,k)) . a) - (( Comput (F,s,k)) . b)) & for d be Data-Location st d <> a holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Element of NAT , s be State of SCM , a,b be Data-Location;

      assume

       A1: ( IC ( Comput (F,s,k))) = n;

      assume (F . n) = ( SubFrom (a,b));

      then ( Comput (F,s,(k + 1))) = ( Exec (( SubFrom (a,b)),( Comput (F,s,k)))) by A1, Lm2;

      hence thesis by A1, AMI_3: 4;

    end;

    theorem :: SCM_1:7

    

     Th7: for k,n be Element of NAT , s be State of SCM , a,b be Data-Location st ( IC ( Comput (F,s,k))) = n & (F . n) = ( MultBy (a,b)) holds ( IC ( Comput (F,s,(k + 1)))) = (n + 1) & (( Comput (F,s,(k + 1))) . a) = ((( Comput (F,s,k)) . a) * (( Comput (F,s,k)) . b)) & for d be Data-Location st d <> a holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Element of NAT , s be State of SCM , a,b be Data-Location;

      assume

       A1: ( IC ( Comput (F,s,k))) = n;

      assume (F . n) = ( MultBy (a,b));

      then ( Comput (F,s,(k + 1))) = ( Exec (( MultBy (a,b)),( Comput (F,s,k)))) by A1, Lm2;

      hence thesis by A1, AMI_3: 5;

    end;

    theorem :: SCM_1:8

    

     Th8: for k,n be Element of NAT , s be State of SCM , a,b be Data-Location st ( IC ( Comput (F,s,k))) = n & (F . n) = ( Divide (a,b)) & a <> b holds ( IC ( Comput (F,s,(k + 1)))) = (n + 1) & (( Comput (F,s,(k + 1))) . a) = ((( Comput (F,s,k)) . a) div (( Comput (F,s,k)) . b)) & (( Comput (F,s,(k + 1))) . b) = ((( Comput (F,s,k)) . a) mod (( Comput (F,s,k)) . b)) & for d be Data-Location st d <> a & d <> b holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Element of NAT , s be State of SCM , a,b be Data-Location;

      assume

       A1: ( IC ( Comput (F,s,k))) = n;

      assume

       A2: (F . n) = ( Divide (a,b)) & a <> b;

      then ( Comput (F,s,(k + 1))) = ( Exec (( Divide (a,b)),( Comput (F,s,k)))) by A1, Lm2;

      hence thesis by A1, A2, AMI_3: 6;

    end;

    theorem :: SCM_1:9

    

     Th9: for k,n be Element of NAT , s be State of SCM , il be Element of NAT st ( IC ( Comput (F,s,k))) = n & (F . n) = ( SCM-goto il) holds ( IC ( Comput (F,s,(k + 1)))) = il & for d be Data-Location holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Element of NAT , s be State of SCM , il be Element of NAT ;

      assume

       A1: ( IC ( Comput (F,s,k))) = n & (F . n) = ( SCM-goto il);

      set csk1 = ( Comput (F,s,(k + 1)));

      set csk = ( Comput (F,s,k));

      

       A2: ( dom F) = NAT by PARTFUN1:def 2;

      

       A3: csk1 = ( Exec (( CurInstr (F,csk)),csk)) by Lm1

      .= ( Exec (( SCM-goto il),csk)) by A1, A2, PARTFUN1:def 6;

      hence ( IC csk1) = il by AMI_3: 7;

      thus thesis by A3, AMI_3: 7;

    end;

    theorem :: SCM_1:10

    

     Th10: for k,n be Nat, s be State of SCM , a be Data-Location, il be Element of NAT st ( IC ( Comput (F,s,k))) = n & (F . n) = (a =0_goto il) holds ((( Comput (F,s,k)) . a) = 0 implies ( IC ( Comput (F,s,(k + 1)))) = il) & ((( Comput (F,s,k)) . a) <> 0 implies ( IC ( Comput (F,s,(k + 1)))) = (n + 1)) & for d be Data-Location holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Nat, s be State of SCM , a be Data-Location, il be Element of NAT ;

      assume that

       A1: ( IC ( Comput (F,s,k))) = n and

       A2: (F . n) = (a =0_goto il);

      set csk1 = ( Comput (F,s,(k + 1)));

      set csk = ( Comput (F,s,k));

      

       A3: ( dom F) = NAT by PARTFUN1:def 2;

      

       A4: csk1 = ( Exec (( CurInstr (F,csk)),csk)) by Lm1

      .= ( Exec ((a =0_goto il),csk)) by A1, A2, A3, PARTFUN1:def 6;

      hence (csk . a) = 0 implies ( IC csk1) = il by AMI_3: 8;

      thus thesis by A1, A4, AMI_3: 8;

    end;

    theorem :: SCM_1:11

    

     Th11: for k,n be Element of NAT , s be State of SCM , a be Data-Location, il be Element of NAT st ( IC ( Comput (F,s,k))) = n & (F . n) = (a >0_goto il) holds ((( Comput (F,s,k)) . a) > 0 implies ( IC ( Comput (F,s,(k + 1)))) = il) & ((( Comput (F,s,k)) . a) <= 0 implies ( IC ( Comput (F,s,(k + 1)))) = (n + 1)) & for d be Data-Location holds (( Comput (F,s,(k + 1))) . d) = (( Comput (F,s,k)) . d)

    proof

      let k,n be Element of NAT , s be State of SCM , a be Data-Location, il be Element of NAT ;

      assume that

       A1: ( IC ( Comput (F,s,k))) = n and

       A2: (F . n) = (a >0_goto il);

      set csk1 = ( Comput (F,s,(k + 1)));

      set csk = ( Comput (F,s,k));

      

       A3: ( dom F) = NAT by PARTFUN1:def 2;

      csk1 = ( Exec (( CurInstr (F,csk)),csk)) by Lm1

      .= ( Exec ((a >0_goto il),csk)) by A1, A2, A3, PARTFUN1:def 6;

      hence thesis by A1, AMI_3: 9;

    end;

    theorem :: SCM_1:12

    

     Th12: (( halt SCM ) `1_3 ) = 0 & (for a,b be Data-Location holds ((a := b) `1_3 ) = 1) & (for a,b be Data-Location holds (( AddTo (a,b)) `1_3 ) = 2) & (for a,b be Data-Location holds (( SubFrom (a,b)) `1_3 ) = 3) & (for a,b be Data-Location holds (( MultBy (a,b)) `1_3 ) = 4) & (for a,b be Data-Location holds (( Divide (a,b)) `1_3 ) = 5) & (for i be Element of NAT holds (( SCM-goto i) `1_3 ) = 6) & (for a be Data-Location, i be Element of NAT holds ((a =0_goto i) `1_3 ) = 7) & for a be Data-Location, i be Element of NAT holds ((a >0_goto i) `1_3 ) = 8 by AMI_3: 26;

    theorem :: SCM_1:13

    for i1,i2,i3,i4 be Integer, s be State of SCM st (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2 & (s . ( dl. 2)) = i3 & (s . ( dl. 3)) = i4 holds s is State-consisting of <%i1, i2, i3, i4%>

    proof

      let i1,i2,i3,i4 be Integer, s be State of SCM such that

       A1: (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2 & (s . ( dl. 2)) = i3 & (s . ( dl. 3)) = i4;

      set D = <%i1, i2, i3, i4%>;

      now

        let k be Element of NAT ;

        

         A2: ( len D) = 4 & 4 = (3 + 1) by AFINSQ_1: 84;

        assume k < ( len D);

        then k <= 3 by A2, NAT_1: 13;

        then k = 0 or ... or k = 3;

        hence (s . ( dl. k)) = (D . k) by A1;

      end;

      hence thesis by Def1;

    end;

    theorem :: SCM_1:14

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st <%( halt SCM )%> c= F holds for s be 0 -started State-consisting of ( <*> INT ) holds F halts_on s & ( LifeSpan (F,s)) = 0 & ( Result (F,s)) = s

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: <%( halt SCM )%> c= F;

      let s be 0 -started State-consisting of ( <*> INT );

      1 = ( len <%( halt SCM )%>) by AFINSQ_1: 34;

      then 0 in ( dom <%( halt SCM )%>) by CARD_1: 49, TARSKI:def 1;

      

      then

       A2: (F . ( 0 + 0 )) = ( <%( halt SCM )%> . 0 ) by A1, GRFUNC_1: 2

      .= ( halt SCM );

      

       A3: s = ( Comput (F,s, 0 )) by EXTPRO_1: 2;

      (F . ( IC s)) = ( halt SCM ) by A2, MEMSTR_0:def 11;

      hence

       A4: F halts_on s by A3, EXTPRO_1: 30;

      ( dom F) = NAT by PARTFUN1:def 2;

      

      then ( CurInstr (F,s)) = (F . ( IC s)) by PARTFUN1:def 6

      .= ( halt SCM ) by A2, MEMSTR_0:def 11;

      hence ( LifeSpan (F,s)) = 0 by A4, A3, EXTPRO_1:def 15;

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

      hence thesis by A2, A3, EXTPRO_1: 7;

    end;

    theorem :: SCM_1:15

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%(( dl. 0 ) := ( dl. 1))%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & (( Result (F,s)) . ( dl. 0 )) = i2 & for d be Data-Location st d <> ( dl. 0 ) holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%(( dl. 0 ) := ( dl. 1))%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: (s . ( dl. 1)) = i2 by Th2;

      

       A3: ( IC s) = 0 & s = ( Comput (F,s, 0 )) by EXTPRO_1: 2, MEMSTR_0:def 11;

      

       A4: (F . 0 ) = (( dl. 0 ) := ( dl. 1)) by A1, Th3;

      then

       A5: ( IC s1) = ( 0 + 1) by A3, Th4;

      

       A6: (F . 1) = ( halt SCM ) by A1, Th3;

      hence F halts_on s by A5, EXTPRO_1: 30;

      thus ( LifeSpan (F,s)) = 1 by A6, A3, A5, EXTPRO_1: 33;

      (s1 . ( dl. 0 )) = (s . ( dl. 1)) by A4, A3, Th4;

      hence (( Result (F,s)) . ( dl. 0 )) = i2 by A6, A2, A5, EXTPRO_1: 7;

      let d be Data-Location;

      assume

       A7: d <> ( dl. 0 );

      

      thus (( Result (F,s)) . d) = (s1 . d) by A6, A5, EXTPRO_1: 7

      .= (s . d) by A4, A3, A7, Th4;

    end;

    theorem :: SCM_1:16

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%( AddTo (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & (( Result (F,s)) . ( dl. 0 )) = (i1 + i2) & for d be Data-Location st d <> ( dl. 0 ) holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%( AddTo (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s0 = ( Comput (F,s, 0 ));

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: s = s0 by EXTPRO_1: 2;

      

       A3: (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2 by Th2;

      

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

      

       A5: (F . 0 ) = ( AddTo (( dl. 0 ),( dl. 1))) by A1, Th3;

      then

       A6: ( IC s1) = ( 0 + 1) by A4, A2, Th5;

      

       A7: (F . 1) = ( halt SCM ) by A1, Th3;

      hence F halts_on s by A6, EXTPRO_1: 30;

      thus ( LifeSpan (F,s)) = 1 by A4, A7, A2, A6, EXTPRO_1: 33;

      (s1 . ( dl. 0 )) = ((s0 . ( dl. 0 )) + (s0 . ( dl. 1))) by A4, A5, A2, Th5;

      hence (( Result (F,s)) . ( dl. 0 )) = (i1 + i2) by A7, A3, A2, A6, EXTPRO_1: 7;

      let d be Data-Location;

      assume

       A8: d <> ( dl. 0 );

      

      thus (( Result (F,s)) . d) = (s1 . d) by A7, A6, EXTPRO_1: 7

      .= (s . d) by A4, A5, A2, A8, Th5;

    end;

    theorem :: SCM_1:17

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%( SubFrom (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & (( Result (F,s)) . ( dl. 0 )) = (i1 - i2) & for d be Data-Location st d <> ( dl. 0 ) holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%( SubFrom (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s0 = ( Comput (F,s, 0 ));

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: s = s0 by EXTPRO_1: 2;

      

       A3: (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2 by Th2;

      

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

      

       A5: (F . 0 ) = ( SubFrom (( dl. 0 ),( dl. 1))) by A1, Th3;

      then

       A6: ( IC s1) = ( 0 + 1) by A4, A2, Th6;

      

       A7: (F . 1) = ( halt SCM ) by A1, Th3;

      hence F halts_on s by A6, EXTPRO_1: 30;

      thus ( LifeSpan (F,s)) = 1 by A4, A7, A2, A6, EXTPRO_1: 33;

      (s1 . ( dl. 0 )) = ((s0 . ( dl. 0 )) - (s0 . ( dl. 1))) by A4, A5, A2, Th6;

      hence (( Result (F,s)) . ( dl. 0 )) = (i1 - i2) by A7, A3, A2, A6, EXTPRO_1: 7;

      let d be Data-Location;

      assume

       A8: d <> ( dl. 0 );

      

      thus (( Result (F,s)) . d) = (s1 . d) by A7, A6, EXTPRO_1: 7

      .= (s . d) by A4, A5, A2, A8, Th6;

    end;

    theorem :: SCM_1:18

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%( MultBy (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & (( Result (F,s)) . ( dl. 0 )) = (i1 * i2) & for d be Data-Location st d <> ( dl. 0 ) holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%( MultBy (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s0 = ( Comput (F,s, 0 ));

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: s = s0 by EXTPRO_1: 2;

      

       A3: (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2 by Th2;

      

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

      

       A5: (F . 0 ) = ( MultBy (( dl. 0 ),( dl. 1))) by A1, Th3;

      then

       A6: ( IC s1) = ( 0 + 1) by A4, A2, Th7;

      

       A7: (F . 1) = ( halt SCM ) by A1, Th3;

      hence F halts_on s by A6, EXTPRO_1: 30;

      thus ( LifeSpan (F,s)) = 1 by A4, A7, A2, A6, EXTPRO_1: 33;

      (s1 . ( dl. 0 )) = ((s0 . ( dl. 0 )) * (s0 . ( dl. 1))) by A4, A5, A2, Th7;

      hence (( Result (F,s)) . ( dl. 0 )) = (i1 * i2) by A7, A3, A2, A6, EXTPRO_1: 7;

      let d be Data-Location;

      assume

       A8: d <> ( dl. 0 );

      

      thus (( Result (F,s)) . d) = (s1 . d) by A7, A6, EXTPRO_1: 7

      .= (s . d) by A4, A5, A2, A8, Th7;

    end;

    theorem :: SCM_1:19

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%( Divide (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & (( Result (F,s)) . ( dl. 0 )) = (i1 div i2) & (( Result (F,s)) . ( dl. 1)) = (i1 mod i2) & for d be Data-Location st d <> ( dl. 0 ) & d <> ( dl. 1) holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%( Divide (( dl. 0 ),( dl. 1)))%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: ( dl. 0 ) <> ( dl. 1) by AMI_3: 10;

      

       A3: ( IC s) = 0 & (F . 0 ) = ( Divide (( dl. 0 ),( dl. 1))) by A1, Th3, MEMSTR_0:def 11;

      

       A4: (s . ( dl. 0 )) = i1 & (s . ( dl. 1)) = i2 by Th2;

      

       A5: s = ( Comput (F,s, 0 )) by EXTPRO_1: 2;

      (F . 1) = ( halt SCM ) by A1, Th3;

      then

       A6: (F . ( IC s1)) = ( halt SCM ) by A3, A2, A5, Th8;

      hence F halts_on s by EXTPRO_1: 30;

      ( Divide (( dl. 0 ),( dl. 1))) <> ( halt SCM ) by Th12;

      hence ( LifeSpan (F,s)) = 1 by A3, A5, A6, EXTPRO_1: 32;

      

      thus (( Result (F,s)) . ( dl. 0 )) = (s1 . ( dl. 0 )) by A6, EXTPRO_1: 7

      .= (i1 div i2) by A3, A4, A2, A5, Th8;

      

      thus (( Result (F,s)) . ( dl. 1)) = (s1 . ( dl. 1)) by A6, EXTPRO_1: 7

      .= (i1 mod i2) by A3, A4, A2, A5, Th8;

      let d be Data-Location;

      assume

       A7: d <> ( dl. 0 ) & d <> ( dl. 1);

      

      thus (( Result (F,s)) . d) = (s1 . d) by A6, EXTPRO_1: 7

      .= (s . d) by A3, A2, A5, A7, Th8;

    end;

    theorem :: SCM_1:20

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%( SCM-goto 1)%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & for d be Data-Location holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%( SCM-goto 1)%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: ( IC s) = 0 & s = ( Comput (F,s, 0 )) by EXTPRO_1: 2, MEMSTR_0:def 11;

      

       A3: (F . 0 ) = ( SCM-goto 1) by A1, Th3;

      then

       A4: ( IC s1) = ( 0 + 1) by A2, Th9;

      

       A5: (F . 1) = ( halt SCM ) by A1, Th3;

      hence F halts_on s by A4, EXTPRO_1: 30;

      thus ( LifeSpan (F,s)) = 1 by A5, A2, A4, EXTPRO_1: 33;

      let d be Data-Location;

      

      thus (( Result (F,s)) . d) = (s1 . d) by A5, A4, EXTPRO_1: 7

      .= (s . d) by A3, A2, Th9;

    end;

    theorem :: SCM_1:21

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%(( dl. 0 ) =0_goto 1)%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & for d be Data-Location holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%(( dl. 0 ) =0_goto 1)%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: (F . 0 ) = (( dl. 0 ) =0_goto 1) by A1, Th3;

      

       A3: (F . 1) = ( halt SCM ) by A1, Th3;

      

       A4: ( IC s) = 0 & s = ( Comput (F,s, 0 )) by EXTPRO_1: 2, MEMSTR_0:def 11;

      (s . ( dl. 0 )) = i1 by Th2;

      then

       A5: ( IC s1) = ( 0 + 1) by A2, A4, Th10;

      hence F halts_on s by A3, EXTPRO_1: 30;

      thus ( LifeSpan (F,s)) = 1 by A3, A4, A5, EXTPRO_1: 33;

      let d be Data-Location;

      

      thus (( Result (F,s)) . d) = (s1 . d) by A3, A5, EXTPRO_1: 7

      .= (s . d) by A2, A4, Th10;

    end;

    theorem :: SCM_1:22

    for F be total NAT -definedthe InstructionsF of SCM -valued Function st ( <%(( dl. 0 ) >0_goto 1)%> ^ <%( halt SCM )%>) c= F holds for i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%> holds F halts_on s & ( LifeSpan (F,s)) = 1 & for d be Data-Location holds (( Result (F,s)) . d) = (s . d)

    proof

      let F be total NAT -definedthe InstructionsF of SCM -valued Function such that

       A1: ( <%(( dl. 0 ) >0_goto 1)%> ^ <%( halt SCM )%>) c= F;

      let i1,i2 be Integer, s be 0 -started State-consisting of <%i1, i2%>;

      set s1 = ( Comput (F,s,( 0 + 1)));

      

       A2: (F . 0 ) = (( dl. 0 ) >0_goto 1) by A1, Th3;

      

       A3: (F . 1) = ( halt SCM ) by A1, Th3;

      

       A4: ( IC s) = 0 & s = ( Comput (F,s, 0 )) by EXTPRO_1: 2, MEMSTR_0:def 11;

      (s . ( dl. 0 )) = i1 by Th2;

      then

       A5: ( IC s1) = ( 0 + 1) by A2, A4, Th11;

      hence F halts_on s by A3, EXTPRO_1: 30;

      thus ( LifeSpan (F,s)) = 1 by A3, A4, A5, EXTPRO_1: 33;

      let d be Data-Location;

      

      thus (( Result (F,s)) . d) = (s1 . d) by A3, A5, EXTPRO_1: 7

      .= (s . d) by A2, A4, Th11;

    end;

    theorem :: SCM_1:23

    for s be State of SCM holds s is State-consisting of ( <*> INT )

    proof

      let s be State of SCM ;

      let k be Element of NAT ;

      thus thesis;

    end;