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