theorem Th17: :: SCMRING2:17

for R being Ring
for r being Element of R
for a being Data-Location of R
for s being State of (SCM R) holds
( (Exec ((a := r),s)) . (IC ) = (IC s) + 1 & (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds
(Exec ((a := r),s)) . c = s . c ) )