:: deftheorem Def10 defines P42address SCMPDS_I:def 10 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b₂ being Element of SCM-Data-Loc holds
( b₂ = x P42address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b₂ = f /. 2 ) );