:: deftheorem Def17 defines ICplusConst SCMPDS_2:def 18 :
for s being State of SCMPDS
for c being Integer
for b₃ being Element of NAT holds
( b₃ = ICplusConst (s,c) iff ex m being Element of NAT st
( m = IC s & b₃ = |.(m + c).| ) );