theorem :: SCMFSA6B:20

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting keeping_0 Program of
for J being really-closed parahalting Program of holds IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))