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


definition
let N be set ;
attr c2 is strict ;
struct Mem-Struct over N -> ZeroStr ;
aggr Mem-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 )
proof 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 by Def1;
end;

registration
let N be with_zero set ;
cluster 1 -element for Mem-Struct over N;
existence
ex b1 being Mem-Struct over N st b1 is 1 -element
proof 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 ;
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;
attr S 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 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 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;

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;
attr IT 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 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 end;
end;

registration
let N be with_zero set ;
cluster non empty V116() 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 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 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 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;
cluster la .--> a -> the_Values_of S -compatible ;
coherence
la .--> a is the_Values_of S -compatible
proof 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 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 ) ;
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;
attr p 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 by RELAT_1:38, XBOOLE_1:65;
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 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 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 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 by Th3, ZFMISC_1:50;
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 ) by RELAT_1:def 18, XBOOLE_1:86, XBOOLE_1:106;

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 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 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 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 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 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 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 Nat;
let s be State of S;
cluster s +* ((IC ),l) -> the_Values_of S -compatible ;
coherence
s +* ((IC ),l) is the_Values_of S -compatible
proof 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;
func Start-At (l,S) -> PartState of S equals :: MEMSTR_0:def 10
(IC ) .--> l;
correctness
coherence
(IC ) .--> l is PartState of S;
proof 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;
attr p 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 ) by TARSKI:def 1, FUNCOP_1:72;
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)) by TARSKI:def 1;

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 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 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;
cluster p +* q -> l -started ;
coherence
p +* q is l -started
proof 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 ) by Th2;
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 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 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 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 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 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 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 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 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 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 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 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 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;
cluster p +* d -> k -started ;
coherence
p +* d is k -started
proof 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 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 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 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 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 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 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 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 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 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 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 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)) ;
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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Nat holds DataPart p c= IncIC (p,k)
proof 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 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 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 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 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 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 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 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 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 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 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 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 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 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;
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 l -started for set ;
existence
ex b1 being FinPartState of S st b1 is l -started
proof 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 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 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 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);
attr IT 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 V38() data-only for Element of K10(K11((FinPartSt S),(FinPartSt S)));
existence
ex b1 being PartFunc of (FinPartSt S),(FinPartSt S) st b1 is data-only
proof end;
end;

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 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 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 Nat holds DataPart s = DataPart (s +* (Start-At (l,S)))
proof 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 end;

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;
attr f 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 );