scmfsa_1.miz



    begin

    reserve x,y,z for set,

k for Nat;

    notation

      synonym SCM+FSA-Data-Loc for SCM-Data-Loc ;

    end

    definition

      ::$Canceled

      :: SCMFSA_1:def2

      func SCM+FSA-Memory -> set equals ( SCM-Memory \/ SCM+FSA-Data*-Loc );

      coherence ;

    end

    registration

      cluster SCM+FSA-Memory -> non empty;

      coherence ;

    end

    theorem :: SCMFSA_1:1

    

     Th1: SCM-Memory c= SCM+FSA-Memory by XBOOLE_1: 7;

    definition

      :: original: SCM+FSA-Data-Loc

      redefine

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

      coherence

      proof

         SCM-Data-Loc c= SCM-Memory ;

        hence thesis by Th1, XBOOLE_1: 1;

      end;

    end

    definition

      :: original: SCM+FSA-Data*-Loc

      redefine

      func SCM+FSA-Data*-Loc -> Subset of SCM+FSA-Memory ;

      coherence by XBOOLE_1: 7;

    end

    registration

      cluster SCM+FSA-Data*-Loc -> non empty;

      coherence ;

    end

    reserve J,J1,K for Element of ( Segm 13),

a for Nat,

b,b1,b2,c,c1,c2 for Element of SCM+FSA-Data-Loc ,

