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