for s1, s2 being State of SCMPDS
for k1, k2 being Nat st IC s1 = IC s2 & k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)