for c being Data-Location
for loc being Nat
for s being State of SCM holds
( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )