let s be State of SCMPDS ; :: thesis: succ (IC s) = ICplusConst s,1
consider j being Element of NAT such that
A1: j = IC s and
A2: ICplusConst s,1 = abs (j + 1) by SCMPDS_2:def 20;
reconsider mj = IC s as Element of NAT ;
A3: j * 1 >= 0 by NAT_1:2;
j >= 0 by NAT_1:2;
then succ (IC s) = (abs mj) + 1 by A1, ABSVALUE:def 1
.= (abs mj) + (abs 1) by ABSVALUE:def 1
.= abs (mj + 1) by A1, A3, ABSVALUE:24 ;
hence succ (IC s) = ICplusConst s,1 by A1, A2; :: thesis: verum