theorem Th42: :: SCMPDS_2:45

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