ami_2.miz



    begin

    reserve x,y,z for set;

    definition

      :: AMI_2:def1

      func SCM-Memory -> set equals ( { NAT } \/ SCM-Data-Loc );

      coherence ;

    end

    registration

      cluster SCM-Memory -> non empty;

      coherence ;

    end

    definition

      :: original: SCM-Data-Loc

      redefine

      func SCM-Data-Loc -> Subset of SCM-Memory ;

      coherence by XBOOLE_1: 7;

    end

    reserve I,J,K for Element of ( Segm 9),

i,a,a1,a2 for Nat,

b,b1,b2,c,c1 for Element of SCM-Data-Loc ;

     Lm1:

    now

      let k be Element of SCM-Memory ;

      k in { NAT } or k in SCM-Data-Loc by XBOOLE_0:def 3;

      hence k = NAT or k in SCM-Data-Loc by TARSKI:def 1;

    end;

    

     Lm2: not NAT in SCM-Data-Loc

    proof

      assume NAT in SCM-Data-Loc ;

      then NAT in [: {1}, NAT :];

      then ex x,y be object st NAT = [x, y] by RELAT_1:def 1;

      hence contradiction;

    end;

    definition

      ::$Canceled

      :: AMI_2:def4

      func SCM-OK -> Function of SCM-Memory , ( Segm 2) means

      : Def2: for k be Element of SCM-Memory holds (k = NAT implies (it . k) = 0 ) & (k in SCM-Data-Loc implies (it . k) = 1);

      existence

      proof

        defpred P[ set, set] means $1 = NAT & $2 = 0 or $1 in SCM-Data-Loc & $2 = 1;

         A1:

        now

          let k be Element of SCM-Memory ;

          

           A2: ( { 0 } \/ {1}) = { 0 , 1} by ENUMSET1: 1;

          then

           A3: 0 in ( {1} \/ { 0 }) by TARSKI:def 2;

          

           A4: P[k, 0 ] or P[k, 1] by Lm1;

          1 in ( {1} \/ { 0 }) by A2, TARSKI:def 2;

          hence ex b be Element of ( Segm 2) st P[k, b] by A2, A3, A4, CARD_1: 50;

        end;

        consider h be Function of SCM-Memory , ( Segm 2) such that

         A5: for a be Element of SCM-Memory holds P[a, (h . a)] from FUNCT_2:sch 3( A1);

        take h;

        let k be Element of SCM-Memory ;

        thus k = NAT implies (h . k) = 0 by A5, Lm2;

        thus k in SCM-Data-Loc implies (h . k) = 1 by A5, Lm2;

        thus thesis;

      end;

      uniqueness

      proof

        let f,g be Function of SCM-Memory , ( Segm 2) such that

         A6: for k be Element of SCM-Memory holds (k = NAT implies (f . k) = 0 ) & (k in SCM-Data-Loc implies (f . k) = 1) and

         A7: for k be Element of SCM-Memory holds (k = NAT implies (g . k) = 0 ) & (k in SCM-Data-Loc implies (g . k) = 1);

        now

          let k be Element of SCM-Memory ;

          now

            per cases by Lm1;

              suppose

               A8: k = NAT ;

              

              hence (f . k) = 0 by A6

              .= (g . k) by A7, A8;

            end;

              suppose

               A9: k in SCM-Data-Loc ;

              

              hence (f . k) = 1 by A6

              .= (g . k) by A7, A9;

            end;

          end;

          hence (f . k) = (g . k);

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    ::$Canceled

    definition

      :: AMI_2:def5

      func SCM-VAL -> ManySortedSet of ( Segm 2) equals <% NAT , INT %>;

      coherence ;

    end

    

     Lm3: NAT in SCM-Memory

    proof

       NAT in { NAT } by TARSKI:def 1;

      hence thesis by XBOOLE_0:def 3;

    end;

    ::$Canceled

    theorem :: AMI_2:6

    

     Th1: (( SCM-VAL * SCM-OK ) . NAT ) = NAT

    proof

       NAT in ( dom SCM-OK ) by Lm3, PARTFUN1:def 2;

      then

       A1: (( SCM-VAL * SCM-OK ) . NAT ) = ( SCM-VAL . ( SCM-OK . NAT )) by FUNCT_1: 13;

      (( SCM-VAL * SCM-OK ) . NAT ) = ( SCM-VAL . 0 ) by A1, Def2, Lm3;

      hence thesis;

    end;

    theorem :: AMI_2:7

    

     Th2: for i be Element of SCM-Memory holds i in SCM-Data-Loc implies (( SCM-VAL * SCM-OK ) . i) = INT

    proof

      let i be Element of SCM-Memory ;

      i in SCM-Memory ;

      then i in ( dom SCM-OK ) by PARTFUN1:def 2;

      then

       A1: (( SCM-VAL * SCM-OK ) . i) = ( SCM-VAL . ( SCM-OK . i)) by FUNCT_1: 13;

      assume i in SCM-Data-Loc ;

      then (( SCM-VAL * SCM-OK ) . i) = ( SCM-VAL . 1) by A1, Def2;

      hence thesis;

    end;

    

     Lm4: ( dom SCM-OK ) = SCM-Memory by PARTFUN1:def 2;

    ( len <% NAT , INT %>) = 2 by AFINSQ_1: 38;

    then ( rng SCM-OK ) c= ( dom SCM-VAL ) by RELAT_1:def 19;

    then

     Lm5: ( dom ( SCM-VAL * SCM-OK )) = SCM-Memory by Lm4, RELAT_1: 27;

    registration

      cluster ( SCM-VAL * SCM-OK ) -> non-empty;

      coherence

      proof

        set F = ( SCM-VAL * SCM-OK );

        let n be object;

        assume

         A1: n in ( dom F);

        per cases by A1, Lm1, Lm5;

          suppose n = NAT ;

          hence (F . n) is non empty by Th1;

        end;

          suppose n in SCM-Data-Loc ;

          hence (F . n) is non empty by Th2;

        end;

      end;

    end

    definition

      mode SCM-State is Element of ( product ( SCM-VAL * SCM-OK ));

    end

    theorem :: AMI_2:8

    for a be Element of SCM-Data-Loc holds (( SCM-VAL * SCM-OK ) . a) = INT by Th2;

    theorem :: AMI_2:9

    

     Th4: ( pi (( product ( SCM-VAL * SCM-OK )), NAT )) = NAT by Th1, Lm5, Lm3, CARD_3: 12;

    theorem :: AMI_2:10

    

     Th5: for a be Element of SCM-Data-Loc holds ( pi (( product ( SCM-VAL * SCM-OK )),a)) = INT

    proof

      let a be Element of SCM-Data-Loc ;

      

      thus ( pi (( product ( SCM-VAL * SCM-OK )),a)) = (( SCM-VAL * SCM-OK ) . a) by Lm5, CARD_3: 12

      .= INT by Th2;

    end;

    definition

      let s be SCM-State;

      :: AMI_2:def6

      func IC (s) -> Element of NAT equals (s . NAT );

      coherence by Th4, CARD_3:def 6;

    end

    definition

      let s be SCM-State, u be natural Number;

      :: AMI_2:def7

      func SCM-Chg (s,u) -> SCM-State equals (s +* ( NAT .--> u));

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom ( SCM-VAL * SCM-OK ));

          per cases ;

            suppose

             A3: x = NAT ;

             NAT in ( dom ( NAT .--> u)) by TARSKI:def 1;

            

            then ((s +* ( NAT .--> u)) . NAT ) = (( NAT .--> u) . NAT ) by FUNCT_4: 13

            .= u by FUNCOP_1: 72;

            hence ((s +* ( NAT .--> u)) . x) in (( SCM-VAL * SCM-OK ) . x) by A3, Th1, ORDINAL1:def 12;

          end;

            suppose

             A4: x <> NAT ;

             not x in ( dom ( NAT .--> u)) by A4, TARSKI:def 1;

            then ((s +* ( NAT .--> u)) . x) = (s . x) by FUNCT_4: 11;

            hence ((s +* ( NAT .--> u)) . x) in (( SCM-VAL * SCM-OK ) . x) by A2, CARD_3: 9;

          end;

        end;

        ( dom s) = SCM-Memory by Lm5, CARD_3: 9;

        

        then ( dom (s +* ( NAT .--> u))) = ( SCM-Memory \/ ( dom ( NAT .--> u))) by FUNCT_4:def 1

        .= ( SCM-Memory \/ { NAT })

        .= ( dom ( SCM-VAL * SCM-OK )) by Lm5, Lm3, ZFMISC_1: 40;

        hence thesis by A1, CARD_3: 9;

      end;

    end

    theorem :: AMI_2:11

    for s be SCM-State, u be natural Number holds (( SCM-Chg (s,u)) . NAT ) = u

    proof

      let s be SCM-State, u be natural Number;

       NAT in ( dom ( NAT .--> u)) by TARSKI:def 1;

      

      hence (( SCM-Chg (s,u)) . NAT ) = (( NAT .--> u) . NAT ) by FUNCT_4: 13

      .= u by FUNCOP_1: 72;

    end;

    theorem :: AMI_2:12

    for s be SCM-State, u be natural Number, mk be Element of SCM-Data-Loc holds (( SCM-Chg (s,u)) . mk) = (s . mk)

    proof

      let s be SCM-State, u be natural Number, mk be Element of SCM-Data-Loc ;

      (( SCM-VAL * SCM-OK ) . NAT ) = NAT & (( SCM-VAL * SCM-OK ) . mk) = INT by Th1, Th2;

      then not mk in ( dom ( NAT .--> u)) by NUMBERS: 7, TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: AMI_2:13

    for s be SCM-State, u,v be natural Number holds (( SCM-Chg (s,u)) . v) = (s . v)

    proof

      let s be SCM-State, u,v be natural Number;

       not v in ( dom ( NAT .--> u)) by TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    definition

      let s be SCM-State, t be Element of SCM-Data-Loc , u be Integer;

      :: AMI_2:def8

      func SCM-Chg (s,t,u) -> SCM-State equals (s +* (t .--> u));

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom ( SCM-VAL * SCM-OK ));

          per cases ;

            suppose

             A3: x = t;

            t in ( dom (t .--> u)) by TARSKI:def 1;

            

            then ((s +* (t .--> u)) . t) = ((t .--> u) . t) by FUNCT_4: 13

            .= u by FUNCOP_1: 72;

            then ((s +* (t .--> u)) . t) in INT by INT_1:def 2;

            hence ((s +* (t .--> u)) . x) in (( SCM-VAL * SCM-OK ) . x) by A3, Th2;

          end;

            suppose

             A4: x <> t;

             not x in ( dom (t .--> u)) by A4, TARSKI:def 1;

            then ((s +* (t .--> u)) . x) = (s . x) by FUNCT_4: 11;

            hence ((s +* (t .--> u)) . x) in (( SCM-VAL * SCM-OK ) . x) by A2, CARD_3: 9;

          end;

        end;

        ( dom s) = SCM-Memory by Lm5, CARD_3: 9;

        

        then ( dom (s +* (t .--> u))) = ( SCM-Memory \/ ( dom (t .--> u))) by FUNCT_4:def 1

        .= ( SCM-Memory \/ {t})

        .= ( dom ( SCM-VAL * SCM-OK )) by Lm5, ZFMISC_1: 40;

        hence thesis by A1, CARD_3: 9;

      end;

    end

    theorem :: AMI_2:14

    for s be SCM-State, t be Element of SCM-Data-Loc , u be Integer holds (( SCM-Chg (s,t,u)) . NAT ) = (s . NAT )

    proof

      let s be SCM-State, t be Element of SCM-Data-Loc , u be Integer;

      (( SCM-VAL * SCM-OK ) . NAT ) = NAT & (( SCM-VAL * SCM-OK ) . t) = INT by Th1, Th2;

      then not NAT in ( dom (t .--> u)) by NUMBERS: 7, TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: AMI_2:15

    for s be SCM-State, t be Element of SCM-Data-Loc , u be Integer holds (( SCM-Chg (s,t,u)) . t) = u

    proof

      let s be SCM-State, t be Element of SCM-Data-Loc , u be Integer;

      t in ( dom (t .--> u)) by TARSKI:def 1;

      

      hence (( SCM-Chg (s,t,u)) . t) = ((t .--> u) . t) by FUNCT_4: 13

      .= u by FUNCOP_1: 72;

    end;

    theorem :: AMI_2:16

    for s be SCM-State, t be Element of SCM-Data-Loc , u be Integer, mk be Element of SCM-Data-Loc st mk <> t holds (( SCM-Chg (s,t,u)) . mk) = (s . mk)

    proof

      let s be SCM-State, t be Element of SCM-Data-Loc , u be Integer, mk be Element of SCM-Data-Loc such that

       A1: mk <> t;

       not mk in ( dom (t .--> u)) by A1, TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    registration

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

      cluster (s . a) -> integer;

      coherence

      proof

        (s . a) in ( pi (( product ( SCM-VAL * SCM-OK )),a)) by CARD_3:def 6;

        then (s . a) in INT by Th5;

        hence thesis;

      end;

    end

    registration

      let x,y be ExtReal, a,b be Nat;

      cluster ( IFGT (x,y,a,b)) -> natural;

      coherence ;

    end

    definition

      ::$Canceled

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

      :: AMI_2:def14

      func SCM-Exec-Res (x,s) -> SCM-State equals ( SCM-Chg (( SCM-Chg (s,(x address_1 ),(s . (x address_2 )))),(( IC s) + 1))) if ex mk,ml be Element of SCM-Data-Loc st x = [1, {} , <*mk, ml*>],

