:: deftheorem defines PopInstrLoc SCMPDS_1:def 19 :
for s being SCM-State
for a being Element of SCM-Data-Loc holds PopInstrLoc (s,a) = |.(s . a).| + 2;