for s1, s2 being State of SCMPDS
for n, m being Nat
for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds
(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)