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