:: deftheorem Def4 defines jump_address SCMRINGI:def 4 :
for R being non empty 1-sorted
for x being Element of SCM-Instr R st ex mk being Element of NAT ex I being Element of Segm 8 st x = [I,<*mk*>,{}] holds
for b₃ being Element of NAT holds
( b₃ = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 & b₃ = f /. 1 ) );