theorem Th43: :: SCMPDS_2:46

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