memstr_0.miz



    begin

    reserve x,N for set,

k for Nat;

    definition

      let N;

      struct ( ZeroStr) Mem-Struct over N (# the carrier -> set,

the ZeroF -> Element of the carrier,

the Object-Kind -> Function of the carrier, N,

the ValuesF -> ManySortedSet of N #)

       attr strict strict;

    end

    reserve N for with_zero set;

    definition

      let N;

      :: MEMSTR_0:def1

      func Trivial-Mem N -> strict Mem-Struct over N means

      : Def1: the carrier of it = { 0 } & the ZeroF of it = 0 & the Object-Kind of it = ( 0 .--> 0 ) & the ValuesF of it = (N --> NAT );

      existence

      proof

        set f = ( 0 .--> 0 );

        

         A1: ( dom f) = { 0 };

        

         A2: ( rng f) c= { 0 } by FUNCOP_1: 13;

         0 in N by MEASURE6:def 2;

        then { 0 } c= N by ZFMISC_1: 31;

        then ( rng f) c= N by A2, XBOOLE_1: 1;

        then

        reconsider f as Function of { 0 }, N by A1, RELSET_1: 4;

        reconsider y = 0 as Element of { 0 } by TARSKI:def 1;

        take Mem-Struct (# { 0 }, y, f, (N --> NAT ) #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let N;

      cluster ( Trivial-Mem N) -> 1 -element;

      coherence by Def1;

    end

    registration

      let N;

      cluster 1 -element for Mem-Struct over N;

      existence

      proof

        take ( Trivial-Mem N);

        thus thesis;

      end;

    end

    notation

      let N;

      let S be Mem-Struct over N;

      synonym IC S for 0. S;

      synonym Data-Locations S for NonZero S;

    end

    registration

      cluster with_zero -> non empty for set;

      coherence ;

    end

    definition

      let N;

      let S be Mem-Struct over N;

      :: MEMSTR_0:def2

      func the_Values_of S -> ManySortedSet of the carrier of S equals (the ValuesF of S * the Object-Kind of S);

      coherence ;

    end

    definition

      let N;

      let S be Mem-Struct over N;

      mode PartState of S is the carrier of S -defined( the_Values_of S) -compatible Function;

    end

    definition

      let N;

      let S be Mem-Struct over N;

      :: MEMSTR_0:def3

      attr S is with_non-empty_values means

      : Def3: ( the_Values_of S) is non-empty;

    end

    registration

      let N;

      cluster ( Trivial-Mem N) -> with_non-empty_values;

      coherence

      proof

        let n be object;

        set S = ( Trivial-Mem N), F = ( the_Values_of S);

        assume

         A1: n in ( dom F);

        then

         A2: (the Object-Kind of S . n) in ( dom the ValuesF of S) by FUNCT_1: 11;

        

         A3: the ValuesF of S = (N --> NAT ) by Def1;

        then

         A4: (the Object-Kind of S . n) in N by A2;

        (F . n) = (the ValuesF of S . (the Object-Kind of S . n)) by A1, FUNCT_1: 12

        .= NAT by A4, A3, FUNCOP_1: 7;

        hence (F . n) is non empty;

      end;

    end

    registration

      let N;

      cluster with_non-empty_values for Mem-Struct over N;

      existence

      proof

        take ( Trivial-Mem N);

        thus thesis;

      end;

    end

    registration

      let N;

      let S be with_non-empty_values Mem-Struct over N;

      cluster ( the_Values_of S) -> non-empty;

      coherence by Def3;

    end

    definition

      let N;

      let S be with_non-empty_values Mem-Struct over N;

      mode State of S is total PartState of S;

    end

    definition

      let N;

      let S be Mem-Struct over N;

      mode Object of S is Element of S;

    end

    begin

    definition

      let N;

      let S be non empty Mem-Struct over N;

      let o be Object of S;

      :: MEMSTR_0:def4

      func ObjectKind o -> Element of N equals (the Object-Kind of S . o);

      correctness ;

    end

    definition

      let N;

      let S be non empty Mem-Struct over N;

      let o be Object of S;

      :: MEMSTR_0:def5

      func Values o -> set equals (( the_Values_of S) . o);

      correctness ;

    end

    definition

      let N;

      let IT be non empty Mem-Struct over N;

      :: MEMSTR_0:def6

      attr IT is IC-Ins-separated means

      : Def6: ( Values ( IC IT)) = NAT ;

    end

    

     Lm1: ( the_Values_of ( Trivial-Mem N)) = ( 0 .--> NAT )

    proof

      set S = ( Trivial-Mem N);

      set f = ( the_Values_of ( Trivial-Mem N)), g = ( 0 .--> NAT );

      the Object-Kind of S = ( 0 .--> 0 ) by Def1;

      then

       A1: f = ((N --> NAT ) * ( 0 .--> 0 )) by Def1;

      

       A2: ( dom (N --> NAT )) = N;

      

       A3: ( rng ( 0 .--> 0 )) = { 0 } by FUNCOP_1: 88;

      

       A4: 0 in N by MEASURE6:def 2;

      then { 0 } c= N by ZFMISC_1: 31;

      

      then

       A5: ( dom f) = ( dom ( 0 .--> 0 )) by A1, A2, A3, RELAT_1: 27

      .= { 0 };

      hence ( dom f) = ( dom g);

      let x be object;

      assume

       A6: x in ( dom f);

      then

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

      

      thus (f . x) = ((N --> NAT ) . (( 0 .--> 0 ) . x)) by A1, A6, FUNCT_1: 12

      .= ((N --> NAT ) . 0 ) by A7, FUNCOP_1: 72

      .= NAT by A4, FUNCOP_1: 7

      .= (g . x) by A7, FUNCOP_1: 72;

    end;

    registration

      let N;

      cluster ( Trivial-Mem N) -> IC-Ins-separated;

      coherence

      proof

        ( IC ( Trivial-Mem N)) = 0 by Def1;

        

        hence ( Values ( IC ( Trivial-Mem N))) = (( 0 .--> NAT ) . 0 ) by Lm1

        .= NAT by FUNCOP_1: 72;

      end;

    end

    registration

      let N;

      cluster IC-Ins-separated with_non-empty_values strict for 1 -element Mem-Struct over N;

      existence

      proof

        take ( Trivial-Mem N);

        thus thesis;

      end;

    end

    definition

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p be PartState of S;

      :: MEMSTR_0:def7

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

      coherence

      proof

        per cases ;

          suppose

           A1: ( IC S) in ( dom p);

          consider s be State of S such that

           A2: p c= s by PBOOLE: 141;

          reconsider ss = s as Element of ( product ( the_Values_of S)) by CARD_3: 107;

          ( dom ( the_Values_of S)) = the carrier of S by PARTFUN1:def 2;

          

          then ( pi (( product ( the_Values_of S)),( IC S))) = ( Values ( IC S)) by CARD_3: 12

          .= NAT by Def6;

          then (ss . ( IC S)) in NAT by CARD_3:def 6;

          hence thesis by A1, A2, GRFUNC_1: 2;

        end;

          suppose not ( IC S) in ( dom p);

          then (p . ( IC S)) = 0 by FUNCT_1:def 2;

          hence thesis;

        end;

      end;

    end

    theorem :: MEMSTR_0:1

    for S be IC-Ins-separated1 -element with_non-empty_values Mem-Struct over N holds for s1,s2 be State of S st ( IC s1) = ( IC s2) holds s1 = s2

    proof

      let T be IC-Ins-separated1 -element with_non-empty_values Mem-Struct over N;

      let s1,s2 be State of T such that

       A1: ( IC s1) = ( IC s2);

      

       A2: ( dom s1) = the carrier of T by PARTFUN1:def 2;

      then

       A3: ( dom s1) = ( dom s2) by PARTFUN1:def 2;

      now

        let x be object;

        assume

         A4: x in ( dom s1);

        

         A5: x = ( IC T) by A4, A2, STRUCT_0:def 10;

        

        hence (s1 . x) = ( IC s1)

        .= (s2 . x) by A1, A5;

      end;

      hence thesis by A3;

    end;

    registration

      let N;

      let S be non empty with_non-empty_values Mem-Struct over N, o be Object of S;

      cluster ( Values o) -> non empty;

      coherence ;

    end

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let la be Object of S;

      let a be Element of ( Values la);

      cluster (la .--> a) -> ( the_Values_of S) -compatible;

      coherence

      proof

        set p = (la .--> a);

        let x be object;

        assume x in ( dom p);

        then

         A2: x = la by TARSKI:def 1;

        then (p . x) = a by FUNCOP_1: 72;

        hence (p . x) in (( the_Values_of S) . x) by A2;

      end;

      let lb be Object of S;

      let b be Element of ( Values lb);

      cluster ((la,lb) --> (a,b)) -> ( the_Values_of S) -compatible;

      coherence ;

    end

    theorem :: MEMSTR_0:2

    

     Th2: for S be non empty with_non-empty_values Mem-Struct over N holds for s be State of S holds ( IC S) in ( dom s)

    proof

      let S be non empty with_non-empty_values Mem-Struct over N;

      let s be State of S;

      ( dom s) = the carrier of S by PARTFUN1:def 2;

      hence thesis;

    end;

    reserve S for IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

    definition

      let N;

      let S be Mem-Struct over N;

      let p be PartState of S;

      :: MEMSTR_0:def8

      func DataPart p -> PartState of S equals (p | ( Data-Locations S));

      coherence ;

      projectivity ;

    end

    definition

      let N;

      let S be Mem-Struct over N;

      let p be PartState of S;

      :: MEMSTR_0:def9

      attr p is data-only means

      : Def9: ( dom p) misses {( IC S)};

    end

    registration

      let N;

      let S be Mem-Struct over N;

      cluster empty -> data-only for PartState of S;

      coherence by RELAT_1: 38, XBOOLE_1: 65;

    end

    registration

      let N;

      let S be Mem-Struct over N;

      cluster empty for PartState of S;

      existence

      proof

        reconsider a = {} as PartState of S by FUNCT_1: 104, RELAT_1: 171;

        take a;

        thus thesis;

      end;

    end

    theorem :: MEMSTR_0:3

    

     Th3: for N holds for S be Mem-Struct over N holds for p be PartState of S holds not ( IC S) in ( dom ( DataPart p))

    proof

      let N;

      let S be Mem-Struct over N;

      let p be PartState of S;

      assume

       A1: ( IC S) in ( dom ( DataPart p));

      ( dom ( DataPart p)) c= (the carrier of S \ {( IC S)}) by RELAT_1: 58;

      then not ( IC S) in {( IC S)} by A1, XBOOLE_0:def 5;

      hence contradiction by TARSKI:def 1;

    end;

    theorem :: MEMSTR_0:4

    for N holds for S be Mem-Struct over N holds for p be PartState of S holds {( IC S)} misses ( dom ( DataPart p)) by Th3, ZFMISC_1: 50;

    theorem :: MEMSTR_0:5

    for p be data-only PartState of S, q be PartState of S holds p c= q iff p c= ( DataPart q)

    proof

      let p be data-only PartState of S, q be PartState of S;

      set X = (the carrier of S \ {( IC S)});

      

       A1: (q | X) c= q by RELAT_1: 59;

      hereby

        

         A2: (X \/ {( IC S)}) = (the carrier of S \/ {( IC S)}) by XBOOLE_1: 39;

        ( dom p) c= the carrier of S by RELAT_1:def 18;

        then

         A3: ( dom p) c= (X \/ {( IC S)}) by A2, XBOOLE_1: 10;

        assume p c= q;

        then

         A4: (p | X) c= ( DataPart q) by RELAT_1: 76;

        ( dom p) misses {( IC S)} by Def9;

        hence p c= ( DataPart q) by A4, A3, RELAT_1: 68, XBOOLE_1: 73;

      end;

      thus thesis by A1, XBOOLE_1: 1;

    end;

    registration

      let N;

      let S be Mem-Struct over N;

      let p be PartState of S;

      cluster ( DataPart p) -> data-only;

      coherence by Th3, ZFMISC_1: 50;

    end

    theorem :: MEMSTR_0:6

    

     Th6: for S be Mem-Struct over N, p be PartState of S holds p is data-only iff ( dom p) c= ( Data-Locations S) by RELAT_1:def 18, XBOOLE_1: 86, XBOOLE_1: 106;

    theorem :: MEMSTR_0:7

    for S be Mem-Struct over N, p be data-only PartState of S holds ( DataPart p) = p

    proof

      let S be Mem-Struct over N, p be data-only PartState of S;

      ( dom p) c= ( Data-Locations S) by Th6;

      hence thesis by RELAT_1: 68;

    end;

    reserve s for State of S;

    theorem :: MEMSTR_0:8

    

     Th8: ( Data-Locations S) c= ( dom s)

    proof

      ( dom s) = the carrier of S by PARTFUN1:def 2;

      hence thesis;

    end;

    theorem :: MEMSTR_0:9

    

     Th9: ( dom ( DataPart s)) = ( Data-Locations S)

    proof

      ( Data-Locations S) c= ( dom s) by Th8;

      hence thesis by RELAT_1: 62;

    end;

    theorem :: MEMSTR_0:10

    

     Th10: for d be data-only PartState of S holds not ( IC S) in ( dom d)

    proof

      let d be data-only PartState of S;

      ( dom d) c= ( Data-Locations S) by Th6;

      hence thesis by STRUCT_0: 3;

    end;

    theorem :: MEMSTR_0:11

    

     Th11: for p be PartState of S, d be data-only PartState of S holds ( IC (p +* d)) = ( IC p)

    proof

      let p be PartState of S, d be data-only PartState of S;

      

       A1: not ( IC S) in ( dom d) by Th10;

      thus ( IC (p +* d)) = ( IC p) by A1, FUNCT_4: 11;

    end;

    reserve p for PartState of S;

    theorem :: MEMSTR_0:12

    for p be PartState of S holds ( DataPart p) c= p by RELAT_1: 59;

    theorem :: MEMSTR_0:13

    

     Th13: ( dom s) = ( {( IC S)} \/ ( Data-Locations S))

    proof

      ( dom s) = the carrier of S by PARTFUN1:def 2;

      hence thesis by STRUCT_0: 4;

    end;

    theorem :: MEMSTR_0:14

    (( dom p) /\ ( Data-Locations S)) = ( dom ( DataPart p)) by RELAT_1: 61;

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat, s be State of S;

      cluster (s +* (( IC S),l)) -> ( the_Values_of S) -compatible;

      coherence

      proof

        let x be object;

        assume x in ( dom (s +* (( IC S),l)));

        then

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

        per cases ;

          suppose

           A2: x = ( IC S);

          then

           A3: ((s +* (( IC S),l)) . x) = l by A1, FUNCT_7: 31;

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

          ( Values ( IC S)) = NAT by Def6;

          then ((s +* (( IC S),l)) . x) in (( the_Values_of S) . x) by A2, A3;

          hence thesis;

        end;

          suppose x <> ( IC S);

          then ((s +* (( IC S),l)) . x) = (s . x) by FUNCT_7: 32;

          hence ((s +* (( IC S),l)) . x) in (( the_Values_of S) . x) by A1, FUNCT_1:def 14;

        end;

      end;

    end

    begin

    definition

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let l be Nat;

      :: MEMSTR_0:def10

      func Start-At (l,S) -> PartState of S equals (( IC S) .--> l);

      correctness

      proof

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

        ( Values ( IC S)) = NAT by Def6;

        then

        reconsider l as Element of ( Values ( IC S));

        (( IC S) .--> l) is PartState of S;

        hence thesis;

      end;

    end

    definition

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat;

      let p be PartState of S;

      :: MEMSTR_0:def11

      attr p is l -started means

      : Def11: ( IC S) in ( dom p) & ( IC p) = l;

    end

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat;

      cluster ( Start-At (l,S)) -> l -started non empty;

      coherence by TARSKI:def 1, FUNCOP_1: 72;

    end

    theorem :: MEMSTR_0:15

    

     Th15: for l be Nat holds ( IC S) in ( dom ( Start-At (l,S))) by TARSKI:def 1;

    theorem :: MEMSTR_0:16

    

     Th16: for n be Nat holds ( IC (p +* ( Start-At (n,S)))) = n

    proof

      let n be Nat;

      

       A1: ( IC S) in ( dom ( Start-At (n,S))) by Th15;

      (( Start-At (n,S)) . ( IC S)) = n by FUNCOP_1: 72;

      hence thesis by A1, FUNCT_4: 13;

    end;

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat;

      cluster l -started for State of S;

      existence

      proof

        take s = ( the State of S +* ( Start-At (l,S)));

        thus ( IC S) in ( dom s) by Th2;

        thus ( IC s) = l by Th16;

      end;

    end

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat, p be PartState of S, q be l -started PartState of S;

      cluster (p +* q) -> l -started;

      coherence

      proof

        

         A1: ( IC S) in ( dom q) by Def11;

        ( dom q) c= ( dom (p +* q)) by FUNCT_4: 10;

        hence ( IC S) in ( dom (p +* q)) by A1;

        ( IC q) = l by Def11;

        hence ( IC (p +* q)) = l by A1, FUNCT_4: 13;

      end;

    end

    definition

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat;

      let s be State of S;

      :: original: -started

      redefine

      :: MEMSTR_0:def12

      attr s is l -started means ( IC s) = l;

      compatibility by Th2;

    end

    theorem :: MEMSTR_0:17

    for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat, p be l -started PartState of S holds for s be PartState of S st p c= s holds s is l -started

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat, p be l -started PartState of S;

      

       A1: ( IC S) in ( dom p) by Def11;

      

       A2: ( IC p) = l by Def11;

      let s be PartState of S;

      assume

       A3: p c= s;

      then ( dom p) c= ( dom s) by RELAT_1: 11;

      hence ( IC S) in ( dom s) by A1;

      thus ( IC s) = l by A3, A2, A1, GRFUNC_1: 2;

    end;

    theorem :: MEMSTR_0:18

    

     Th18: for s be State of S holds ( Start-At (( IC s),S)) = (s | {( IC S)})

    proof

      let s be State of S;

      

       A1: ( IC S) in ( dom s) by Th2;

      

      thus ( Start-At (( IC s),S)) = { [( IC S), (s . ( IC S))]} by FUNCT_4: 82

      .= (s | {( IC S)}) by A1, GRFUNC_1: 28;

    end;

    theorem :: MEMSTR_0:19

    

     Th19: for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for p be PartState of S st ( IC S) in ( dom p) holds p = (( Start-At (( IC p),S)) +* ( DataPart p))

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p be PartState of S;

      assume ( IC S) in ( dom p);

      then

       A1: {( IC S)} is Subset of ( dom p) by SUBSET_1: 41;

      

       A2: ( {( IC S)} \/ (the carrier of S \ {( IC S)})) = (the carrier of S \/ {( IC S)}) by XBOOLE_1: 39

      .= the carrier of S by XBOOLE_1: 12;

      

       A3: ( dom p) c= the carrier of S by RELAT_1:def 18;

       A4:

      now

        let x be object;

        assume

         A5: x in ( dom p);

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

          suppose

           A6: x in {( IC S)};

          ( IC S) in ( dom ( Start-At (( IC p),S))) by TARSKI:def 1;

          then

           A7: ( IC S) in (( dom ( Start-At (( IC p),S))) \/ ( dom ( DataPart p))) by XBOOLE_0:def 3;

          

           A8: x = ( IC S) by A6, TARSKI:def 1;

           not ( IC S) in ( dom ( DataPart p)) by Th3;

          

          then ((( Start-At (( IC p),S)) +* ( DataPart p)) . x) = (( Start-At (( IC p),S)) . x) by A8, A7, FUNCT_4:def 1

          .= ( IC p) by A8, FUNCOP_1: 72;

          hence (p . x) = ((( Start-At (( IC p),S)) +* ( DataPart p)) . x) by A6, TARSKI:def 1;

        end;

          suppose x in (the carrier of S \ {( IC S)});

          then x in (( dom p) /\ (the carrier of S \ {( IC S)})) by A5, XBOOLE_0:def 4;

          then

           A9: x in ( dom (p | (the carrier of S \ {( IC S)}))) by RELAT_1: 61;

          ((( Start-At (( IC p),S)) +* ( DataPart p)) . x) = (( DataPart p) . x) by A9, FUNCT_4: 13

          .= (p . x) by A9, FUNCT_1: 47;

          hence (p . x) = ((( Start-At (( IC p),S)) +* ( DataPart p)) . x);

        end;

      end;

      

       A10: ( dom p) c= the carrier of S by RELAT_1:def 18;

      ( dom (( Start-At (( IC p),S)) +* ( DataPart p))) = (( dom ( Start-At (( IC p),S))) \/ ( dom ( DataPart p))) by FUNCT_4:def 1

      .= ( {( IC S)} \/ ( dom ( DataPart p)))

      .= ((( dom p) /\ {( IC S)}) \/ ( dom (p | (the carrier of S \ {( IC S)})))) by A1, XBOOLE_1: 28

      .= ((( dom p) /\ {( IC S)}) \/ (( dom p) /\ (the carrier of S \ {( IC S)}))) by RELAT_1: 61

      .= (( dom p) /\ the carrier of S) by A2, XBOOLE_1: 23

      .= ( dom p) by A10, XBOOLE_1: 28;

      hence thesis by A4;

    end;

    theorem :: MEMSTR_0:20

    

     Th20: for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat holds ( DataPart ( Start-At (l,S))) = {}

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat;

      ( Data-Locations S) misses {( IC S)} by XBOOLE_1: 79;

      then ( Data-Locations S) misses ( dom ( Start-At (l,S)));

      hence thesis by RELAT_1: 66;

    end;

    theorem :: MEMSTR_0:21

    for l1,l2,k be Nat holds ( Start-At ((l1 + k),S)) = ( Start-At ((l2 + k),S)) iff ( Start-At (l1,S)) = ( Start-At (l2,S))

    proof

      let l1,l2,k be Nat;

      hereby

        assume ( Start-At ((l1 + k),S)) = ( Start-At ((l2 + k),S));

        then { [( IC S), (l1 + k)]} = (( IC S) .--> (l2 + k)) by FUNCT_4: 82;

        then { [( IC S), (l1 + k)]} = { [( IC S), (l2 + k)]} by FUNCT_4: 82;

        then [( IC S), (l1 + k)] = [( IC S), (l2 + k)] by ZFMISC_1: 3;

        then (l1 + k) = (l2 + k) by XTUPLE_0: 1;

        hence ( Start-At (l1,S)) = ( Start-At (l2,S));

      end;

      assume ( Start-At (l1,S)) = ( Start-At (l2,S));

      then { [( IC S), l1]} = ( Start-At (l2,S)) by FUNCT_4: 82;

      then { [( IC S), l1]} = { [( IC S), l2]} by FUNCT_4: 82;

      then [( IC S), l1] = [( IC S), l2] by ZFMISC_1: 3;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: MEMSTR_0:22

    for l1,l2,k be Nat st ( Start-At (l1,S)) = ( Start-At (l2,S)) holds ( Start-At ((l1 -' k),S)) = ( Start-At ((l2 -' k),S))

    proof

      let l1,l2,k be Nat;

      assume ( Start-At (l1,S)) = ( Start-At (l2,S));

      

      then { [( IC S), l1]} = ( Start-At (l2,S)) by FUNCT_4: 82

      .= { [( IC S), l2]} by FUNCT_4: 82;

      then [( IC S), l1] = [( IC S), l2] by ZFMISC_1: 3;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: MEMSTR_0:23

    

     Th23: for d be data-only PartState of S, k be Nat holds d tolerates ( Start-At (k,S))

    proof

      let d be data-only PartState of S, k be Nat;

      ( dom d) misses ( dom ( Start-At (k,S))) by Th10, ZFMISC_1: 50;

      hence thesis by PARTFUN1: 56;

    end;

    theorem :: MEMSTR_0:24

    

     Th24: for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for p be PartState of S st ( IC S) in ( dom p) holds ( dom p) = ( {( IC S)} \/ ( dom ( DataPart p)))

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p be PartState of S;

      assume ( IC S) in ( dom p);

      then

       A1: p = (( Start-At (( IC p),S)) +* ( DataPart p)) by Th19;

      ( dom p) = (( dom ( Start-At (( IC p),S))) \/ ( dom ( DataPart p))) by A1, FUNCT_4:def 1

      .= ( {( IC S)} \/ ( dom ( DataPart p)));

      hence thesis;

    end;

    theorem :: MEMSTR_0:25

    for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for s be State of S holds ( dom s) = ( {( IC S)} \/ ( dom ( DataPart s))) by Th2, Th24;

    theorem :: MEMSTR_0:26

    

     Th26: for p be PartState of S st ( IC S) in ( dom p) holds p = (( DataPart p) +* ( Start-At (( IC p),S)))

    proof

      let p be PartState of S;

      

       A2: ( dom ( DataPart p)) misses ( dom ( Start-At (( IC p),S))) by Th3, ZFMISC_1: 50;

      

       A3: ( dom ( Start-At (( IC p),S))) misses ( dom ( DataPart p)) by Th3, ZFMISC_1: 50;

      assume ( IC S) in ( dom p);

      then p = (( Start-At (( IC p),S)) +* ( DataPart p)) by Th19;

      then

       A4: p = (( Start-At (( IC p),S)) \/ ( DataPart p)) by A3, FUNCT_4: 31;

      thus thesis by A2, A4, FUNCT_4: 31;

    end;

    theorem :: MEMSTR_0:27

    

     Th27: ( IC S) in ( dom (p +* ( Start-At (k,S))))

    proof

      ( IC S) in ( dom ( Start-At (k,S))) by TARSKI:def 1;

      hence thesis by FUNCT_4: 12;

    end;

    theorem :: MEMSTR_0:28

    (p +* ( Start-At (k,S))) c= s implies ( IC s) = k

    proof

      assume

       A1: (p +* ( Start-At (k,S))) c= s;

      ( IC S) in ( dom (p +* ( Start-At (k,S)))) by Th27;

      

      hence ( IC s) = ( IC (p +* ( Start-At (k,S)))) by A1, GRFUNC_1: 2

      .= k by Th16;

    end;

    theorem :: MEMSTR_0:29

    

     Th29: for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat holds for p be PartState of S holds p is l -started iff ( Start-At (l,S)) c= p

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat;

      let p be PartState of S;

      thus p is l -started implies ( Start-At (l,S)) c= p

      proof

        assume

         A2: p is l -started;

        ( IC S) in ( dom p) by A2;

        then

         A3: ( dom ( Start-At (l,S))) c= ( dom p) by ZFMISC_1: 31;

        for x be object st x in ( dom ( Start-At (l,S))) holds (( Start-At (l,S)) . x) = (p . x)

        proof

          let x be object;

          assume

           A4: x in ( dom ( Start-At (l,S)));

          

          hence (( Start-At (l,S)) . x) = ( IC ( Start-At (l,S))) by TARSKI:def 1

          .= l by FUNCOP_1: 72

          .= ( IC p) by A2

          .= (p . x) by A4, TARSKI:def 1;

        end;

        hence ( Start-At (l,S)) c= p by A3, GRFUNC_1: 2;

      end;

      assume

       A5: ( Start-At (l,S)) c= p;

      then

       A6: ( dom ( Start-At (l,S))) c= ( dom p) by RELAT_1: 11;

      

       A7: ( IC S) in ( dom ( Start-At (l,S))) by TARSKI:def 1;

      hence ( IC S) in ( dom p) by A6;

      

      thus ( IC p) = ( IC ( Start-At (l,S))) by A5, A7, GRFUNC_1: 2

      .= l by FUNCOP_1: 72;

    end;

    registration

      let N, S;

      let k be Nat;

      let p be k -started PartState of S, d be data-only PartState of S;

      cluster (p +* d) -> k -started;

      coherence

      proof

        

         A1: ( IC S) in ( dom p) by Def11;

        ( dom (p +* d)) = (( dom p) \/ ( dom d)) by FUNCT_4:def 1;

        hence ( IC S) in ( dom (p +* d)) by A1, XBOOLE_0:def 3;

         not ( IC S) in ( dom d) by Th10;

        

        hence ( IC (p +* d)) = ( IC p) by FUNCT_4: 11

        .= k by Def11;

      end;

    end

    theorem :: MEMSTR_0:30

    

     Th30: ( Start-At (( IC s),S)) c= s

    proof

      ( Start-At (( IC s),S)) = (s | {( IC S)}) by Th18;

      hence thesis by RELAT_1: 59;

    end;

    theorem :: MEMSTR_0:31

    for s be State of S holds (s +* ( Start-At (( IC s),S))) = s by Th30, FUNCT_4: 98;

    theorem :: MEMSTR_0:32

    ( dom p) c= ( {( IC S)} \/ ( dom ( DataPart p)))

    proof

      set S0 = ( Start-At ( 0 ,S));

      per cases ;

        suppose ( IC S) in ( dom p);

        hence thesis by Th24;

      end;

        suppose

         A1: not ( IC S) in ( dom p);

        

         A3: ( dom (p +* S0)) = ( {( IC S)} \/ ( dom ( DataPart (p +* S0)))) by Th24, Th27

        .= ( {( IC S)} \/ ( dom (( DataPart p) +* ( DataPart S0)))) by FUNCT_4: 71

        .= ( {( IC S)} \/ ( dom (( DataPart p) +* {} ))) by Th20

        .= ( {( IC S)} \/ ( dom ( DataPart p)));

        now

          assume ( dom p) meets ( dom S0);

          then

          consider x be object such that

           A4: x in ( dom p) and

           A5: x in ( dom S0) by XBOOLE_0: 3;

          thus contradiction by A4, A1, A5, TARSKI:def 1;

        end;

        then p c= (p +* S0) by FUNCT_4: 32;

        hence ( dom p) c= ( {( IC S)} \/ ( dom ( DataPart p))) by A3, RELAT_1: 11;

      end;

    end;

    theorem :: MEMSTR_0:33

    

     Th33: for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for s be State of S holds s = (s | (( Data-Locations S) \/ {( IC S)}))

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let s be State of S;

      

      thus s = (s | ( dom s))

      .= (s | ( {( IC S)} \/ ( dom ( DataPart s)))) by Th2, Th24

      .= (s | (( Data-Locations S) \/ {( IC S)})) by Th9;

    end;

    theorem :: MEMSTR_0:34

    for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for s1,s2 be State of S st (s1 | (( Data-Locations S) \/ {( IC S)})) = (s2 | (( Data-Locations S) \/ {( IC S)})) holds s1 = s2

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let s1,s2 be State of S;

      s1 = (s1 | (( Data-Locations S) \/ {( IC S)})) by Th33;

      hence thesis by Th33;

    end;

    theorem :: MEMSTR_0:35

    ( IC S) in ( dom p) implies p = (( Start-At (( IC p),S)) +* ( DataPart p)) by Th19;

    theorem :: MEMSTR_0:36

    

     Th36: for p be PartState of S, k,l be Nat holds ((p +* ( Start-At (k,S))) +* ( Start-At (l,S))) = (p +* ( Start-At (l,S)))

    proof

      let p be PartState of S, k,l be Nat;

      ( dom ( Start-At (k,S))) = {( IC S)}

      .= ( dom ( Start-At (l,S)));

      hence ((p +* ( Start-At (k,S))) +* ( Start-At (l,S))) = (p +* ( Start-At (l,S))) by FUNCT_4: 74;

    end;

    theorem :: MEMSTR_0:37

    for p be PartState of S st ( IC S) in ( dom p) holds (p +* ( Start-At (( IC p),S))) = p by FUNCT_4: 7, FUNCT_4: 98;

    theorem :: MEMSTR_0:38

    (p +* ( Start-At (k,S))) c= s implies ( IC s) = k

    proof

      assume

       A1: (p +* ( Start-At (k,S))) c= s;

      ( IC S) in ( dom (p +* ( Start-At (k,S)))) by Th27;

      

      hence ( IC s) = ( IC (p +* ( Start-At (k,S)))) by A1, GRFUNC_1: 2

      .= k by Th16;

    end;

    theorem :: MEMSTR_0:39

    for p be PartState of S holds ( Start-At ( 0 ,S)) c= p implies ( IC p) = 0

    proof

      let p be PartState of S;

      

       A1: ( IC ( Start-At ( 0 ,S))) = 0 by Def11;

      ( IC S) in ( dom ( Start-At ( 0 ,S))) by Def11;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: MEMSTR_0:40

    for p be PartState of S st ( Start-At (k,S)) c= p holds ( IC p) = k

    proof

      let p be PartState of S;

      assume ( Start-At (k,S)) c= p;

      then p is k -started by Th29;

      hence ( IC p) = k;

    end;

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      cluster non empty for PartState of S;

      existence

      proof

        take ( Start-At ( 0 ,S));

        thus thesis;

      end;

    end

    theorem :: MEMSTR_0:41

    for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for p be non empty PartState of S holds ( dom p) meets ( {( IC S)} \/ ( Data-Locations S))

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p be non empty PartState of S;

      ( dom p) c= the carrier of S by RELAT_1:def 18;

      then ( dom p) meets the carrier of S by XBOOLE_1: 69;

      hence ( dom p) meets ( {( IC S)} \/ ( Data-Locations S)) by STRUCT_0: 4;

    end;

    begin

    definition

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p be PartState of S;

      :: MEMSTR_0:def13

      func Initialize p -> PartState of S equals (p +* ( Start-At ( 0 ,S)));

      coherence ;

      projectivity ;

    end

    registration

      let N, S;

      let p be PartState of S;

      cluster ( Initialize p) -> 0 -started;

      coherence ;

    end

    theorem :: MEMSTR_0:42

    

     Th42: for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, p be PartState of S holds ( dom ( Initialize p)) = (( dom p) \/ {( IC S)})

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p be PartState of S;

      

      thus ( dom ( Initialize p)) = (( dom p) \/ ( dom ( Start-At ( 0 ,S)))) by FUNCT_4:def 1

      .= (( dom p) \/ {( IC S)});

    end;

    theorem :: MEMSTR_0:43

    for x be set st x in ( dom ( Initialize p)) holds x in ( dom p) or x = ( IC S)

    proof

      let x be set;

      assume

       A1: x in ( dom ( Initialize p));

      ( dom ( Initialize p)) = (( dom p) \/ {( IC S)}) by Th42;

      then x in ( dom p) or x in {( IC S)} by A1, XBOOLE_0:def 3;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: MEMSTR_0:44

    for p be 0 -started PartState of S holds ( Initialize p) = p

    proof

      let p be 0 -started PartState of S;

      ( IC S) in ( dom p) & ( IC p) = 0 by Def11;

      hence ( Initialize p) = p by FUNCT_4: 85, FUNCT_4: 98;

    end;

    theorem :: MEMSTR_0:45

    

     Th45: for p be PartState of S holds ( DataPart ( Initialize p)) = ( DataPart p)

    proof

      let p be PartState of S;

      

      thus ( DataPart ( Initialize p)) = (( DataPart p) +* ( DataPart ( Start-At ( 0 ,S)))) by FUNCT_4: 71

      .= (( DataPart p) +* {} ) by Th20

      .= ( DataPart p);

    end;

    theorem :: MEMSTR_0:46

    for s be State of S st ( IC s) = 0 holds ( Initialize s) = s

    proof

      let s be State of S;

      ( IC S) in ( dom s) by Th2;

      hence thesis by FUNCT_7: 96;

    end;

    registration

      let N, S;

      let s be State of S;

      cluster ( Initialize s) -> total;

      coherence ;

    end

    theorem :: MEMSTR_0:47

    

     Th47: for p be PartState of S holds ( Initialize p) c= s implies ( IC s) = 0

    proof

      let p be PartState of S;

      

       A1: ( IC ( Initialize p)) = 0 by Def11;

      

       A2: ( IC S) in ( dom ( Initialize p)) by Def11;

      assume ( Initialize p) c= s;

      hence thesis by A1, A2, GRFUNC_1: 2;

    end;

    theorem :: MEMSTR_0:48

    

     Th48: for p be PartState of S holds ( IC S) in ( dom ( Initialize p))

    proof

      let p be PartState of S;

      

       A1: ( dom ( Initialize p)) = (( dom p) \/ {( IC S)}) by Th42;

      ( IC S) in {( IC S)} by TARSKI:def 1;

      hence ( IC S) in ( dom ( Initialize p)) by A1, XBOOLE_0:def 3;

    end;

    theorem :: MEMSTR_0:49

    for p,q be PartState of S holds ( IC S) in ( dom (p +* ( Initialize q)))

    proof

      let p,q be PartState of S;

      

       A1: ( dom (p +* ( Initialize q))) = (( dom p) \/ ( dom ( Initialize q))) by FUNCT_4:def 1;

      ( IC S) in ( dom ( Initialize q)) by Th48;

      hence ( IC S) in ( dom (p +* ( Initialize q))) by A1, XBOOLE_0:def 3;

    end;

    theorem :: MEMSTR_0:50

    for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for p,q be PartState of S holds ( Initialize p) c= q implies ( Start-At ( 0 ,S)) c= q

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p,q be PartState of S;

      ( Start-At ( 0 ,S)) c= ( Initialize p) by FUNCT_4: 25;

      hence thesis by XBOOLE_1: 1;

    end;

    begin

    definition

      let N, S;

      let p be PartState of S, k be Nat;

      :: MEMSTR_0:def14

      func IncIC (p,k) -> PartState of S equals (p +* ( Start-At ((( IC p) + k),S)));

      correctness ;

    end

    theorem :: MEMSTR_0:51

    

     Th51: for p be PartState of S, k be Nat holds ( DataPart ( IncIC (p,k))) = ( DataPart p)

    proof

      let p be PartState of S, k be Nat;

      

      thus ( DataPart ( IncIC (p,k))) = (( DataPart p) +* ( DataPart ( Start-At ((( IC p) + k),S)))) by FUNCT_4: 71

      .= (( DataPart p) +* {} ) by Th20

      .= ( DataPart p);

    end;

    theorem :: MEMSTR_0:52

    

     Th52: for p be PartState of S, k be Nat holds ( IC S) in ( dom ( IncIC (p,k)))

    proof

      let p be PartState of S, k be Nat;

      

       A1: ( dom ( IncIC (p,k))) = (( dom p) \/ ( dom ( Start-At ((( IC p) + k),S)))) by FUNCT_4:def 1;

      ( IC S) in ( dom ( Start-At ((( IC p) + k),S))) by Th15;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    theorem :: MEMSTR_0:53

    

     Th53: for p be PartState of S, k be Nat holds ( IC ( IncIC (p,k))) = (( IC p) + k)

    proof

      let p be PartState of S, k be Nat;

      ( IC S) in ( dom ( Start-At ((( IC p) + k),S))) by TARSKI:def 1;

      

      hence ( IC ( IncIC (p,k))) = (( Start-At ((( IC p) + k),S)) . ( IC S)) by FUNCT_4: 13

      .= (( IC p) + k) by FUNCOP_1: 72;

    end;

    theorem :: MEMSTR_0:54

    for d be data-only PartState of S, k be Nat holds ( IncIC ((p +* d),k)) = (( IncIC (p,k)) +* d)

    proof

      let d be data-only PartState of S, k be Nat;

      

       A1: d tolerates ( Start-At ((( IC p) + k),S)) by Th23;

      

      thus ( IncIC ((p +* d),k)) = ((p +* d) +* ( Start-At ((( IC p) + k),S))) by Th11

      .= (p +* (d +* ( Start-At ((( IC p) + k),S)))) by FUNCT_4: 14

      .= (p +* (( Start-At ((( IC p) + k),S)) +* d)) by A1, FUNCT_4: 34

      .= (( IncIC (p,k)) +* d) by FUNCT_4: 14;

    end;

    theorem :: MEMSTR_0:55

    for p be PartState of S, k be Nat holds ( Start-At ((( IC p) + k),S)) c= ( IncIC (p,k))

    proof

      let p be PartState of S, k be Nat;

      

       A1: ( IC ( IncIC (p,k))) = (( IC p) + k) by Th53;

      

       A2: ( IC S) in ( dom ( IncIC (p,k))) by Th52;

      

       A3: ( Start-At ((( IC p) + k),S)) = { [( IC S), (( IC p) + k)]} & [( IC S), (( IC p) + k)] in ( IncIC (p,k)) by A2, A1, FUNCT_1:def 2, FUNCT_4: 82;

      for x be object st x in ( Start-At ((( IC p) + k),S)) holds x in ( IncIC (p,k)) by A3, TARSKI:def 1;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: MEMSTR_0:56

    for p be PartState of S st ( IC S) in ( dom p) holds ( IncIC (p,k)) = (( DataPart p) +* ( Start-At ((( IC p) + k),S)))

    proof

      let p be PartState of S;

      

       A1: ( dom ( Start-At ((( IC p) + k),S))) = {( IC S)}

      .= ( dom ( Start-At (( IC p),S)));

      assume

       A2: ( IC S) in ( dom p);

      

      thus ( IncIC (p,k)) = ((( DataPart p) +* ( Start-At (( IC p),S))) +* ( Start-At ((( IC p) + k),S))) by A2, Th26

      .= (( DataPart p) +* ( Start-At ((( IC p) + k),S))) by A1, FUNCT_4: 74;

    end;

    registration

      let N, S;

      let s be State of S, k be Nat;

      cluster ( IncIC (s,k)) -> total;

      coherence ;

    end

    theorem :: MEMSTR_0:57

    for p be PartState of S, i,j be Nat holds ( IncIC (( IncIC (p,i)),j)) = ( IncIC (p,(i + j)))

    proof

      let p be PartState of S, i,j be Nat;

      

      thus ( IncIC (( IncIC (p,i)),j)) = ((p +* ( Start-At ((( IC p) + i),S))) +* ( Start-At (((( IC p) + i) + j),S))) by Th53

      .= ( IncIC (p,(i + j))) by FUNCT_4: 114;

    end;

    theorem :: MEMSTR_0:58

    for p be PartState of S, j,k be Nat holds ( IncIC ((p +* ( Start-At (j,S))),k)) = (p +* ( Start-At ((j + k),S)))

    proof

      let p be PartState of S, j,k be Nat;

      

      thus ( IncIC ((p +* ( Start-At (j,S))),k)) = (p +* ( Start-At ((( IC (p +* ( Start-At (j,S)))) + k),S))) by FUNCT_4: 114

      .= (p +* ( Start-At ((j + k),S))) by Th16;

    end;

    theorem :: MEMSTR_0:59

    for k be Nat holds (( IC ( IncIC (s,k))) -' k) = ( IC s)

    proof

      let k be Nat;

      

      thus (( IC ( IncIC (s,k))) -' k) = ((( IC s) + k) -' k) by Th53

      .= ( IC s) by NAT_D: 34;

    end;

    theorem :: MEMSTR_0:60

    for p,q be PartState of S, k be Nat st ( IC S) in ( dom q) holds ( IncIC ((p +* q),k)) = (p +* ( IncIC (q,k)))

    proof

      let p,q be PartState of S, k be Nat;

      assume ( IC S) in ( dom q);

      then ( IC (p +* q)) = ( IC q) by FUNCT_4: 13;

      hence ( IncIC ((p +* q),k)) = (p +* ( IncIC (q,k))) by FUNCT_4: 14;

    end;

    theorem :: MEMSTR_0:61

    for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for k be Nat, p be PartState of S, s1,s2 be State of S st p c= s1 & ( IncIC (p,k)) c= s2 holds p c= (s1 +* ( DataPart s2))

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let k be Nat, p be PartState of S, s1,s2 be State of S such that

       A1: p c= s1 and

       A2: ( IncIC (p,k)) c= s2;

      set s3 = ( DataPart s2);

      reconsider s = (s1 +* ( DataPart s2)) as State of S;

      

       A3: ( dom p) c= the carrier of S by RELAT_1:def 18;

      then

       A4: ( dom p) c= ( {( IC S)} \/ ( Data-Locations S)) by STRUCT_0: 4;

       A5:

      now

        ( Data-Locations S) = (( dom s2) /\ ( Data-Locations S)) by Th8, XBOOLE_1: 28;

        then

         A6: ( dom s3) = ( Data-Locations S) by RELAT_1: 61;

        let x be object such that

         A7: x in ( dom p);

        per cases by A4, A7, XBOOLE_0:def 3;

          suppose

           A8: x in {( IC S)};

          x = ( IC S) by A8, TARSKI:def 1;

          then (s1 . x) = (s . x) by A6, FUNCT_4: 11, STRUCT_0: 3;

          hence (p . x) = (s . x) by A1, A7, GRFUNC_1: 2;

        end;

          suppose

           A9: x in ( Data-Locations S);

          set DPp = ( DataPart p);

          x in (( dom p) /\ ( Data-Locations S)) by A9, A7, XBOOLE_0:def 4;

          then

           A10: x in ( dom DPp) by RELAT_1: 61;

          

           A11: ( DataPart ( IncIC (p,k))) = DPp by Th51;

          DPp c= ( IncIC (p,k)) by A11, RELAT_1: 59;

          then

           A12: DPp c= s2 by A2, XBOOLE_1: 1;

          then ( dom DPp) c= ( dom s2) by GRFUNC_1: 2;

          then x in (( dom s2) /\ ( Data-Locations S)) by A9, A10, XBOOLE_0:def 4;

          then

           A13: x in ( dom s3) by RELAT_1: 61;

          DPp c= p by RELAT_1: 59;

          then

           A14: (DPp . x) = (p . x) by A10, GRFUNC_1: 2;

          

           A15: (s2 . x) = (s3 . x) by A9, FUNCT_1: 49;

          (DPp . x) = (s2 . x) by A10, A12, GRFUNC_1: 2;

          hence (p . x) = (s . x) by A14, A15, A13, FUNCT_4: 13;

        end;

      end;

      ( dom p) c= ( dom s) by A3, PARTFUN1:def 2;

      hence thesis by A5, GRFUNC_1: 2;

    end;

    theorem :: MEMSTR_0:62

    for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for p be PartState of S, k be Nat holds ( DataPart p) c= ( IncIC (p,k))

    proof

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let p be PartState of S, k be Nat;

      ( DataPart ( IncIC (p,k))) = ( DataPart p) by Th51;

      hence ( DataPart p) c= ( IncIC (p,k)) by RELAT_1: 59;

    end;

    definition

      let N, S;

      let p be PartState of S, k be Nat;

      :: MEMSTR_0:def15

      func DecIC (p,k) -> PartState of S equals (p +* ( Start-At ((( IC p) -' k),S)));

      correctness ;

    end

    theorem :: MEMSTR_0:63

    for p be PartState of S, k be Nat holds ( DataPart ( DecIC (p,k))) = ( DataPart p)

    proof

      let p be PartState of S, k be Nat;

      

      thus ( DataPart ( DecIC (p,k))) = (( DataPart p) +* ( DataPart ( Start-At ((( IC p) -' k),S)))) by FUNCT_4: 71

      .= (( DataPart p) +* {} ) by Th20

      .= ( DataPart p);

    end;

    theorem :: MEMSTR_0:64

    

     Th64: for k be Nat holds ( IC S) in ( dom ( DecIC (p,k)))

    proof

      let k be Nat;

      

       A1: ( dom ( DecIC (p,k))) = (( dom p) \/ ( dom ( Start-At ((( IC p) -' k),S)))) by FUNCT_4:def 1;

      ( IC S) in ( dom ( Start-At ((( IC p) -' k),S))) by Th15;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    theorem :: MEMSTR_0:65

    

     Th65: for p be PartState of S, k be Nat holds ( IC ( DecIC (p,k))) = (( IC p) -' k)

    proof

      let p be PartState of S, k be Nat;

      ( IC S) in ( dom ( Start-At ((( IC p) -' k),S))) by TARSKI:def 1;

      

      hence ( IC ( DecIC (p,k))) = (( Start-At ((( IC p) -' k),S)) . ( IC S)) by FUNCT_4: 13

      .= (( IC p) -' k) by FUNCOP_1: 72;

    end;

    theorem :: MEMSTR_0:66

    for p be PartState of S, d be data-only PartState of S, k be Nat holds ( DecIC ((p +* d),k)) = (( DecIC (p,k)) +* d)

    proof

      let p be PartState of S;

      let d be data-only PartState of S, k be Nat;

      

       A1: d tolerates ( Start-At ((( IC p) -' k),S)) by Th23;

      

      thus ( DecIC ((p +* d),k)) = ((p +* d) +* ( Start-At ((( IC p) -' k),S))) by Th11

      .= (p +* (d +* ( Start-At ((( IC p) -' k),S)))) by FUNCT_4: 14

      .= (p +* (( Start-At ((( IC p) -' k),S)) +* d)) by A1, FUNCT_4: 34

      .= (( DecIC (p,k)) +* d) by FUNCT_4: 14;

    end;

    theorem :: MEMSTR_0:67

    for p be PartState of S, k be Nat holds ( Start-At ((( IC p) -' k),S)) c= ( DecIC (p,k))

    proof

      let p be PartState of S, k be Nat;

      

       A1: ( IC ( DecIC (p,k))) = (( IC p) -' k) by Th65;

      

       A2: ( IC S) in ( dom ( DecIC (p,k))) by Th64;

      

       A3: ( Start-At ((( IC p) -' k),S)) = { [( IC S), (( IC p) -' k)]} & [( IC S), (( IC p) -' k)] in ( DecIC (p,k)) by A2, A1, FUNCT_1:def 2, FUNCT_4: 82;

      for x be object st x in ( Start-At ((( IC p) -' k),S)) holds x in ( DecIC (p,k)) by A3, TARSKI:def 1;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: MEMSTR_0:68

    for p be PartState of S, k be Nat st ( IC S) in ( dom p) holds ( DecIC (p,k)) = (( DataPart p) +* ( Start-At ((( IC p) -' k),S)))

    proof

      let p be PartState of S, k be Nat;

      

       A1: ( dom ( Start-At ((( IC p) -' k),S))) = {( IC S)}

      .= ( dom ( Start-At (( IC p),S)));

      assume

       A2: ( IC S) in ( dom p);

      

      thus ( DecIC (p,k)) = ((( DataPart p) +* ( Start-At (( IC p),S))) +* ( Start-At ((( IC p) -' k),S))) by A2, Th26

      .= (( DataPart p) +* ( Start-At ((( IC p) -' k),S))) by A1, FUNCT_4: 74;

    end;

    registration

      let N, S;

      let s be State of S, k be Nat;

      cluster ( DecIC (s,k)) -> total;

      coherence ;

    end

    theorem :: MEMSTR_0:69

    for p be PartState of S, i,j be Nat holds ( DecIC (( DecIC (p,i)),j)) = ( DecIC (p,(i + j)))

    proof

      let p be PartState of S, i,j be Nat;

      

      thus ( DecIC (( DecIC (p,i)),j)) = ((p +* ( Start-At ((( IC p) -' i),S))) +* ( Start-At (((( IC p) -' i) -' j),S))) by Th65

      .= ((p +* ( Start-At ((( IC p) -' i),S))) +* ( Start-At ((( IC p) -' (i + j)),S))) by NAT_2: 30

      .= ( DecIC (p,(i + j))) by FUNCT_4: 114;

    end;

    theorem :: MEMSTR_0:70

    for p be PartState of S, j,k be Nat holds ( DecIC ((p +* ( Start-At (j,S))),k)) = (p +* ( Start-At ((j -' k),S)))

    proof

      let p be PartState of S, j,k be Nat;

      

      thus ( DecIC ((p +* ( Start-At (j,S))),k)) = (p +* ( Start-At ((( IC (p +* ( Start-At (j,S)))) -' k),S))) by FUNCT_4: 114

      .= (p +* ( Start-At ((j -' k),S))) by Th16;

    end;

    theorem :: MEMSTR_0:71

    for s be State of S, k be Nat st k <= ( IC s) holds (( IC ( DecIC (s,k))) + k) = ( IC s)

    proof

      let s be State of S, k be Nat such that

       A1: k <= ( IC s);

      

      thus (( IC ( DecIC (s,k))) + k) = ((( IC s) -' k) + k) by Th65

      .= ( IC s) by A1, XREAL_1: 235;

    end;

    theorem :: MEMSTR_0:72

    

     Th72: for p,q be PartState of S, k be Nat st ( IC S) in ( dom q) holds ( DecIC ((p +* q),k)) = (p +* ( DecIC (q,k)))

    proof

      let p,q be PartState of S, k be Nat;

      assume ( IC S) in ( dom q);

      then ( IC (p +* q)) = ( IC q) by FUNCT_4: 13;

      hence ( DecIC ((p +* q),k)) = (p +* ( DecIC (q,k))) by FUNCT_4: 14;

    end;

    theorem :: MEMSTR_0:73

    

     Th73: for p be PartState of S, k be Nat st ( IC S) in ( dom p) holds ( DecIC (( IncIC (p,k)),k)) = p

    proof

      let p be PartState of S, k be Nat such that

       A1: ( IC S) in ( dom p);

      

      thus ( DecIC (( IncIC (p,k)),k)) = (( IncIC (p,k)) +* ( Start-At (((( IC p) + k) -' k),S))) by Th53

      .= (( IncIC (p,k)) +* ( Start-At (( IC p),S))) by NAT_D: 34

      .= (p +* ( Start-At (( IC p),S))) by Th36

      .= p by A1, FUNCT_4: 7, FUNCT_4: 98;

    end;

    theorem :: MEMSTR_0:74

    for p,q be PartState of S, k be Nat st ( IC S) in ( dom q) holds ( DecIC ((p +* ( IncIC (q,k))),k)) = (p +* q)

    proof

      let p,q be PartState of S, k be Nat such that

       A1: ( IC S) in ( dom q);

      ( IC S) in ( dom ( IncIC (q,k))) by Th52;

      

      hence ( DecIC ((p +* ( IncIC (q,k))),k)) = (p +* ( DecIC (( IncIC (q,k)),k))) by Th72

      .= (p +* q) by A1, Th73;

    end;

    registration

      let N, S;

      let k be Nat;

      let p be k -started PartState of S;

      cluster ( DecIC (p,k)) -> 0 -started;

      coherence

      proof

        thus ( IC S) in ( dom ( DecIC (p,k))) by Th64;

        

        thus ( IC ( DecIC (p,k))) = (( IC p) -' k) by Th65

        .= (k -' k) by Def11

        .= 0 by XREAL_1: 232;

      end;

    end

    begin

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      let l be Nat;

      cluster ( Start-At (l,S)) -> finite;

      correctness ;

    end

    definition

      let N;

      let S be Mem-Struct over N;

      mode FinPartState of S is finite PartState of S;

    end

    registration

      let N;

      let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N, l be Nat;

      cluster l -started for FinPartState of S;

      existence

      proof

        take ( Start-At (l,S));

        thus thesis;

      end;

    end

    registration

      let N;

      let S be Mem-Struct over N;

      let p be FinPartState of S;

      cluster ( DataPart p) -> finite;

      coherence ;

    end

    registration

      let N, S;

      let p be FinPartState of S;

      cluster ( Initialize p) -> finite;

      coherence ;

    end

    registration

      let N, S;

      let p be FinPartState of S, k be Nat;

      cluster ( IncIC (p,k)) -> finite;

      coherence ;

    end

    registration

      let N, S;

      let p be FinPartState of S, k be Nat;

      cluster ( DecIC (p,k)) -> finite;

      coherence ;

    end

    definition

      let N;

      let S be with_non-empty_values Mem-Struct over N;

      :: MEMSTR_0:def16

      func FinPartSt S -> Subset of ( sproduct ( the_Values_of S)) equals { p where p be Element of ( sproduct ( the_Values_of S)) : p is finite };

      coherence

      proof

        defpred P[ set] means $1 is finite;

        { p where p be Element of ( sproduct ( the_Values_of S)) : P[p] } c= ( sproduct ( the_Values_of S)) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: MEMSTR_0:75

    

     Th75: for S be with_non-empty_values Mem-Struct over N holds for p be FinPartState of S holds p in ( FinPartSt S)

    proof

      let S be with_non-empty_values Mem-Struct over N;

      let p be FinPartState of S;

      p in ( sproduct ( the_Values_of S)) by CARD_3: 103;

      hence thesis;

    end;

    registration

      let N;

      let S be with_non-empty_values Mem-Struct over N;

      cluster ( FinPartSt S) -> non empty;

      coherence by Th75;

    end

    theorem :: MEMSTR_0:76

    for S be with_non-empty_values Mem-Struct over N, p be Element of ( FinPartSt S) holds p is FinPartState of S

    proof

      let S be with_non-empty_values Mem-Struct over N;

      let p be Element of ( FinPartSt S);

      p in ( FinPartSt S);

      then ex q be Element of ( sproduct ( the_Values_of S)) st q = p & q is finite;

      hence thesis;

    end;

    definition

      let N, S;

      let IT be PartFunc of ( FinPartSt S), ( FinPartSt S);

      :: MEMSTR_0:def17

      attr IT is data-only means for p be PartState of S st p in ( dom IT) holds p is data-only & for q be PartState of S st q = (IT . p) holds q is data-only;

    end

    registration

      let N, S;

      cluster data-only for PartFunc of ( FinPartSt S), ( FinPartSt S);

      existence

      proof

        reconsider f = {} as PartFunc of ( FinPartSt S), ( FinPartSt S) by RELSET_1: 12;

        take f;

        let p be PartState of S;

        thus thesis;

      end;

    end

    begin

    theorem :: MEMSTR_0:77

    for A be non empty with_non-empty_values Mem-Struct over N, s be State of A, o be Object of A holds (s . o) in ( Values o)

    proof

      let A be non empty with_non-empty_values Mem-Struct over N, s be State of A, o be Object of A;

      ( dom s) = the carrier of A by PARTFUN1:def 2;

      hence thesis by FUNCT_1:def 14;

    end;

    theorem :: MEMSTR_0:78

    

     Th78: for A be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N holds for s1,s2 be State of A st ( IC s1) = ( IC s2) & ( DataPart s1) = ( DataPart s2) holds s1 = s2

    proof

      let A be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;

      set D = ( Data-Locations A);

      let s1,s2 be State of A;

      assume that

       A1: ( IC s1) = ( IC s2) and

       A2: ( DataPart s1) = ( DataPart s2);

      

       A3: ( dom s2) = ( {( IC A)} \/ D) by Th13;

      

       A4: ( dom s1) = ( {( IC A)} \/ D) by Th13;

      then (s1 | {( IC A)}) = (s2 | {( IC A)}) by A1, A3, GRFUNC_1: 29;

      then (s1 | ( {( IC A)} \/ D)) = (s2 | ( {( IC A)} \/ D)) by A2, RELAT_1: 150;

      then (s1 | ( {( IC A)} \/ D)) = (s2 | ( {( IC A)} \/ D));

      

      hence s1 = (s2 | ( dom s2)) by A4, A3

      .= s2;

    end;

    theorem :: MEMSTR_0:79

    for s be State of S, l be Nat holds ( DataPart s) = ( DataPart (s +* ( Start-At (l,S))))

    proof

      let s be State of S;

      let l be Nat;

      

      thus ( DataPart s) = (( DataPart s) +* {} )

      .= (( DataPart s) +* ( DataPart ( Start-At (l,S)))) by Th20

      .= ( DataPart (s +* ( Start-At (l,S)))) by FUNCT_4: 71;

    end;

    theorem :: MEMSTR_0:80

    for s1,s2 be State of S holds ( DataPart s1) = ( DataPart s2) implies ( Initialize s1) = ( Initialize s2)

    proof

      let s1,s2 be State of S;

      assume

       A1: ( DataPart s1) = ( DataPart s2);

      set S1 = ( Initialize s1), S2 = ( Initialize s2);

      

       A2: ( IC S1) = 0 & ( IC S2) = 0 by Th47;

      ( DataPart S1) = ( DataPart s1) by Th45

      .= ( DataPart S2) by A1, Th45;

      hence thesis by A2, Th78;

    end;

    theorem :: MEMSTR_0:81

    ( the_Values_of ( Trivial-Mem N)) = ( 0 .--> NAT ) by Lm1;

    definition

      let N, S;

      let f be Function of ( product ( the_Values_of S)), NAT ;

      :: MEMSTR_0:def18

      attr f is on_data_only means for s1,s2 be State of S st ( DataPart s1) = ( DataPart s2) holds (f . s1) = (f . s2);

    end