:: deftheorem Def6 defines cjump_address SCM_INST:def 6 :
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 Nat holds
( b₂ = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 & b₂ = <*mk*> /. 1 ) );