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, AMI_1:122 ;
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