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 (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) & J is_halting_on Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (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 (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) & J is_halting_on Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) ) )
set s1 = s +* (Initialized (stop I));
set sm = Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (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 (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) & J is_halting_on Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) )
A4: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by A1, SCMPDS_6:def 3;
dom (s | NAT ) = NAT by SCMPDS_6:1;
then DataPart (IExec I,s) = DataPart (Result (s +* (Initialized (stop I)))) by AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by A4, AMI_1:122 ;
hence ( J is_closed_on Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) & J is_halting_on Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) ) by A2, A3, SCMPDS_6:37; :: thesis: verum