for s being State of SCMPDS
for m, n being Nat st IC s = m holds
ICplusConst (s,(n - m)) = n