:: Memory Structures
::  by Andrzej Trybulec
::
:: Received April 28, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, CARD_1,
      FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, CAT_1, FSM_1, FINSET_1, NAT_1,
      ARYTM_1, PARTFUN1, AMI_1, ARYTM_3, COMPOS_1, SCMFSA6C, XXREAL_0,
      SUPINF_2, MEMSTR_0, PBOOLE, GOBRD13, QUANTAL1, SCMFSA9A;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, PBOOLE, FUNCT_7,
      CARD_1, CARD_3, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, NUMBERS,
      INT_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, AFINSQ_1, FINSEQ_1, FUNCT_2,
      DOMAIN_1, VALUED_0, VALUED_1, STRUCT_0, XXREAL_0, MEASURE6;
 constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7,
      PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
      FUNCT_4, FINSET_1, XREAL_0, CARD_3, STRUCT_0, RELSET_1, PBOOLE, NAT_1,
      CARD_1, MEASURE6;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Terminology

reserve x,N for set,
        k for Nat;

definition let N;
  struct (ZeroStr) Mem-Struct over N (# carrier -> set,
    ZeroF -> Element of the carrier,
    Object-Kind -> Function of the carrier, N,
    ValuesF -> ManySortedSet of N
     #);
end;

reserve N for with_zero set;

:: 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;
  func Trivial-Mem N -> strict Mem-Struct over N means
:: 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;
end;

registration let N;
  cluster Trivial-Mem N -> 1-element;
end;

registration let N;
  cluster 1-element for Mem-Struct over N;
end;

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

registration
 :: gdzie to ma byc, dlaczego nie dziala SETFAM_1
 cluster with_zero -> non empty for set;
end;

definition let N;
  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);
end;

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

registration let N;
 cluster Trivial-Mem N ->with_non-empty_values;
end;

registration let N;
 cluster with_non-empty_values for Mem-Struct over N;
end;

registration let N;
  let S be with_non-empty_values Mem-Struct over N;
 cluster the_Values_of S -> non-empty;
end;

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

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

begin :: the Object Kind

definition let N;
  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;
end;

definition let N;
  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;
end;

:: 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;
  let IT be non empty Mem-Struct over N;
  attr IT is IC-Ins-separated means
:: MEMSTR_0:def 6
 Values IC IT = NAT;
end;

registration let N;
  cluster Trivial-Mem N -> IC-Ins-separated;
end;

registration let N;
  cluster IC-Ins-separated with_non-empty_values strict
    for 1-element Mem-Struct over N;
end;

definition
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
  let p be PartState of S;
  func IC p -> Element of NAT equals
:: MEMSTR_0:def 7
  p.IC S;
end;

theorem :: MEMSTR_0:1
 for S being IC-Ins-separated 1-element with_non-empty_values Mem-Struct over N
  for s1, s2 being State of S st IC s1 = IC s2 holds s1= s2;

registration
  let N;
  let S be non empty with_non-empty_values Mem-Struct over N,
      o be Object of S;
  cluster Values o -> non empty;
end;

registration
  let N;
  let S be IC-Ins-separated non empty
       with_non-empty_values 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;
  let lb be Object of S;
  let b be Element of Values lb;
  cluster (la,lb) --> (a,b) -> (the_Values_of S)-compatible;
end;

theorem :: MEMSTR_0:2
  for S being non empty with_non-empty_values Mem-Struct over N
  for s being State of S holds IC S in dom s;

reserve S for IC-Ins-separated non empty with_non-empty_values
     Mem-Struct over N;

definition
  let N;
  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 S;
  projectivity;
end;

definition
  let N; let S be Mem-Struct over N;
  let p be PartState of S;
  attr p is data-only means
:: MEMSTR_0:def 9

  dom p misses {IC S};
end;

registration
  let N; let S be Mem-Struct over N;
  cluster empty -> data-only for PartState of S;
end;

registration
  let N; let S be Mem-Struct over N;
  cluster empty for PartState of S;
end;

theorem :: MEMSTR_0:3
  for N for S being Mem-Struct over N
  for p being PartState of S holds not IC S in dom DataPart p;

theorem :: MEMSTR_0:4
  for N for S being Mem-Struct over N for p being
  PartState of S holds {IC S} misses dom DataPart p;

theorem :: MEMSTR_0:5
  for p being data-only PartState of S, q being PartState of S
  holds p c= q iff p c= DataPart q;

registration
  let N;
  let S be Mem-Struct over N;
  let p be PartState of S;
  cluster DataPart p -> data-only;
end;

theorem :: MEMSTR_0:6
  for S being Mem-Struct over N, p being PartState
  of S holds p is data-only iff dom p c= Data-Locations S;

