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