let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being parahalting 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
let s be State of SCM+FSA; :: thesis: for I being parahalting 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
let I be parahalting Program of SCM+FSA; :: thesis: 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
let a be read-write Int-Location; :: thesis: (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a
I is_halting_on Initialized s,P by SCMFSA7B:19;
hence (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a by Th49; :: thesis: verum