theorem Th18: :: SCM_HALT:20

for s being State of SCM+FSA
for a being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA
for J being really-closed InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . a = (IExec (J,p,(IExec (I,p,s)))) . a