let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of SCMPDS st I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) )
let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of SCMPDS st I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) )
let I, J be Program of SCMPDS; :: thesis: ( I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P implies ( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) ) )
set s1 = Initialize s;
set P1 = P +* (stop I);
set sm = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set sE = IExec (I,P,(Initialize s));
assume that
A1: I is_halting_on s,P and
A2: J is_closed_on IExec (I,P,(Initialize s)),P and
A3: J is_halting_on IExec (I,P,(Initialize s)),P ; :: thesis: ( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) )
A4: P +* (stop I) halts_on Initialize s by A1, SCMPDS_6:def 3;
DataPart (IExec (I,P,(Initialize s))) = DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A4, EXTPRO_1:23;
hence ( J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) & J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I) ) by A2, A3, SCMPDS_6:23; :: thesis: verum