let k1 be Integer; :: thesis: for s1, s2 being State of SCMPDS st IC s1 = IC s2 holds
ICplusConst s1,k1 = ICplusConst s2,k1
let s1, s2 be State of SCMPDS ; :: thesis: ( IC s1 = IC s2 implies ICplusConst s1,k1 = ICplusConst s2,k1 )
A1: ex i being Element of NAT st
( i = IC s1 & ICplusConst s1,k1 = abs (i + k1) ) by SCMPDS_2:def 20;
assume IC s1 = IC s2 ; :: thesis: ICplusConst s1,k1 = ICplusConst s2,k1
hence ICplusConst s1,k1 = ICplusConst s2,k1 by A1, SCMPDS_2:def 20; :: thesis: verum