theorem :: MEMSTR_0:7
  for S being Mem-Struct over N, p being data-only PartState of S
   holds DataPart p = p;

reserve s for State of S;

theorem :: MEMSTR_0:8
  Data-Locations S c= dom s;

theorem :: MEMSTR_0:9
  dom DataPart s = Data-Locations S;

theorem :: MEMSTR_0:10
  for d being data-only PartState of S holds not IC S in dom d;

theorem :: MEMSTR_0:11
  for p being PartState of S, d being data-only PartState of S
  holds IC(p+*d) = IC p;

reserve p for PartState of S;

theorem :: MEMSTR_0:12
  for p being PartState of S holds DataPart p c=  p;

theorem :: MEMSTR_0:13
 dom s = {IC S} \/ Data-Locations S;

theorem :: MEMSTR_0:14
 dom  p /\ Data-Locations S = dom DataPart p;

registration let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat, s be State of S;
  cluster s+*(IC S,l) -> (the_Values_of S)-compatible;
end;

begin :: The value of the Instruction Counter

definition
  let N;
  let S be IC-Ins-separated non empty
    with_non-empty_values Mem-Struct over N;
  let l be Nat;
  func Start-At(l,S) -> PartState of S equals
:: MEMSTR_0:def 10
   IC S .--> l;
end;

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

registration
 let N;
 let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
     l be Nat;
  cluster Start-At(l,S) -> l-started non empty;
end;

theorem :: MEMSTR_0:15
 for l being Nat holds IC S in dom Start-At(l,S);

theorem :: MEMSTR_0:16
 for n being Nat
 holds IC(p +* Start-At( n,S)) =  n;

registration
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  cluster l-started for State of S;
end;

registration
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat,
      p being PartState of S,
      q be l-started PartState of S;
  cluster p +* q -> l-started;
end;

definition
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  let s be State of S;
  redefine attr s is l-started means
:: MEMSTR_0:def 12
  IC s = l;
end;

theorem :: MEMSTR_0:17
  for S being IC-Ins-separated non empty with_non-empty_values
               Mem-Struct over N,
      l being Nat,
      p being l-started PartState of S
  for s being PartState of S st p c= s holds s is l-started;

theorem :: MEMSTR_0:18
  for s being State of S holds Start-At(IC s,S) = s | {IC S};

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

theorem :: MEMSTR_0:20
 for S be IC-Ins-separated non empty
 with_non-empty_values Mem-Struct over N, l be Nat
  holds DataPart Start-At(l,S) = {};

theorem :: MEMSTR_0:21
  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);

theorem :: MEMSTR_0:22
  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);

theorem :: MEMSTR_0:23
  for d being data-only PartState of S, k being Nat
  holds d tolerates Start-At(k,S);

theorem :: MEMSTR_0:24
 for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
 for p being PartState of S st IC S in dom p
  holds dom  p = {IC S} \/ dom DataPart p;

theorem :: MEMSTR_0:25
 for S being IC-Ins-separated non empty with_non-empty_values
       Mem-Struct over N
 for s being State of S
  holds dom  s = {IC S} \/ dom DataPart s;

theorem :: MEMSTR_0:26
 for p being PartState of S st IC S in dom p
  holds p = DataPart p +* Start-At (IC p,S);

theorem :: MEMSTR_0:27
  IC S in dom (p +* Start-At( k,S));

theorem :: MEMSTR_0:28
  p +* Start-At( k,S) c= s implies IC s =  k;

theorem :: MEMSTR_0:29
  for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat
  for p be PartState of S
  holds p is l-started iff Start-At(l,S) c= p;

registration let N,S; let k be Nat;
 let p be k-started PartState of S, d be data-only PartState of S;
 cluster p +* d -> k-started;
end;

theorem :: MEMSTR_0:30
  Start-At(IC s,S) c= s;

theorem :: MEMSTR_0:31
 for s being State of S
  holds s +* Start-At(IC s,S) = s;

theorem :: MEMSTR_0:32
 dom  p c= {IC S} \/ dom DataPart p;

theorem :: MEMSTR_0:33
 for S being IC-Ins-separated non empty with_non-empty_values
         Mem-Struct over N
 for s be State of S holds s = s|(Data-Locations S \/ {IC S});

theorem :: MEMSTR_0:34
 for S being IC-Ins-separated non empty with_non-empty_values
        Mem-Struct over N
 for s1,s2 be State of S
  st s1|(Data-Locations S \/ {IC S}) = s2|(Data-Locations S \/ {IC S})
 holds s1 =  s2;

theorem :: MEMSTR_0:35
 IC S in dom p implies  p = Start-At(IC p,S) +* DataPart p;

