set D = SCM-Data-Loc ;
let I be parahalting No-StopCode Program of SCMPDS ; :: thesis:
let J be parahalting shiftable Program of SCMPDS ; :: thesis:
let s, s1 be State of SCMPDS ; :: thesis:
set IsI = Initialized (stop I);
set spJ = stop J;
set IsJ = Initialized (stop J);
set sIJ = stop (I ';' J);
set IsIJ = Initialized (stop (I ';' J));
set m1 = LifeSpan s1;
set s3 = (Computation s1,(LifeSpan s1)) +* (Initialized (stop J));
set m3 = LifeSpan ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J)));
assume that
A1: Initialized (stop (I ';' J)) c= s and
A2: s1 = s +* (Initialized (stop I)) ; :: thesis:
A3: DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) = (DataPart (Computation s1,(LifeSpan s1))) +* (DataPart (Initialized (stop J))) by FUNCT_4:75;
set s4 = Computation s,(LifeSpan s1);
A4: Initialized I c= Initialized (stop (I ';' J)) by Th15;
hence A5: IC (Computation s,(LifeSpan s1)) = inspos (card I) by A1, A2, Th30, XBOOLE_1:1; :: thesis:

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)) by XBOOLE_0:def 4;
A9: x in SCM-Data-Loc by A7, XBOOLE_0:def 4;

per cases by A8, SCMPDS_4:28;

suppose A10: 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 A10, AMI_1:def 4;
(DataPart (Initialized (stop J))) . l = (DataPart (Computation s1,(LifeSpan s1))) . l by A9, SCMPDS_4:22;
hence (DataPart (Initialized (stop J))) . x = (DataPart (Computation s1,(LifeSpan s1))) . x ; :: 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;

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 s,((LifeSpan s1) + k)) = halt SCMPDS ; :: thesis:
CurInstr (Computation ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))),k) = CurInstr (Computation (Computation s,(LifeSpan s1)),k) by A13, A5, A16, A17, SCMPDS_4:84
.= halt SCMPDS by A21, AMI_1:51 ;
hence contradiction by A14, A20, AMI_1:def 46; :: thesis:

end;

now

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

per cases ;

suppose k < LifeSpan s1 ; :: thesis:

hence CurInstr (Computation s,k) <> halt SCMPDS by A1, A2, A4, Th32, XBOOLE_1:1; :: thesis:

end;

suppose LifeSpan s1 <= k ; :: thesis:

then consider kk being Nat such that
A23: (LifeSpan s1) + kk = k by NAT_1:10;
kk in NAT by ORDINAL1:def 13;
hence CurInstr (Computation s,k) <> halt SCMPDS by A19, A22, A23; :: thesis:

end;

then A24: for k being Element of NAT st CurInstr (Computation s,k) = halt SCMPDS holds
m <= k ;
A25: Initialized (stop I) c= s1 by A2, FUNCT_4:26;
s is halting by A1, SCMPDS_4:63;
then LifeSpan s = m by A18, A24, AMI_1:def 46;
hence LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) by A25, AMI_1:122, SCMPDS_4:63; :: thesis: