for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((a := b),s)) . (IC ) = (IC s) + 1 & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )