let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS st I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,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 the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I, J being Program of SCMPDS st I is_halting_on s,P & J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,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,s),P & J is_halting_on IExec (I,P,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,s);
assume that
A1: I is_halting_on s,P and
A2: J is_closed_on IExec (I,P,s),P and
A3: J is_halting_on IExec (I,P,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;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then DataPart (IExec (I,P,s)) = DataPart (Result ((P +* (stop I)),(Initialize s))) by AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= 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:37; :: thesis: verum