f,f1,f2 for Element of SCM+FSA-Data*-Loc ;

    definition

      ::$Canceled

      :: SCMFSA_1:def4

      func SCM+FSA-OK -> Function of SCM+FSA-Memory , ( Segm 3) equals (( SCM+FSA-Memory --> 2) +* SCM-OK );

      coherence

      proof

        

         A1: ( rng (( SCM+FSA-Memory --> 2) +* SCM-OK )) c= 3

        proof

          ( rng ( SCM+FSA-Memory --> 2)) = {2} by FUNCOP_1: 8;

          then

           A2: ( rng (( SCM+FSA-Memory --> 2) +* SCM-OK )) c= ( {2} \/ ( rng SCM-OK )) by FUNCT_4: 17;

          ( rng SCM-OK ) c= ( Segm 2) by RELAT_1:def 19;

          then ( {2} \/ ( rng SCM-OK )) c= (2 \/ {2}) by XBOOLE_1: 9;

          then ( rng (( SCM+FSA-Memory --> 2) +* SCM-OK )) c= (2 \/ {2}) by A2;

          then ( rng (( SCM+FSA-Memory --> 2) +* SCM-OK )) c= ( succ 2);

          hence thesis;

        end;

        ( dom (( SCM+FSA-Memory --> 2) +* SCM-OK )) = (( dom ( SCM+FSA-Memory --> 2)) \/ ( dom SCM-OK )) by FUNCT_4:def 1

        .= ( SCM+FSA-Memory \/ ( dom SCM-OK ))

        .= ( SCM+FSA-Memory \/ SCM-Memory ) by FUNCT_2:def 1

        .= SCM+FSA-Memory by XBOOLE_1: 7, XBOOLE_1: 12;

        

        then ( dom (( SCM+FSA-Memory --> 2) +* SCM-OK )) = SCM+FSA-Memory

        .= SCM+FSA-Memory ;

        hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    ::$Canceled

    theorem :: SCMFSA_1:5

    

     Th2: NAT in SCM+FSA-Memory

    proof

       NAT in { NAT } by TARSKI:def 1;

      then NAT in ( { NAT } \/ SCM-Data-Loc ) by XBOOLE_0:def 3;

      then NAT in SCM-Memory ;

      hence thesis by XBOOLE_0:def 3;

    end;

    ::$Canceled

    theorem :: SCMFSA_1:8

     SCM+FSA-Memory = (( { NAT } \/ SCM+FSA-Data-Loc ) \/ SCM+FSA-Data*-Loc );

    definition

      :: SCMFSA_1:def5

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

      coherence ;

    end

    

     Lm1: SCM+FSA-Data*-Loc misses SCM-Memory

    proof

      assume SCM+FSA-Data*-Loc meets SCM-Memory ;

      then

      consider x be object such that

       A1: x in SCM+FSA-Data*-Loc and

       A2: x in SCM-Memory by XBOOLE_0: 3;

      

       A3: x in ( { NAT } \/ SCM-Data-Loc ) or x in NAT by A2;

      x in (( NAT \/ [: { 0 }, NAT :]) \ { [ 0 , 0 ]}) by A1, NUMBERS:def 4;

      then

       A4: x in NAT or x in [: { 0 }, NAT :] by XBOOLE_0:def 3;

      per cases by A3, XBOOLE_0:def 3;

        suppose

         A5: x in { NAT };

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

        hence contradiction by A5, TARSKI:def 1;

      end;

        suppose x in SCM-Data-Loc ;

        then

         A6: ex k st x = [1, k] by AMI_2: 23;

        then

        consider y,z be object such that

         A7: y in { 0 } and z in NAT and

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

        y = 0 by A7, TARSKI:def 1;

        hence contradiction by A6, A8, XTUPLE_0: 1;

      end;

        suppose x in NAT ;

        hence contradiction by A1, XBOOLE_0:def 5;

      end;

    end;

    

     Lm2: ( dom SCM-OK ) c= ( dom SCM+FSA-OK )

    proof

      ( dom SCM+FSA-OK ) = (( dom ( SCM+FSA-Memory --> 2)) \/ ( dom SCM-OK )) by FUNCT_4:def 1;

      hence ( dom SCM-OK ) c= ( dom SCM+FSA-OK ) by XBOOLE_1: 7;

    end;

    

     Lm3: NAT in ( dom SCM+FSA-OK )

    proof

      

       A1: NAT in ( dom SCM-OK ) by AMI_2: 22, FUNCT_2:def 1;

      ( dom SCM-OK ) c= ( dom SCM+FSA-OK ) by Lm2;

      hence thesis by A1;

    end;

    

     Lm4: ( SCM+FSA-OK . NAT ) = 0

    proof

      

       A1: NAT in ( dom SCM-OK ) by AMI_2: 22, FUNCT_2:def 1;

      

      thus ( SCM+FSA-OK . NAT ) = ((( SCM+FSA-Memory --> 2) +* SCM-OK ) . NAT )

      .= ( SCM-OK . NAT ) by A1, FUNCT_4: 13

      .= 0 by AMI_2: 22, AMI_2:def 4;

    end;

    theorem :: SCMFSA_1:9

    

     Th4: (( SCM*-VAL * SCM+FSA-OK ) . NAT ) = NAT

    proof

      

       A1: ( SCM+FSA-OK . NAT ) = 0 by Lm4;

      

      thus (( SCM*-VAL * SCM+FSA-OK ) . NAT ) = ( SCM*-VAL . ( SCM+FSA-OK . NAT )) by Lm3, FUNCT_1: 13

      .= NAT by A1;

    end;

    

     Lm5: ( SCM+FSA-OK . b) = 1

    proof

      

       A1: b in SCM-Data-Loc ;

      then b in SCM-Memory ;

      then

       A2: b in ( dom SCM-OK ) by FUNCT_2:def 1;

      

      thus ( SCM+FSA-OK . b) = ((( SCM+FSA-Memory --> 2) +* SCM-OK ) . b)

      .= ( SCM-OK . b) by A2, FUNCT_4: 13

      .= 1 by A1, AMI_2:def 4;

    end;

    theorem :: SCMFSA_1:10

    

     Th5: (( SCM*-VAL * SCM+FSA-OK ) . b) = INT

    proof

      b in SCM-Data-Loc ;

      then b in SCM-Memory ;

      then

       A1: b in ( dom SCM-OK ) by FUNCT_2:def 1;

      

       A2: ( SCM+FSA-OK . b) = 1 by Lm5;

      

       A3: b in ( dom SCM+FSA-OK ) by A1, Lm2;

      

      thus (( SCM*-VAL * SCM+FSA-OK ) . b) = ( SCM*-VAL . ( SCM+FSA-OK . b)) by A3, FUNCT_1: 13

      .= ( SCM*-VAL . 1) by A2

      .= INT ;

    end;

    

     Lm6: ( SCM+FSA-OK . f) = 2

    proof

       not f in SCM-Memory by Lm1, XBOOLE_0: 3;

      then

       A1: not f in ( dom SCM-OK ) by FUNCT_2:def 1;

      

      thus ( SCM+FSA-OK . f) = ((( SCM+FSA-Memory --> 2) +* SCM-OK ) . f)

      .= (( SCM+FSA-Memory --> 2) . f) by A1, FUNCT_4: 11

      .= 2;

    end;

    theorem :: SCMFSA_1:11

    

     Th6: (( SCM*-VAL * SCM+FSA-OK ) . f) = ( INT * )

    proof

      

       A1: ( SCM+FSA-OK . f) = 2 by Lm6;

      f in SCM+FSA-Memory ;

      then

       A2: f in ( dom SCM+FSA-OK ) by FUNCT_2:def 1;

      

      thus (( SCM*-VAL * SCM+FSA-OK ) . f) = ( SCM*-VAL . ( SCM+FSA-OK . f)) by A2, FUNCT_1: 13

      .= ( SCM*-VAL . 2) by A1

      .= ( INT * );

    end;

    

     Lm7: ( dom SCM+FSA-OK ) = SCM+FSA-Memory by PARTFUN1:def 2;

    ( len <% NAT , INT , ( INT * )%>) = 3 by AFINSQ_1: 39;

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

    then

     Lm8: ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm7, RELAT_1: 27;

    registration

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

      coherence

      proof

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

        let n be object;

        assume

         A1: n in ( dom F);

        ( dom F) = SCM+FSA-Memory by Lm8;

        then n in SCM-Memory or n in SCM+FSA-Data*-Loc by A1, XBOOLE_0:def 3;

        per cases by AMI_2: 26;

          suppose n = NAT ;

          then (( SCM*-VAL * SCM+FSA-OK ) . n) = NAT by Th4;

          hence (F . n) is non empty;

        end;

          suppose n in SCM-Data-Loc ;

          then (( SCM*-VAL * SCM+FSA-OK ) . n) = INT by Th5;

          hence (F . n) is non empty;

        end;

          suppose n in SCM+FSA-Data*-Loc ;

          then (( SCM*-VAL * SCM+FSA-OK ) . n) = ( INT * ) by Th6;

          hence (F . n) is non empty;

        end;

      end;

    end

    definition

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

    end

    ::$Canceled

    theorem :: SCMFSA_1:17

    

     Th7: for s be SCM+FSA-State, I be Element of SCM-Instr holds (s | SCM-Memory ) is SCM-State

    proof

      let s be SCM+FSA-State, I be Element of SCM-Instr ;

      

       A1: ( dom (s | SCM-Memory )) = (( dom s) /\ SCM-Memory ) by RELAT_1: 61

      .= ( SCM+FSA-Memory /\ SCM-Memory ) by Lm8, CARD_3: 9

      .= SCM-Memory by XBOOLE_1: 21;

       A2:

      now

        let x be object;

        assume x in ( dom ( SCM-VAL * SCM-OK ));

        then

         A3: x in SCM-Memory by AMI_2: 27;

        then

         A4: x in ( { NAT } \/ SCM-Data-Loc );

        per cases by A4, XBOOLE_0:def 3;

          suppose

           A5: x in { NAT };

          

           A6: ((s | SCM-Memory ) . x) = ((s | SCM-Memory ) . x)

          .= (s . x) by A1, A3, FUNCT_1: 47;

          reconsider a = x as Element of SCM+FSA-Memory by A3, Th1;

          

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

          

           A8: x = NAT by A5, TARSKI:def 1;

          ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

          then ( pi (( product ( SCM*-VAL * SCM+FSA-OK )),a)) = NAT by A8, Th4, CARD_3: 12;

          hence ((s | SCM-Memory ) . x) in (( SCM-VAL * SCM-OK ) . x) by A8, A6, A7, AMI_2: 6;

        end;

          suppose

           A9: x in SCM-Data-Loc ;

          

           A10: ((s | SCM-Memory ) . x) = ((s | SCM-Memory ) . x)

          .= (s . x) by A1, A3, FUNCT_1: 47;

          reconsider a = x as Element of SCM+FSA-Memory by A3, Th1;

          ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

          

          then

           A11: ( pi (( product ( SCM*-VAL * SCM+FSA-OK )),a)) = (( SCM*-VAL * SCM+FSA-OK ) . a) by CARD_3: 12

          .= INT by A9, Th5;

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

          hence ((s | SCM-Memory ) . x) in (( SCM-VAL * SCM-OK ) . x) by A9, A10, A11, AMI_2: 8;

        end;

      end;

      ( dom (s | SCM-Memory )) = ( dom (s | SCM-Memory ))

      .= SCM-Memory by A1

      .= ( dom ( SCM-VAL * SCM-OK )) by AMI_2: 27;

      hence thesis by A2, CARD_3: 9;

    end;

    theorem :: SCMFSA_1:18

    

     Th8: for s be SCM+FSA-State, s1 be SCM-State holds (s +* s1) is SCM+FSA-State

    proof

      let s be SCM+FSA-State, s1 be SCM-State;

      

       A1: ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

      then

      reconsider f = ( SCM*-VAL * SCM+FSA-OK ) as non-empty ManySortedSet of SCM+FSA-Memory by PARTFUN1:def 2;

      

       A2: ( dom s1) = ( dom ( SCM-VAL * SCM-OK )) by CARD_3: 9

      .= SCM-Memory by AMI_2: 27;

      now

        let x be set;

        assume

         A3: x in ( dom s1);

        then

         A4: x in ( { NAT } \/ SCM-Data-Loc ) by A2;

        per cases by A4, XBOOLE_0:def 3;

          suppose

           A5: x in { NAT };

          reconsider a = x as Element of SCM-Memory by A2, A3;

          

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

          

           A7: x = NAT by A5, TARSKI:def 1;

          ( dom ( SCM-VAL * SCM-OK )) = SCM-Memory by AMI_2: 27;

          

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

          .= NAT by A7, AMI_2: 6;

          hence (s1 . x) in (f . x) by A5, A6, Th4, TARSKI:def 1;

        end;

          suppose

           A8: x in SCM-Data-Loc ;

          reconsider a = x as Element of SCM-Memory by A2, A3;

          

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

          ( dom ( SCM-VAL * SCM-OK )) = SCM-Memory by AMI_2: 27;

          then

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

          (( SCM*-VAL * SCM+FSA-OK ) . x) = INT by A8, Th5;

          hence (s1 . x) in (f . x) by A8, A10, A9, AMI_2: 8;

        end;

      end;

      then (s +* s1) is SCM+FSA-State by A1, A2, PRE_CIRC: 6, XBOOLE_1: 7;

      hence thesis;

    end;

    definition

      let s be SCM+FSA-State, u be Nat;

      :: SCMFSA_1:def6

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

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom ( SCM*-VAL * SCM+FSA-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+FSA-OK ) . x) by A3, Th4, 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+FSA-OK ) . x) by A2, CARD_3: 9;

          end;

        end;

        

         A5: ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

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

        

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

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

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

        hence thesis by A1, CARD_3: 9;

      end;

    end

    definition

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

      :: SCMFSA_1:def7

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

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom ( SCM*-VAL * SCM+FSA-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+FSA-OK ) . x) by A3, Th5;

          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+FSA-OK ) . x) by A2, CARD_3: 9;

          end;

        end;

        

         A5: ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

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

        

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

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

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

        hence thesis by A1, CARD_3: 9;

      end;

    end

    definition

      let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc , u be FinSequence of INT ;

      :: SCMFSA_1:def8

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

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in ( dom ( SCM*-VAL * SCM+FSA-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 FINSEQ_1:def 11;

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

          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+FSA-OK ) . x) by A2, CARD_3: 9;

          end;

        end;

        

         A5: ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

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

        

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

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

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

        hence thesis by A1, CARD_3: 9;

      end;

    end

    registration

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

      cluster (s . a) -> integer;

      coherence

      proof

        ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

        

        then

         A1: ( pi (( product ( SCM*-VAL * SCM+FSA-OK )),a)) = (( SCM*-VAL * SCM+FSA-OK ) . a) by CARD_3: 12

        .= INT by Th5;

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

        hence thesis by A1;

      end;

    end

    definition

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

      :: original: .

      redefine

      func s . a -> FinSequence of INT ;

      coherence

      proof

        ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

        

        then

         A1: ( pi (( product ( SCM*-VAL * SCM+FSA-OK )),a)) = (( SCM*-VAL * SCM+FSA-OK ) . a) by CARD_3: 12

        .= ( INT * ) by Th6;

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

        hence thesis by A1, FINSEQ_1:def 11;

      end;

    end

    definition

      ::$Canceled

      let s be SCM+FSA-State;

      :: SCMFSA_1:def15

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

      coherence

      proof

        reconsider z = NAT as Element of SCM+FSA-Memory by Th2;

        ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

        

        then ( pi (( product ( SCM*-VAL * SCM+FSA-OK )), NAT )) = (( SCM*-VAL * SCM+FSA-OK ) . z) by CARD_3: 12

        .= NAT by Th4;

        hence thesis by CARD_3:def 6;

      end;

    end

    definition

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

      :: SCMFSA_1:def16

      func SCM+FSA-Exec-Res (x,s) -> SCM+FSA-State means ex x9 be Element of SCM-Instr , s9 be SCM-State st x = x9 & s9 = (s | SCM-Memory ) & it = (s +* ( SCM-Exec-Res (x9,s9))) if (x `1_3 ) <= 8,

ex i be Integer, k st k = |.(s . (x int_addr2 )).| & i = ((s . (x coll_addr1 )) /. k) & it = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr1 ),i)),(( IC s) + 1))) if (x `1_3 ) = 9,

