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