:: MEMSTR_0 semantic presentation

begin


definition
let N be set ;
attrc2 is strict ;
struct Mem-Struct over N ->  ZeroStr ;
aggrMem-Struct(# carrier, ZeroF, Object-Kind, ValuesF #) ->  Mem-Struct over N;
sel Object-Kind c2 ->  Function of the carrier of c2,N;
sel ValuesF c2 ->  ManySortedSet of N;
end;

definition
let N be with_zero set ;
func Trivial-Mem N ->  strict Mem-Struct over N means :Def1: :: MEMSTR_0:def 1
( the carrier of it = {0} & the ZeroF of it = 0 & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT );
existence
 ex b1 being strict Mem-Struct over N st
( the carrier of b1 = {0} & the ZeroF of b1 = 0 & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT )
proof
set f = 0 .--> 0;
A1: dom (0 .--> 0) = {0} by FUNCOP_1:13;
A2: rng (0 .--> 0) c= {0} by FUNCOP_1:13;
 0 in N by MEASURE6:def_2;
then  {0} c= N by ZFMISC_1:31;
then  rng (0 .--> 0) c= N by A2, XBOOLE_1:1;
then reconsider f = 0 .--> 0 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) #) ; ::_thesis: ( the carrier of Mem-Struct(# {0},y,f,(N --> NAT) #) = {0} & the ZeroF of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 & the Object-Kind of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 .--> 0 & the ValuesF of Mem-Struct(# {0},y,f,(N --> NAT) #) = N --> NAT )
thus  ( the carrier of Mem-Struct(# {0},y,f,(N --> NAT) #) = {0} & the ZeroF of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 & the Object-Kind of Mem-Struct(# {0},y,f,(N --> NAT) #) = 0 .--> 0 & the ValuesF of Mem-Struct(# {0},y,f,(N --> NAT) #) = N --> NAT ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Mem-Struct over N st the carrier of b1 = {0} & the ZeroF of b1 = 0 & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the carrier of b2 = {0} & the ZeroF of b2 = 0 & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT holds
b1 = b2 ;
end;

:: deftheorem Def1 defines Trivial-Mem MEMSTR_0:def_1_:_
 for N being with_zero set
for b2 being strict Mem-Struct over N holds
( b2 = Trivial-Mem N iff ( the carrier of b2 = {0} & the ZeroF of b2 = 0 & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT ) );

registration
let N be with_zero set ;
cluster Trivial-Mem N -> 1 -element strict ;
coherence
 Trivial-Mem N is 1 -element
proof
 the carrier of (Trivial-Mem N) = {0} by Def1;
hence  the carrier of (Trivial-Mem N) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster1 -element for Mem-Struct over N;
existence
 ex b1 being Mem-Struct over N st b1 is 1 -element
proof
take  Trivial-Mem N ; ::_thesis: Trivial-Mem N is 1 -element
thus  Trivial-Mem N is 1 -element ; ::_thesis: verum
end;
end;

notation
let N be with_zero set ;
let S be Mem-Struct over N;
synonym  IC S for  0. N;
synonym  Data-Locations S for  NonZero N;
end;

registration
cluster with_zero  ->  non empty for set ;
coherence
 for b1 being set st b1 is with_zero holds
not b1 is empty by MEASURE6:def_2;
end;

definition
let N be with_zero set ;
let S be Mem-Struct over N;
func the_Values_of S ->  ManySortedSet of the carrier of S equals :: MEMSTR_0:def 2
 the ValuesF of S * the Object-Kind of S;
coherence
 the ValuesF of S * the Object-Kind of S is ManySortedSet of the carrier of S ;
end;

:: deftheorem  defines the_Values_of MEMSTR_0:def_2_:_
 for N being with_zero set
for S being Mem-Struct over N holds the_Values_of S = the ValuesF of S * the Object-Kind of S;

definition
let N be with_zero set ;
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 be with_zero set ;
let S be Mem-Struct over N;
attrS is with_non-empty_values  means :Def3: :: MEMSTR_0:def 3
 the_Values_of S is non-empty ;
end;

:: deftheorem Def3 defines with_non-empty_values MEMSTR_0:def_3_:_
 for N being with_zero set
for S being Mem-Struct over N holds
( S is with_non-empty_values iff the_Values_of S is non-empty );

registration
let N be with_zero set ;
cluster Trivial-Mem N ->  strict with_non-empty_values ;
coherence
 Trivial-Mem N is with_non-empty_values
proof
let n be set ; :: according to FUNCT_1:def_9,MEMSTR_0:def_3 ::_thesis: ( not n in dom (the_Values_of (Trivial-Mem N)) or not (the_Values_of (Trivial-Mem N)) . n is empty )
set S = Trivial-Mem N;
set F = the_Values_of (Trivial-Mem N);
assume A1: n in dom (the_Values_of (Trivial-Mem N)) ; ::_thesis: not (the_Values_of (Trivial-Mem N)) . n is empty
then A2: the Object-Kind of (Trivial-Mem N) . n in dom the ValuesF of (Trivial-Mem N) by FUNCT_1:11;
A3: the ValuesF of (Trivial-Mem N) = N --> NAT by Def1;
then A4: the Object-Kind of (Trivial-Mem N) . n in N by A2, FUNCOP_1:13;
(the_Values_of (Trivial-Mem N)) . n = the ValuesF of (Trivial-Mem N) . ( the Object-Kind of (Trivial-Mem N) . n) by A1, FUNCT_1:12
.= NAT by A4, A3, FUNCOP_1:7 ;
hence  not (the_Values_of (Trivial-Mem N)) . n is empty ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster with_non-empty_values for Mem-Struct over N;
existence
 ex b1 being Mem-Struct over N st b1 is with_non-empty_values
proof
take  Trivial-Mem N ; ::_thesis: Trivial-Mem N is with_non-empty_values
thus  Trivial-Mem N is with_non-empty_values ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be with_non-empty_values Mem-Struct over N;
cluster the_Values_of S ->  non-empty ;
coherence
 the_Values_of S is non-empty by Def3;
end;

definition
let N be with_zero set ;
let S be with_non-empty_values Mem-Struct over N;
mode State of S is total PartState of S;
end;

definition
let N be with_zero set ;
let S be Mem-Struct over N;
mode Object of S is Element of S;
end;

begin

definition
let N be with_zero set ;
let S be non empty Mem-Struct over N;
let o be Object of S;
func ObjectKind o ->  Element of N equals :: MEMSTR_0:def 4
 the Object-Kind of S . o;
correctness
coherence
the Object-Kind of S . o is Element of N;
;
end;

:: deftheorem  defines ObjectKind MEMSTR_0:def_4_:_
 for N being with_zero set
for S being non empty Mem-Struct over N
for o being Object of S holds ObjectKind o = the Object-Kind of S . o;

definition
let N be with_zero set ;
let S be non empty Mem-Struct over N;
let o be Object of S;
func Values o ->  set  equals :: MEMSTR_0:def 5
(the_Values_of S) . o;
correctness
coherence
(the_Values_of S) . o is set ;
;
end;

:: deftheorem  defines Values MEMSTR_0:def_5_:_
 for N being with_zero set
for S being non empty Mem-Struct over N
for o being Object of S holds Values o = (the_Values_of S) . o;

definition
let N be with_zero set ;
let IT be non empty Mem-Struct over N;
attrIT is IC-Ins-separated  means :Def6: :: MEMSTR_0:def 6
 Values (IC ) = NAT ;
end;

:: deftheorem Def6 defines IC-Ins-separated MEMSTR_0:def_6_:_
 for N being with_zero set
for IT being non empty Mem-Struct over N holds
( IT is IC-Ins-separated iff Values (IC ) = NAT );

Lm1:  for N being with_zero set holds the_Values_of (Trivial-Mem N) = 0 .--> NAT
proof
let N be with_zero set ; ::_thesis: the_Values_of (Trivial-Mem N) = 0 .--> NAT
set S = Trivial-Mem N;
set f = the_Values_of (Trivial-Mem N);
set g = 0 .--> NAT;
 the Object-Kind of (Trivial-Mem N) = 0 .--> 0 by Def1;
then A1: the_Values_of (Trivial-Mem N) = (N --> NAT) * (0 .--> 0) by Def1;
A2: dom (N --> NAT) = N by FUNCOP_1:13;
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 (the_Values_of (Trivial-Mem N)) = dom (0 .--> 0) by A1, A2, A3, RELAT_1:27
.= {0} by FUNCOP_1:13 ;
hence  dom (the_Values_of (Trivial-Mem N)) = dom (0 .--> NAT) by FUNCOP_1:13; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom (the_Values_of (Trivial-Mem N)) or (the_Values_of (Trivial-Mem N)) . b1 = (0 .--> NAT) . b1 )
let x be set ; ::_thesis: ( not x in dom (the_Values_of (Trivial-Mem N)) or (the_Values_of (Trivial-Mem N)) . x = (0 .--> NAT) . x )
assume A6: x in dom (the_Values_of (Trivial-Mem N)) ; ::_thesis: (the_Values_of (Trivial-Mem N)) . x = (0 .--> NAT) . x
then A7: x = 0 by A5, TARSKI:def_1;
thus (the_Values_of (Trivial-Mem N)) . 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
.= (0 .--> NAT) . x by A7, FUNCOP_1:72 ; ::_thesis: verum
end;

registration
let N be with_zero set ;
cluster Trivial-Mem N ->  strict IC-Ins-separated ;
coherence
 Trivial-Mem N is IC-Ins-separated
proof
 IC = 0 by Def1;
hence  Values (IC ) = (0 .--> NAT) . 0 by Lm1
.= NAT by FUNCOP_1:72 ;
:: according to MEMSTR_0:def_6 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster non empty trivial finite 1 -element strict with_non-empty_values IC-Ins-separated for Mem-Struct over N;
existence
 ex b1 being 1 -element Mem-Struct over N st
( b1 is IC-Ins-separated & b1 is with_non-empty_values & b1 is strict )
proof
take  Trivial-Mem N ; ::_thesis: ( Trivial-Mem N is IC-Ins-separated & Trivial-Mem N is with_non-empty_values & Trivial-Mem N is strict )
thus  ( Trivial-Mem N is IC-Ins-separated & Trivial-Mem N is with_non-empty_values & Trivial-Mem N is strict ) ; ::_thesis: verum
end;
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be PartState of S;
func IC p ->  Element of NAT  equals :: MEMSTR_0:def 7
p . (IC );
coherence
 p . (IC ) is Element of NAT
proof
percases ( IC in dom p or not IC in dom p ) ;
supposeA1: IC in dom p ; ::_thesis: p . (IC ) is Element of NAT
consider s being 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 )) = Values (IC ) by CARD_3:12
.= NAT by Def6 ;
then  ss . (IC ) in NAT by CARD_3:def_6;
hence  p . (IC ) is Element of NAT by A1, A2, GRFUNC_1:2; ::_thesis: verum
end;
suppose not IC in dom p ; ::_thesis: p . (IC ) is Element of NAT
then  p . (IC ) = 0 by FUNCT_1:def_2;
hence  p . (IC ) is Element of NAT ; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem  defines IC MEMSTR_0:def_7_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds IC p = p . (IC );

theorem :: MEMSTR_0:1
for N being with_zero set
for S being 1 -element with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of S st IC s1 = IC s2 holds
s1 = s2
proof
let N be with_zero set ; ::_thesis: for S being 1 -element with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of S st IC s1 = IC s2 holds
s1 = s2
let T be 1 -element with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s1, s2 being State of T st IC s1 = IC s2 holds
s1 = s2
let s1, s2 be State of T; ::_thesis: ( IC s1 = IC s2 implies s1 = s2 )
assume A1: IC s1 = IC s2 ; ::_thesis: s1 = s2
A2: dom s1 = the carrier of T by PARTFUN1:def_2;
then A3: dom s1 = dom s2 by PARTFUN1:def_2;
now__::_thesis:_for_x_being_set_st_x_in_dom_s1_holds_
s1_._x_=_s2_._x
let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume A4: x in dom s1 ; ::_thesis: s1 . x = s2 . x
A5: x = IC by A4, A2, STRUCT_0:def_10;
hence s1 . x = IC s1
.= s2 . x by A1, A5 ;
::_thesis: verum
end;
hence  s1 = s2 by A3, FUNCT_1:2; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values Mem-Struct over N;
let o be Object of S;
cluster Values o ->  non empty ;
coherence
 not Values o is empty ;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let la be Object of S;
let a be Element of Values la;
clusterla .--> a ->  the_Values_of S -compatible ;
coherence
 la .--> a is the_Values_of S -compatible
proof
set p = la .--> a;
A1: dom (la .--> a) = {la} by FUNCOP_1:13;
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom (la .--> a) or (la .--> a) . x in (the_Values_of S) . x )
assume  x in dom (la .--> a) ; ::_thesis: (la .--> a) . x in (the_Values_of S) . x
then A2: x = la by A1, TARSKI:def_1;
then  (la .--> a) . x = a by FUNCOP_1:72;
hence  (la .--> a) . x in (the_Values_of S) . x by A2; ::_thesis: verum
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
 (la,lb) --> (a,b) is the_Values_of S -compatible ;
end;

theorem Th2: :: MEMSTR_0:2
for N being with_zero set
for S being non empty with_non-empty_values Mem-Struct over N
for s being State of S holds IC in dom s
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values Mem-Struct over N
for s being State of S holds IC in dom s
let S be non empty with_non-empty_values Mem-Struct over N; ::_thesis: for s being State of S holds IC in dom s
let s be State of S; ::_thesis: IC in dom s
 dom s = the carrier of S by PARTFUN1:def_2;
hence  IC in dom s ; ::_thesis: verum
end;

definition
let N be with_zero set ;
let S be Mem-Struct over N;
let p be PartState of S;
func DataPart p ->  PartState of S equals :: MEMSTR_0:def 8
p | (Data-Locations );
coherence
 p | (Data-Locations ) is PartState of S ;
projectivity
 for b1, b2 being PartState of S st b1 = b2 | (Data-Locations ) holds
b1 = b1 | (Data-Locations ) by RELAT_1:72;
end;

:: deftheorem  defines DataPart MEMSTR_0:def_8_:_
 for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds DataPart p = p | (Data-Locations );

definition
let N be with_zero set ;
let S be Mem-Struct over N;
let p be PartState of S;
attrp is data-only  means :Def9: :: MEMSTR_0:def 9
 dom p misses {(IC )};
end;

:: deftheorem Def9 defines data-only MEMSTR_0:def_9_:_
 for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds
( p is data-only iff dom p misses {(IC )} );

registration
let N be with_zero set ;
let S be Mem-Struct over N;
cluster empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible  ->  data-only for set ;
coherence
 for b1 being PartState of S st b1 is empty holds
b1 is data-only
proof
let p be PartState of S; ::_thesis: ( p is empty implies p is data-only )
assume  p is empty ; ::_thesis: p is data-only
hence  dom p misses {(IC )} by RELAT_1:38, XBOOLE_1:65; :: according to MEMSTR_0:def_9 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be Mem-Struct over N;
cluster empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible for set ;
existence
 ex b1 being PartState of S st b1 is empty
proof
reconsider a = {} as PartState of S by FUNCT_1:104, RELAT_1:171;
take  a ; ::_thesis: a is empty
thus  a is empty ; ::_thesis: verum
end;
end;

theorem Th3: :: MEMSTR_0:3
for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds not IC in dom (DataPart p)
proof
let N be with_zero set ; ::_thesis: for S being Mem-Struct over N
for p being PartState of S holds not IC in dom (DataPart p)
let S be Mem-Struct over N; ::_thesis: for p being PartState of S holds not IC in dom (DataPart p)
let p be PartState of S; ::_thesis: not IC in dom (DataPart p)
assume A1: IC in dom (DataPart p) ; ::_thesis: contradiction
 dom (DataPart p) c= the carrier of S \ {(IC )} by RELAT_1:58;
then  not IC in {(IC )} by A1, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;

theorem :: MEMSTR_0:4
for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds {(IC )} misses dom (DataPart p) by Th3, ZFMISC_1:50;

theorem :: MEMSTR_0:5
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being data-only PartState of S
for q being PartState of S holds
( p c= q iff p c= DataPart q )
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being data-only PartState of S
for q being PartState of S holds
( p c= q iff p c= DataPart q )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being data-only PartState of S
for q being PartState of S holds
( p c= q iff p c= DataPart q )
let p be data-only PartState of S; ::_thesis: for q being PartState of S holds
( p c= q iff p c= DataPart q )
let q be PartState of S; ::_thesis: ( p c= q iff p c= DataPart q )
set X = the carrier of S \ {(IC )};
A1: q | ( the carrier of S \ {(IC )}) c= q by RELAT_1:59;
hereby  ::_thesis: ( p c= DataPart q implies p c= q )
A2: ( the carrier of S \ {(IC )}) \/ {(IC )} = the carrier of S \/ {(IC )} by XBOOLE_1:39;
 dom p c= the carrier of S by RELAT_1:def_18;
then A3: dom p c= ( the carrier of S \ {(IC )}) \/ {(IC )} by A2, XBOOLE_1:10;
assume  p c= q ; ::_thesis: p c= DataPart q
then A4: p | ( the carrier of S \ {(IC )}) c= DataPart q by RELAT_1:76;
 dom p misses {(IC )} by Def9;
hence  p c= DataPart q by A4, A3, RELAT_1:68, XBOOLE_1:73; ::_thesis: verum
end;
thus  ( p c= DataPart q implies p c= q ) by A1, XBOOLE_1:1; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be Mem-Struct over N;
let p be PartState of S;
cluster DataPart p ->  data-only ;
coherence
 DataPart p is data-only
proof
thus  dom (DataPart p) misses {(IC )} by Th3, ZFMISC_1:50; :: according to MEMSTR_0:def_9 ::_thesis: verum
end;
end;

theorem Th6: :: MEMSTR_0:6
for N being with_zero set
for S being Mem-Struct over N
for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations )
proof
let N be with_zero set ; ::_thesis: for S being Mem-Struct over N
for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations )
let S be Mem-Struct over N; ::_thesis: for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations )
let p be PartState of S; ::_thesis: ( p is data-only iff dom p c= Data-Locations )
thus  ( p is data-only implies dom p c= Data-Locations ) ::_thesis: ( dom p c= Data-Locations implies p is data-only )
proof
A1: dom p c= the carrier of S by RELAT_1:def_18;
assume  dom p misses {(IC )} ; :: according to MEMSTR_0:def_9 ::_thesis: dom p c= Data-Locations
hence  dom p c= Data-Locations by A1, XBOOLE_1:86; ::_thesis: verum
end;
assume  dom p c= Data-Locations ; ::_thesis: p is data-only
hence  dom p misses {(IC )} by XBOOLE_1:106; :: according to MEMSTR_0:def_9 ::_thesis: verum
end;

theorem :: MEMSTR_0:7
for N being with_zero set
for S being Mem-Struct over N
for p being data-only PartState of S holds DataPart p = p
proof
let N be with_zero set ; ::_thesis: for S being Mem-Struct over N
for p being data-only PartState of S holds DataPart p = p
let S be Mem-Struct over N; ::_thesis: for p being data-only PartState of S holds DataPart p = p
let p be data-only PartState of S; ::_thesis: DataPart p = p
 dom p c= Data-Locations by Th6;
hence  DataPart p = p by RELAT_1:68; ::_thesis: verum
end;

theorem Th8: :: MEMSTR_0:8
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds Data-Locations c= dom s
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds Data-Locations c= dom s
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S holds Data-Locations c= dom s
let s be State of S; ::_thesis: Data-Locations c= dom s
 dom s = the carrier of S by PARTFUN1:def_2;
hence  Data-Locations c= dom s ; ::_thesis: verum
end;

theorem Th9: :: MEMSTR_0:9
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds dom (DataPart s) = Data-Locations
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds dom (DataPart s) = Data-Locations
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S holds dom (DataPart s) = Data-Locations
let s be State of S; ::_thesis: dom (DataPart s) = Data-Locations
 Data-Locations c= dom s by Th8;
hence  dom (DataPart s) = Data-Locations by RELAT_1:62; ::_thesis: verum
end;

theorem Th10: :: MEMSTR_0:10
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for d being data-only PartState of S holds not IC in dom d
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for d being data-only PartState of S holds not IC in dom d
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for d being data-only PartState of S holds not IC in dom d
let d be data-only PartState of S; ::_thesis: not IC in dom d
 dom d c= Data-Locations by Th6;
hence  not IC in dom d by STRUCT_0:3; ::_thesis: verum
end;

theorem Th11: :: MEMSTR_0:11
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for d being data-only PartState of S holds IC (p +* d) = IC p
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for d being data-only PartState of S holds IC (p +* d) = IC p
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for d being data-only PartState of S holds IC (p +* d) = IC p
let p be PartState of S; ::_thesis: for d being data-only PartState of S holds IC (p +* d) = IC p
let d be data-only PartState of S; ::_thesis: IC (p +* d) = IC p
A1: not IC in dom d by Th10;
thus  IC (p +* d) = IC p by A1, FUNCT_4:11; ::_thesis: verum
end;

theorem :: MEMSTR_0:12
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds DataPart p c= p by RELAT_1:59;

theorem Th13: :: MEMSTR_0:13
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds dom s = {(IC )} \/ (Data-Locations )
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds dom s = {(IC )} \/ (Data-Locations )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S holds dom s = {(IC )} \/ (Data-Locations )
let s be State of S; ::_thesis: dom s = {(IC )} \/ (Data-Locations )
 dom s = the carrier of S by PARTFUN1:def_2;
hence  dom s = {(IC )} \/ (Data-Locations ) by STRUCT_0:4; ::_thesis: verum
end;

theorem :: MEMSTR_0:14
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds (dom p) /\ (Data-Locations ) = dom (DataPart p) by RELAT_1:61;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Element of NAT ;
let s be State of S;
clusters +* ((IC ),l) ->  the_Values_of S -compatible ;
coherence
 s +* ((IC ),l) is the_Values_of S -compatible
proof
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom (s +* ((IC ),l)) or (s +* ((IC ),l)) . x in (the_Values_of S) . x )
assume  x in dom (s +* ((IC ),l)) ; ::_thesis: (s +* ((IC ),l)) . x in (the_Values_of S) . x
then A1: x in dom s by FUNCT_7:30;
percases ( x = IC or x <> IC ) ;
supposeA2: x = IC ; ::_thesis: (s +* ((IC ),l)) . x in (the_Values_of S) . x
then A3: (s +* ((IC ),l)) . x = l by A1, FUNCT_7:31;
 Values (IC ) = NAT by Def6;
hence  (s +* ((IC ),l)) . x in (the_Values_of S) . x by A2, A3; ::_thesis: verum
end;
suppose x <> IC ; ::_thesis: (s +* ((IC ),l)) . x in (the_Values_of S) . x
then  (s +* ((IC ),l)) . x = s . x by FUNCT_7:32;
hence  (s +* ((IC ),l)) . x in (the_Values_of S) . x by A1, FUNCT_1:def_14; ::_thesis: verum
end;
end;
end;
end;

begin

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
func Start-At (l,S) ->  PartState of S equals :: MEMSTR_0:def 10
(IC ) .--> l;
correctness
coherence
(IC ) .--> l is PartState of S;
proof
reconsider l = l as Element of NAT by ORDINAL1:def_12;
 Values (IC ) = NAT by Def6;
then reconsider l = l as Element of Values (IC ) ;
 (IC ) .--> l is PartState of S ;
hence  (IC ) .--> l is PartState of S ; ::_thesis: verum
end;
end;

:: deftheorem  defines Start-At MEMSTR_0:def_10_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat holds Start-At (l,S) = (IC ) .--> l;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
let p be PartState of S;
attrp is l -started  means :Def11: :: MEMSTR_0:def 11
( IC in dom p & IC p = l );
end;

:: deftheorem Def11 defines -started MEMSTR_0:def_11_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat
for p being PartState of S holds
( p is l -started iff ( IC in dom p & IC p = l ) );

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
cluster Start-At (l,S) ->  non empty l -started ;
coherence
 ( Start-At (l,S) is l -started & not Start-At (l,S) is empty )
proof
 dom (Start-At (l,S)) = {(IC )} by FUNCOP_1:13;
hence  IC in dom (Start-At (l,S)) by TARSKI:def_1; :: according to MEMSTR_0:def_11 ::_thesis: ( IC (Start-At (l,S)) = l & not Start-At (l,S) is empty )
thus  ( IC (Start-At (l,S)) = l & not Start-At (l,S) is empty ) by FUNCOP_1:72; ::_thesis: verum
end;
end;

theorem Th15: :: MEMSTR_0:15
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat holds IC in dom (Start-At (l,S))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat holds IC in dom (Start-At (l,S))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for l being Nat holds IC in dom (Start-At (l,S))
let l be Nat; ::_thesis: IC in dom (Start-At (l,S))
 dom (Start-At (l,S)) = {(IC )} by FUNCOP_1:13;
hence  IC in dom (Start-At (l,S)) by TARSKI:def_1; ::_thesis: verum
end;

theorem Th16: :: MEMSTR_0:16
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for n being Nat holds IC (p +* (Start-At (n,S))) = n
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for n being Nat holds IC (p +* (Start-At (n,S))) = n
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for n being Nat holds IC (p +* (Start-At (n,S))) = n
let p be PartState of S; ::_thesis: for n being Nat holds IC (p +* (Start-At (n,S))) = n
let n be Nat; ::_thesis: IC (p +* (Start-At (n,S))) = n
A1: IC in dom (Start-At (n,S)) by Th15;
 (Start-At (n,S)) . (IC ) = n by FUNCOP_1:72;
hence  IC (p +* (Start-At (n,S))) = n by A1, FUNCT_4:13; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
cluster non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total l -started for set ;
existence
 ex b1 being State of S st b1 is l -started
proof
take s = the State of S +* (Start-At (l,S)); ::_thesis: s is l -started
thus  IC in dom s by Th2; :: according to MEMSTR_0:def_11 ::_thesis: IC s = l
thus  IC s = l by Th16; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
let p be PartState of S;
let q be l -started PartState of S;
clusterp +* q -> l -started ;
coherence
 p +* q is l -started
proof
A1: IC in dom q by Def11;
 dom q c= dom (p +* q) by FUNCT_4:10;
hence  IC in dom (p +* q) by A1; :: according to MEMSTR_0:def_11 ::_thesis: IC (p +* q) = l
 IC q = l by Def11;
hence  IC (p +* q) = l by A1, FUNCT_4:13; ::_thesis: verum
end;
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
let s be State of S;
redefine attr s is l -started  means :: MEMSTR_0:def 12
 IC s = l;
compatibility
 ( s is l -started iff IC s = l )
proof
thus  ( s is l -started implies IC s = l ) by Def11; ::_thesis: ( IC s = l implies s is l -started )
assume A1: IC s = l ; ::_thesis: s is l -started
thus  IC in dom s by Th2; :: according to MEMSTR_0:def_11 ::_thesis: IC s = l
thus  IC s = l by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines -started MEMSTR_0:def_12_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat
for s being State of S holds
( s is l -started iff IC s = l );

theorem :: MEMSTR_0:17
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat
for p being b3 -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat
for p being b2 -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for l being Nat
for p being b1 -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
let l be Nat; ::_thesis: for p being l -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
let p be l -started PartState of S; ::_thesis: for s being PartState of S st p c= s holds
s is l -started
A1: IC in dom p by Def11;
A2: IC p = l by Def11;
let s be PartState of S; ::_thesis: ( p c= s implies s is l -started )
assume A3: p c= s ; ::_thesis: s is l -started
then  dom p c= dom s by RELAT_1:11;
hence  IC in dom s by A1; :: according to MEMSTR_0:def_11 ::_thesis: IC s = l
thus  IC s = l by A3, A2, A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th18: :: MEMSTR_0:18
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds Start-At ((IC s),S) = s | {(IC )}
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds Start-At ((IC s),S) = s | {(IC )}
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S holds Start-At ((IC s),S) = s | {(IC )}
let s be State of S; ::_thesis: Start-At ((IC s),S) = s | {(IC )}
A1: IC in dom s by Th2;
thus  Start-At ((IC s),S) = {[(IC ),(s . (IC ))]} by FUNCT_4:82
.= s | {(IC )} by A1, GRFUNC_1:28 ; ::_thesis: verum
end;

theorem Th19: :: MEMSTR_0:19
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
p = (Start-At ((IC p),S)) +* (DataPart p)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
p = (Start-At ((IC p),S)) +* (DataPart p)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S st IC in dom p holds
p = (Start-At ((IC p),S)) +* (DataPart p)
let p be PartState of S; ::_thesis: ( IC in dom p implies p = (Start-At ((IC p),S)) +* (DataPart p) )
assume  IC in dom p ; ::_thesis: p = (Start-At ((IC p),S)) +* (DataPart p)
then A1: {(IC )} is Subset of (dom p) by SUBSET_1:41;
A2: {(IC )} \/ ( the carrier of S \ {(IC )}) = the carrier of S \/ {(IC )} 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__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_
p_._x_=_((Start-At_((IC_p),S))_+*_(DataPart_p))_._x
let x be set ; ::_thesis: ( x in dom p implies p . b1 = ((Start-At ((IC p),S)) +* (DataPart p)) . b1 )
assume A5: x in dom p ; ::_thesis: p . b1 = ((Start-At ((IC p),S)) +* (DataPart p)) . b1
percases ( x in {(IC )} or x in the carrier of S \ {(IC )} ) by A5, A3, A2, XBOOLE_0:def_3;
supposeA6: x in {(IC )} ; ::_thesis: p . b1 = ((Start-At ((IC p),S)) +* (DataPart p)) . b1
 {(IC )} = dom (Start-At ((IC p),S)) by FUNCOP_1:13;
then  IC in dom (Start-At ((IC p),S)) by TARSKI:def_1;
then A7: IC in (dom (Start-At ((IC p),S))) \/ (dom (DataPart p)) by XBOOLE_0:def_3;
A8: x = IC by A6, TARSKI:def_1;
 not IC 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; ::_thesis: verum
end;
suppose x in the carrier of S \ {(IC )} ; ::_thesis: p . b1 = ((Start-At ((IC p),S)) +* (DataPart p)) . b1
then  x in (dom p) /\ ( the carrier of S \ {(IC )}) by A5, XBOOLE_0:def_4;
then A9: x in dom (p | ( the carrier of S \ {(IC )})) 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 ; ::_thesis: verum
end;
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 )} \/ (dom (DataPart p)) by FUNCOP_1:13
.= ((dom p) /\ {(IC )}) \/ (dom (p | ( the carrier of S \ {(IC )}))) by A1, XBOOLE_1:28
.= ((dom p) /\ {(IC )}) \/ ((dom p) /\ ( the carrier of S \ {(IC )})) by RELAT_1:61
.= (dom p) /\ the carrier of S by A2, XBOOLE_1:23
.= dom p by A10, XBOOLE_1:28 ;
hence  p = (Start-At ((IC p),S)) +* (DataPart p) by A4, FUNCT_1:2; ::_thesis: verum
end;

theorem Th20: :: MEMSTR_0:20
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat holds DataPart (Start-At (l,S)) = {}
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat holds DataPart (Start-At (l,S)) = {}
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for l being Nat holds DataPart (Start-At (l,S)) = {}
let l be Nat; ::_thesis: DataPart (Start-At (l,S)) = {}
 Data-Locations misses {(IC )} by XBOOLE_1:79;
then  Data-Locations misses dom (Start-At (l,S)) by FUNCOP_1:13;
hence  DataPart (Start-At (l,S)) = {} by RELAT_1:66; ::_thesis: verum
end;

theorem :: MEMSTR_0:21
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l1, l2, k being Nat holds
( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l1, l2, k being Nat holds
( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for l1, l2, k being Nat holds
( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )
let l1, l2, k be Nat; ::_thesis: ( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )
hereby  ::_thesis: ( Start-At (l1,S) = Start-At (l2,S) implies Start-At ((l1 + k),S) = Start-At ((l2 + k),S) )
assume  Start-At ((l1 + k),S) = Start-At ((l2 + k),S) ; ::_thesis: Start-At (l1,S) = Start-At (l2,S)
then  {[(IC ),(l1 + k)]} = (IC ) .--> (l2 + k) by FUNCT_4:82;
then  {[(IC ),(l1 + k)]} = {[(IC ),(l2 + k)]} by FUNCT_4:82;
then  [(IC ),(l1 + k)] = [(IC ),(l2 + k)] by ZFMISC_1:3;
then  l1 + k = l2 + k by XTUPLE_0:1;
hence  Start-At (l1,S) = Start-At (l2,S) ; ::_thesis: verum
end;
assume  Start-At (l1,S) = Start-At (l2,S) ; ::_thesis: Start-At ((l1 + k),S) = Start-At ((l2 + k),S)
then  {[(IC ),l1]} = Start-At (l2,S) by FUNCT_4:82;
then  {[(IC ),l1]} = {[(IC ),l2]} by FUNCT_4:82;
then  [(IC ),l1] = [(IC ),l2] by ZFMISC_1:3;
hence  Start-At ((l1 + k),S) = Start-At ((l2 + k),S) by XTUPLE_0:1; ::_thesis: verum
end;

theorem :: MEMSTR_0:22
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l1, l2, k being Nat st Start-At (l1,S) = Start-At (l2,S) holds
Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l1, l2, k being Nat st Start-At (l1,S) = Start-At (l2,S) holds
Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for l1, l2, k being Nat st Start-At (l1,S) = Start-At (l2,S) holds
Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)
let l1, l2, k be Nat; ::_thesis: ( Start-At (l1,S) = Start-At (l2,S) implies Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S) )
assume  Start-At (l1,S) = Start-At (l2,S) ; ::_thesis: Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)
then {[(IC ),l1]} = Start-At (l2,S) by FUNCT_4:82
.= {[(IC ),l2]} by FUNCT_4:82 ;
then  [(IC ),l1] = [(IC ),l2] by ZFMISC_1:3;
hence  Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S) by XTUPLE_0:1; ::_thesis: verum
end;

theorem Th23: :: MEMSTR_0:23
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for d being data-only PartState of S
for k being Nat holds d tolerates Start-At (k,S)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for d being data-only PartState of S
for k being Nat holds d tolerates Start-At (k,S)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for d being data-only PartState of S
for k being Nat holds d tolerates Start-At (k,S)
let d be data-only PartState of S; ::_thesis: for k being Nat holds d tolerates Start-At (k,S)
let k be Nat; ::_thesis: d tolerates Start-At (k,S)
 dom (Start-At (k,S)) = {(IC )} by FUNCOP_1:13;
then  dom d misses dom (Start-At (k,S)) by Th10, ZFMISC_1:50;
hence  d tolerates Start-At (k,S) by PARTFUN1:56; ::_thesis: verum
end;

theorem Th24: :: MEMSTR_0:24
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
dom p = {(IC )} \/ (dom (DataPart p))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
dom p = {(IC )} \/ (dom (DataPart p))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S st IC in dom p holds
dom p = {(IC )} \/ (dom (DataPart p))
let p be PartState of S; ::_thesis: ( IC in dom p implies dom p = {(IC )} \/ (dom (DataPart p)) )
assume  IC in dom p ; ::_thesis: dom p = {(IC )} \/ (dom (DataPart 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 )} \/ (dom (DataPart p)) by FUNCOP_1:13 ;
hence  dom p = {(IC )} \/ (dom (DataPart p)) ; ::_thesis: verum
end;

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

theorem Th26: :: MEMSTR_0:26
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
p = (DataPart p) +* (Start-At ((IC p),S))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
p = (DataPart p) +* (Start-At ((IC p),S))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S st IC in dom p holds
p = (DataPart p) +* (Start-At ((IC p),S))
let p be PartState of S; ::_thesis: ( IC in dom p implies p = (DataPart p) +* (Start-At ((IC p),S)) )
A1: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:13;
then 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 A1, Th3, ZFMISC_1:50;
assume  IC in dom p ; ::_thesis: p = (DataPart p) +* (Start-At ((IC p),S))
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  p = (DataPart p) +* (Start-At ((IC p),S)) by A2, A4, FUNCT_4:31; ::_thesis: verum
end;

theorem Th27: :: MEMSTR_0:27
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds IC in dom (p +* (Start-At (k,S)))
proof
let k be Nat; ::_thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds IC in dom (p +* (Start-At (k,S)))
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds IC in dom (p +* (Start-At (k,S)))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S holds IC in dom (p +* (Start-At (k,S)))
let p be PartState of S; ::_thesis: IC in dom (p +* (Start-At (k,S)))
 dom (Start-At (k,S)) = {(IC )} by FUNCOP_1:13;
then  IC in dom (Start-At (k,S)) by TARSKI:def_1;
hence  IC in dom (p +* (Start-At (k,S))) by FUNCT_4:12; ::_thesis: verum
end;

theorem :: MEMSTR_0:28
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
proof
let k be Nat; ::_thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let s be State of S; ::_thesis: for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let p be PartState of S; ::_thesis: ( p +* (Start-At (k,S)) c= s implies IC s = k )
assume A1: p +* (Start-At (k,S)) c= s ; ::_thesis: IC s = k
 IC 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 ;
::_thesis: verum
end;

theorem Th29: :: MEMSTR_0:29
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat
for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat
for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for l being Nat
for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let l be Nat; ::_thesis: for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let p be PartState of S; ::_thesis: ( p is l -started iff Start-At (l,S) c= p )
A1: dom (Start-At (l,S)) = {(IC )} by FUNCOP_1:13;
thus  ( p is l -started implies Start-At (l,S) c= p ) ::_thesis: ( Start-At (l,S) c= p implies p is l -started )
proof
assume A2: p is l -started ; ::_thesis: Start-At (l,S) c= p
 IC in dom p by A2, Def11;
then A3: dom (Start-At (l,S)) c= dom p by A1, ZFMISC_1:31;
 for x being set st x in dom (Start-At (l,S)) holds
(Start-At (l,S)) . x = p . x
proof
let x be set ; ::_thesis: ( x in dom (Start-At (l,S)) implies (Start-At (l,S)) . x = p . x )
assume A4: x in dom (Start-At (l,S)) ; ::_thesis: (Start-At (l,S)) . x = p . x
hence (Start-At (l,S)) . x = IC (Start-At (l,S)) by A1, TARSKI:def_1
.= l by FUNCOP_1:72
.= IC p by A2, Def11
.= p . x by A1, A4, TARSKI:def_1 ;
::_thesis: verum
end;
hence  Start-At (l,S) c= p by A3, GRFUNC_1:2; ::_thesis: verum
end;
assume A5: Start-At (l,S) c= p ; ::_thesis: p is l -started
then A6: dom (Start-At (l,S)) c= dom p by RELAT_1:11;
A7: IC in dom (Start-At (l,S)) by A1, TARSKI:def_1;
hence  IC in dom p by A6; :: according to MEMSTR_0:def_11 ::_thesis: IC p = l
thus  IC p = IC (Start-At (l,S)) by A5, A7, GRFUNC_1:2
.= l by FUNCOP_1:72 ; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let k be Nat;
let p be k -started PartState of S;
let d be data-only PartState of S;
clusterp +* d -> k -started ;
coherence
 p +* d is k -started
proof
A1: IC in dom p by Def11;
 dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def_1;
hence  IC in dom (p +* d) by A1, XBOOLE_0:def_3; :: according to MEMSTR_0:def_11 ::_thesis: IC (p +* d) = k
 not IC in dom d by Th10;
hence  IC (p +* d) = IC p by FUNCT_4:11
.= k by Def11 ;
::_thesis: verum
end;
end;

theorem Th30: :: MEMSTR_0:30
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds Start-At ((IC s),S) c= s
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds Start-At ((IC s),S) c= s
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S holds Start-At ((IC s),S) c= s
let s be State of S; ::_thesis: Start-At ((IC s),S) c= s
 Start-At ((IC s),S) = s | {(IC )} by Th18;
hence  Start-At ((IC s),S) c= s by RELAT_1:59; ::_thesis: verum
end;

theorem :: MEMSTR_0:31
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds s +* (Start-At ((IC s),S)) = s by Th30, FUNCT_4:98;

theorem :: MEMSTR_0:32
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds dom p c= {(IC )} \/ (dom (DataPart p))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds dom p c= {(IC )} \/ (dom (DataPart p))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S holds dom p c= {(IC )} \/ (dom (DataPart p))
let p be PartState of S; ::_thesis: dom p c= {(IC )} \/ (dom (DataPart p))
set S0 = Start-At (0,S);
percases ( IC in dom p or not IC in dom p ) ;
suppose IC in dom p ; ::_thesis: dom p c= {(IC )} \/ (dom (DataPart p))
hence  dom p c= {(IC )} \/ (dom (DataPart p)) by Th24; ::_thesis: verum
end;
supposeA1: not IC in dom p ; ::_thesis: dom p c= {(IC )} \/ (dom (DataPart p))
A2: dom (Start-At (0,S)) = {(IC )} by FUNCOP_1:13;
A3: dom (p +* (Start-At (0,S))) = {(IC )} \/ (dom (DataPart (p +* (Start-At (0,S))))) by Th24, Th27
.= {(IC )} \/ (dom ((DataPart p) +* (DataPart (Start-At (0,S))))) by FUNCT_4:71
.= {(IC )} \/ (dom ((DataPart p) +* {})) by Th20
.= {(IC )} \/ (dom (DataPart p)) ;
now__::_thesis:_not_dom_p_meets_dom_(Start-At_(0,S))
assume  dom p meets dom (Start-At (0,S)) ; ::_thesis: contradiction
then consider x being set  such that
A4: x in dom p and
A5: x in dom (Start-At (0,S)) by XBOOLE_0:3;
thus  contradiction by A4, A1, A2, A5, TARSKI:def_1; ::_thesis: verum
end;
then  p c= p +* (Start-At (0,S)) by FUNCT_4:32;
hence  dom p c= {(IC )} \/ (dom (DataPart p)) by A3, RELAT_1:11; ::_thesis: verum
end;
end;
end;

theorem Th33: :: MEMSTR_0:33
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds s = s | ((Data-Locations ) \/ {(IC )})
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S holds s = s | ((Data-Locations ) \/ {(IC )})
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S holds s = s | ((Data-Locations ) \/ {(IC )})
let s be State of S; ::_thesis: s = s | ((Data-Locations ) \/ {(IC )})
thus s = s | (dom s)
.= s | ({(IC )} \/ (dom (DataPart s))) by Th2, Th24
.= s | ((Data-Locations ) \/ {(IC )}) by Th9 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:34
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds
s1 = s2
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds
s1 = s2
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds
s1 = s2
let s1, s2 be State of S; ::_thesis: ( s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) implies s1 = s2 )
 s1 = s1 | ((Data-Locations ) \/ {(IC )}) by Th33;
hence  ( s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) implies s1 = s2 ) by Th33; ::_thesis: verum
end;

theorem :: MEMSTR_0:35
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
p = (Start-At ((IC p),S)) +* (DataPart p) by Th19;

theorem Th36: :: MEMSTR_0:36
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k, l being Nat holds (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k, l being Nat holds (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k, l being Nat holds (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))
let p be PartState of S; ::_thesis: for k, l being Nat holds (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))
let k, l be Nat; ::_thesis: (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))
dom (Start-At (k,S)) = {(IC )} by FUNCOP_1:13
.= dom (Start-At (l,S)) by FUNCOP_1:13 ;
hence  (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S)) by FUNCT_4:74; ::_thesis: verum
end;

theorem :: MEMSTR_0:37
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
p +* (Start-At ((IC p),S)) = p by FUNCT_4:7, FUNCT_4:98;

theorem :: MEMSTR_0:38
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
proof
let k be Nat; ::_thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let s be State of S; ::_thesis: for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k
let p be PartState of S; ::_thesis: ( p +* (Start-At (k,S)) c= s implies IC s = k )
assume A1: p +* (Start-At (k,S)) c= s ; ::_thesis: IC s = k
 IC 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 ;
::_thesis: verum
end;

theorem :: MEMSTR_0:39
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st Start-At (0,S) c= p holds
IC p = 0
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st Start-At (0,S) c= p holds
IC p = 0
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S st Start-At (0,S) c= p holds
IC p = 0
let p be PartState of S; ::_thesis: ( Start-At (0,S) c= p implies IC p = 0 )
A1: IC (Start-At (0,S)) = 0 by Def11;
 IC in dom (Start-At (0,S)) by Def11;
hence  ( Start-At (0,S) c= p implies IC p = 0 ) by A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: MEMSTR_0:40
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st Start-At (k,S) c= p holds
IC p = k
proof
let k be Nat; ::_thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st Start-At (k,S) c= p holds
IC p = k
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st Start-At (k,S) c= p holds
IC p = k
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S st Start-At (k,S) c= p holds
IC p = k
let p be PartState of S; ::_thesis: ( Start-At (k,S) c= p implies IC p = k )
assume  Start-At (k,S) c= p ; ::_thesis: IC p = k
then  p is k -started by Th29;
hence  IC p = k by Def11; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
cluster non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible for set ;
existence
 not for b1 being PartState of S holds b1 is empty
proof
take  Start-At (0,S) ; ::_thesis: not Start-At (0,S) is empty
thus  not Start-At (0,S) is empty ; ::_thesis: verum
end;
end;

theorem :: MEMSTR_0:41
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being non empty PartState of S holds dom p meets {(IC )} \/ (Data-Locations )
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being non empty PartState of S holds dom p meets {(IC )} \/ (Data-Locations )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being non empty PartState of S holds dom p meets {(IC )} \/ (Data-Locations )
let p be non empty PartState of S; ::_thesis: dom p meets {(IC )} \/ (Data-Locations )
 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 )} \/ (Data-Locations ) by STRUCT_0:4; ::_thesis: verum
end;

begin

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be PartState of S;
func Initialize p ->  PartState of S equals :: MEMSTR_0:def 13
p +* (Start-At (0,S));
coherence
 p +* (Start-At (0,S)) is PartState of S ;
projectivity
 for b1, b2 being PartState of S st b1 = b2 +* (Start-At (0,S)) holds
b1 = b1 +* (Start-At (0,S))
proof
let q, p be PartState of S; ::_thesis: ( q = p +* (Start-At (0,S)) implies q = q +* (Start-At (0,S)) )
assume A1: q = p +* (Start-At (0,S)) ; ::_thesis: q = q +* (Start-At (0,S))
hence q = (p +* (Start-At (0,S))) +* (Start-At (0,S))
.= q +* (Start-At (0,S)) by A1 ;
::_thesis: verum
end;
end;

:: deftheorem  defines Initialize MEMSTR_0:def_13_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds Initialize p = p +* (Start-At (0,S));

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be PartState of S;
cluster Initialize p ->  0 -started ;
coherence
 Initialize p is 0 -started ;
end;

theorem Th42: :: MEMSTR_0:42
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC )}
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC )}
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC )}
let p be PartState of S; ::_thesis: dom (Initialize p) = (dom p) \/ {(IC )}
thus  dom (Initialize p) = (dom p) \/ (dom (Start-At (0,S))) by FUNCT_4:def_1
.= (dom p) \/ {(IC )} by FUNCOP_1:13 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:43
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )
let p be PartState of S; ::_thesis: for x being set holds
( not x in dom (Initialize p) or x in dom p or x = IC )
let x be set ; ::_thesis: ( not x in dom (Initialize p) or x in dom p or x = IC )
assume A1: x in dom (Initialize p) ; ::_thesis: ( x in dom p or x = IC )
 dom (Initialize p) = (dom p) \/ {(IC )} by Th42;
then  ( x in dom p or x in {(IC )} ) by A1, XBOOLE_0:def_3;
hence  ( x in dom p or x = IC ) by TARSKI:def_1; ::_thesis: verum
end;

theorem :: MEMSTR_0:44
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being 0 -started PartState of S holds Initialize p = p
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being 0 -started PartState of S holds Initialize p = p
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being 0 -started PartState of S holds Initialize p = p
let p be 0 -started PartState of S; ::_thesis: Initialize p = p
 ( IC in dom p & IC p = 0 ) by Def11;
hence  Initialize p = p by FUNCT_4:85, FUNCT_4:98; ::_thesis: verum
end;

theorem Th45: :: MEMSTR_0:45
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds DataPart (Initialize p) = DataPart p
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds DataPart (Initialize p) = DataPart p
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S holds DataPart (Initialize p) = DataPart p
let p be PartState of S; ::_thesis: DataPart (Initialize p) = DataPart p
thus  DataPart (Initialize p) = (DataPart p) +* (DataPart (Start-At (0,S))) by FUNCT_4:71
.= (DataPart p) +* {} by Th20
.= DataPart p ; ::_thesis: verum
end;

theorem :: MEMSTR_0:46
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S st IC s = 0 holds
Initialize s = s
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S st IC s = 0 holds
Initialize s = s
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S st IC s = 0 holds
Initialize s = s
let s be State of S; ::_thesis: ( IC s = 0 implies Initialize s = s )
assume A1: IC s = 0 ; ::_thesis: Initialize s = s
A2: IC in dom s by Th2;
thus  Initialize s = s by A1, A2, FUNCT_7:109; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let s be State of S;
cluster Initialize s ->  total ;
coherence
 Initialize s is total ;
end;

theorem Th47: :: MEMSTR_0:47
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st Initialize p c= s holds
IC s = 0
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st Initialize p c= s holds
IC s = 0
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S
for p being PartState of S st Initialize p c= s holds
IC s = 0
let s be State of S; ::_thesis: for p being PartState of S st Initialize p c= s holds
IC s = 0
let p be PartState of S; ::_thesis: ( Initialize p c= s implies IC s = 0 )
A1: IC (Initialize p) = 0 by Def11;
A2: IC in dom (Initialize p) by Def11;
assume  Initialize p c= s ; ::_thesis: IC s = 0
hence  IC s = 0 by A1, A2, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th48: :: MEMSTR_0:48
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds IC in dom (Initialize p)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds IC in dom (Initialize p)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S holds IC in dom (Initialize p)
let p be PartState of S; ::_thesis: IC in dom (Initialize p)
A1: dom (Initialize p) = (dom p) \/ {(IC )} by Th42;
 IC in {(IC )} by TARSKI:def_1;
hence  IC in dom (Initialize p) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: MEMSTR_0:49
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S holds IC in dom (p +* (Initialize q))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S holds IC in dom (p +* (Initialize q))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p, q being PartState of S holds IC in dom (p +* (Initialize q))
let p, q be PartState of S; ::_thesis: IC in dom (p +* (Initialize q))
A1: dom (p +* (Initialize q)) = (dom p) \/ (dom (Initialize q)) by FUNCT_4:def_1;
 IC in dom (Initialize q) by Th48;
hence  IC in dom (p +* (Initialize q)) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: MEMSTR_0:50
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S st Initialize p c= q holds
Start-At (0,S) c= q
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S st Initialize p c= q holds
Start-At (0,S) c= q
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p, q being PartState of S st Initialize p c= q holds
Start-At (0,S) c= q
let p, q be PartState of S; ::_thesis: ( Initialize p c= q implies Start-At (0,S) c= q )
 Start-At (0,S) c= Initialize p by FUNCT_4:25;
hence  ( Initialize p c= q implies Start-At (0,S) c= q ) by XBOOLE_1:1; ::_thesis: verum
end;

begin

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be PartState of S;
let k be Nat;
func IncIC (p,k) ->  PartState of S equals :: MEMSTR_0:def 14
p +* (Start-At (((IC p) + k),S));
correctness
coherence
p +* (Start-At (((IC p) + k),S)) is PartState of S;
;
end;

:: deftheorem  defines IncIC MEMSTR_0:def_14_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IncIC (p,k) = p +* (Start-At (((IC p) + k),S));

theorem Th51: :: MEMSTR_0:51
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds DataPart (IncIC (p,k)) = DataPart p
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds DataPart (IncIC (p,k)) = DataPart p
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds DataPart (IncIC (p,k)) = DataPart p
let p be PartState of S; ::_thesis: for k being Nat holds DataPart (IncIC (p,k)) = DataPart p
let k be Nat; ::_thesis: DataPart (IncIC (p,k)) = DataPart p
thus  DataPart (IncIC (p,k)) = (DataPart p) +* (DataPart (Start-At (((IC p) + k),S))) by FUNCT_4:71
.= (DataPart p) +* {} by Th20
.= DataPart p ; ::_thesis: verum
end;

theorem Th52: :: MEMSTR_0:52
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC in dom (IncIC (p,k))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC in dom (IncIC (p,k))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds IC in dom (IncIC (p,k))
let p be PartState of S; ::_thesis: for k being Nat holds IC in dom (IncIC (p,k))
let k be Nat; ::_thesis: IC in dom (IncIC (p,k))
A1: dom (IncIC (p,k)) = (dom p) \/ (dom (Start-At (((IC p) + k),S))) by FUNCT_4:def_1;
 IC in dom (Start-At (((IC p) + k),S)) by Th15;
hence  IC in dom (IncIC (p,k)) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th53: :: MEMSTR_0:53
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC (IncIC (p,k)) = (IC p) + k
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC (IncIC (p,k)) = (IC p) + k
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds IC (IncIC (p,k)) = (IC p) + k
let p be PartState of S; ::_thesis: for k being Nat holds IC (IncIC (p,k)) = (IC p) + k
let k be Nat; ::_thesis: IC (IncIC (p,k)) = (IC p) + k
 dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:13;
then  IC in dom (Start-At (((IC p) + k),S)) by TARSKI:def_1;
hence  IC (IncIC (p,k)) = (Start-At (((IC p) + k),S)) . (IC ) by FUNCT_4:13
.= (IC p) + k by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: MEMSTR_0:54
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for d being data-only PartState of S
for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for d being data-only PartState of S
for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for d being data-only PartState of S
for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let p be PartState of S; ::_thesis: for d being data-only PartState of S
for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let d be data-only PartState of S; ::_thesis: for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let k be Nat; ::_thesis: IncIC ((p +* d),k) = (IncIC (p,k)) +* d
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 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:55
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds Start-At (((IC p) + k),S) c= IncIC (p,k)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds Start-At (((IC p) + k),S) c= IncIC (p,k)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds Start-At (((IC p) + k),S) c= IncIC (p,k)
let p be PartState of S; ::_thesis: for k being Nat holds Start-At (((IC p) + k),S) c= IncIC (p,k)
let k be Nat; ::_thesis: Start-At (((IC p) + k),S) c= IncIC (p,k)
A1: IC (IncIC (p,k)) = (IC p) + k by Th53;
A2: IC in dom (IncIC (p,k)) by Th52;
A3: ( Start-At (((IC p) + k),S) = {[(IC ),((IC p) + k)]} & [(IC ),((IC p) + k)] in IncIC (p,k) ) by A2, A1, FUNCT_1:def_2, FUNCT_4:82;
 for x being set st x in Start-At (((IC p) + k),S) holds
x in IncIC (p,k) by A3, TARSKI:def_1;
hence  Start-At (((IC p) + k),S) c= IncIC (p,k) by TARSKI:def_3; ::_thesis: verum
end;

theorem :: MEMSTR_0:56
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S))
proof
let k be Nat; ::_thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S))
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S st IC in dom p holds
IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S))
let p be PartState of S; ::_thesis: ( IC in dom p implies IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S)) )
A1: dom (Start-At (((IC p) + k),S)) = {(IC )} by FUNCOP_1:13
.= dom (Start-At ((IC p),S)) by FUNCOP_1:13 ;
assume A2: IC in dom p ; ::_thesis: IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S))
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 ; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let s be State of S;
let k be Nat;
cluster IncIC (s,k) ->  total ;
coherence
 IncIC (s,k) is total ;
end;

theorem :: MEMSTR_0:57
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
let p be PartState of S; ::_thesis: for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
let i, j be Nat; ::_thesis: IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
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 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:58
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for j, k being Nat holds IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for j, k being Nat holds IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for j, k being Nat holds IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))
let p be PartState of S; ::_thesis: for j, k being Nat holds IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))
let j, k be Nat; ::_thesis: IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))
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 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:59
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for k being Nat holds (IC (IncIC (s,k))) -' k = IC s
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for k being Nat holds (IC (IncIC (s,k))) -' k = IC s
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S
for k being Nat holds (IC (IncIC (s,k))) -' k = IC s
let s be State of S; ::_thesis: for k being Nat holds (IC (IncIC (s,k))) -' k = IC s
let k be Nat; ::_thesis: (IC (IncIC (s,k))) -' k = IC s
thus (IC (IncIC (s,k))) -' k = ((IC s) + k) -' k by Th53
.= IC s by NAT_D:34 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:60
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S
for k being Nat st IC in dom q holds
IncIC ((p +* q),k) = p +* (IncIC (q,k))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S
for k being Nat st IC in dom q holds
IncIC ((p +* q),k) = p +* (IncIC (q,k))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p, q being PartState of S
for k being Nat st IC in dom q holds
IncIC ((p +* q),k) = p +* (IncIC (q,k))
let p, q be PartState of S; ::_thesis: for k being Nat st IC in dom q holds
IncIC ((p +* q),k) = p +* (IncIC (q,k))
let k be Nat; ::_thesis: ( IC in dom q implies IncIC ((p +* q),k) = p +* (IncIC (q,k)) )
assume  IC in dom q ; ::_thesis: IncIC ((p +* q),k) = p +* (IncIC (q,k))
then  IC (p +* q) = IC q by FUNCT_4:13;
hence  IncIC ((p +* q),k) = p +* (IncIC (q,k)) by FUNCT_4:14; ::_thesis: verum
end;

theorem :: MEMSTR_0:61
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let k be Nat; ::_thesis: for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let p be PartState of S; ::_thesis: for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let s1, s2 be State of S; ::_thesis: ( p c= s1 & IncIC (p,k) c= s2 implies p c= s1 +* (DataPart s2) )
assume that
A1: p c= s1 and
A2: IncIC (p,k) c= s2 ; ::_thesis: p c= s1 +* (DataPart 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 )} \/ (Data-Locations ) by STRUCT_0:4;
A5: now__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_
p_._x_=_s_._x
 Data-Locations = (dom s2) /\ (Data-Locations ) by Th8, XBOOLE_1:28;
then A6: dom (DataPart s2) = Data-Locations by RELAT_1:61;
let x be set ; ::_thesis: ( x in dom p implies p . b1 = s . b1 )
assume A7: x in dom p ; ::_thesis: p . b1 = s . b1
percases ( x in {(IC )} or x in Data-Locations ) by A4, A7, XBOOLE_0:def_3;
supposeA8: x in {(IC )} ; ::_thesis: p . b1 = s . b1
 x = IC 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; ::_thesis: verum
end;
supposeA9: x in Data-Locations ; ::_thesis: p . b1 = s . b1
set DPp = DataPart p;
 x in (dom p) /\ (Data-Locations ) by A9, A7, XBOOLE_0:def_4;
then A10: x in dom (DataPart p) by RELAT_1:61;
A11: DataPart (IncIC (p,k)) = DataPart p by Th51;
 DataPart p c= IncIC (p,k) by A11, RELAT_1:59;
then A12: DataPart p c= s2 by A2, XBOOLE_1:1;
then  dom (DataPart p) c= dom s2 by GRFUNC_1:2;
then  x in (dom s2) /\ (Data-Locations ) by A9, A10, XBOOLE_0:def_4;
then A13: x in dom (DataPart s2) by RELAT_1:61;
 DataPart p c= p by RELAT_1:59;
then A14: (DataPart p) . x = p . x by A10, GRFUNC_1:2;
A15: s2 . x = (DataPart s2) . x by A9, FUNCT_1:49;
 (DataPart p) . x = s2 . x by A10, A12, GRFUNC_1:2;
hence  p . x = s . x by A14, A15, A13, FUNCT_4:13; ::_thesis: verum
end;
end;
end;
 dom p c= dom s by A3, PARTFUN1:def_2;
hence  p c= s1 +* (DataPart s2) by A5, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: MEMSTR_0:62
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Element of NAT holds DataPart p c= IncIC (p,k)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Element of NAT holds DataPart p c= IncIC (p,k)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Element of NAT holds DataPart p c= IncIC (p,k)
let p be PartState of S; ::_thesis: for k being Element of NAT holds DataPart p c= IncIC (p,k)
let k be Element of NAT ; ::_thesis: DataPart p c= IncIC (p,k)
 DataPart (IncIC (p,k)) = DataPart p by Th51;
hence  DataPart p c= IncIC (p,k) by RELAT_1:59; ::_thesis: verum
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be PartState of S;
let k be Nat;
func DecIC (p,k) ->  PartState of S equals :: MEMSTR_0:def 15
p +* (Start-At (((IC p) -' k),S));
correctness
coherence
p +* (Start-At (((IC p) -' k),S)) is PartState of S;
;
end;

:: deftheorem  defines DecIC MEMSTR_0:def_15_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds DecIC (p,k) = p +* (Start-At (((IC p) -' k),S));

theorem :: MEMSTR_0:63
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds DataPart (DecIC (p,k)) = DataPart p
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds DataPart (DecIC (p,k)) = DataPart p
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds DataPart (DecIC (p,k)) = DataPart p
let p be PartState of S; ::_thesis: for k being Nat holds DataPart (DecIC (p,k)) = DataPart p
let k be Nat; ::_thesis: DataPart (DecIC (p,k)) = DataPart p
thus  DataPart (DecIC (p,k)) = (DataPart p) +* (DataPart (Start-At (((IC p) -' k),S))) by FUNCT_4:71
.= (DataPart p) +* {} by Th20
.= DataPart p ; ::_thesis: verum
end;

theorem Th64: :: MEMSTR_0:64
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC in dom (DecIC (p,k))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC in dom (DecIC (p,k))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds IC in dom (DecIC (p,k))
let p be PartState of S; ::_thesis: for k being Nat holds IC in dom (DecIC (p,k))
let k be Nat; ::_thesis: IC in dom (DecIC (p,k))
A1: dom (DecIC (p,k)) = (dom p) \/ (dom (Start-At (((IC p) -' k),S))) by FUNCT_4:def_1;
 IC in dom (Start-At (((IC p) -' k),S)) by Th15;
hence  IC in dom (DecIC (p,k)) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th65: :: MEMSTR_0:65
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC (DecIC (p,k)) = (IC p) -' k
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds IC (DecIC (p,k)) = (IC p) -' k
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds IC (DecIC (p,k)) = (IC p) -' k
let p be PartState of S; ::_thesis: for k being Nat holds IC (DecIC (p,k)) = (IC p) -' k
let k be Nat; ::_thesis: IC (DecIC (p,k)) = (IC p) -' k
 dom (Start-At (((IC p) -' k),S)) = {(IC )} by FUNCOP_1:13;
then  IC in dom (Start-At (((IC p) -' k),S)) by TARSKI:def_1;
hence  IC (DecIC (p,k)) = (Start-At (((IC p) -' k),S)) . (IC ) by FUNCT_4:13
.= (IC p) -' k by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: MEMSTR_0:66
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for d being data-only PartState of S
for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for d being data-only PartState of S
for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for d being data-only PartState of S
for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let p be PartState of S; ::_thesis: for d being data-only PartState of S
for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let d be data-only PartState of S; ::_thesis: for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let k be Nat; ::_thesis: DecIC ((p +* d),k) = (DecIC (p,k)) +* d
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 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:67
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds Start-At (((IC p) -' k),S) c= DecIC (p,k)
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat holds Start-At (((IC p) -' k),S) c= DecIC (p,k)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat holds Start-At (((IC p) -' k),S) c= DecIC (p,k)
let p be PartState of S; ::_thesis: for k being Nat holds Start-At (((IC p) -' k),S) c= DecIC (p,k)
let k be Nat; ::_thesis: Start-At (((IC p) -' k),S) c= DecIC (p,k)
A1: IC (DecIC (p,k)) = (IC p) -' k by Th65;
A2: IC in dom (DecIC (p,k)) by Th64;
A3: ( Start-At (((IC p) -' k),S) = {[(IC ),((IC p) -' k)]} & [(IC ),((IC p) -' k)] in DecIC (p,k) ) by A2, A1, FUNCT_1:def_2, FUNCT_4:82;
 for x being set st x in Start-At (((IC p) -' k),S) holds
x in DecIC (p,k) by A3, TARSKI:def_1;
hence  Start-At (((IC p) -' k),S) c= DecIC (p,k) by TARSKI:def_3; ::_thesis: verum
end;

theorem :: MEMSTR_0:68
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat st IC in dom p holds
DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat st IC in dom p holds
DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat st IC in dom p holds
DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S))
let p be PartState of S; ::_thesis: for k being Nat st IC in dom p holds
DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S))
let k be Nat; ::_thesis: ( IC in dom p implies DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S)) )
A1: dom (Start-At (((IC p) -' k),S)) = {(IC )} by FUNCOP_1:13
.= dom (Start-At ((IC p),S)) by FUNCOP_1:13 ;
assume A2: IC in dom p ; ::_thesis: DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S))
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 ; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let s be State of S;
let k be Nat;
cluster DecIC (s,k) ->  total ;
coherence
 DecIC (s,k) is total ;
end;

theorem :: MEMSTR_0:69
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
let p be PartState of S; ::_thesis: for i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
let i, j be Nat; ::_thesis: DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
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 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:70
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for j, k being Nat holds DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for j, k being Nat holds DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for j, k being Nat holds DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))
let p be PartState of S; ::_thesis: for j, k being Nat holds DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))
let j, k be Nat; ::_thesis: DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))
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 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:71
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for k being Nat st k <= IC s holds
(IC (DecIC (s,k))) + k = IC s
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for k being Nat st k <= IC s holds
(IC (DecIC (s,k))) + k = IC s
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S
for k being Nat st k <= IC s holds
(IC (DecIC (s,k))) + k = IC s
let s be State of S; ::_thesis: for k being Nat st k <= IC s holds
(IC (DecIC (s,k))) + k = IC s
let k be Nat; ::_thesis: ( k <= IC s implies (IC (DecIC (s,k))) + k = IC s )
assume A1: k <= IC s ; ::_thesis: (IC (DecIC (s,k))) + k = IC s
thus (IC (DecIC (s,k))) + k = ((IC s) -' k) + k by Th65
.= IC s by A1, XREAL_1:235 ; ::_thesis: verum
end;

theorem Th72: :: MEMSTR_0:72
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* q),k) = p +* (DecIC (q,k))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* q),k) = p +* (DecIC (q,k))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* q),k) = p +* (DecIC (q,k))
let p, q be PartState of S; ::_thesis: for k being Nat st IC in dom q holds
DecIC ((p +* q),k) = p +* (DecIC (q,k))
let k be Nat; ::_thesis: ( IC in dom q implies DecIC ((p +* q),k) = p +* (DecIC (q,k)) )
assume  IC in dom q ; ::_thesis: DecIC ((p +* q),k) = p +* (DecIC (q,k))
then  IC (p +* q) = IC q by FUNCT_4:13;
hence  DecIC ((p +* q),k) = p +* (DecIC (q,k)) by FUNCT_4:14; ::_thesis: verum
end;

theorem Th73: :: MEMSTR_0:73
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S
for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p being PartState of S
for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let p be PartState of S; ::_thesis: for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let k be Nat; ::_thesis: ( IC in dom p implies DecIC ((IncIC (p,k)),k) = p )
assume A1: IC in dom p ; ::_thesis: DecIC ((IncIC (p,k)),k) = 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 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:74
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* (IncIC (q,k))),k) = p +* q
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* (IncIC (q,k))),k) = p +* q
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for p, q being PartState of S
for k being Nat st IC in dom q holds
DecIC ((p +* (IncIC (q,k))),k) = p +* q
let p, q be PartState of S; ::_thesis: for k being Nat st IC in dom q holds
DecIC ((p +* (IncIC (q,k))),k) = p +* q
let k be Nat; ::_thesis: ( IC in dom q implies DecIC ((p +* (IncIC (q,k))),k) = p +* q )
assume A1: IC in dom q ; ::_thesis: DecIC ((p +* (IncIC (q,k))),k) = p +* q
 IC 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 ;
::_thesis: verum
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let k be Nat;
let p be k -started PartState of S;
cluster DecIC (p,k) ->  0 -started ;
coherence
 DecIC (p,k) is 0 -started
proof
thus  IC in dom (DecIC (p,k)) by Th64; :: according to MEMSTR_0:def_11 ::_thesis: IC (DecIC (p,k)) = 0
thus  IC (DecIC (p,k)) = (IC p) -' k by Th65
.= k -' k by Def11
.= 0 by XREAL_1:232 ; ::_thesis: verum
end;
end;

begin

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
cluster Start-At (l,S) ->  finite ;
correctness
coherence
Start-At (l,S) is finite ;
;
end;

definition
let N be with_zero set ;
let S be Mem-Struct over N;
mode FinPartState of S is finite PartState of S;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let l be Nat;
cluster Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V93() l -started for set ;
existence
 ex b1 being FinPartState of S st b1 is l -started
proof
take  Start-At (l,S) ; ::_thesis: Start-At (l,S) is l -started
thus  Start-At (l,S) is l -started ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be Mem-Struct over N;
let p be FinPartState of S;
cluster DataPart p ->  finite ;
coherence
 DataPart p is finite ;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be FinPartState of S;
cluster Initialize p ->  finite ;
coherence
 Initialize p is finite ;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be FinPartState of S;
let k be Nat;
cluster IncIC (p,k) ->  finite ;
coherence
 IncIC (p,k) is finite ;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let p be FinPartState of S;
let k be Nat;
cluster DecIC (p,k) ->  finite ;
coherence
 DecIC (p,k) is finite ;
end;

definition
let N be with_zero set ;
let S be with_non-empty_values Mem-Struct over N;
func FinPartSt S ->  Subset of (sproduct (the_Values_of S)) equals :: MEMSTR_0:def 16
 {  p where p is Element of sproduct (the_Values_of S) : p is finite  }  ;
coherence
  {  p where p is Element of sproduct (the_Values_of S) : p is finite  }  is Subset of (sproduct (the_Values_of S))
proof
defpred S1[ set ] means $1 is finite ;
  {  p where p is Element of sproduct (the_Values_of S) : S1[p]  }  c= sproduct (the_Values_of S) from FRAENKEL:sch_10();
hence   {  p where p is Element of sproduct (the_Values_of S) : p is finite  }  is Subset of (sproduct (the_Values_of S)) ; ::_thesis: verum
end;
end;

:: deftheorem  defines FinPartSt MEMSTR_0:def_16_:_
 for N being with_zero set
for S being with_non-empty_values Mem-Struct over N holds FinPartSt S =  {  p where p is Element of sproduct (the_Values_of S) : p is finite  }  ;

theorem Th75: :: MEMSTR_0:75
for N being with_zero set
for S being with_non-empty_values Mem-Struct over N
for p being FinPartState of S holds p in FinPartSt S
proof
let N be with_zero set ; ::_thesis: for S being with_non-empty_values Mem-Struct over N
for p being FinPartState of S holds p in FinPartSt S
let S be with_non-empty_values Mem-Struct over N; ::_thesis: for p being FinPartState of S holds p in FinPartSt S
let p be FinPartState of S; ::_thesis: p in FinPartSt S
 p in sproduct (the_Values_of S) by CARD_3:103;
hence  p in FinPartSt S ; ::_thesis: verum
end;

registration
let N be with_zero set ;
let S be with_non-empty_values Mem-Struct over N;
cluster FinPartSt S ->  non empty ;
coherence
 not FinPartSt S is empty by Th75;
end;

theorem :: MEMSTR_0:76
for N being with_zero set
for S being with_non-empty_values Mem-Struct over N
for p being Element of FinPartSt S holds p is FinPartState of S
proof
let N be with_zero set ; ::_thesis: for S being with_non-empty_values Mem-Struct over N
for p being Element of FinPartSt S holds p is FinPartState of S
let S be with_non-empty_values Mem-Struct over N; ::_thesis: for p being Element of FinPartSt S holds p is FinPartState of S
let p be Element of FinPartSt S; ::_thesis: p is FinPartState of S
 p in FinPartSt S ;
then  ex q being Element of sproduct (the_Values_of S) st
( q = p & q is finite ) ;
hence  p is FinPartState of S ; ::_thesis: verum
end;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let IT be PartFunc of (FinPartSt S),(FinPartSt S);
attrIT is data-only  means :: MEMSTR_0:def 17
 for p being PartState of S st p in dom IT holds
( p is data-only & ( for q being PartState of S st q = IT . p holds
q is data-only ) );
end;

:: deftheorem  defines data-only MEMSTR_0:def_17_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for IT being PartFunc of (FinPartSt S),(FinPartSt S) holds
( IT is data-only iff for p being PartState of S st p in dom IT holds
( p is data-only & ( for q being PartState of S st q = IT . p holds
q is data-only ) ) );

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
cluster Relation-like FinPartSt S -defined FinPartSt S -valued Function-like Function-yielding V35() data-only for Element of bool [:(FinPartSt S),(FinPartSt S):];
existence
 ex b1 being PartFunc of (FinPartSt S),(FinPartSt S) st b1 is data-only
proof
reconsider f = {} as PartFunc of (FinPartSt S),(FinPartSt S) by RELSET_1:12;
take  f ; ::_thesis: f is data-only
let p be PartState of S; :: according to MEMSTR_0:def_17 ::_thesis: ( p in dom f implies ( p is data-only & ( for q being PartState of S st q = f . p holds
q is data-only ) ) )
thus  ( p in dom f implies ( p is data-only & ( for q being PartState of S st q = f . p holds
q is data-only ) ) ) ; ::_thesis: verum
end;
end;

begin

theorem :: MEMSTR_0:77
for N being with_zero set
for A being non empty with_non-empty_values Mem-Struct over N
for s being State of A
for o being Object of A holds s . o in Values o
proof
let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values Mem-Struct over N
for s being State of A
for o being Object of A holds s . o in Values o
let A be non empty with_non-empty_values Mem-Struct over N; ::_thesis: for s being State of A
for o being Object of A holds s . o in Values o
let s be State of A; ::_thesis: for o being Object of A holds s . o in Values o
let o be Object of A; ::_thesis: s . o in Values o
 dom s = the carrier of A by PARTFUN1:def_2;
hence  s . o in Values o by FUNCT_1:def_14; ::_thesis: verum
end;

theorem Th78: :: MEMSTR_0:78
for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
s1 = s2
proof
let N be with_zero set ; ::_thesis: for A being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
s1 = s2
let A be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
s1 = s2
set D = Data-Locations ;
let s1, s2 be State of A; ::_thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: DataPart s1 = DataPart s2 ; ::_thesis: s1 = s2
A3: dom s2 = {(IC )} \/ (Data-Locations ) by Th13;
A4: dom s1 = {(IC )} \/ (Data-Locations ) by Th13;
then  s1 | {(IC )} = s2 | {(IC )} by A1, A3, GRFUNC_1:29;
then  s1 | ({(IC )} \/ (Data-Locations )) = s2 | ({(IC )} \/ (Data-Locations )) by A2, RELAT_1:150;
then  s1 | ({(IC )} \/ (Data-Locations )) = s2 | ({(IC )} \/ (Data-Locations )) ;
hence s1 = s2 | (dom s2) by A4, A3, RELAT_1:68
.= s2 ;
::_thesis: verum
end;

theorem :: MEMSTR_0:79
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for l being Element of NAT holds DataPart s = DataPart (s +* (Start-At (l,S)))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for l being Element of NAT holds DataPart s = DataPart (s +* (Start-At (l,S)))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s being State of S
for l being Element of NAT holds DataPart s = DataPart (s +* (Start-At (l,S)))
let s be State of S; ::_thesis: for l being Element of NAT holds DataPart s = DataPart (s +* (Start-At (l,S)))
let l be Element of NAT ; ::_thesis: DataPart s = DataPart (s +* (Start-At (l,S)))
thus  DataPart s = (DataPart s) +* {}
.= (DataPart s) +* (DataPart (Start-At (l,S))) by Th20
.= DataPart (s +* (Start-At (l,S))) by FUNCT_4:71 ; ::_thesis: verum
end;

theorem :: MEMSTR_0:80
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of S st DataPart s1 = DataPart s2 holds
Initialize s1 = Initialize s2
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of S st DataPart s1 = DataPart s2 holds
Initialize s1 = Initialize s2
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; ::_thesis: for s1, s2 being State of S st DataPart s1 = DataPart s2 holds
Initialize s1 = Initialize s2
let s1, s2 be State of S; ::_thesis: ( DataPart s1 = DataPart s2 implies Initialize s1 = Initialize s2 )
assume A1: DataPart s1 = DataPart s2 ; ::_thesis: Initialize s1 = Initialize s2
set S1 = Initialize s1;
set S2 = Initialize s2;
A2: ( IC (Initialize s1) = 0 & IC (Initialize s2) = 0 ) by Th47;
DataPart (Initialize s1) = DataPart s1 by Th45
.= DataPart (Initialize s2) by A1, Th45 ;
hence  Initialize s1 = Initialize s2 by A2, Th78; ::_thesis: verum
end;

theorem :: MEMSTR_0:81
for N being with_zero set holds the_Values_of (Trivial-Mem N) = 0 .--> NAT by Lm1;

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;
let f be Function of (product (the_Values_of S)),NAT;
attrf is on_data_only  means :: MEMSTR_0:def 18
 for s1, s2 being State of S st DataPart s1 = DataPart s2 holds
f . s1 = f . s2;
end;

:: deftheorem  defines on_data_only MEMSTR_0:def_18_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for f being Function of (product (the_Values_of S)),NAT holds
( f is on_data_only iff for s1, s2 being State of S st DataPart s1 = DataPart s2 holds
f . s1 = f . s2 );