ex f be FinSequence of INT , k st k = |.(s . (x int_addr2 )).| & f = ((s . (x coll_addr1 )) +* (k,(s . (x int_addr1 )))) & it = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr1 ),f)),(( IC s) + 1))) if (x `1_3 ) = 10,

it = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr3 ),( len (s . (x coll_addr2 ))))),(( IC s) + 1))) if (x `1_3 ) = 11,

ex f be FinSequence of INT , k st k = |.(s . (x int_addr3 )).| & f = (k |-> 0 ) & it = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr2 ),f)),(( IC s) + 1))) if (x `1_3 ) = 12,

ex i be Integer st i = 1 & it = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr ),i)),(( IC s) + 1))) if (x `1_3 ) = 13

      otherwise it = s;

      existence

      proof

        hereby

          assume (x `1_3 ) <= 8;

          then

          reconsider x9 = x as Element of SCM-Instr by SCMFSA_I: 2;

          reconsider s9 = (s | SCM-Memory ) as SCM-State by Th7;

          reconsider s1 = (s +* ( SCM-Exec-Res (x9,s9))) as SCM+FSA-State by Th8;

          take s1, x9, s9;

          thus x = x9;

          thus s9 = (s | SCM-Memory );

          thus s1 = (s +* ( SCM-Exec-Res (x9,s9)));

        end;

        hereby

          reconsider k = |.(s . (x int_addr2 )).| as Nat;

          assume (x `1_3 ) = 9;

          reconsider i = ((s . (x coll_addr1 )) /. k) as Integer;

          take s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr1 ),i)),(( IC s) + 1)));

          take i, k;

          thus k = |.(s . (x int_addr2 )).| & i = ((s . (x coll_addr1 )) /. k) & s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr1 ),i)),(( IC s) + 1)));

        end;

        hereby

          reconsider k = |.(s . (x int_addr2 )).| as Nat;

          assume (x `1_3 ) = 10;

          per cases ;

            suppose

             A1: k in ( dom (s . (x coll_addr1 )));

            set f = ((s . (x coll_addr1 )) +* (k .--> (s . (x int_addr1 ))));

            

             A2: {k} c= ( dom (s . (x coll_addr1 ))) by A1, ZFMISC_1: 31;

            ( dom f) = (( dom (s . (x coll_addr1 ))) \/ ( dom (k .--> (s . (x int_addr1 ))))) by FUNCT_4:def 1

            .= (( dom (s . (x coll_addr1 ))) \/ {k})

            .= ( dom (s . (x coll_addr1 ))) by A2, XBOOLE_1: 12

            .= ( Seg ( len (s . (x coll_addr1 )))) by FINSEQ_1:def 3;

            then

            reconsider f as FinSequence by FINSEQ_1:def 2;

            (s . (x int_addr1 )) in INT & ( rng (k .--> (s . (x int_addr1 )))) = {(s . (x int_addr1 ))} by FUNCOP_1: 8, INT_1:def 2;

            then ( rng (s . (x coll_addr1 ))) c= INT & ( rng (k .--> (s . (x int_addr1 )))) c= INT by FINSEQ_1:def 4, ZFMISC_1: 31;

            then ( rng f) c= (( rng (s . (x coll_addr1 ))) \/ ( rng (k .--> (s . (x int_addr1 ))))) & (( rng (s . (x coll_addr1 ))) \/ ( rng (k .--> (s . (x int_addr1 ))))) c= INT by FUNCT_4: 17, XBOOLE_1: 8;

            then ( rng f) c= INT ;

            then

            reconsider f as FinSequence of INT by FINSEQ_1:def 4;

            take s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr1 ),f)),(( IC s) + 1)));

            take f, k;

            thus k = |.(s . (x int_addr2 )).|;

            thus f = ((s . (x coll_addr1 )) +* (k,(s . (x int_addr1 )))) by A1, FUNCT_7:def 3;

            thus s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr1 ),f)),(( IC s) + 1)));

          end;

            suppose

             A3: not k in ( dom (s . (x coll_addr1 )));

            reconsider f = (s . (x coll_addr1 )) as FinSequence of INT ;

            take s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr1 ),f)),(( IC s) + 1)));

            take f, k;

            thus k = |.(s . (x int_addr2 )).|;

            thus f = ((s . (x coll_addr1 )) +* (k,(s . (x int_addr1 )))) by A3, FUNCT_7:def 3;

            thus s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr1 ),f)),(( IC s) + 1)));

          end;

        end;

        thus (x `1_3 ) = 11 implies ex s1 be SCM+FSA-State st s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr3 ),( len (s . (x coll_addr2 ))))),(( IC s) + 1)));

        hereby

          reconsider k = |.(s . (x int_addr3 )).| as Nat;

          assume (x `1_3 ) = 12;

           0 in INT by INT_1:def 2;

          then

           A4: { 0 } c= INT by ZFMISC_1: 31;

          (k |-> 0 ) = (( Seg k) --> 0 ) by FINSEQ_2:def 2;

          then ( rng (k |-> 0 )) c= { 0 } by FUNCOP_1: 13;

          then ( rng (k |-> 0 )) c= INT by A4;

          then

          reconsider f = (k |-> 0 ) as FinSequence of INT by FINSEQ_1:def 4;

          take s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr2 ),f)),(( IC s) + 1)));

          take f, k;

          thus k = |.(s . (x int_addr3 )).| & f = (k |-> 0 ) & s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x coll_addr2 ),f)),(( IC s) + 1)));

        end;

        hereby

          assume (x `1_3 ) = 13;

          reconsider i = 1 as Integer;

          take s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr ),i)),(( IC s) + 1)));

          take i;

          thus i = 1 & s1 = ( SCM+FSA-Chg (( SCM+FSA-Chg (s,(x int_addr ),i)),(( IC s) + 1)));

        end;

        thus thesis;

      end;

      uniqueness ;

      consistency ;

    end

    definition

      :: SCMFSA_1:def17

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

      existence

      proof

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

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

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

        take ( curry f);

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

        

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

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

      end;

      uniqueness

      proof

        let f,g be Function of SCM+FSA-Instr , ( Funcs (( product ( SCM*-VAL * SCM+FSA-OK )),( product ( SCM*-VAL * SCM+FSA-OK )))) such that

         A2: for x be Element of SCM+FSA-Instr , y be SCM+FSA-State holds ((f . x) qua Element of ( Funcs (( product ( SCM*-VAL * SCM+FSA-OK )),( product ( SCM*-VAL * SCM+FSA-OK )))) . y) = ( SCM+FSA-Exec-Res (x,y)) and

         A3: for x be Element of SCM+FSA-Instr , y be SCM+FSA-State holds ((g . x) qua Element of ( Funcs (( product ( SCM*-VAL * SCM+FSA-OK )),( product ( SCM*-VAL * SCM+FSA-OK )))) . y) = ( SCM+FSA-Exec-Res (x,y));

        now

          let x be Element of SCM+FSA-Instr ;

          reconsider gx = (g . x), fx = (f . x) as Function of ( product ( SCM*-VAL * SCM+FSA-OK )), ( product ( SCM*-VAL * SCM+FSA-OK ));

          now

            let y be SCM+FSA-State;

            

            thus (fx . y) = ( SCM+FSA-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

    theorem :: SCMFSA_1:19

    for s be SCM+FSA-State, u be Nat holds (( SCM+FSA-Chg (s,u)) . NAT ) = u

    proof

      let s be SCM+FSA-State, u be Nat;

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

      

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

      .= u by FUNCOP_1: 72;

    end;

    theorem :: SCMFSA_1:20

    for s be SCM+FSA-State, u be Nat, mk be Element of SCM+FSA-Data-Loc holds (( SCM+FSA-Chg (s,u)) . mk) = (s . mk)

    proof

      let s be SCM+FSA-State, u be Nat, mk be Element of SCM+FSA-Data-Loc ;

      (( SCM*-VAL * SCM+FSA-OK ) . mk) = INT & { NAT } = ( dom ( NAT .--> u)) by Th5;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMFSA_1:21

    for s be SCM+FSA-State, u be Nat, p be Element of SCM+FSA-Data*-Loc holds (( SCM+FSA-Chg (s,u)) . p) = (s . p)

    proof

      let s be SCM+FSA-State, u be Nat, mk be Element of SCM+FSA-Data*-Loc ;

      

       A2: ( SCM+FSA-OK . NAT ) = 0 by Lm4;

      ( SCM+FSA-OK . mk) = 2 by Lm6;

      then NAT <> mk by A2;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMFSA_1:22

    for s be SCM+FSA-State, u,v be Nat holds (( SCM+FSA-Chg (s,u)) . v) = (s . v)

    proof

      let s be SCM+FSA-State, u,v be Nat;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMFSA_1:23

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

    proof

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

      (( SCM*-VAL * SCM+FSA-OK ) . t) = INT & {t} = ( dom (t .--> u)) by Th5;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMFSA_1:24

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

    proof

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

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

      

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

      .= u by FUNCOP_1: 72;

    end;

    theorem :: SCMFSA_1:25

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

    proof

      let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc , u be Integer, mk be Element of SCM+FSA-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;

    theorem :: SCMFSA_1:26

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

    proof

      let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc , u be Integer, mk be Element of SCM+FSA-Data*-Loc ;

      (( SCM*-VAL * SCM+FSA-OK ) . t) = INT & (( SCM*-VAL * SCM+FSA-OK ) . mk) = ( INT * ) by Th5, Th6;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMFSA_1:27

    for s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc , u be FinSequence of INT holds (( SCM+FSA-Chg (s,t,u)) . t) = u

    proof

      let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc , u be FinSequence of INT ;

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

      

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

      .= u by FUNCOP_1: 72;

    end;

    theorem :: SCMFSA_1:28

    for s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc , u be FinSequence of INT , mk be Element of SCM+FSA-Data*-Loc st mk <> t holds (( SCM+FSA-Chg (s,t,u)) . mk) = (s . mk)

    proof

      let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc , u be FinSequence of INT , mk be Element of SCM+FSA-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;

    theorem :: SCMFSA_1:29

    for s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc , u be FinSequence of INT , a be Element of SCM+FSA-Data-Loc holds (( SCM+FSA-Chg (s,t,u)) . a) = (s . a)

    proof

      let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc , u be FinSequence of INT , mk be Element of SCM+FSA-Data-Loc ;

      (( SCM*-VAL * SCM+FSA-OK ) . t) = ( INT * ) & (( SCM*-VAL * SCM+FSA-OK ) . mk) = INT by Th5, Th6;

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

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SCMFSA_1:30

     SCM+FSA-Data*-Loc misses SCM-Memory by Lm1;

    ::$Canceled

    theorem :: SCMFSA_1:32

    ( dom ( SCM*-VAL * SCM+FSA-OK )) = SCM+FSA-Memory by Lm8;

    theorem :: SCMFSA_1:33

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