let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of st I is_halting_on s,P & J is_closed_on IExec (I,P,()),P & J is_halting_on IExec (I,P,()),P holds
( J is_closed_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) )

let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of st I is_halting_on s,P & J is_closed_on IExec (I,P,()),P & J is_halting_on IExec (I,P,()),P holds
( J is_closed_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) )

let I, J be Program of ; :: thesis: ( I is_halting_on s,P & J is_closed_on IExec (I,P,()),P & J is_halting_on IExec (I,P,()),P implies ( J is_closed_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) ) )
set s1 = Initialize s;
set P1 = P +* (stop I);
set sm = Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())));
set sE = IExec (I,P,());
assume that
A1: I is_halting_on s,P and
A2: J is_closed_on IExec (I,P,()),P and
A3: J is_halting_on IExec (I,P,()),P ; :: thesis: ( J is_closed_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) )
A4: P +* (stop I) halts_on Initialize s by ;
DataPart (IExec (I,P,())) = DataPart (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))) by ;
hence ( J is_closed_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))),P +* (stop I) ) by ; :: thesis: verum