let s be State of SCMPDS; :: thesis: for I, J being Program of SCMPDS st I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) holds
( J is_closed_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) & J is_halting_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) )
let I, J be Program of SCMPDS; :: thesis: ( I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) implies ( J is_closed_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) & J is_halting_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) ) )
set s1 = (Initialize s) +* (stop I);
set sm = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
set sE = IExec (I,s);
assume that
A1: I is_halting_on s and
A2: J is_closed_on IExec (I,s) and
A3: J is_halting_on IExec (I,s) ; :: thesis: ( J is_closed_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) & J is_halting_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) )
A4: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A1, SCMPDS_6:def 3;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then DataPart (IExec (I,s)) = DataPart (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by A4, EXTPRO_1:23 ;
hence ( J is_closed_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) & J is_halting_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) ) by A2, A3, SCMPDS_6:37; :: thesis: verum