scmring1.miz



    begin

    reserve i,j,k for Element of NAT ,

I for Element of ( Segm 8),

i1,i2 for Element of NAT ,

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

S for non empty 1-sorted;

    reserve G for non empty 1-sorted;

    definition

      ::$Canceled

      let S be non empty 1-sorted;

      :: SCMRING1:def3

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

      coherence ;

    end

    

     Lm1: ( dom (( SCM-VAL S) * SCM-OK )) = SCM-Memory

    proof

      

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

      ( len <% NAT , the carrier of S%>) = 2 by AFINSQ_1: 38;

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

      hence ( dom (( SCM-VAL S) * SCM-OK )) = SCM-Memory by A1, RELAT_1: 27;

    end;

    ::$Canceled

    theorem :: SCMRING1:2

    

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

    proof

      

       A1: NAT in SCM-Memory by AMI_2: 22;

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

      then

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

      ((( SCM-VAL G) * SCM-OK ) . NAT ) = (( SCM-VAL G) . 0 ) by A2, A1, AMI_2:def 4;

      hence thesis;

    end;

    theorem :: SCMRING1:3

    

     Th2: for i be Element of SCM-Memory st i in SCM-Data-Loc holds ((( SCM-VAL G) * SCM-OK ) . i) = the carrier of G

    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 G) * SCM-OK ) . i) = (( SCM-VAL G) . ( SCM-OK . i)) by FUNCT_1: 13;

      assume i in SCM-Data-Loc ;

      then ((( SCM-VAL G) * SCM-OK ) . i) = (( SCM-VAL G) . 1) by A1, AMI_2:def 4;

      hence thesis;

    end;

    registration

      let G;

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

      coherence

      proof

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

        let n be object;

        assume

         A1: n in ( dom F);

        ( dom F) = SCM-Memory by Lm1;

        per cases by A1, AMI_2: 26;

          suppose

           A2: n = NAT ;

          ((( SCM-VAL G) * SCM-OK ) . n) = NAT by A2, Th1;

          hence (F . n) is non empty;

        end;

          suppose n in SCM-Data-Loc ;

          then ((( SCM-VAL G) * SCM-OK ) . n) = the carrier of G by Th2;

          hence (F . n) is non empty;

        end;

      end;

    end

    definition

      let S be non empty 1-sorted;

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

    end

    theorem :: SCMRING1:4

    ((( SCM-VAL G) * SCM-OK ) . d1) = the carrier of G by Th2;

    theorem :: SCMRING1:5

    

     Th4: ( pi (( product (( SCM-VAL G) * SCM-OK )), NAT )) = NAT

    proof

       NAT in ( dom (( SCM-VAL G) * SCM-OK )) by Lm1, AMI_2: 22;

      

      hence ( pi (( product (( SCM-VAL G) * SCM-OK )), NAT )) = ((( SCM-VAL G) * SCM-OK ) . NAT ) by CARD_3: 12

      .= NAT by Th1;

    end;

    theorem :: SCMRING1:6

    

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

    proof

      let a be Element of SCM-Data-Loc ;

      a in SCM-Memory ;

      then a in ( dom (( SCM-VAL G) * SCM-OK )) by Lm1;

      

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

      .= the carrier of G by Th2;

    end;

    definition

      let G;

      let s be SCM-State of G;

      :: SCMRING1:def4

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

      coherence

      proof

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

        hence thesis by Th4;

      end;

    end

    definition

      let R be non empty 1-sorted, s be SCM-State of R, u be natural Number;

      :: SCMRING1:def5

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

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom (( SCM-VAL R) * 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;

            then ((s +* ( NAT .--> u)) . NAT ) in NAT by ORDINAL1:def 12;

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

          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 R) * SCM-OK ) . x) by A2, CARD_3: 9;

          end;

        end;

        

         A5: ( dom (( SCM-VAL R) * SCM-OK )) = SCM-Memory by Lm1;

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

        

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

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

        .= ( dom (( SCM-VAL R) * SCM-OK )) by A5, AMI_2: 22, ZFMISC_1: 40;

        hence thesis by A1, CARD_3: 9;

      end;

    end

    theorem :: SCMRING1:7

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

    proof

      let s be SCM-State of G, 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 :: SCMRING1:8

    for s be SCM-State of G, 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 of G, u be natural Number, mk be Element of SCM-Data-Loc ;

       NAT in SCM-Memory by AMI_2: 22;

      then ( SCM-OK . NAT ) = 0 & ( SCM-OK . mk) = 1 by AMI_2:def 4;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMRING1:9

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

    proof

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

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

      hence thesis by FUNCT_4: 11;

    end;

    definition

      let R be non empty 1-sorted, s be SCM-State of R, t be Element of SCM-Data-Loc , u be Element of R;

      :: SCMRING1:def6

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

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom (( SCM-VAL R) * 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 the carrier of R;

            hence ((s +* (t .--> u)) . x) in ((( SCM-VAL R) * 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 R) * SCM-OK ) . x) by A2, CARD_3: 9;

          end;

        end;

        

         A5: ( dom (( SCM-VAL R) * SCM-OK )) = SCM-Memory by Lm1;

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

        

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

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

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

        hence thesis by A1, CARD_3: 9;

      end;

    end

    theorem :: SCMRING1:10

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

    proof

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

       NAT in SCM-Memory by AMI_2: 22;

      then ( SCM-OK . NAT ) = 0 & ( SCM-OK . t) = 1 by AMI_2:def 4;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMRING1:11

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

    proof

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

      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 :: SCMRING1:12

    for s be SCM-State of G, t be Element of SCM-Data-Loc , u be Element of G, 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 of G, t be Element of SCM-Data-Loc , u be Element of G, 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;

    definition

      let R be non empty 1-sorted, s be SCM-State of R, a be Element of SCM-Data-Loc ;

      :: original: .

      redefine

      func s . a -> Element of R ;

      coherence

      proof

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

        hence thesis by Th5;

      end;

    end

    definition

      let S be non empty 1-sorted, d be Element of SCM-Data-Loc , s be Element of S;

      :: original: <*

      redefine

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

      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 x = 2;

          then y = s by A3, FINSEQ_1: 44;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

    end

    definition

      ::$Canceled

      let R be Ring, x be Element of ( SCM-Instr R), s be SCM-State of R;

      :: SCMRING1:def14

      func SCM-Exec-Res (x,s) -> SCM-State of R 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 (s,(x jump_address ))) if ex mk be Element of NAT st x = [6, <*mk*>, {} ],

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

( SCM-Chg (( SCM-Chg (s,(x const_address ),(x const_value ))),(( IC s) + 1))) if ex mk be Element of SCM-Data-Loc , r be Element of R st x = [5, {} , <*mk, r*>]

      otherwise s;

      coherence ;

      consistency by XTUPLE_0: 3;

    end

    definition

      let R be Ring;

      :: SCMRING1:def15

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

      existence

      proof

        deffunc U( Element of ( SCM-Instr R), SCM-State of R) = ( SCM-Exec-Res ($1,$2));

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

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

        take ( curry f);

        let x be Element of ( SCM-Instr R), y be SCM-State of R;

        

        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 R), ( product (( SCM-VAL R) * SCM-OK )) such that

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

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

        now

          let x be Element of ( SCM-Instr R);

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

          now

            let y be SCM-State of R;

            

            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

    ::$Canceled

    theorem :: SCMRING1:19

    for s be SCM-State of S holds ( dom s) = SCM-Memory

    proof

      let s be SCM-State of S;

      ( dom s) = ( dom (( SCM-VAL S) * SCM-OK )) by CARD_3: 9;

      hence thesis by Lm1;

    end;