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