theorem Th42: :: SCM_HALT:51

for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a