:: deftheorem Def7 defines P32const SCMPDS_I:def 7 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds
for b₂ being Integer holds
( b₂ = x P32const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b₂ = f /. 2 ) );