:: deftheorem Def6 defines cond_address SCMRINGI:def 6 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 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 ) );