:: deftheorem defines DataLoc SCMPDS_2:def 3 :
for m, n being Integer holds DataLoc (m,n) = [1,|.(m + n).|];