:: deftheorem Def7 defines const_address SCMRINGI:def 7 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds
for b₃ being Element of SCM-Data-Loc holds
( b₃ = x const_address iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b₃ = f /. 1 ) );