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);
A1: (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) +* (Initialize (stop J)) = (Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J) by COMPOS_1:125;
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
A2: I is_closed_on s and
A3: I is_halting_on s and
A4: J is_closed_on IExec (I,s) and
A5: J is_halting_on IExec (I,s) and
A6: s2 = (Initialize s) +* (stop (I ';' J)) and
A7: 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)))) )
A8: s +* (Initialize (stop (I ';' J))) = (Initialize s) +* (stop (I ';' J)) by COMPOS_1:125;
A9: 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 A1, FUNCT_4:75;
set s4 = Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)));
thus A10: IC (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) = card I by A2, A3, A6, A7, 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)))) )

A11: 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 A12: x in (dom (Initialize (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then A13: x in dom (Initialize (stop J)) by XBOOLE_0:def 4;
A14: x in SCM-Data-Loc by A12, XBOOLE_0:def 4;

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

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

reconsider l = x as Element of NAT by A15;
l = x ;
hence (DataPart (Initialize (stop J))) . x = (DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) . x by A14, SCMPDS_4:22; :: thesis: verum

end;

suppose x = IC ; :: 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 A12, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A16: dom (DataPart (Initialize (stop J))) = (dom (Initialize (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
A17: Initialize (stop J) c= (Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J) by A1, 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 A16, 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 A11, GRFUNC_1:8;
then A18: DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) by A9, LATTICE2:8;
s2 = (Initialize s) +* (I ';' (J ';' (Stop SCMPDS))) by A6, AFINSQ_1:30;
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 A2, A3, A7, Th38;
hence A19: DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) by A18, COMPOS_1:138; :: 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 ;
A20: stop (I ';' J) c= Initialize (stop (I ';' J)) by COMPOS_1:126;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30
.= I +* (Shift ((stop J),(card I))) ;
then A21: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:26;
Initialize (stop (I ';' J)) c= s2 by A6, A8, FUNCT_4:26;
then stop (I ';' J) c= s2 by A20, XBOOLE_1:1;
then Shift ((stop J),(card I)) c= s2 by A21, XBOOLE_1:1;
hence A22: 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 A3, A4, A5, A7, Th42;
then A23: 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;
A24: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) by AMI_1:123;
A25: 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 EXTPRO_1:5;
A26: 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;
A27: 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 A3, A4, A5, A7, Th42;
then A28: 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 A17, A10, A19, A22, A26, A27, 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 A25, A24;
then A29: CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,m))) = halt SCMPDS by A23, EXTPRO_1:def 14;

A30: 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 A31: 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 A32: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,((LifeSpan ((ProgramPart s1),s1)) + k)))),(Comput ((ProgramPart s2),s2,((LifeSpan ((ProgramPart s1),s1)) + k)))) = halt SCMPDS ; :: thesis: contradiction
A33: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) by AMI_1:123;
A34: 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;
A35: 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;
A36: Comput ((ProgramPart s2),s2,((LifeSpan ((ProgramPart s1),s1)) + k)) = Comput ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))),k) by EXTPRO_1:5;
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 A17, A28, A10, A19, A22, A34, A35, SCMPDS_6:45
.= halt SCMPDS by A32, A36, A33, A35 ;
hence contradiction by A23, A31, EXTPRO_1:def 14; :: 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 A37: k < m ; :: thesis: CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,b₁))) <> halt SCMPDS
A38: 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 A2, A3, A6, A7, Th46, A38; :: 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
A39: (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 A39;
hence CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) <> halt SCMPDS by A30, A37, A38; :: thesis: verum

end;

end;

end;

then A40: for k being Element of NAT st CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) = halt SCMPDS holds
m <= k ;
A41: ProgramPart s1 halts_on s1 by A3, A7, SCMPDS_6:def 3;
A42: Result ((ProgramPart s1),s1) = Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))) by A41, EXTPRO_1:23;
I ';' J is_halting_on s by A2, A3, A4, A5, Th43;
then ProgramPart s2 halts_on s2 by A6, SCMPDS_6:def 3;
then LifeSpan ((ProgramPart s2),s2) = m by A29, A40, EXTPRO_1:def 14;
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 A42; :: thesis: verum