theorem Th19: :: SFMASTR2:23

for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)