scmfsa_m.miz



    begin

    reserve l,m,n for Nat;

    set SA0 = ( Start-At ( 0 , SCM+FSA ));

    reserve a,b for Int-Location,

f for FinSeq-Location,

s,s1,s2 for State of SCM+FSA ;

    set q = (( intloc 0 ) .--> 1);

    set f = ( the_Values_of SCM+FSA );

    registration

      let n be Nat;

      let i be Integer;

      cluster (( intloc n) .--> i) -> ( the_Values_of SCM+FSA ) -compatible;

      coherence

      proof

        set q = (( intloc n) .--> i);

        i in INT by INT_1:def 2;

        then

         A2: ( rng q) = {i} & {i} c= INT by FUNCOP_1: 8, ZFMISC_1: 31;

        let x be object;

        assume

         A3: x in ( dom q);

        reconsider l = x as Int-Location by A3, TARSKI:def 1;

        

         A4: (f . l) = ( Values l)

        .= INT by SCMFSA_2: 11;

        (q . x) in ( rng q) by A3, FUNCT_1:def 3;

        hence (q . x) in (f . x) by A4, A2;

      end;

    end

    definition

      let I be PartState of SCM+FSA ;

      :: SCMFSA_M:def1

      func Initialized I -> PartState of SCM+FSA equals (I +* ( Initialize (( intloc 0 ) .--> 1)));

      coherence ;

      projectivity ;

    end

    registration

      let I be PartState of SCM+FSA ;

      cluster ( Initialized I) -> 0 -started;

      coherence ;

    end

    registration

      let I be FinPartState of SCM+FSA ;

      cluster ( Initialized I) -> finite;

      coherence ;

    end

    scheme :: SCMFSA_M:sch1

    SCMFSAEx { G( set) -> Integer , H( set) -> FinSequence of INT , I() -> Element of NAT } :

