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