let s be State of ; :: thesis: for I being parahalting Program of
for a being Int_position holds (IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a
let I be parahalting Program of ; :: thesis: for a being Int_position holds (IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a
let a be Int_position ; :: thesis: (IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a
I is_halting_on s by SCMPDS_6:35;
hence (IExec I,s) . a = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a by Th31; :: thesis: verum