let I be No-StopCode Program of SCMPDS ; :: thesis:
let J be shiftable Program of SCMPDS ; :: thesis:
let s, s1, s2 be State of SCMPDS ; :: thesis:
set IsI = Initialized (stop I);
set spJ = stop J;
set IsJ = Initialized (stop J);
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set IsIJ = Initialized (stop (I ';' J));
set m1 = LifeSpan s1;
set sm = Computation s1,(LifeSpan s1);
set s3 = (Computation s1,(LifeSpan s1)) +* (Initialized (stop J));
set m3 = LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J)));
set sE = IExec I,s;
assume A1: ( 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 = s +* (Initialized (stop (I ';' J))) & s1 = s +* (Initialized (stop I)) ) ; :: thesis:
then A2: s2 = s +* ((I ';' (J ';' (Stop SCMPDS ))) +* (Start-At (inspos 0 ))) by SCMPDS_4:46;
A3: Initialized (stop (I ';' J)) c= s2 by A1, FUNCT_4:26;
stop (I ';' J) c= Initialized (stop (I ';' J)) by SCMPDS_4:9;
then A4: stop (I ';' J) c= s2 by A3, XBOOLE_1:1;
A5: DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) = (DataPart (Computation s1,(LifeSpan s1))) +* (DataPart (Initialized (stop J))) by FUNCT_4:75;

A6: now

let x be set ; :: thesis:
assume x in dom (DataPart (Initialized (stop J))) ; :: thesis:
then A7: x in (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then A8: ( x in dom (Initialized (stop J)) & x in SCM-Data-Loc ) by XBOOLE_0:def 4;

per cases by A8, SCMPDS_4:28;

suppose A9: x in dom (stop J) ; :: thesis:

dom (stop J) c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCMPDS by A9, AMI_1:def 4;
l = x ;
hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation s1,(LifeSpan s1))) . x by A8, SCMPDS_4:22; :: thesis:

end;

suppose x = IC SCMPDS ; :: thesis:

hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation s1,(LifeSpan s1))) . x by A7, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis:

end;

A10: Initialized (stop J) c= (Computation s1,(LifeSpan s1)) +* (Initialized (stop J)) by FUNCT_4:26;
then dom (Initialized (stop J)) c= dom ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by GRFUNC_1:8;
then A11: dom (Initialized (stop J)) c= the carrier of SCMPDS by AMI_1:79;
dom (DataPart (Initialized (stop J))) = (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
then dom (DataPart (Initialized (stop J))) c= the carrier of SCMPDS /\ SCM-Data-Loc by A11, XBOOLE_1:26;
then dom (DataPart (Initialized (stop J))) c= (dom (Computation s1,(LifeSpan s1))) /\ SCM-Data-Loc by AMI_1:79;
then dom (DataPart (Initialized (stop J))) c= dom (DataPart (Computation s1,(LifeSpan s1))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (Initialized (stop J)) c= DataPart (Computation s1,(LifeSpan s1)) by A6, GRFUNC_1:8;
then A12: DataPart (Computation s1,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by A5, LATTICE2:8;
set s4 = Computation s2,(LifeSpan s1);
A13: ( J is_closed_on Computation s1,(LifeSpan s1) & J is_halting_on Computation s1,(LifeSpan s1) ) by A1, Th42;
then A14: J is_closed_on (Computation s1,(LifeSpan s1)) +* (Initialized (stop J)) by SCMPDS_6:38;
A15: (Computation s1,(LifeSpan s1)) +* (Initialized (stop J)) is halting by A13, SCMPDS_6:def 3;
thus A16: IC (Computation s2,(LifeSpan s1)) = inspos (card I) by A1, Th17, Th44; :: thesis:
thus A17: DataPart (Computation s2,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by A1, A2, A12, Th38, SCMPDS_4:24; :: thesis:
reconsider m = (LifeSpan s1) + (LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J)))) as Element of NAT ;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46
.= I +* (Shift (stop J),(card I)) ;
then Shift (stop J),(card I) c= stop (I ';' J) by FUNCT_4:26;
then Shift (stop J),(card I) c= s2 by A4, XBOOLE_1:1;
hence A18: Shift (stop J),(card I) c= Computation s2,(LifeSpan s1) by AMI_1:81; :: thesis:

A19: now

let k be Element of NAT ; :: thesis:
assume (LifeSpan s1) + k < m ; :: thesis:
then A20: k < LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) by XREAL_1:8;
assume A21: CurInstr (Computation s2,((LifeSpan s1) + k)) = halt SCMPDS ; :: thesis:
CurInstr (Computation ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))),k) = CurInstr (Computation (Computation s2,(LifeSpan s1)),k) by A10, A14, A16, A17, A18, SCMPDS_6:45
.= halt SCMPDS by A21, AMI_1:51 ;
hence contradiction by A15, A20, AMI_1:def 46; :: thesis:

end;

CurInstr (Computation ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))))) = CurInstr (Computation (Computation s2,(LifeSpan s1)),(LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))))) by A10, A14, A16, A17, A18, SCMPDS_6:45;
then CurInstr (Computation ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))))) = CurInstr (Computation s2,((LifeSpan s1) + (LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J)))))) by AMI_1:51;
then A22: CurInstr (Computation s2,m) = halt SCMPDS by A15, AMI_1:def 46;

now

let k be Element of NAT ; :: thesis:
assume A23: k < m ; :: thesis:

per cases ;

suppose k < LifeSpan s1 ; :: thesis:

hence CurInstr (Computation s2,k) <> halt SCMPDS by A1, Th46; :: thesis:

end;

suppose LifeSpan s1 <= k ; :: thesis:

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

end;

then A25: for k being Element of NAT st CurInstr (Computation s2,k) = halt SCMPDS holds
m <= k ;
I ';' J is_halting_on s by A1, Th43;
then s2 is halting by A1, SCMPDS_6:def 3;
then A26: LifeSpan s2 = m by A22, A25, AMI_1:def 46;
s1 is halting by A1, SCMPDS_6:def 3;
hence LifeSpan s2 = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) by A26, AMI_1:122; :: thesis: