:: 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 );