:: deftheorem defines are_correct_wrt NOMIN_7:def 7 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for d1 being NonatomicND of V,A
for size being non zero Nat holds
( loc,val,size are_correct_wrt d1 iff ( not V is empty & A is_without_nonatomicND_wrt V & val is_valid_wrt d1 & dom (LocalOverlapSeq (A,loc,val,d1,size)) c= dom val ) );