:: deftheorem defines Address_Add SCMPDS_1:def 6 :
for s being SCM-State
for a being Element of SCM-Data-Loc
for n being Integer holds Address_Add (s,a,n) = [1,|.((s . a) + n).|];