set D = SCM-Data-Loc ;
let I be parahalting No-StopCode Program of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS
for s, s1 being State of SCMPDS st Initialized (stop (I ';' J)) c= s & s1 = s +* (Initialized (stop I)) holds
( IC (Comput (ProgramPart s),s,(LifeSpan s1)) = card I & DataPart (Comput (ProgramPart s),s,(LifeSpan s1)) = DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
let J be parahalting shiftable Program of SCMPDS ; :: thesis: for s, s1 being State of SCMPDS st Initialized (stop (I ';' J)) c= s & s1 = s +* (Initialized (stop I)) holds
( IC (Comput (ProgramPart s),s,(LifeSpan s1)) = card I & DataPart (Comput (ProgramPart s),s,(LifeSpan s1)) = DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
let s, s1 be State of SCMPDS ; :: thesis: ( Initialized (stop (I ';' J)) c= s & s1 = s +* (Initialized (stop I)) implies ( IC (Comput (ProgramPart s),s,(LifeSpan s1)) = card I & DataPart (Comput (ProgramPart s),s,(LifeSpan s1)) = DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) ) )
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 = (Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J));
set m3 = LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)));
assume that
A1: Initialized (stop (I ';' J)) c= s and
A2: s1 = s +* (Initialized (stop I)) ; :: thesis: ( IC (Comput (ProgramPart s),s,(LifeSpan s1)) = card I & DataPart (Comput (ProgramPart s),s,(LifeSpan s1)) = DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
A3: DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1))) +* (DataPart (Initialized (stop J))) by FUNCT_4:75;
set s4 = Comput (ProgramPart s),s,(LifeSpan s1);
A4: Initialized I c= Initialized (stop (I ';' J)) by Th15;
hence A5: IC (Comput (ProgramPart s),s,(LifeSpan s1)) = card I by A1, A2, Th30, XBOOLE_1:1; :: thesis: ( DataPart (Comput (ProgramPart s),s,(LifeSpan s1)) = DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )

A6: now

let x be set ; :: thesis: ( x in dom (DataPart (Initialized (stop J))) implies (DataPart (Initialized (stop J))) . b₁ = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1))) . b₁ )
assume x in dom (DataPart (Initialized (stop J))) ; :: thesis: (DataPart (Initialized (stop J))) . b₁ = (DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1))) . b₁
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 ( x in dom (stop J) or x = IC SCMPDS ) by A8, SCMPDS_4:28;

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

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

end;

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

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

end;

end;

end;

A11: dom (DataPart (Initialized (stop J))) = (dom (Initialized (stop J))) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
reconsider m = (LifeSpan s1) + (LifeSpan ((Comput (ProgramPart s1),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 A12: Shift (stop J),(card I) c= stop (I ';' J) by FUNCT_4:26;
A13: Initialized (stop J) c= (Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)) by FUNCT_4:26;
then A14: ProgramPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) halts_on (Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)) by AMI_1:def 26;
dom (Initialized (stop J)) c= dom ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) by A13, GRFUNC_1:8;
then dom (Initialized (stop J)) c= the carrier of SCMPDS by PARTFUN1:def 4;
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 (Comput (ProgramPart s1),s1,(LifeSpan s1))) /\ SCM-Data-Loc by PARTFUN1:def 4;
then dom (DataPart (Initialized (stop J))) c= dom (DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (Initialized (stop J)) c= DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) by A6, GRFUNC_1:8;
then A15: DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) by A3, LATTICE2:8;
s = s +* (Initialized (stop (I ';' J))) by A1, FUNCT_4:79
.= s +* ((I ';' (J ';' (Stop SCMPDS ))) +* (Start-At 0 ,SCMPDS )) by SCMPDS_4:46 ;
hence A16: DataPart (Comput (ProgramPart s),s,(LifeSpan s1)) = DataPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) by A2, A15, Th33, SCMPDS_4:24; :: thesis: ( Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(LifeSpan s1)) by AMI_1:144;
x: Comput (ProgramPart s),s,((LifeSpan s1) + (LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))))) = Comput (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan s1)),(LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))) by AMI_1:51;
stop (I ';' J) c= s by A1, SCMPDS_4:57;
then Shift (stop J),(card I) c= s by A12, XBOOLE_1:1;
hence A17: Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan s1) by AMI_1:81; :: thesis: LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J))))
then CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))),((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))))),(Comput (ProgramPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))),((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))))) = CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan s1))),(Comput (ProgramPart s),s,(LifeSpan s1)),(LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))))),(Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan s1))),(Comput (ProgramPart s),s,(LifeSpan s1)),(LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))))) by A13, A5, A16, SCMPDS_4:84;
then CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))),((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))))),(Comput (ProgramPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))),((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))))) = CurInstr (ProgramPart (Comput (ProgramPart s),s,((LifeSpan s1) + (LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))))))),(Comput (ProgramPart s),s,((LifeSpan s1) + (LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))))) by x, T;
then A18: CurInstr (ProgramPart (Comput (ProgramPart s),s,m)),(Comput (ProgramPart s),s,m) = halt SCMPDS by A14, AMI_1:def 46;

A19: now

let k be Element of NAT ; :: thesis: ( (LifeSpan s1) + k < m implies not CurInstr (ProgramPart (Comput (ProgramPart s),s,((LifeSpan s1) + k))),(Comput (ProgramPart s),s,((LifeSpan s1) + k)) = halt SCMPDS )
assume (LifeSpan s1) + k < m ; :: thesis: not CurInstr (ProgramPart (Comput (ProgramPart s),s,((LifeSpan s1) + k))),(Comput (ProgramPart s),s,((LifeSpan s1) + k)) = halt SCMPDS
then A20: k < LifeSpan ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))) by XREAL_1:8;
assume A21: CurInstr (ProgramPart (Comput (ProgramPart s),s,((LifeSpan s1) + k))),(Comput (ProgramPart s),s,((LifeSpan s1) + k)) = halt SCMPDS ; :: thesis: contradiction
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(LifeSpan s1)) by AMI_1:144;
x: Comput (ProgramPart s),s,((LifeSpan s1) + k) = Comput (ProgramPart s),(Comput (ProgramPart s),s,(LifeSpan s1)),k by AMI_1:51;
CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))),((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))),k)),(Comput (ProgramPart ((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J)))),((Comput (ProgramPart s1),s1,(LifeSpan s1)) +* (Initialized (stop J))),k) = CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan s1))),(Comput (ProgramPart s),s,(LifeSpan s1)),k)),(Comput (ProgramPart (Comput (ProgramPart s),s,(LifeSpan s1))),(Comput (ProgramPart s),s,(LifeSpan s1)),k) by A13, A5, A16, A17, SCMPDS_4:84
.= halt SCMPDS by A21, x, T ;
hence contradiction by A14, A20, AMI_1:def 46; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k < m implies CurInstr (ProgramPart (Comput (ProgramPart s),s,b₁)),(Comput (ProgramPart s),s,b₁) <> halt SCMPDS )
assume A22: k < m ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart s),s,b₁)),(Comput (ProgramPart s),s,b₁) <> halt SCMPDS

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

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

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

end;

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

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 (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCMPDS by A19, A22, A23; :: thesis: verum

end;

end;

end;

then A24: for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCMPDS holds
m <= k ;
Initialized (stop I) c= s1 by A2, FUNCT_4:26;
then B25: ProgramPart s1 halts_on s1 by SCMPDS_4:63;
ProgramPart s halts_on s 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 B25, AMI_1:122; :: thesis: verum