theorem Th1: :: SCMPDS_7:1

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