theorem Th16: :: SCMRING2:16

for R being Ring
for a, c being Data-Location of R
for i1 being Nat
for s being State of (SCM R) holds
( ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) & ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = (IC s) + 1 ) & (Exec ((a =0_goto i1),s)) . c = s . c )