:: deftheorem Def8 defines P33const SCMPDS_I:def 8 :
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 P33const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b₂ = f /. 3 ) );