let I be halt-free Program of SCMPDS ; :: thesis: for J being shiftable Program of SCMPDS
for s, s1, s2 being State of SCMPDS st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = (Initialize s) +* (stop (I ';' J)) & s1 = (Initialize s) +* (stop I) holds
( IC (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = card I & DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) & Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) )
let J be shiftable Program of SCMPDS ; :: thesis: for s, s1, s2 being State of SCMPDS st I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = (Initialize s) +* (stop (I ';' J)) & s1 = (Initialize s) +* (stop I) holds
( IC (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = card I & DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) & Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) )
let s, s1, s2 be State of SCMPDS ; :: thesis: ( I is_closed_on s & I is_halting_on s & J is_closed_on IExec I,s & J is_halting_on IExec I,s & s2 = (Initialize s) +* (stop (I ';' J)) & s1 = (Initialize s) +* (stop I) implies ( IC (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = card I & DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) & Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) ) )
set spJ = stop J;
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set m1 = LifeSpan (ProgramPart s1),s1;
set sm = Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1);
set s3 = (Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J);
I3: (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) +* (Initialize (stop J)) = (Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J) by SCMPDS_4:5;
set m3 = LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J));
set sE = IExec I,s;
assume that
A1: I is_closed_on s and
A2: I is_halting_on s and
A3: J is_closed_on IExec I,s and
A4: J is_halting_on IExec I,s and
A5: s2 = (Initialize s) +* (stop (I ';' J)) and
A6: s1 = (Initialize s) +* (stop I) ; :: thesis: ( IC (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = card I & DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) & Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) )
I1: s +* (Initialize (stop (I ';' J))) = (Initialize s) +* (stop (I ';' J)) by SCMPDS_4:5;
A7: DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (DataPart (Initialize (stop J))) by I3, FUNCT_4:75;
set s4 = Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1);
thus A8: IC (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = card I by A1, A2, A5, A6, Th17, Th44; :: thesis: ( DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) & Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) )

A9: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialize (stop J))) implies (DataPart (Initialize (stop J))) . b₁ = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) . b₁ )
assume x in dom (DataPart (Initialize (stop J))) ; :: thesis: (DataPart (Initialize (stop J))) . b₁ = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) . b₁
then A10: x in (dom (Initialize (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then A11: x in dom (Initialize (stop J)) by XBOOLE_0:def 4;
A12: x in SCM-Data-Loc by A10, XBOOLE_0:def 4;

per cases ( x in dom (stop J) or x = IC SCMPDS ) by A11, COMPOS_1:77;

suppose A13: x in dom (stop J) ; :: thesis: (DataPart (Initialize (stop J))) . b₁ = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) . b₁

dom (stop J) c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A13;
l = x ;
hence (DataPart (Initialize (stop J))) . x = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) . x by A12, SCMPDS_4:22; :: thesis: verum

end;

suppose x = IC SCMPDS ; :: thesis: (DataPart (Initialize (stop J))) . b₁ = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) . b₁

