set D = SCM-Data-Loc ;
let I be halt-free parahalting Program of SCMPDS; :: thesis: for J being parahalting shiftable Program of SCMPDS
for s being 0 -started State of SCMPDS
for s1 being State of SCMPDS st stop (I ';' J) c= s & s1 = s +* (stop I) holds
( IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = card I & DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) )
let J be parahalting shiftable Program of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for s1 being State of SCMPDS st stop (I ';' J) c= s & s1 = s +* (stop I) holds
( IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = card I & DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) )
let s be 0 -started State of SCMPDS; :: thesis: for s1 being State of SCMPDS st stop (I ';' J) c= s & s1 = s +* (stop I) holds
( IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = card I & DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) )
let s1 be State of SCMPDS; :: thesis: ( stop (I ';' J) c= s & s1 = s +* (stop I) implies ( IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = card I & DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) ) )
A1: Initialize s = s by COMPOS_1:78;
set spJ = stop J;
set sIJ = stop (I ';' J);
set m1 = LifeSpan ((ProgramPart s1),s1);
set s3 = (Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J);
A2: (Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J) = (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) +* (Initialize (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)));
assume that
A3: stop (I ';' J) c= s and
A4: s1 = s +* (stop I) ; :: thesis: ( IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = card I & DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) )
A5: 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 A2, FUNCT_4:75;
set s4 = Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)));
A6: ProgramPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = ProgramPart s by AMI_1:123;
A7: I c= stop (I ';' J) by Th15;
hence A8: IC (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = card I by A3, A4, Th30, XBOOLE_1:1; :: thesis: ( DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) & Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (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 ) 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;
(DataPart (Initialize (stop J))) . l = (DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) . l by A12, SCMPDS_4:22;
hence (DataPart (Initialize (stop J))) . x = (DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) . x ; :: 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 A10, SCMPDS_3:6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A14: dom (DataPart (stop J)) = (dom (stop J)) /\ SCM-Data-Loc by RELAT_1:90, SCMPDS_2:100;
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 ;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30
.= I +* (Shift ((stop J),(card I))) ;
then A15: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:26;
A16: stop J c= (Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J) by FUNCT_4:26;
A17: 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 FUNCT_4:26, SCMPDS_4:def 10;
A18: (Initialize s) +* (stop (I ';' J)) = s +* (Initialize (stop (I ';' J))) by COMPOS_1:125;
A19: DataPart (Initialize (stop J)) = DataPart (stop J) by COMPOS_1:80;
dom (stop J) c= dom ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) by A16, GRFUNC_1:8;
then dom (stop J) c= the carrier of SCMPDS by PARTFUN1:def 4;
then dom (DataPart (stop J)) c= the carrier of SCMPDS /\ SCM-Data-Loc by A14, XBOOLE_1:26;
then dom (DataPart (stop J)) c= (dom (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) /\ SCM-Data-Loc by PARTFUN1:def 4;
then dom (DataPart (stop J)) c= dom (DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) by RELAT_1:90, SCMPDS_2:100;
then DataPart (stop J) c= DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) by A9, A19, GRFUNC_1:8;
then A20: DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) by A5, A19, LATTICE2:8;
s = (Initialize s) +* (stop (I ';' J)) by A3, A1, FUNCT_4:79
.= s +* (Initialize (I ';' (J ';' (Stop SCMPDS)))) by A18, AFINSQ_1:30 ;
hence A21: DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) = DataPart ((Initialize (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) +* (stop J)) by A4, A20, Th33, A1, COMPOS_1:138; :: thesis: ( Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) & LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) )
A22: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1)))) by AMI_1:123;
A23: Comput ((ProgramPart s),s,((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 s),(Comput ((ProgramPart s),s,(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;
Shift ((stop J),(card I)) c= s by A15, A3, XBOOLE_1:1;
hence A24: Shift ((stop J),(card I)) c= Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart s1),s1))) by AMI_1:81; :: thesis: LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))))
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 s),(Comput ((ProgramPart s),s,((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 A23, A22, A16, A8, A21, SCMPDS_4:84;
then A25: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = halt SCMPDS by A17, EXTPRO_1:def 14;

A26: now

let k be Element of NAT ; :: thesis: ( (LifeSpan ((ProgramPart s1),s1)) + k < m implies not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart s1),s1)) + k)))) = halt SCMPDS )
assume (LifeSpan ((ProgramPart s1),s1)) + k < m ; :: thesis: not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart s1),s1)) + k)))) = halt SCMPDS
then A27: 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 A28: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart s1),s1)) + k)))) = halt SCMPDS ; :: thesis: contradiction
A29: Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart s1),s1)) + k)) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,(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))) = halt SCMPDS by A28, A29, A16, A8, A21, A24, A6, SCMPDS_4:84;
hence contradiction by A17, A27, EXTPRO_1:def 14; :: thesis: verum

end;

now

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

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

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

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

end;

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

then consider kk being Nat such that
A31: (LifeSpan ((ProgramPart s1),s1)) + kk = k by NAT_1:10;
kk in NAT by ORDINAL1:def 13;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCMPDS by A26, A30, A31; :: thesis: verum

end;

end;

end;

then A32: for k being Element of NAT st CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCMPDS holds
m <= k ;
ProgramPart s1 halts_on s1 by A4, FUNCT_4:26, SCMPDS_4:def 10;
then A33: Result ((ProgramPart s1),s1) = Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))) by EXTPRO_1:23;
ProgramPart s halts_on s by A3, SCMPDS_4:def 10;
hence LifeSpan ((ProgramPart s),s) = (LifeSpan ((ProgramPart s1),s1)) + (LifeSpan ((ProgramPart ((Initialize (Result ((ProgramPart s1),s1))) +* (stop J))),((Initialize (Result ((ProgramPart s1),s1))) +* (stop J)))) by A33, A25, A32, EXTPRO_1:def 14; :: thesis: verum