:: deftheorem defines int_addr SCMFSA_I:def 6 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc st x = [13,{},<*c*>] holds
for b₂ being Element of SCM-Data-Loc holds
( b₂ = x int_addr iff ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b₂ = c ) );