theorem Th56: :: SCMPDS_2:59

for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((saveIC (a,k1)),s)) . (IC ) = (IC s) + 1 & (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = IC s & ( for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b ) )