theorem :: MEMSTR_0:36
 for p being PartState of S, k,l being Nat
  holds p +* Start-At(k,S) +* Start-At(l,S)  = p +* Start-At(l,S);

theorem :: MEMSTR_0:37
 for p being PartState of S st IC S in dom p
  holds p +* Start-At(IC p,S) = p;

theorem :: MEMSTR_0:38
  p +* Start-At(k,S) c= s implies IC s = k;

theorem :: MEMSTR_0:39
 for p being PartState of S holds Start-At(0,S) c= p implies IC p = 0;

theorem :: MEMSTR_0:40
 for p being PartState of S st Start-At(k,S) c= p holds IC p = k;

registration let N;
 let S be IC-Ins-separated non empty
 with_non-empty_values Mem-Struct over N;
 cluster non empty for PartState of S;
end;

theorem :: MEMSTR_0:41
 for S being IC-Ins-separated non empty with_non-empty_values
    Mem-Struct over N
 for p being non empty PartState of S
 holds dom p meets {IC S} \/ Data-Locations S;

begin :: Initialize

definition let N;
  let S be IC-Ins-separated non empty
  with_non-empty_values 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);
  projectivity;
end;

registration let N,S;
  let p be PartState of S;
 cluster Initialize p -> 0-started;
end;

theorem :: MEMSTR_0:42
  for S being IC-Ins-separated non empty
  with_non-empty_values Mem-Struct over N,
      p being PartState of S
  holds dom Initialize p = dom p \/ {IC S};

theorem :: MEMSTR_0:43
  for x being set st x in dom Initialize p holds x in dom p or x = IC S;

theorem :: MEMSTR_0:44
 for p being 0-started PartState of S
  holds Initialize p = p;

theorem :: MEMSTR_0:45
 for p being PartState of S
  holds DataPart Initialize p = DataPart p;

theorem :: MEMSTR_0:46
 for s being State of S st IC s =  0 holds Initialize s = s;

registration let N,S;
  let s be State of S;
  cluster Initialize s -> total;
end;

theorem :: MEMSTR_0:47
 for p being PartState of S
 holds Initialize p c= s implies IC s = 0;

theorem :: MEMSTR_0:48
 for p being PartState of S holds IC S in dom Initialize p;

theorem :: MEMSTR_0:49
 for p,q being PartState of S holds IC S in dom(p +* Initialize q);

theorem :: MEMSTR_0:50
 for S being IC-Ins-separated non empty
 with_non-empty_values Mem-Struct over N
 for p,q being PartState of S
 holds Initialize p c= q implies Start-At(0,S) c= q;

begin :: Increment & Decrement, of the Instruction Counter

definition let N,S;
 let p be PartState of S, k be Nat;
  func IncIC(p,k) -> PartState of S equals
:: MEMSTR_0:def 14
  p +* Start-At(IC p+k,S);
end;

theorem :: MEMSTR_0:51
  for p being PartState of S, k being Nat
  holds DataPart IncIC(p,k) = DataPart p;

theorem :: MEMSTR_0:52
 for p being PartState of S, k being Nat holds IC S in dom IncIC(p,k);

theorem :: MEMSTR_0:53
  for p being PartState of S, k being Nat
   holds IC IncIC (p,k) = IC p + k;

theorem :: MEMSTR_0:54
  for d being data-only PartState of S, k being Nat
  holds IncIC(p+*d,k) = IncIC(p,k) +* d;

theorem :: MEMSTR_0:55
  for p being PartState of S, k being Nat holds
  Start-At(IC p+k,S) c= IncIC (p,k);

theorem :: MEMSTR_0:56
 for p being PartState of S st IC S in dom p
  holds IncIC( p,k) = DataPart p +* Start-At ((IC p) +k,S);

registration
  let N,S;
  let s be State of S, k be Nat;
  cluster IncIC(s,k) -> total;
end;

theorem :: MEMSTR_0:57
 for p being PartState of S, i,j being Nat
 holds IncIC(IncIC(p,i),j) = IncIC(p,i+j);

theorem :: MEMSTR_0:58
 for p being PartState of S, j,k being Nat
 holds IncIC(p +* Start-At(j,S),k) = p +* Start-At(j+k,S);

theorem :: MEMSTR_0:59
 for k being Nat
 holds IC IncIC(s,k) -' k = IC s;

theorem :: MEMSTR_0:60
 for p,q being PartState of S, k being Nat st IC S in dom q
  holds IncIC(p+*q,k) = p +* IncIC(q,k);