hence (DataPart (Initialize (stop J))) . x = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) . x by A10, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A14: dom (DataPart (Initialize (stop J))) = (dom (Initialize (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
A15: Initialize (stop J) c= (Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J) by I3, FUNCT_4:26;
then dom (Initialize (stop J)) c= dom ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) by GRFUNC_1:8;
then dom (Initialize (stop J)) c= the carrier of SCMPDS by PARTFUN1:def 4;
then dom (DataPart (Initialize (stop J))) c= the carrier of SCMPDS /\ SCM-Data-Loc by A14, XBOOLE_1:26;
then dom (DataPart (Initialize (stop J))) c= (dom (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) /\ SCM-Data-Loc by PARTFUN1:def 4;
then dom (DataPart (Initialize (stop J))) c= dom (DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (Initialize (stop J)) c= DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) by A9, GRFUNC_1:8;
then A16: DataPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) by A7, LATTICE2:8;
s2 = (Initialize s) +* (I ';' (J ';' (Stop SCMPDS ))) by A5, SCMPDS_4:46;
then Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) = Comput (ProgramPart ((Initialize s) +* (I ';' (J ';' (Stop SCMPDS ))))),((Initialize s) +* (I ';' (J ';' (Stop SCMPDS )))),(LifeSpan (ProgramPart s1),s1) ;
then Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1), Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) equal_outside NAT by A1, A2, A6, Th38;
hence A17: DataPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) by A16, SCMPDS_4:24; :: thesis: ( Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) )
reconsider m = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))) as Element of NAT ;
A18: stop (I ';' J) c= Initialize (stop (I ';' J)) by SCMPDS_4:9;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46
.= I +* (Shift (stop J),(card I)) ;
then A19: Shift (stop J),(card I) c= stop (I ';' J) by FUNCT_4:26;
Initialize (stop (I ';' J)) c= s2 by A5, I1, FUNCT_4:26;
then stop (I ';' J) c= s2 by A18, XBOOLE_1:1;
then Shift (stop J),(card I) c= s2 by A19, XBOOLE_1:1;
hence A20: Shift (stop J),(card I) c= Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) by AMI_1:81; :: thesis: LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J)))
J is_halting_on Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1) by A2, A3, A4, A6, Th42;
then A21: ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) halts_on (Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J) by SCMPDS_6:def 3;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) by AMI_1:123;
x: Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)))) = Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))) by AMI_1:51;
TX3: ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) = ProgramPart (Comput (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)))) by AMI_1:123;
TX4: ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)))) by AMI_1:123;
J is_closed_on Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1) by A2, A3, A4, A6, Th42;
then A22: J is_closed_on (Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J) by SCMPDS_6:38;
then CurInstr (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),(Comput (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)))) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1))),(Comput (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)))) by A15, A8, A17, A20, TX3, TX4, SCMPDS_6:45;
then CurInstr (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),(Comput (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)),(LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)))) = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))))) by x, T;
then A23: CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,m) = halt SCMPDS by A21, AMI_1:def 46;

A24: now

let k be Element of NAT ; :: thesis: ( (LifeSpan (ProgramPart s1),s1) + k < m implies not CurInstr (ProgramPart (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + k))),(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + k)) = halt SCMPDS )
assume (LifeSpan (ProgramPart s1),s1) + k < m ; :: thesis: not CurInstr (ProgramPart (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + k))),(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + k)) = halt SCMPDS
then A25: k < LifeSpan (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) by XREAL_1:8;
assume A26: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + k))),(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + k)) = halt SCMPDS ; :: thesis: contradiction
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) by AMI_1:123;
TX3: ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) = ProgramPart (Comput (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)),k) by AMI_1:123;
TX4: ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)),k) by AMI_1:123;
x: Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart s1),s1) + k) = Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)),k by AMI_1:51;
CurInstr (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),(Comput (ProgramPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J))),((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)),k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1))),(Comput (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)),k) by A15, A22, A8, A17, A20, TX3, TX4, SCMPDS_6:45
.= halt SCMPDS by A26, x, T, TX4 ;
hence contradiction by A21, A25, AMI_1:def 46; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k < m implies CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,b₁) <> halt SCMPDS )
assume A27: k < m ; :: thesis: CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,b₁) <> halt SCMPDS
TX: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,k) by AMI_1:123;

per cases ( k < LifeSpan (ProgramPart s1),s1 or LifeSpan (ProgramPart s1),s1 <= k ) ;

suppose k < LifeSpan (ProgramPart s1),s1 ; :: thesis: CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,b₁) <> halt SCMPDS

hence CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,k) <> halt SCMPDS by A1, A2, A5, A6, Th46, TX; :: thesis: verum

end;

suppose LifeSpan (ProgramPart s1),s1 <= k ; :: thesis: CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,b₁) <> halt SCMPDS

then consider kk being Nat such that
A28: (LifeSpan (ProgramPart s1),s1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
(LifeSpan (ProgramPart s1),s1) + kk = k by A28;
hence CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,k) <> halt SCMPDS by A24, A27, TX; :: thesis: verum

end;

end;

end;

then A29: for k being Element of NAT st CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,k) = halt SCMPDS holds
m <= k ;
A30: ProgramPart s1 halts_on s1 by A2, A6, SCMPDS_6:def 3;
X: Result (ProgramPart s1),s1 = Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1) by A30, AMI_1:122;
I ';' J is_halting_on s by A1, A2, A3, A4, Th43;
then ProgramPart s2 halts_on s2 by A5, SCMPDS_6:def 3;
then LifeSpan (ProgramPart s2),s2 = m by A23, A29, AMI_1:def 46;
hence LifeSpan (ProgramPart s2),s2 = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) by X; :: thesis: verum