scmpds_1.miz



    begin

    reserve i,j,k for Element of NAT ,

I,I2,I3,I4 for Element of ( Segm 15),

i1 for Element of NAT ,

d1,d2,d3,d4,d5 for Element of SCM-Data-Loc ,

k1,k2 for Integer;

    ::$Canceled

    theorem :: SCMPDS_1:3

    for d be Element of SCM-Data-Loc holds d in ( SCM-Data-Loc \/ INT ) by XBOOLE_1: 7, TARSKI:def 3;

    begin

    definition

      ::$Canceled

      let s be SCM-State, a be Element of SCM-Data-Loc , n be Integer;

      :: SCMPDS_1:def6

      func Address_Add (s,a,n) -> Element of SCM-Data-Loc equals [1, |.((s . a) + n).|];

      coherence by AMI_2: 24;

    end

    definition

      let s be SCM-State, n be Integer;

      :: SCMPDS_1:def7

      func jump_address (s,n) -> Element of NAT equals |.(( IC s) qua Element of NAT + n).|;

      coherence ;

    end

    definition

      let d be Element of SCM-Data-Loc , s be Integer;

      :: original: <*

      redefine

      func <*d,s*> -> FinSequence of ( SCM-Data-Loc \/ INT ) ;

      coherence

      proof

        let y be object;

        

         A1: ( dom <*d, s*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        assume y in ( rng <*d, s*>);

        then

        consider x be object such that

         A2: x in ( dom <*d, s*>) and

         A3: ( <*d, s*> . x) = y by FUNCT_1:def 3;

        per cases by A2, A1, TARSKI:def 2;

          suppose x = 1;

          then y = d by A3, FINSEQ_1: 44;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A4: x = 2;

          

           A5: s in INT by INT_1:def 2;

          y = s by A3, A4, FINSEQ_1: 44;

          hence thesis by A5, XBOOLE_0:def 3;

        end;

      end;

    end

    definition

      ::$Canceled

      let s be SCM-State, a be Element of SCM-Data-Loc ;

      :: SCMPDS_1:def19

      func PopInstrLoc (s,a) -> Element of NAT equals ( |.(s . a).| + 2);

      coherence ;

    end

    ::$Canceled

    definition

      let x be Element of SCMPDS-Instr , s be SCM-State;

      :: SCMPDS_1:def20

      func SCM-Exec-Res (x,s) -> SCM-State equals ( SCM-Chg (s,( jump_address (s,(x const_INT ))))) if ( InsCode x) = 14,

( SCM-Chg (( SCM-Chg (s,(x P21address ),(x P22const ))),(( IC s) + 1))) if ( InsCode x) = 2,

( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P21address ),(x P22const ))),( IC s) qua Element of NAT )),(( IC s) + 1))) if ( InsCode x) = 3,

( SCM-Chg (( SCM-Chg (s,(x address_1 ),(s . ( Address_Add (s,(x address_1 ), RetSP ))))),( PopInstrLoc (s,( Address_Add (s,(x address_1 ), RetIC )))))) if ( InsCode x) = 1,

( SCM-Chg (s,( IFEQ ((s . ( Address_Add (s,(x P31address ),(x P32const )))), 0 ,(( IC s) + 1),( jump_address (s,(x P33const ))))))) if ( InsCode x) = 4,

( SCM-Chg (s,( IFGT ((s . ( Address_Add (s,(x P31address ),(x P32const )))), 0 ,(( IC s) + 1),( jump_address (s,(x P33const ))))))) if ( InsCode x) = 5,

( SCM-Chg (s,( IFGT ( 0 ,(s . ( Address_Add (s,(x P31address ),(x P32const )))),(( IC s) + 1),( jump_address (s,(x P33const ))))))) if ( InsCode x) = 6,

( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P31address ),(x P32const ))),(x P33const ))),(( IC s) + 1))) if ( InsCode x) = 7,

( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P31address ),(x P32const ))),((s . ( Address_Add (s,(x P31address ),(x P32const )))) + (x P33const )))),(( IC s) + 1))) if ( InsCode x) = 8,

( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P41address ),(x P43const ))),((s . ( Address_Add (s,(x P41address ),(x P43const )))) + (s . ( Address_Add (s,(x P42address ),(x P44const ))))))),(( IC s) + 1))) if ( InsCode x) = 9,

( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P41address ),(x P43const ))),((s . ( Address_Add (s,(x P41address ),(x P43const )))) - (s . ( Address_Add (s,(x P42address ),(x P44const ))))))),(( IC s) + 1))) if ( InsCode x) = 10,

( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P41address ),(x P43const ))),((s . ( Address_Add (s,(x P41address ),(x P43const )))) * (s . ( Address_Add (s,(x P42address ),(x P44const ))))))),(( IC s) + 1))) if ( InsCode x) = 11,

( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P41address ),(x P43const ))),(s . ( Address_Add (s,(x P42address ),(x P44const )))))),(( IC s) + 1))) if ( InsCode x) = 13,

( SCM-Chg (( SCM-Chg (( SCM-Chg (s,( Address_Add (s,(x P41address ),(x P43const ))),((s . ( Address_Add (s,(x P41address ),(x P43const )))) div (s . ( Address_Add (s,(x P42address ),(x P44const ))))))),( Address_Add (s,(x P42address ),(x P44const ))),((s . ( Address_Add (s,(x P41address ),(x P43const )))) mod (s . ( Address_Add (s,(x P42address ),(x P44const ))))))),(( IC s) + 1))) if ( InsCode x) = 12

      otherwise s;

      coherence ;

      consistency ;

    end

    definition

      :: SCMPDS_1:def21

      func SCMPDS-Exec -> Action of SCMPDS-Instr , ( product ( SCM-VAL * SCM-OK )) means for x be Element of SCMPDS-Instr , y be SCM-State holds ((it . x) . y) = ( SCM-Exec-Res (x,y));

      existence

      proof

        consider f be Function of [: SCMPDS-Instr , ( product ( SCM-VAL * SCM-OK )):], ( product ( SCM-VAL * SCM-OK )) such that

         A1: for x be Element of SCMPDS-Instr , y be SCM-State holds (f . (x,y)) = ( SCM-Exec-Res (x,y)) from BINOP_1:sch 4;

        take ( curry f);

        let x be Element of SCMPDS-Instr , y be SCM-State;

        

        thus ((( curry f) . x) . y) = (f . (x,y)) by FUNCT_5: 69

        .= ( SCM-Exec-Res (x,y)) by A1;

      end;

      uniqueness

      proof

        let f,g be Action of SCMPDS-Instr , ( product ( SCM-VAL * SCM-OK )) such that

         A2: for x be Element of SCMPDS-Instr , y be SCM-State holds ((f . x) . y) = ( SCM-Exec-Res (x,y)) and

         A3: for x be Element of SCMPDS-Instr , y be SCM-State holds ((g . x) . y) = ( SCM-Exec-Res (x,y));

        now

          let x be Element of SCMPDS-Instr ;

          reconsider gx = (g . x), fx = (f . x) as Function of ( product ( SCM-VAL * SCM-OK )), ( product ( SCM-VAL * SCM-OK )) by FUNCT_2: 66;

          now

            let y be SCM-State;

            

            thus (fx . y) = ( SCM-Exec-Res (x,y)) by A2

            .= (gx . y) by A3;

          end;

          hence (f . x) = (g . x) by FUNCT_2: 63;

        end;

        hence f = g by FUNCT_2: 63;

      end;

    end