:: deftheorem Def7 defines cond_address SCM_INST:def 7 :
for x being Element of SCM-Instr st ex mk being Nat ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b₂ being Element of SCM-Data-Loc holds
( b₂ = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b₂ = <*ml*> /. 1 ) );