( SCM-Chg (( SCM-Chg (s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 ))))),(( IC s) + 1))) if ex mk,ml be Element of SCM-Data-Loc st x = [2, {} , <*mk, ml*>],

( SCM-Chg (( SCM-Chg (s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 ))))),(( IC s) + 1))) if ex mk,ml be Element of SCM-Data-Loc st x = [3, {} , <*mk, ml*>],

( SCM-Chg (( SCM-Chg (s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 ))))),(( IC s) + 1))) if ex mk,ml be Element of SCM-Data-Loc st x = [4, {} , <*mk, ml*>],

( SCM-Chg (( SCM-Chg (( SCM-Chg (s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 ))))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 ))))),(( IC s) + 1))) if ex mk,ml be Element of SCM-Data-Loc st x = [5, {} , <*mk, ml*>],

( SCM-Chg (s,(x jump_address ))) if ex mk be Nat st x = [6, <*mk*>, {} ],

( SCM-Chg (s,( IFEQ ((s . (x cond_address )), 0 ,(x cjump_address ),(( IC s) + 1))))) if ex mk be Nat, ml be Element of SCM-Data-Loc st x = [7, <*mk*>, <*ml*>],

( SCM-Chg (s,( IFGT ((s . (x cond_address )), 0 ,(x cjump_address ),(( IC s) + 1))))) if ex mk be Nat, ml be Element of SCM-Data-Loc st x = [8, <*mk*>, <*ml*>]

      otherwise s;

      consistency by XTUPLE_0: 3;

      coherence ;

    end

    definition

      :: AMI_2:def15

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

      existence

      proof

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

         A1: for x be Element of SCM-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 SCM-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 SCM-Instr , ( product ( SCM-VAL * SCM-OK )) such that

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

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

        now

          let x be Element of SCM-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

    begin

    ::$Canceled

    theorem :: AMI_2:20

     not NAT in SCM-Data-Loc by Lm2;

    ::$Canceled

    theorem :: AMI_2:22

     NAT in SCM-Memory by Lm3;

    theorem :: AMI_2:23

    x in SCM-Data-Loc implies ex k be Nat st x = [1, k]

    proof

      assume x in SCM-Data-Loc ;

      then

      consider y,z be object such that

       A1: y in {1} and

       A2: z in NAT and

       A3: x = [y, z] by ZFMISC_1: 84;

      reconsider k = z as Nat by A2;

      take k;

      thus thesis by A1, A3, TARSKI:def 1;

    end;

    theorem :: AMI_2:24

    for k be Nat holds [1, k] in SCM-Data-Loc

    proof

      let k be Nat;

      1 in {1} & k in NAT by ORDINAL1:def 12, TARSKI:def 1;

      hence thesis by ZFMISC_1: 87;

    end;

    ::$Canceled

    theorem :: AMI_2:26

    for k be Element of SCM-Memory holds k = NAT or k in SCM-Data-Loc by Lm1;

    theorem :: AMI_2:27

    ( dom ( SCM-VAL * SCM-OK )) = SCM-Memory by Lm5;

    theorem :: AMI_2:28

    for s be SCM-State holds ( dom s) = SCM-Memory by Lm5, CARD_3: 9;

    definition

      let x be set;

      :: AMI_2:def16

      attr x is Int-like means x in SCM-Data-Loc ;

    end

    theorem :: AMI_2:29

    for S be SCM-State holds S is total SCM-Memory -defined Function;