let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for a being Int_position holds (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
let s be State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS
for a being Int_position holds (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
let I be parahalting Program of SCMPDS; :: thesis: for a being Int_position holds (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
let a be Int_position ; :: thesis: (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a
I is_halting_on s,P by SCMPDS_6:21;
hence (IExec (I,P,(Initialize s))) . a = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . a by Th31; :: thesis: verum