begin
:: deftheorem Def1 defines Trivial-Mem MEMSTR_0:def 1 :
for N being set
for b2 being strict Mem-Struct of N holds
( b2 = Trivial-Mem N iff ( the carrier of b2 = {0} & the ZeroF of b2 = 0 & the Object-Kind of b2 = 0 .--> NAT ) );
begin
:: deftheorem defines ObjectKind MEMSTR_0:def 2 :
for N being set
for S being non empty Mem-Struct of N
for o being Object of S holds ObjectKind o = the Object-Kind of S . o;
:: deftheorem Def6 defines IC-Ins-separated MEMSTR_0:def 3 :
for N being set
for IT being non empty Mem-Struct of N holds
( IT is IC-Ins-separated iff ObjectKind (IC ) = NAT );
:: deftheorem defines IC MEMSTR_0:def 4 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of N
for p being PartState of S holds IC p = p . (IC );
theorem
theorem Lm6:
:: deftheorem defines DataPart MEMSTR_0:def 5 :
for N being set
for S being Mem-Struct of N
for p being PartState of S holds DataPart p = p | (Data-Locations );
:: deftheorem Def23 defines data-only MEMSTR_0:def 6 :
for N being set
for S being Mem-Struct of N
for p being PartState of S holds
( p is data-only iff dom p misses {(IC )} );
theorem Th11:
theorem
theorem
theorem Th31:
theorem
theorem Th49:
theorem Th50:
theorem Th57:
theorem Th58:
theorem
theorem Th13:
theorem
begin
:: deftheorem defines Start-At MEMSTR_0:def 7 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of N
for l being Nat holds Start-At (l,S) = (IC ) .--> l;
:: deftheorem Def16 defines -started MEMSTR_0:def 8 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of N
for l being Nat
for p being PartState of S holds
( p is l -started iff ( IC in dom p & IC p = l ) );
theorem Lm52:
theorem Lm142:
:: deftheorem defines -started MEMSTR_0:def 9 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of N
for l being Nat
for s being State of S holds
( s is l -started iff IC s = l );
theorem
theorem Th10:
theorem Th18:
theorem Th30:
theorem
theorem
theorem Th59:
theorem Th70:
theorem
theorem Th74:
theorem Th141:
theorem
theorem Th151:
theorem Th164:
theorem
theorem
theorem LmAA:
theorem
theorem
theorem Th199:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem defines Initialize MEMSTR_0:def 10 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of N
for p being PartState of S holds Initialize p = p +* (Start-At (0,S));
theorem Th76:
theorem
theorem
theorem Th45:
theorem
theorem Th47:
theorem Th225:
theorem
theorem
begin
:: deftheorem defines IncIC MEMSTR_0:def 11 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of N
for p being PartState of S
for k being Nat holds IncIC (p,k) = p +* (Start-At (((IC p) + k),S));
theorem Th48:
theorem Th53:
theorem Th54:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines DecIC MEMSTR_0:def 12 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of N
for p being PartState of S
for k being Nat holds DecIC (p,k) = p +* (Start-At (((IC p) -' k),S));
theorem
theorem Th187:
theorem Th188:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th198:
theorem Th201:
theorem
begin
:: deftheorem defines FinPartSt MEMSTR_0:def 13 :
for N being set
for S being Mem-Struct of N holds FinPartSt S = { p where p is Element of sproduct the Object-Kind of S : p is finite } ;
theorem Lm5:
theorem
:: deftheorem defines data-only MEMSTR_0:def 14 :
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated Mem-Struct of 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 ) ) );
begin
theorem
theorem Th78:
theorem
theorem