for s being State of SCMPDS
for a being Int_position holds
( (Exec ((return a),s)) . (IC ) = |.(s . (DataLoc ((s . a),RetIC))).| + 2 & (Exec ((return a),s)) . a = s . (DataLoc ((s . a),RetSP)) & ( for b being Int_position st a <> b holds
(Exec ((return a),s)) . b = s . b ) )