for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( ( s . (DataLoc ((s . a),k1)) <= 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = (IC s) + 1 ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )