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 18;
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:11 ;
hence succ (IC s) = ICplusConst (s,1) by A1, A2; :: thesis: verum