ex S be State of SCM+FSA st ( IC S) = I() & for i be Nat holds (S . ( intloc i)) = G(i) & (S . ( fsloc i)) = H(i);

      defpred P[ object, object] means ex m st $1 = ( IC SCM+FSA ) & $2 = I() or $1 = ( intloc m) & $2 = G(m) or $1 = ( fsloc m) & $2 = H(m);

      

       A1: for e be object st e in the carrier of SCM+FSA holds ex u be object st P[e, u]

      proof

        let e be object;

        assume e in the carrier of SCM+FSA ;

        then e in (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by STRUCT_0: 4;

        then

         A2: e in ( Data-Locations SCM+FSA ) or e in {( IC SCM+FSA )} by XBOOLE_0:def 3;

        now

          per cases by A2, SCMFSA_2: 100, XBOOLE_0:def 3;

            case e in {( IC SCM+FSA )};

            hence e = ( IC SCM+FSA ) by TARSKI:def 1;

          end;

            case e in Int-Locations ;

            then e is Int-Location by AMI_2:def 16;

            hence ex m be Nat st e = ( intloc m) by SCMFSA_2: 8;

          end;

            case e in FinSeq-Locations ;

            then e is FinSeq-Location by SCMFSA_2:def 5;

            hence ex m be Nat st e = ( fsloc m) by SCMFSA_2: 9;

          end;

        end;

        then

        consider m such that

         A3: e = ( IC SCM+FSA ) or e = ( intloc m) or e = ( fsloc m);

        per cases by A3;

          suppose

           A4: e = ( IC SCM+FSA );

          take u = I();

          thus thesis by A4;

        end;

          suppose

           A5: e = ( intloc m);

          take u = G(m);

          thus thesis by A5;

        end;

          suppose

           A6: e = ( fsloc m);

          take u = H(m);

          thus thesis by A6;

        end;

      end;

      consider f be Function such that

       A7: ( dom f) = the carrier of SCM+FSA and

       A8: for e be object st e in the carrier of SCM+FSA holds P[e, (f . e)] from CLASSES1:sch 1( A1);

      

       A9: ( dom the Object-Kind of SCM+FSA ) = the carrier of SCM+FSA by FUNCT_2:def 1;

      now

        let x be object;

        assume

         A10: x in ( dom the Object-Kind of SCM+FSA );

        then

        consider m such that

         A11: x = ( IC SCM+FSA ) & (f . x) = I() or x = ( intloc m) & (f . x) = G(m) or x = ( fsloc m) & (f . x) = H(m) by A8, A9;

        x in (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by A10, A9, STRUCT_0: 4;

        then

         A12: x in ( Data-Locations SCM+FSA ) or x in {( IC SCM+FSA )} by XBOOLE_0:def 3;

        per cases by A12, SCMFSA_2: 100, XBOOLE_0:def 3;

          suppose x in Int-Locations ;

          then

           A13: x is Int-Location by AMI_2:def 16;

          

          then (( the_Values_of SCM+FSA ) . x) = ( Values ( intloc m)) by A11, SCMFSA_2: 56, SCMFSA_2: 58

          .= INT by SCMFSA_2: 11;

          hence (f . x) in (( the_Values_of SCM+FSA ) . x) by A11, A13, INT_1:def 2, SCMFSA_2: 58;

        end;

          suppose x in FinSeq-Locations ;

          then

           A14: x is FinSeq-Location by SCMFSA_2:def 5;

          

          then (( the_Values_of SCM+FSA ) . x) = ( Values ( fsloc m)) by A11, SCMFSA_2: 57, SCMFSA_2: 58

          .= ( INT * ) by SCMFSA_2: 12;

          hence (f . x) in (( the_Values_of SCM+FSA ) . x) by A11, A14, FINSEQ_1:def 11, SCMFSA_2: 57, SCMFSA_2: 58;

        end;

          suppose

           A15: x in {( IC SCM+FSA )};

          

          then

           A16: (( the_Values_of SCM+FSA ) . x) = ( Values ( IC SCM+FSA )) by TARSKI:def 1

          .= NAT by MEMSTR_0:def 6;

          x = ( IC SCM+FSA ) by A15, TARSKI:def 1;

          hence (f . x) in (( the_Values_of SCM+FSA ) . x) by A11, A16, SCMFSA_2: 56, SCMFSA_2: 57;

        end;

      end;

      then

      reconsider f as State of SCM+FSA by A7, A9, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

      take f;

      ex m st (( IC SCM+FSA ) = ( IC SCM+FSA ) & (f . ( IC SCM+FSA )) = I() or ( IC SCM+FSA ) = ( intloc m) & (f . ( IC SCM+FSA )) = G(m) or ( IC SCM+FSA ) = ( fsloc m) & (f . ( IC SCM+FSA )) = H(m)) by A8;

      hence ( IC f) = I() by SCMFSA_2: 56, SCMFSA_2: 57;

      let i be Nat;

      ex m st (( intloc i) = ( IC SCM+FSA ) & (f . ( intloc i)) = I() or ( intloc i) = ( intloc m) & (f . ( intloc i)) = G(m) or ( intloc i) = ( fsloc m) & (f . ( intloc i)) = H(m)) by A8;

      hence (f . ( intloc i)) = G(i) by AMI_3: 10, SCMFSA_2: 56, SCMFSA_2: 58;

      ex m st (( fsloc i) = ( IC SCM+FSA ) & (f . ( fsloc i)) = I() or ( fsloc i) = ( intloc m) & (f . ( fsloc i)) = G(m) or ( fsloc i) = ( fsloc m) & (f . ( fsloc i)) = H(m)) by A8;

      hence thesis by SCMFSA_2: 57, SCMFSA_2: 58;

    end;

    theorem :: SCMFSA_M:1

    

     Th1: for s be State of SCM+FSA , x be set st x in ( dom s) holds x is Int-Location or x is FinSeq-Location or x = ( IC SCM+FSA )

    proof

      let s be State of SCM+FSA ;

      let x be set;

      assume

       A1: x in ( dom s);

      x in (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by A1, MEMSTR_0: 13;

      then x in ( Data-Locations SCM+FSA ) or x in {( IC SCM+FSA )} by XBOOLE_0:def 3;

      then x in Int-Locations or x in FinSeq-Locations or x = ( IC SCM+FSA ) by SCMFSA_2: 100, TARSKI:def 1, XBOOLE_0:def 3;

      hence thesis by AMI_2:def 16, SCMFSA_2:def 5;

    end;

    theorem :: SCMFSA_M:2

    for s1,s2 be State of SCM+FSA holds ((for a be Int-Location holds (s1 . a) = (s2 . a)) & for f be FinSeq-Location holds (s1 . f) = (s2 . f)) iff ( DataPart s1) = ( DataPart s2)

    proof

      let s1,s2 be State of SCM+FSA ;

       A1:

      now

        assume that

         A2: for a be Int-Location holds (s1 . a) = (s2 . a) and

         A3: for f be FinSeq-Location holds (s1 . f) = (s2 . f);

        hereby

          let x be set;

          assume

           A4: x in ( Data-Locations SCM+FSA );

          per cases ;

            suppose x in Int-Locations ;

            then x is Int-Location by AMI_2:def 16;

            hence (s1 . x) = (s2 . x) by A2;

          end;

            suppose not x in Int-Locations ;

            then x in FinSeq-Locations by A4, SCMFSA_2: 100, XBOOLE_0:def 3;

            then x is FinSeq-Location by SCMFSA_2:def 5;

            hence (s1 . x) = (s2 . x) by A3;

          end;

        end;

      end;

       A5:

      now

        assume

         A6: for x be set st x in ( Data-Locations SCM+FSA ) holds (s1 . x) = (s2 . x);

        hereby

          let a be Int-Location;

          a in Int-Locations by AMI_2:def 16;

          then a in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

          hence (s1 . a) = (s2 . a) by A6;

        end;

        hereby

          let f be FinSeq-Location;

          f in FinSeq-Locations by SCMFSA_2:def 5;

          then f in ( Data-Locations SCM+FSA ) by SCMFSA_2: 100, XBOOLE_0:def 3;

          hence (s1 . f) = (s2 . f) by A6;

        end;

      end;

      ( dom s2) = (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by MEMSTR_0: 13;

      then

       A7: ( Data-Locations SCM+FSA ) c= ( dom s2) by XBOOLE_1: 7;

      ( dom s1) = (( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) by MEMSTR_0: 13;

      then ( Data-Locations SCM+FSA ) c= ( dom s1) by XBOOLE_1: 7;

      hence thesis by A7, A1, A5, FUNCT_1: 95;

    end;

    theorem :: SCMFSA_M:3

    

     Th3: for p be PartState of SCM+FSA holds ( dom ( Initialized p)) = ((( dom p) \/ {( intloc 0 )}) \/ {( IC SCM+FSA )})

    proof

      let p be PartState of SCM+FSA ;

      

       A1: ( dom q) = {( intloc 0 )} & ( dom SA0) = {( IC SCM+FSA )};

      ( Initialized p) = ( Initialize (p +* q)) by FUNCT_4: 14;

      

      hence ( dom ( Initialized p)) = (( dom (p +* q)) \/ ( dom SA0)) by FUNCT_4:def 1

      .= ((( dom p) \/ {( intloc 0 )}) \/ {( IC SCM+FSA )}) by A1, FUNCT_4:def 1;

    end;

    registration

      let s be State of SCM+FSA ;

      cluster ( Initialized s) -> total;

      coherence ;

    end

    theorem :: SCMFSA_M:4

    

     Th4: for p be PartState of SCM+FSA holds ( intloc 0 ) in ( dom ( Initialized p))

    proof

      let p be PartState of SCM+FSA ;

      

       A1: ( dom q) = {( intloc 0 )} & ( dom SA0) = {( IC SCM+FSA )};

      ( intloc 0 ) in {( intloc 0 )} by TARSKI:def 1;

      then

       A2: ( intloc 0 ) in (( dom p) \/ {( intloc 0 )}) by XBOOLE_0:def 3;

      ( Initialized p) = ( Initialize (p +* q)) by FUNCT_4: 14;

      

      then ( dom ( Initialized p)) = (( dom (p +* q)) \/ ( dom SA0)) by FUNCT_4:def 1

      .= ((( dom p) \/ {( intloc 0 )}) \/ {( IC SCM+FSA )}) by A1, FUNCT_4:def 1;

      hence thesis by A2, XBOOLE_0:def 3;

    end;

    theorem :: SCMFSA_M:5

    for p be PartState of SCM+FSA holds (( Initialized p) . ( intloc 0 )) = 1 & (( Initialized p) . ( IC SCM+FSA )) = 0

    proof

      let p be PartState of SCM+FSA ;

      ( intloc 0 ) in {( intloc 0 )} by TARSKI:def 1;

      then

       A1: ( intloc 0 ) in ( dom q);

      

       A2: ( Initialized p) = ( Initialize (p +* q)) by FUNCT_4: 14;

      ( intloc 0 ) <> ( IC SCM+FSA ) by SCMFSA_2: 56;

      then not ( intloc 0 ) in {( IC SCM+FSA )} by TARSKI:def 1;

      then not ( intloc 0 ) in ( dom SA0);

      

      hence (( Initialized p) . ( intloc 0 )) = ((p +* q) . ( intloc 0 )) by A2, FUNCT_4: 11

      .= (q . ( intloc 0 )) by A1, FUNCT_4: 13

      .= 1 by FUNCOP_1: 72;

      ( IC SCM+FSA ) in {( IC SCM+FSA )} by TARSKI:def 1;

      then ( IC SCM+FSA ) in ( dom SA0);

      

      hence (( Initialized p) . ( IC SCM+FSA )) = (SA0 . ( IC SCM+FSA )) by A2, FUNCT_4: 13

      .= 0 by FUNCOP_1: 72;

    end;

    theorem :: SCMFSA_M:6

    for p be PartState of SCM+FSA , a be Int-Location st a <> ( intloc 0 ) & not a in ( dom p) holds not a in ( dom ( Initialized p))

    proof

      let p be PartState of SCM+FSA ;

      let a be Int-Location;

      assume that

       A1: a <> ( intloc 0 ) and

       A2: not a in ( dom p);

      assume a in ( dom ( Initialized p));

      then a in ((( dom p) \/ {( intloc 0 )}) \/ {( IC SCM+FSA )}) by Th3;

      then

       A3: a in (( dom p) \/ {( intloc 0 )}) or a in {( IC SCM+FSA )} by XBOOLE_0:def 3;

      per cases by A3, A2, XBOOLE_0:def 3;

        suppose a in {( intloc 0 )};

        hence contradiction by A1, TARSKI:def 1;

      end;

        suppose a in {( IC SCM+FSA )};

        then a = ( IC SCM+FSA ) by TARSKI:def 1;

        hence contradiction by SCMFSA_2: 56;

      end;

    end;

    theorem :: SCMFSA_M:7

    for p be PartState of SCM+FSA , f be FinSeq-Location st not f in ( dom p) holds not f in ( dom ( Initialized p))

    proof

      let p be PartState of SCM+FSA ;

      let f be FinSeq-Location;

      assume

       A1: not f in ( dom p);

      assume f in ( dom ( Initialized p));

      then f in ((( dom p) \/ {( intloc 0 )}) \/ {( IC SCM+FSA )}) by Th3;

      then

       A2: f in (( dom p) \/ {( intloc 0 )}) or f in {( IC SCM+FSA )} by XBOOLE_0:def 3;

      per cases by A2, A1, XBOOLE_0:def 3;

        suppose f in {( intloc 0 )};

        then f = ( intloc 0 ) by TARSKI:def 1;

        hence contradiction by SCMFSA_2: 58;

      end;

        suppose f in {( IC SCM+FSA )};

        then f = ( IC SCM+FSA ) by TARSKI:def 1;

        hence contradiction by SCMFSA_2: 57;

      end;

    end;

    theorem :: SCMFSA_M:8

    for s be State of SCM+FSA st (s . ( intloc 0 )) = 1 & ( IC s) = 0 holds ( Initialized s) = s

    proof

      let s be State of SCM+FSA ;

      assume

       A1: (s . ( intloc 0 )) = 1;

      assume

       A2: ( IC s) = 0 ;

      

       A3: ( IC SCM+FSA ) in ( dom s) by MEMSTR_0: 2;

      

       A4: ( intloc 0 ) in ( dom s) by SCMFSA_2: 42;

      

      thus ( Initialized s) = ( Initialize (s +* (( intloc 0 ) .--> 1))) by FUNCT_4: 14

      .= (s +* (( IC SCM+FSA ) .--> 0 )) by A1, A4, FUNCT_7: 96

      .= s by A2, A3, FUNCT_7: 96;

    end;

    theorem :: SCMFSA_M:9

    for p be PartState of SCM+FSA holds (( Initialized p) . ( intloc 0 )) = 1

    proof

      let p be PartState of SCM+FSA ;

      

       A1: ((( intloc 0 ) .--> 1) . ( intloc 0 )) = 1 by FUNCOP_1: 72;

      

       A2: ( Initialized p) = ( Initialize (p +* (( intloc 0 ) .--> 1))) by FUNCT_4: 14;

      

       A3: ( intloc 0 ) in ( dom (( intloc 0 ) .--> 1)) by TARSKI:def 1;

       not ( intloc 0 ) in ( dom SA0) by SCMFSA_2: 102;

      

      hence (( Initialized p) . ( intloc 0 )) = ((p +* (( intloc 0 ) .--> 1)) . ( intloc 0 )) by A2, FUNCT_4: 11

      .= 1 by A3, A1, FUNCT_4: 13;

    end;

    theorem :: SCMFSA_M:10

    

     Th10: ( intloc 0 ) in ( dom ( Initialize (( intloc 0 ) .--> 1)))

    proof

      

       A1: ( dom ( Initialize (( intloc 0 ) .--> 1))) = (( dom ( Start-At ( 0 , SCM+FSA ))) \/ ( dom (( intloc 0 ) .--> 1))) by FUNCT_4:def 1;

      ( intloc 0 ) in ( dom (( intloc 0 ) .--> 1)) by TARSKI:def 1;

      hence ( intloc 0 ) in ( dom ( Initialize (( intloc 0 ) .--> 1))) by A1, XBOOLE_0:def 3;

    end;

    theorem :: SCMFSA_M:11

    

     Th11: ( dom ( Initialize (( intloc 0 ) .--> 1))) = {( intloc 0 ), ( IC SCM+FSA )}

    proof

      

      thus ( dom ( Initialize (( intloc 0 ) .--> 1))) = (( dom (( intloc 0 ) .--> 1)) \/ ( dom SA0)) by FUNCT_4:def 1

      .= (( dom (( intloc 0 ) .--> 1)) \/ {( IC SCM+FSA )})

      .= ( {( intloc 0 )} \/ {( IC SCM+FSA )})

      .= {( intloc 0 ), ( IC SCM+FSA )} by ENUMSET1: 1;

    end;

    theorem :: SCMFSA_M:12

    

     Th12: (( Initialize (( intloc 0 ) .--> 1)) . ( intloc 0 )) = 1

    proof

       not ( intloc 0 ) in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 102;

      

      hence (( Initialize (( intloc 0 ) .--> 1)) . ( intloc 0 )) = ((( intloc 0 ) .--> 1) . ( intloc 0 )) by FUNCT_4: 11

      .= 1 by FUNCOP_1: 72;

    end;

    theorem :: SCMFSA_M:13

    for p be PartState of SCM+FSA holds ( Initialize (( intloc 0 ) .--> 1)) c= ( Initialized p) by FUNCT_4: 25;

    begin

    registration

      cluster Int-Locations -> non empty;

      coherence ;

    end

    definition

      let IT be Int-Location;

      :: SCMFSA_M:def2

      attr IT is read-only means

      : Def2: IT = ( intloc 0 );

    end

    notation

      let IT be Int-Location;

      antonym IT is read-write for IT is read-only;

    end

    registration

      cluster ( intloc 0 ) -> read-only;

      coherence ;

    end

    registration

      cluster read-write for Int-Location;

      existence

      proof

        take ( intloc 1);

        ( intloc 1) <> ( intloc 0 ) by AMI_3: 10;

        hence thesis;

      end;

    end

    reserve L for finite Subset of Int-Locations ;

    definition

      let L be finite Subset of Int-Locations ;

      :: SCMFSA_M:def3

      func FirstNotIn L -> Int-Location means

      : Def3: ex sn be non empty Subset of NAT st it = ( intloc ( min sn)) & sn = { k where k be Element of NAT : not ( intloc k) in L };

      existence

      proof

        defpred X[ Nat] means not ( intloc $1) in L;

        set sn = { k where k be Element of NAT : X[k] };

        

         A1: sn is Subset of NAT from DOMAIN_1:sch 7;

         Int-Locations = [: {1}, NAT :] by SCM_INST:def 1;

        then not Int-Locations c= L;

        then

        consider x be object such that

         A2: x in Int-Locations and

         A3: not x in L;

        reconsider x as Int-Location by A2, AMI_2:def 16;

        consider k be Nat such that

         A4: x = ( intloc k) by SCMFSA_2: 8;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        k in sn by A3, A4;

        then

        reconsider sn as non empty Subset of NAT by A1;

        take ( intloc ( min sn)), sn;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: SCMFSA_M:14

     not ( FirstNotIn L) in L

    proof

      set FNI = ( FirstNotIn L);

      consider sn be non empty Subset of NAT such that

       A1: FNI = ( intloc ( min sn)) and

       A2: sn = { k where k be Element of NAT : not ( intloc k) in L } by Def3;

      ( min sn) in sn by XXREAL_2:def 7;

      then ex k be Element of NAT st k = ( min sn) & not ( intloc k) in L by A2;

      hence thesis by A1;

    end;

    theorem :: SCMFSA_M:15

    ( FirstNotIn L) = ( intloc m) & not ( intloc n) in L implies m <= n

    proof

      consider sn be non empty Subset of NAT such that

       A1: ( FirstNotIn L) = ( intloc ( min sn)) & sn = { k where k be Element of NAT : not ( intloc k) in L } by Def3;

      

       A2: n in NAT by ORDINAL1:def 12;

      assume ( FirstNotIn L) = ( intloc m) & not ( intloc n) in L;

      then m = ( min sn) & n in sn by A1, AMI_3: 10, A2;

      hence thesis by XXREAL_2:def 7;

    end;

    reserve L for finite Subset of FinSeq-Locations ;

    definition

      let L be finite Subset of FinSeq-Locations ;

      :: SCMFSA_M:def4

      func First*NotIn L -> FinSeq-Location means

      : Def4: ex sn be non empty Subset of NAT st it = ( fsloc ( min sn)) & sn = { k where k be Element of NAT : not ( fsloc k) in L };

      existence

      proof

        defpred X[ Nat] means not ( fsloc $1) in L;

        set sn = { k where k be Element of NAT : X[k] };

        

         A1: sn is Subset of NAT from DOMAIN_1:sch 7;

         not FinSeq-Locations c= L;

        then

        consider x be object such that

         A2: x in FinSeq-Locations and

         A3: not x in L;

        reconsider x as FinSeq-Location by A2, SCMFSA_2:def 5;

        consider k be Nat such that

         A4: x = ( fsloc k) by SCMFSA_2: 9;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        k in sn by A3, A4;

        then

        reconsider sn as non empty Subset of NAT by A1;

        take ( fsloc ( min sn)), sn;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: SCMFSA_M:16

     not ( First*NotIn L) in L

    proof

      set FNI = ( First*NotIn L);

      consider sn be non empty Subset of NAT such that

       A1: FNI = ( fsloc ( min sn)) and

       A2: sn = { k where k be Element of NAT : not ( fsloc k) in L } by Def4;

      ( min sn) in sn by XXREAL_2:def 7;

      then ex k be Element of NAT st k = ( min sn) & not ( fsloc k) in L by A2;

      hence thesis by A1;

    end;

    theorem :: SCMFSA_M:17

    ( First*NotIn L) = ( fsloc m) & not ( fsloc n) in L implies m <= n

    proof

      assume that

       A1: ( First*NotIn L) = ( fsloc m) and

       A2: not ( fsloc n) in L;

      consider sn be non empty Subset of NAT such that

       A3: ( First*NotIn L) = ( fsloc ( min sn)) and

       A4: sn = { k where k be Element of NAT : not ( fsloc k) in L } by Def4;

      n in NAT by ORDINAL1:def 12;

      then n in sn by A2, A4;

      hence thesis by A1, A3, XXREAL_2:def 7;

    end;

    registration

      let s be State of SCM+FSA , li be Int-Location, k be Integer;

      cluster (s +* (li,k)) -> ( the_Values_of SCM+FSA ) -compatible;

      coherence

      proof

        let x be object;

        assume x in ( dom (s +* (li,k)));

        then

         A1: x in ( dom s) by FUNCT_7: 30;

        per cases ;

          suppose

           A2: x = li;

          

          then

           A3: (( the_Values_of SCM+FSA ) . x) = ( Values li)

          .= INT by SCMFSA_2: 11;

          ((s +* (li,k)) . x) = k by A2, A1, FUNCT_7: 31;

          hence ((s +* (li,k)) . x) in (( the_Values_of SCM+FSA ) . x) by A3, INT_1:def 2;

        end;

          suppose x <> li;

          then ((s +* (li,k)) . x) = (s . x) by FUNCT_7: 32;

          hence ((s +* (li,k)) . x) in (( the_Values_of SCM+FSA ) . x) by A1, FUNCT_1:def 14;

        end;

      end;

    end

    begin

    registration

      let a be Int-Location, n be Nat;

      cluster (a .--> n) -> data-only;

      coherence ;

    end

    theorem :: SCMFSA_M:18

    for s be State of SCM+FSA st (s . ( intloc 0 )) = 1 holds ( Initialize s) = ( Initialized s)

    proof

      let s be State of SCM+FSA ;

      

       A1: ( intloc 0 ) in ( dom s) by SCMFSA_2: 42;

      assume (s . ( intloc 0 )) = 1;

      then

       A2: s = (s +* (( intloc 0 ) .--> 1)) by A1, FUNCT_7: 96;

      thus ( Initialized s) = ( Initialize s) by A2, FUNCT_4: 14;

    end;

    theorem :: SCMFSA_M:19

    for s be State of SCM+FSA st (s . ( intloc 0 )) = 1 holds ( DataPart ( Initialized s)) = ( DataPart s)

    proof

      let s be State of SCM+FSA ;

      assume

       A1: (s . ( intloc 0 )) = 1;

      

       A2: ( intloc 0 ) in ( dom s) by SCMFSA_2: 42;

      ( Initialized s) = ( Initialize (s +* (( intloc 0 ) .--> 1))) by FUNCT_4: 14;

      then ( Initialized s) = ( Initialize s) by A1, A2, FUNCT_7: 96;

      hence thesis by MEMSTR_0: 79;

    end;

    theorem :: SCMFSA_M:20

    for s1,s2 be State of SCM+FSA st (s1 . ( intloc 0 )) = (s2 . ( intloc 0 )) & ((for a be read-write Int-Location holds (s1 . a) = (s2 . a)) & for f be FinSeq-Location holds (s1 . f) = (s2 . f)) holds ( DataPart s1) = ( DataPart s2)

    proof

      let s1,s2 be State of SCM+FSA ;

      set D = ( Data-Locations SCM+FSA );

      assume

       A1: (s1 . ( intloc 0 )) = (s2 . ( intloc 0 ));

      assume

       A2: for a be read-write Int-Location holds (s1 . a) = (s2 . a);

      

       A3: ( dom ( DataPart s1)) = (( dom s1) /\ D) by RELAT_1: 61

      .= ((( Data-Locations SCM+FSA ) \/ {( IC SCM+FSA )}) /\ D) by MEMSTR_0: 13

      .= (( dom s2) /\ D) by MEMSTR_0: 13

      .= ( dom ( DataPart s2)) by RELAT_1: 61;

      assume

       A4: for f be FinSeq-Location holds (s1 . f) = (s2 . f);

      now

        let x be object;

        assume

         A5: x in ( dom ( DataPart s1));

        then

         A6: x in (( dom s1) /\ D) by RELAT_1: 61;

        then

         A7: x in ( dom s1) by XBOOLE_0:def 4;

        per cases by A7, Th1;

          suppose

           A8: x is Int-Location;

          hereby

            per cases ;

              suppose

               A9: x is read-write Int-Location;

              

              thus (( DataPart s1) . x) = (s1 . x) by A5, FUNCT_1: 47

              .= (s2 . x) by A2, A9

              .= (( DataPart s2) . x) by A3, A5, FUNCT_1: 47;

            end;

              suppose

               A10: not x is read-write Int-Location;

              reconsider a = x as Int-Location by A8;

              a = ( intloc 0 ) by A10, Def2;

              

              hence (( DataPart s1) . x) = (s2 . a) by A1, A5, FUNCT_1: 47

              .= (( DataPart s2) . x) by A3, A5, FUNCT_1: 47;

            end;

          end;

        end;

          suppose

           A11: x is FinSeq-Location;

          

          thus (( DataPart s1) . x) = (s1 . x) by A5, FUNCT_1: 47

          .= (s2 . x) by A4, A11

          .= (( DataPart s2) . x) by A3, A5, FUNCT_1: 47;

        end;

          suppose x = ( IC SCM+FSA );

          then not x in ( Data-Locations SCM+FSA ) by STRUCT_0: 3;

          hence (( DataPart s1) . x) = (( DataPart s2) . x) by A6, XBOOLE_0:def 4;

        end;

      end;

      then ( DataPart s1) c= ( DataPart s2) by A3, GRFUNC_1: 2;

      hence thesis by A3, GRFUNC_1: 3;

    end;

    theorem :: SCMFSA_M:21

    for s be State of SCM+FSA , a be Int-Location, l be Nat holds ((s +* ( Start-At (l, SCM+FSA ))) . a) = (s . a)

    proof

      let s be State of SCM+FSA ;

      let a be Int-Location;

      let l be Nat;

       not a in ( dom ( Start-At (l, SCM+FSA ))) by SCMFSA_2: 102;

      hence thesis by FUNCT_4: 11;

    end;

    begin

    definition

      let d be Int-Location;

      :: original: {

      redefine

      func {d} -> Subset of Int-Locations ;

      coherence

      proof

        d in SCM-Data-Loc by AMI_2:def 16;

        hence thesis by SUBSET_1: 33;

      end;

      let e be Int-Location;

      :: original: {

      redefine

      func {d,e} -> Subset of Int-Locations ;

      coherence

      proof

        

         A1: e in SCM-Data-Loc by AMI_2:def 16;

        d in SCM-Data-Loc by AMI_2:def 16;

        hence thesis by A1, SUBSET_1: 34;

      end;

      let f be Int-Location;

      :: original: {

      redefine

      func {d,e,f} -> Subset of Int-Locations ;

      coherence

      proof

        

         A2: f in SCM-Data-Loc by AMI_2:def 16;

        

         A3: e in SCM-Data-Loc by AMI_2:def 16;

        d in SCM-Data-Loc by AMI_2:def 16;

        hence thesis by A3, A2, SUBSET_1: 35;

      end;

      let g be Int-Location;

      :: original: {

      redefine

      func {d,e,f,g} -> Subset of Int-Locations ;

      coherence

      proof

        

         A4: g in SCM-Data-Loc by AMI_2:def 16;

        

         A5: f in SCM-Data-Loc by AMI_2:def 16;

        

         A6: e in SCM-Data-Loc by AMI_2:def 16;

        d in SCM-Data-Loc by AMI_2:def 16;

        hence thesis by A6, A5, A4, SUBSET_1: 36;

      end;

    end

    definition

      let L be finite Subset of Int-Locations ;

      :: SCMFSA_M:def5

      func RWNotIn-seq L -> sequence of ( bool NAT ) means

      : Def5: (it . 0 ) = { k where k be Element of NAT : not ( intloc k) in L & k <> 0 } & (for i be Nat, sn be non empty Subset of NAT st (it . i) = sn holds (it . (i + 1)) = (sn \ {( min sn)})) & for i be Nat holds (it . i) is infinite;

      existence

      proof

        set M = (L \/ {( intloc 0 )});

        defpred X[ Element of omega ] means not ( intloc $1) in L & $1 <> 0 ;

        set sn = { k where k be Element of NAT : X[k] };

        

         A1: sn is Subset of NAT from DOMAIN_1:sch 7;

         not Int-Locations c= M by AMI_3: 27;

        then

        consider x be object such that

         A2: x in Int-Locations and

         A3: not x in M;

        reconsider x as Int-Location by A2, AMI_2:def 16;

        consider k be Nat such that

         A4: x = ( intloc k) by SCMFSA_2: 8;

        reconsider k as Element of NAT by ORDINAL1:def 12;

         not ( intloc k) in {( intloc 0 )} by A3, A4, XBOOLE_0:def 3;

        then

         A5: k <> 0 by TARSKI:def 1;

         not ( intloc k) in L by A3, A4, XBOOLE_0:def 3;

        then k in sn by A5;

        then

        reconsider sn as non empty Subset of NAT by A1;

        defpred P[ Nat, Subset of NAT , Subset of NAT ] means for N be non empty Subset of NAT st N = $2 holds $3 = ($2 \ {( min N)});

         A6:

        now

          let n be Nat;

          let x be Subset of NAT ;

          per cases ;

            suppose x is empty;

            then P[n, x, ( {} NAT )];

            hence ex y be Subset of NAT st P[n, x, y];

          end;

            suppose x is non empty;

            then

            reconsider x9 = x as non empty Subset of NAT ;

            now

              reconsider mx9 = {( min x9)} as Subset of NAT ;

              reconsider t = (x9 \ mx9) as Subset of NAT ;

              take t;

              let N be non empty Subset of NAT ;

              assume N = x;

              hence t = (x \ {( min N)});

            end;

            hence ex y be Subset of NAT st P[n, x, y];

          end;

        end;

        consider f be sequence of ( bool NAT ) such that

         A7: (f . 0 ) = sn and

         A8: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A6);

        take f;

        thus (f . 0 ) = { v where v be Element of NAT : not ( intloc v) in L & v <> 0 } by A7;

        thus for i be Nat, sn be non empty Subset of NAT st (f . i) = sn holds (f . (i + 1)) = (sn \ {( min sn)}) by A8;

        defpred X[ Nat] means (f . $1) is infinite;

        

         A9: X[ 0 ]

        proof

          deffunc U( Nat) = ( intloc $1);

          set Isn = { U(v) where v be Element of NAT : v in sn };

          assume (f . 0 ) is finite;

          then

           A10: sn is finite by A7;

          Isn is finite from FRAENKEL:sch 21( A10);

          then

          reconsider Isn as finite set;

          now

            let x be object;

            hereby

              assume

               A11: x in (M \/ Isn);

              per cases by A11, XBOOLE_0:def 3;

                suppose x in M;

                hence x in Int-Locations ;

              end;

                suppose x in Isn;

                then ex k be Element of NAT st ( intloc k) = x & k in sn;

                hence x in Int-Locations by AMI_2:def 16;

              end;

            end;

            assume x in Int-Locations ;

            then

            reconsider x9 = x as Int-Location by AMI_2:def 16;

            consider i be Nat such that

             A12: x9 = ( intloc i) by SCMFSA_2: 8;

            now

              assume

               A13: not x in M;

              then not x9 in {( intloc 0 )} by XBOOLE_0:def 3;

              then

               A14: i <> 0 by A12, TARSKI:def 1;

              reconsider i as Element of NAT by ORDINAL1:def 12;

               not ( intloc i) in L by A12, A13, XBOOLE_0:def 3;

              then i in sn by A14;

              hence x in Isn by A12;

            end;

            hence x in (M \/ Isn) by XBOOLE_0:def 3;

          end;

          hence contradiction by AMI_3: 27, TARSKI: 2;

        end;

        

         A15: for n be Nat st X[n] holds X[(n + 1)]

        proof

          let n be Nat;

          assume

           A16: (f . n) is infinite;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          reconsider sn = (f . nn) as non empty Subset of NAT by A16;

          ( min sn) in sn by XXREAL_2:def 7;

          then

           A17: {( min sn)} c= sn by ZFMISC_1: 31;

          assume (f . (n + 1)) is finite;

          then

          reconsider sn1 = (f . (n + 1)) as finite set;

          

           A18: (sn1 \/ {( min sn)}) is finite;

          (f . (n + 1)) = (sn \ {( min sn)}) by A8;

          hence contradiction by A16, A17, A18, XBOOLE_1: 45;

        end;

        thus for n be Nat holds X[n] from NAT_1:sch 2( A9, A15);

      end;

      uniqueness

      proof

        let IT1,IT2 be sequence of ( bool NAT ) such that

         A19: (IT1 . 0 ) = { k where k be Element of NAT : not ( intloc k) in L & k <> 0 } and

         A20: for i be Nat, sn be non empty Subset of NAT st (IT1 . i) = sn holds (IT1 . (i + 1)) = (sn \ {( min sn)}) and for i be Nat holds (IT1 . i) is infinite and

         A21: (IT2 . 0 ) = { k where k be Element of NAT : not ( intloc k) in L & k <> 0 } and

         A22: for i be Nat, sn be non empty Subset of NAT st (IT2 . i) = sn holds (IT2 . (i + 1)) = (sn \ {( min sn)}) and

         A23: for i be Nat holds (IT2 . i) is infinite;

        now

          defpred X[ Nat] means (IT1 . $1) = (IT2 . $1);

          thus NAT = ( dom IT1) by FUNCT_2:def 1;

          thus NAT = ( dom IT2) by FUNCT_2:def 1;

          

           A24: for n be Nat st X[n] holds X[(n + 1)]

          proof

            let n be Nat;

            assume

             A25: (IT1 . n) = (IT2 . n);

            then

            reconsider IT1n = (IT1 . n) as non empty Subset of NAT by A23;

            

            thus (IT1 . (n + 1)) = (IT1n \ {( min IT1n)}) by A20

            .= (IT2 . (n + 1)) by A22, A25;

          end;

          

           A26: X[ 0 ] by A19, A21;

          for n be Nat holds X[n] from NAT_1:sch 2( A26, A24);

          hence for x be object st x in NAT holds (IT1 . x) = (IT2 . x);

        end;

        hence IT1 = IT2;

      end;

    end

    registration

      let L be finite Subset of Int-Locations , n be Nat;

      cluster (( RWNotIn-seq L) . n) -> non empty;

      coherence by Def5;

    end

    reserve L for finite Subset of Int-Locations ;

    theorem :: SCMFSA_M:22

    

     Th22: not 0 in (( RWNotIn-seq L) . n) & for m st m in (( RWNotIn-seq L) . n) holds not ( intloc m) in L

    proof

      set RL = ( RWNotIn-seq L);

      defpred X[ Nat] means not 0 in (RL . $1) & for m st m in (RL . $1) holds not ( intloc m) in L;

      

       A1: X[ 0 ]

      proof

        

         A2: (RL . 0 ) = { k where k be Element of NAT : not ( intloc k) in L & k <> 0 } by Def5;

        hereby

          assume 0 in (RL . 0 );

          then ex k be Element of NAT st k = 0 & ( not ( intloc k) in L) & k <> 0 by A2;

          hence contradiction;

        end;

        let m;

        assume m in (RL . 0 );

        then ex k be Element of NAT st k = m & ( not ( intloc k) in L) & k <> 0 by A2;

        hence thesis;

      end;

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n such that

         A4: not 0 in (RL . n) and

         A5: for m st m in (RL . n) holds not ( intloc m) in L;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        reconsider sn = (RL . nn) as non empty Subset of NAT ;

        

         A6: (RL . (n + 1)) = (sn \ {( min sn)}) by Def5;

        hence not 0 in (RL . (n + 1)) by A4, XBOOLE_0:def 5;

        let m;

        assume m in (RL . (n + 1));

        then m in (RL . n) by A6, XBOOLE_0:def 5;

        hence thesis by A5;

      end;

      for n holds X[n] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    theorem :: SCMFSA_M:23

    

     Th23: for n be Nat holds ( min (( RWNotIn-seq L) . n)) < ( min (( RWNotIn-seq L) . (n + 1)))

    proof

      let n be Nat;

      set RL = ( RWNotIn-seq L);

      set sn = (RL . n);

      set sn1 = (RL . (n + 1));

      assume

       A1: ( min (( RWNotIn-seq L) . n)) >= ( min (( RWNotIn-seq L) . (n + 1)));

      

       A2: sn1 = (sn \ {( min sn)}) by Def5;

      then ( min sn) <= ( min sn1) by XBOOLE_1: 36, XXREAL_2: 60;

      then ( min sn) = ( min sn1) by A1, XXREAL_0: 1;

      then

       A3: ( min sn1) in {( min sn)} by TARSKI:def 1;

      ( min sn1) in sn1 by XXREAL_2:def 7;

      hence contradiction by A2, A3, XBOOLE_0:def 5;

    end;

    theorem :: SCMFSA_M:24

    

     Th24: for n,m be Element of NAT holds n < m implies ( min (( RWNotIn-seq L) . n)) < ( min (( RWNotIn-seq L) . m))

    proof

      let n,m be Element of NAT ;

      set RL = ( RWNotIn-seq L);

      now

        let n be Element of NAT ;

        defpred X[ Nat] means n < $1 implies ( min (RL . n)) < ( min (RL . $1));

        

         A1: for m be Nat st X[m] holds X[(m + 1)]

        proof

          let m be Nat such that

           A2: n < m implies ( min (RL . n)) < ( min (RL . m));

          assume n < (m + 1);

          then

           A3: n <= m by NAT_1: 13;

          per cases by A3, XXREAL_0: 1;

            suppose n = m;

            hence ( min (RL . n)) < ( min (RL . (m + 1))) by Th23;

          end;

            suppose n < m;

            hence ( min (RL . n)) < ( min (RL . (m + 1))) by A2, Th23, XXREAL_0: 2;

          end;

        end;

        

         A4: X[ 0 ];

        thus for n be Nat holds X[n] from NAT_1:sch 2( A4, A1);

      end;

      hence thesis;

    end;

    definition

      let n be Element of NAT , L be finite Subset of Int-Locations ;

      :: SCMFSA_M:def6

      func n -thRWNotIn L -> Int-Location equals ( intloc ( min (( RWNotIn-seq L) . n)));

      correctness ;

    end

    notation

      let n be Element of NAT , L be finite Subset of Int-Locations ;

      synonym n -stRWNotIn L for n -thRWNotIn L;

      synonym n -ndRWNotIn L for n -thRWNotIn L;

      synonym n -rdRWNotIn L for n -thRWNotIn L;

    end

    registration

      let n be Element of NAT , L be finite Subset of Int-Locations ;

      cluster (n -thRWNotIn L) -> read-write;

      coherence

      proof

        set sn = (( RWNotIn-seq L) . n);

        

         A1: ( min sn) in sn by XXREAL_2:def 7;

        assume (n -thRWNotIn L) = ( intloc 0 );

        then ( min (( RWNotIn-seq L) . n)) = 0 by AMI_3: 10;

        hence contradiction by A1, Th22;

      end;

    end

    theorem :: SCMFSA_M:25

    for n be Element of NAT holds not (n -thRWNotIn L) in L

    proof

      let n be Element of NAT ;

      set FNI = (n -thRWNotIn L);

      set sn = (( RWNotIn-seq L) . n);

      ( min sn) in sn by XXREAL_2:def 7;

      hence thesis by Th22;

    end;

    theorem :: SCMFSA_M:26

    for n,m be Element of NAT holds n <> m implies (n -thRWNotIn L) <> (m -thRWNotIn L)

    proof

      let n,m be Element of NAT ;

      assume n <> m;

      then n < m or m < n by XXREAL_0: 1;

      then

       A1: ( min (( RWNotIn-seq L) . n)) <> ( min (( RWNotIn-seq L) . m)) by Th24;

      assume (n -thRWNotIn L) = (m -thRWNotIn L);

      hence contradiction by A1, AMI_3: 10;

    end;

    begin

    theorem :: SCMFSA_M:27

    

     Th27: for Iloc be Subset of Int-Locations , Floc be Subset of FinSeq-Locations holds (s1 | (Iloc \/ Floc)) = (s2 | (Iloc \/ Floc)) iff (for x be Int-Location st x in Iloc holds (s1 . x) = (s2 . x)) & for x be FinSeq-Location st x in Floc holds (s1 . x) = (s2 . x)

    proof

      let Iloc be Subset of Int-Locations , Floc be Subset of FinSeq-Locations ;

       FinSeq-Locations c= ( dom s1) by SCMFSA_2: 46;

      then

       A1: Floc c= ( dom s1);

       FinSeq-Locations c= ( dom s2) by SCMFSA_2: 46;

      then

       A2: Floc c= ( dom s2);

       Int-Locations c= ( dom s2) by SCMFSA_2: 45;

      then

       A3: Iloc c= ( dom s2);

      then

       A4: (Iloc \/ Floc) c= ( dom s2) by A2, XBOOLE_1: 8;

       Int-Locations c= ( dom s1) by SCMFSA_2: 45;

      then

       A5: Iloc c= ( dom s1);

      then

       A6: (Iloc \/ Floc) c= ( dom s1) by A1, XBOOLE_1: 8;

      hereby

        assume

         A7: (s1 | (Iloc \/ Floc)) = (s2 | (Iloc \/ Floc));

        hereby

          let x be Int-Location;

          assume x in Iloc;

          then x in (Iloc \/ Floc) by XBOOLE_0:def 3;

          hence (s1 . x) = (s2 . x) by A6, A4, A7, FUNCT_1: 95;

        end;

        let x be FinSeq-Location;

        assume x in Floc;

        then x in (Iloc \/ Floc) by XBOOLE_0:def 3;

        hence (s1 . x) = (s2 . x) by A6, A4, A7, FUNCT_1: 95;

      end;

      assume that

       A8: for x be Int-Location st x in Iloc holds (s1 . x) = (s2 . x) and

       A9: for x be FinSeq-Location st x in Floc holds (s1 . x) = (s2 . x);

       A10:

      now

        hereby

          let x be set;

          assume

           A11: x in Iloc;

          then x in Int-Locations ;

          then

          reconsider x9 = x as Int-Location by AMI_2:def 16;

          

          thus (s1 . x) = (s2 . x9) by A8, A11

          .= (s2 . x);

        end;

        let x be set;

        assume

         A12: x in Floc;

        then x in FinSeq-Locations ;

        then

        reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;

        

        thus (s1 . x) = (s2 . x9) by A9, A12

        .= (s2 . x);

      end;

      then

       A13: (s1 | Floc) = (s2 | Floc) by A1, A2, FUNCT_1: 95;

      (s1 | Iloc) = (s2 | Iloc) by A5, A3, A10, FUNCT_1: 95;

      hence thesis by A13, RELAT_1: 150;

    end;

    theorem :: SCMFSA_M:28

    for Iloc be Subset of Int-Locations holds (s1 | (Iloc \/ FinSeq-Locations )) = (s2 | (Iloc \/ FinSeq-Locations )) iff (for x be Int-Location st x in Iloc holds (s1 . x) = (s2 . x)) & for x be FinSeq-Location holds (s1 . x) = (s2 . x)

    proof

      set FSL = FinSeq-Locations ;

      let Iloc be Subset of Int-Locations ;

      

       A1: (for x be FinSeq-Location holds (s1 . x) = (s2 . x)) implies for x be FinSeq-Location st x in FSL holds (s1 . x) = (s2 . x);

      

       A2: (for x be FinSeq-Location st x in FSL holds (s1 . x) = (s2 . x)) implies for x be FinSeq-Location holds (s1 . x) = (s2 . x) by SCMFSA_2:def 5;

      ( [#] FSL) = FSL;

      hence thesis by A1, A2, Th27;

    end;

    begin

    theorem :: SCMFSA_M:29

    for x be set, i,m,n be Nat st x in ( dom ((( intloc i) .--> m) +* ( Start-At (n, SCM+FSA )))) holds x = ( intloc i) or x = ( IC SCM+FSA )

    proof

      let x be set, i,m,n be Nat;

      set iS = ((( intloc i) .--> m) +* ( Start-At (n, SCM+FSA )));

      ( dom (( intloc i) .--> m)) = {( intloc i)} & ( dom ( Start-At (n, SCM+FSA ))) = {( IC SCM+FSA )};

      then

       A1: ( dom iS) = ( {( intloc i)} \/ {( IC SCM+FSA )}) by FUNCT_4:def 1;

      assume x in ( dom iS);

      then x in {( intloc i)} or x in {( IC SCM+FSA )} by A1, XBOOLE_0:def 3;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: SCMFSA_M:30

    for s be State of SCM+FSA st ( Initialize (( intloc 0 ) .--> 1)) c= s holds (s . ( intloc 0 )) = 1

    proof

      let s be State of SCM+FSA ;

      set iS = ( Initialize (( intloc 0 ) .--> 1));

      

       A1: ( dom iS) = (( dom (( intloc 0 ) .--> 1)) \/ ( dom SA0)) by FUNCT_4:def 1;

      ( intloc 0 ) in ( dom (( intloc 0 ) .--> 1)) by FUNCOP_1: 74;

      then

       A2: ( intloc 0 ) in ( dom iS) by A1, XBOOLE_0:def 3;

      ( IC SCM+FSA ) <> ( intloc 0 ) by SCMFSA_2: 56;

      then not ( intloc 0 ) in ( dom SA0) by TARSKI:def 1;

      

      then (iS . ( intloc 0 )) = ((( intloc 0 ) .--> 1) . ( intloc 0 )) by FUNCT_4: 11

      .= 1 by FUNCOP_1: 72;

      hence thesis by A2, GRFUNC_1: 2;

    end;

    registration

      let n be Nat;

      cluster ( intloc (n + 1)) -> read-write;

      coherence by AMI_3: 10;

    end

    begin

    registration

      let f be FinSeq-Location, t be FinSequence of INT ;

      cluster (f .--> t) -> ( the_Values_of SCM+FSA ) -compatible;

      coherence

      proof

        

         A1: t is Element of ( INT * ) by FINSEQ_1:def 11;

        ( Values f) = ( INT * ) by SCMFSA_2: 12;

        hence thesis by A1;

      end;

    end

    theorem :: SCMFSA_M:31

    for w be FinSequence of INT , f be FinSeq-Location holds ( dom ( Initialized (f .--> w))) = {( intloc 0 ), ( IC SCM+FSA ), f}

    proof

      let w be FinSequence of INT , f be FinSeq-Location;

      ( dom ( Initialized (f .--> w))) = (( dom ( Initialize (( intloc 0 ) .--> 1))) \/ ( dom (f .--> w))) by FUNCT_4:def 1

      .= ( {( intloc 0 ), ( IC SCM+FSA )} \/ {f}) by Th11;

      hence thesis by ENUMSET1: 3;

    end;

    theorem :: SCMFSA_M:32

    for t be FinSequence of INT , f be FinSeq-Location holds ( dom ( Initialize (( intloc 0 ) .--> 1))) misses ( dom (f .--> t))

    proof

      let t be FinSequence of INT , f be FinSeq-Location;

      set x = (f .--> t);

      set DI = ( dom ( Initialize (( intloc 0 ) .--> 1)));

      assume (DI /\ ( dom x)) <> {} ;

      then

      consider y be object such that

       A2: y in (DI /\ ( dom x)) by XBOOLE_0:def 1;

      

       A3: y in DI by A2, XBOOLE_0:def 4;

      y in ( dom x) by A2, XBOOLE_0:def 4;

      then

       A4: y = f by TARSKI:def 1;

      y = ( intloc 0 ) or y = ( IC SCM+FSA ) by A3, Th11, TARSKI:def 2;

      hence contradiction by A4, SCMFSA_2: 57, SCMFSA_2: 58;

    end;

    theorem :: SCMFSA_M:33

    for w be FinSequence of INT , f be FinSeq-Location, s be State of SCM+FSA st ( Initialized (f .--> w)) c= s holds (s . f) = w & (s . ( intloc 0 )) = 1

    proof

      let w be FinSequence of INT , f be FinSeq-Location, s be State of SCM+FSA ;

      set t = (f .--> w), p = ( Initialized t);

      assume

       A1: p c= s;

      reconsider pt = p as PartState of SCM+FSA ;

      

       A2: f in ( dom t) by TARSKI:def 1;

      

       A3: f in ( dom pt) by A2, FUNCT_4: 12;

      

       A4: ( intloc 0 ) in ( dom pt) by Th4;

      ex i be Nat st f = ( fsloc i) by SCMFSA_2: 9;

      then f <> ( intloc 0 ) by SCMFSA_2: 99;

      then not f in {( intloc 0 )} by TARSKI:def 1;

      then

       A5: not f in ( dom (( intloc 0 ) .--> 1));

      

       A6: ( dom ( Initialize (( intloc 0 ) .--> 1))) = (( dom (( intloc 0 ) .--> 1)) \/ ( dom ( Start-At ( 0 , SCM+FSA )))) by FUNCT_4:def 1;

       not f in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 103;

      then

       A7: not f in ( dom ( Initialize (( intloc 0 ) .--> 1))) by A5, A6, XBOOLE_0:def 3;

      

      thus (s . f) = (pt . f) by A1, A3, GRFUNC_1: 2

      .= (t . f) by A7, FUNCT_4: 11

      .= w by FUNCOP_1: 72;

      

      thus (s . ( intloc 0 )) = (p . ( intloc 0 )) by A1, A4, GRFUNC_1: 2

      .= 1 by Th12, Th10, FUNCT_4: 13;

    end;

    theorem :: SCMFSA_M:34

    for f be FinSeq-Location, a be Int-Location, s be State of SCM+FSA holds {a, ( IC SCM+FSA ), f} c= ( dom s)

    proof

      let f be FinSeq-Location, a be Int-Location, s be State of SCM+FSA ;

      

       A1: a in ( dom s) by SCMFSA_2: 42;

      ( IC SCM+FSA ) in ( dom s) by MEMSTR_0: 2;

      then

       A2: {a, ( IC SCM+FSA )} c= ( dom s) by A1, ZFMISC_1: 32;

      f in ( dom s) by SCMFSA_2: 43;

      then {f} c= ( dom s) by ZFMISC_1: 31;

      then ( {a, ( IC SCM+FSA )} \/ {f}) c= ( dom s) by A2, XBOOLE_1: 8;

      hence thesis by ENUMSET1: 3;

    end;

    definition

      :: SCMFSA_M:def7

      func Sorting-Function -> PartFunc of ( FinPartSt SCM+FSA ), ( FinPartSt SCM+FSA ) means

      : Def7: for p,q be FinPartState of SCM+FSA holds [p, q] in it iff ex t be FinSequence of INT , u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (( fsloc 0 ) .--> t) & q = (( fsloc 0 ) .--> u);

      existence

      proof

        defpred X[ object, object] means ex t be FinSequence of INT , u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & $1 = (( fsloc 0 ) .--> t) & $2 = (( fsloc 0 ) .--> u);

        

         A1: for x,y1,y2 be object st X[x, y1] & X[x, y2] holds y1 = y2

        proof

          let p,q1,q2 be object;

          given t1 be FinSequence of INT , u1 be FinSequence of REAL such that

           A2: (t1,u1) are_fiberwise_equipotent and u1 is FinSequence of INT and

           A3: u1 is non-increasing and

           A4: p = (( fsloc 0 ) .--> t1) and

           A5: q1 = (( fsloc 0 ) .--> u1);

          given t2 be FinSequence of INT , u2 be FinSequence of REAL such that

           A6: (t2,u2) are_fiberwise_equipotent and u2 is FinSequence of INT and

           A7: u2 is non-increasing and

           A8: p = (( fsloc 0 ) .--> t2) and

           A9: q2 = (( fsloc 0 ) .--> u2);

          t1 = ((( fsloc 0 ) .--> t1) . ( fsloc 0 )) by FUNCOP_1: 72

          .= t2 by A4, A8, FUNCOP_1: 72;

          hence thesis by A2, A3, A5, A6, A7, A9, CLASSES1: 76, RFINSEQ: 23;

        end;

        consider f be Function such that

         A10: for p,q be object holds [p, q] in f iff p in ( FinPartSt SCM+FSA ) & X[p, q] from FUNCT_1:sch 1( A1);

        

         A11: ( dom f) c= ( FinPartSt SCM+FSA )

        proof

          let e be object;

          assume e in ( dom f);

          then [e, (f . e)] in f by FUNCT_1: 1;

          hence thesis by A10;

        end;

        ( rng f) c= ( FinPartSt SCM+FSA )

        proof

          let q be object;

          assume q in ( rng f);

          then

          consider p be object such that

           A12: [p, q] in f by XTUPLE_0:def 13;

          consider t be FinSequence of INT , u be FinSequence of REAL such that (t,u) are_fiberwise_equipotent and

           A13: u is FinSequence of INT and u is non-increasing and p = (( fsloc 0 ) .--> t) and

           A14: q = (( fsloc 0 ) .--> u) by A10, A12;

          reconsider u as FinSequence of INT by A13;

          (( fsloc 0 ) .--> u) is FinPartState of SCM+FSA ;

          hence thesis by A14, MEMSTR_0: 75;

        end;

        then

        reconsider f as PartFunc of ( FinPartSt SCM+FSA ), ( FinPartSt SCM+FSA ) by A11, RELSET_1: 4;

        take f;

        let p,q be FinPartState of SCM+FSA ;

        thus [p, q] in f implies ex t be FinSequence of INT , u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (( fsloc 0 ) .--> t) & q = (( fsloc 0 ) .--> u) by A10;

        given t be FinSequence of INT , u be FinSequence of REAL such that

         A15: (t,u) are_fiberwise_equipotent and

         A16: u is FinSequence of INT and

         A17: u is non-increasing and

         A18: p = (( fsloc 0 ) .--> t) and

         A19: q = (( fsloc 0 ) .--> u);

        p in ( FinPartSt SCM+FSA ) by MEMSTR_0: 75;

        hence thesis by A10, A15, A16, A17, A18, A19;

      end;

      uniqueness

      proof

        let IT1,IT2 be PartFunc of ( FinPartSt SCM+FSA ), ( FinPartSt SCM+FSA ) such that

         A20: for p,q be FinPartState of SCM+FSA holds [p, q] in IT1 iff ex t be FinSequence of INT , u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (( fsloc 0 ) .--> t) & q = (( fsloc 0 ) .--> u) and

         A21: for p,q be FinPartState of SCM+FSA holds [p, q] in IT2 iff ex t be FinSequence of INT , u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (( fsloc 0 ) .--> t) & q = (( fsloc 0 ) .--> u);

        defpred X[ set, set] means ex t be FinSequence of INT , u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & $1 = (( fsloc 0 ) .--> t) & $2 = (( fsloc 0 ) .--> u);

        

         A22: for p,q be Element of ( FinPartSt SCM+FSA ) holds [p, q] in IT1 iff X[p, q]

        proof

          let p,q be Element of ( FinPartSt SCM+FSA );

          reconsider p, q as FinPartState of SCM+FSA by MEMSTR_0: 76;

           [p, q] in IT1 iff X[p, q] by A20;

          hence thesis;

        end;

        

         A23: for p,q be Element of ( FinPartSt SCM+FSA ) holds [p, q] in IT2 iff X[p, q]

        proof

          let p,q be Element of ( FinPartSt SCM+FSA );

          reconsider p, q as FinPartState of SCM+FSA by MEMSTR_0: 76;

           [p, q] in IT2 iff X[p, q] by A21;

          hence thesis;

        end;

        thus IT1 = IT2 from RELSET_1:sch 4( A22, A23);

      end;

    end

    theorem :: SCMFSA_M:35

    for p be set holds p in ( dom Sorting-Function ) iff ex t be FinSequence of INT st p = (( fsloc 0 ) .--> t)

    proof

      set f = Sorting-Function ;

      let p be set;

      hereby

        set q = (f . p);

        assume

         A1: p in ( dom f);

        then

         A2: [p, (f . p)] in f by FUNCT_1: 1;

        ( dom f) c= ( FinPartSt SCM+FSA ) by RELAT_1:def 18;

        then

         A3: p is FinPartState of SCM+FSA by A1, MEMSTR_0: 76;

        q in ( FinPartSt SCM+FSA ) by A1, PARTFUN1: 4;

        then q is FinPartState of SCM+FSA by MEMSTR_0: 76;

        then

        consider t be FinSequence of INT , u be FinSequence of REAL such that (t,u) are_fiberwise_equipotent and u is FinSequence of INT and u is non-increasing and

         A4: p = (( fsloc 0 ) .--> t) and q = (( fsloc 0 ) .--> u) by A2, A3, Def7;

        take t;

        thus p = (( fsloc 0 ) .--> t) by A4;

      end;

      given t be FinSequence of INT such that

       A5: p = (( fsloc 0 ) .--> t);

      consider u be FinSequence of REAL such that

       A6: (t,u) are_fiberwise_equipotent and

       A7: u is FinSequence of INT and

       A8: u is non-increasing by RFINSEQ: 33;

      reconsider u1 = u as FinSequence of INT by A7;

      set q = (( fsloc 0 ) .--> u1);

       [p, q] in f by A5, A6, A8, Def7;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: SCMFSA_M:36

    for t be FinSequence of INT holds ex u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & ( Sorting-Function . (( fsloc 0 ) .--> t)) = (( fsloc 0 ) .--> u)

    proof

      let t be FinSequence of INT ;

      consider u be FinSequence of REAL such that

       A1: (t,u) are_fiberwise_equipotent and

       A2: u is FinSequence of INT and

       A3: u is non-increasing by RFINSEQ: 33;

      reconsider u as FinSequence of INT by A2;

      set p = (( fsloc 0 ) .--> t);

      set q = (( fsloc 0 ) .--> u);

       [p, q] in Sorting-Function by A1, A3, Def7;

      then ( Sorting-Function . p) = q by FUNCT_1: 1;

      hence thesis by A1, A3;

    end;

    theorem :: SCMFSA_M:37

    (for a be read-write Int-Location holds (( Initialized s) . a) = (s . a)) & (for f holds (( Initialized s) . f) = (s . f))

    proof

      

       A1: ( Initialized s) = ( Initialize (s +* (( intloc 0 ) .--> 1))) by FUNCT_4: 14;

      hereby

        let a be read-write Int-Location;

        

         A3: not a in ( dom (( intloc 0 ) .--> 1)) by TARSKI:def 1;

         not a in ( dom SA0) by SCMFSA_2: 102;

        

        hence (( Initialized s) . a) = ((s +* (( intloc 0 ) .--> 1)) . a) by A1, FUNCT_4: 11

        .= (s . a) by A3, FUNCT_4: 11;

      end;

      hereby

        let f be FinSeq-Location;

        ( intloc 0 ) <> f by SCMFSA_2: 58;

        then

         A4: not f in ( dom (( intloc 0 ) .--> 1)) by TARSKI:def 1;

         not f in ( dom SA0) by SCMFSA_2: 103;

        

        hence (( Initialized s) . f) = ((s +* (( intloc 0 ) .--> 1)) . f) by A1, FUNCT_4: 11

        .= (s . f) by A4, FUNCT_4: 11;

      end;

    end;

    theorem :: SCMFSA_M:38

    (( Initialize s) . a) = (s . a)

    proof

       not a in ( dom ( Start-At ( 0 , SCM+FSA ))) by SCMFSA_2: 102;

      hence (( Initialize s) . a) = (s . a) by FUNCT_4: 11;

    end;