:: Memory Structures
:: by Andrzej Trybulec
::
:: Received April 28, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


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;

:: wymaganie zeby N byl 'with_zero' jest troche na zapas
:: na razie wykorzystujemy tylko rejestracje, ze 'with_zero'
:: musi byc 'non empty' i w definicji Trivial-Mem N
:: ale tutaj mozna sie tego pozbyc, biorac zamiast 0
:: the Element of N i potrzebujemy tylko to, ze N jest niepusty
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 )
proofend;
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
proofend;
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
proofend;
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;

:: Jest potrzeba zagwarantowania, ze
:: the_Values_of S is non-empty
:: to bylo wczsniej obsluzone, ze stary N byl
:: with_non-empty_elements
:: teraz jest to wlasnosc Mem-Str
:: sa tutaj rozne warianty, najprosciej jednak napisac co wymgamy:
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
proofend;
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
proofend;
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;

:: Jezeli dodamy wartosci, to pewnie nie unikniemy zdefiniowania
:: funktora, ktory odpowiada staremu Object-Kind
:: np. the_Object-Kind_of, lub the_Values_of
:: i wtedy podmiana nie powinna byc zbyt skomplikowana.
:: Poza tym trzeba bedzie zmienic komputery, dodajac pole ValuesF
:: wykorzystac mozna atrybut with_zero, ale trzeba wprowadzic nowy:
:: (the ValuesF of S).0 = NAT
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
proofend;

registration
let N be with_zero set ;
cluster Trivial-Mem N ->  strict IC-Ins-separated ;
coherence
 Trivial-Mem N is IC-Ins-separated
proofend;
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 )
proofend;
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
proofend;
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
proofend;

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
proofend;
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
proofend;

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

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

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

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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

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

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
proofend;

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

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 )}
proofend;

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

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)) = {}
proofend;

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

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

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

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

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

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

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
proofend;

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

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
proofend;
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
proofend;

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

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 )})
proofend;

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
proofend;

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

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
proofend;

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
proofend;

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
proofend;

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

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))
proofend;
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 )}
proofend;

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

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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

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

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
proofend;

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
proofend;

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

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
proofend;

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
proofend;

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

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

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

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

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
proofend;

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

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

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

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
proofend;

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

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
proofend;

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
proofend;

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

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

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

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

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
proofend;

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

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
proofend;

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
proofend;

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

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
proofend;

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 &amp; ( 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 &amp; ( 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
proofend;
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
proofend;

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 &amp; DataPart s1 = DataPart s2 holds
s1 = s2
proofend;

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

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
proofend;

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

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