theorem :: MEMSTR_0:61
 for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
  for k being Nat, p being PartState of S,
      s1, s2 being State of S st p c= s1 & IncIC(p,k) c= s2
   holds p c= s1 +* DataPart s2;

theorem :: MEMSTR_0:62
 for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
 for p being PartState of S, k being Nat
 holds DataPart p c= IncIC(p,k);

definition let N,S;
  let p be PartState of S, k be Nat;
  func DecIC(p,k) -> PartState of S equals
:: MEMSTR_0:def 15
  p +* Start-At(IC p-'k,S);
end;

theorem :: MEMSTR_0:63
  for p being PartState of S, k being Nat
  holds DataPart DecIC(p,k) = DataPart p;

theorem :: MEMSTR_0:64
 for k being Nat holds IC S in dom DecIC(p,k);

theorem :: MEMSTR_0:65
  for p being PartState of S, k being Nat
   holds IC DecIC (p,k) = IC p -' k;

theorem :: MEMSTR_0:66
  for p being PartState of S,
   d being data-only PartState of S, k being Nat
  holds DecIC(p+*d,k) = DecIC(p,k) +* d;

theorem :: MEMSTR_0:67
  for p being PartState of S,k being Nat holds
  Start-At(IC p-'k,S) c= DecIC (p,k);

theorem :: MEMSTR_0:68
 for p being PartState of S, k being Nat st IC S in dom p
  holds DecIC( p,k) = DataPart p +* Start-At ((IC p) -'k,S);

registration
  let N,S;
  let s be State of S, k be Nat;
  cluster DecIC(s,k) -> total;
end;

theorem :: MEMSTR_0:69
 for p being PartState of S, i,j being Nat
 holds DecIC(DecIC(p,i),j) = DecIC(p,i+j);

theorem :: MEMSTR_0:70
 for p being PartState of S, j,k being Nat
 holds DecIC(p +* Start-At(j,S),k) = p +* Start-At(j-'k,S);

theorem :: MEMSTR_0:71
 for s being State of S, k being Nat st k <= IC s
 holds IC DecIC(s,k) + k = IC s;

theorem :: MEMSTR_0:72
 for p,q being PartState of S, k being Nat st IC S in dom q
  holds DecIC(p+*q,k) = p +* DecIC(q,k);

theorem :: MEMSTR_0:73
 for p being PartState of S, k being Nat st IC S in dom p
  holds DecIC(IncIC(p,k),k) = p;

theorem :: MEMSTR_0:74
 for p,q being PartState of S, k being Nat st IC S in dom q
  holds DecIC(p+*IncIC(q,k),k) = p +* q;

registration let N,S; let k be Nat;
 let p be k-started PartState of S;
 cluster DecIC(p,k) -> 0-started;
end;

begin :: Finite Partial States

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

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

registration
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  cluster l-started for FinPartState of S;
end;

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

registration let N,S;
  let p be FinPartState of S;
  cluster Initialize p -> finite;
end;

registration let N,S;
  let p be FinPartState of S, k be Nat;
  cluster IncIC(p,k) -> finite;
end;

registration let N,S;
  let p be FinPartState of S, k be Nat;
  cluster DecIC(p,k) -> finite;
end;

definition
  let N;
  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 };
end;

theorem :: MEMSTR_0:75
 for S be with_non-empty_values Mem-Struct over N
 for p being FinPartState of S holds p in FinPartSt S;

registration
  let N;
  let S be with_non-empty_values Mem-Struct over N;
  cluster FinPartSt S -> non empty;
end;

theorem :: MEMSTR_0:76
  for S being with_non-empty_values Mem-Struct over N,
      p being Element of FinPartSt S holds
  p is FinPartState of S;

definition
  let N,S;
  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;

registration let N,S;
 cluster data-only for PartFunc of FinPartSt S, FinPartSt S;
end;

begin :: Addenda

theorem :: MEMSTR_0:77
  for A being non empty with_non-empty_values Mem-Struct over N, s
  being State of A, o being Object of A holds s.o in Values o;

theorem :: MEMSTR_0:78
  for A being IC-Ins-separated non empty with_non-empty_values
        Mem-Struct over N
  for s1,s2 being State of A st IC s1= IC s2 & DataPart s1 =
  DataPart s2 holds s1=s2;

theorem :: MEMSTR_0:79
  for s being State of S, l being Nat
  holds DataPart s = DataPart(s +* Start-At(l,S));

theorem :: MEMSTR_0:80
  for s1,s2 be State of S holds
  DataPart s1 = DataPart s2 implies
    Initialize s1 =  Initialize s2;

theorem :: MEMSTR_0:81
  the_Values_of Trivial-Mem N = 0 .--> NAT;

::from SCMFSA9A

definition let N,S;
  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;