let P, P1 be Instruction-Sequence of SCMPDS; :: thesis: for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds
( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
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 st stop (I ';' J) c= P & P1 = P +* (stop I) holds
( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
let J be parahalting shiftable Program of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds
( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
let s be 0 -started State of SCMPDS; :: thesis: ( stop (I ';' J) c= P & P1 = P +* (stop I) implies ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) )
A1: Initialize s = s by MEMSTR_0:44;
set spJ = stop J;
set sIJ = stop (I ';' J);
set m1 = LifeSpan (P1,s);
set s3 = Initialize (Comput (P1,s,(LifeSpan (P1,s))));
set P3 = P1 +* (stop J);
set m3 = LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))));
assume that
A3: stop (I ';' J) c= P and
A4: P1 = P +* (stop I) ; :: thesis: ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
set s4 = Comput (P,s,(LifeSpan (P1,s)));
set P4 = P;
A7: I c= stop (I ';' J) by Th12;
hence A8: IC (Comput (P,s,(LifeSpan (P1,s)))) = card I by A3, A4, Th30, XBOOLE_1:1; :: thesis: ( DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
reconsider m = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))) as Element of NAT ;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27
.= I +* (Shift ((stop J),(card I))) ;
then A15: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:25;
A16: stop J c= P1 +* (stop J) by FUNCT_4:25;
then A17: P1 +* (stop J) halts_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))) by SCMPDS_4:def 7;
A20: DataPart (Comput (P1,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by MEMSTR_0:45;
I ';' J c= stop (I ';' J) by AFINSQ_1:74;
then P +* (I ';' J) = P by FUNCT_4:98, A3, XBOOLE_1:1;
hence A21: DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by A20, A4, Th33, A1; :: thesis: ( Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
A23: Comput (P,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))) = Comput (P,(Comput (P,s,(LifeSpan (P1,s)))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))) by EXTPRO_1:4;
thus A24: Shift ((stop J),(card I)) c= P by A15, A3, XBOOLE_1:1; :: thesis: LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s)))))
then CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))))) = CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))))) by A23, A16, A8, A21, SCMPDS_4:29;
then A25: CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by A17, EXTPRO_1:def 15;

A26: now

let k be Element of NAT ; :: thesis: ( (LifeSpan (P1,s)) + k < m implies not CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS )
assume (LifeSpan (P1,s)) + k < m ; :: thesis: not CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS
then A27: k < LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))) by XREAL_1:6;
assume A28: CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS ; :: thesis: contradiction
A29: Comput (P,s,((LifeSpan (P1,s)) + k)) = Comput (P,(Comput (P,s,(LifeSpan (P1,s)))),k) by EXTPRO_1:4;
CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),k))) = halt SCMPDS by A28, A29, A16, A8, A21, A24, SCMPDS_4:29;
hence contradiction by A17, A27, EXTPRO_1:def 15; :: thesis: verum

end;

now

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

per cases ( k < LifeSpan (P1,s) or LifeSpan (P1,s) <= k ) ;

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

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

end;

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

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

end;

end;

end;

then A32: for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt SCMPDS holds
m <= k ;
stop I c= P1 by A4, FUNCT_4:25;
then P1 halts_on s by SCMPDS_4:def 7;
then A33: Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by EXTPRO_1:23;
P halts_on s by A3, SCMPDS_4:def 7;
hence LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) by A33, A25, A32, EXTPRO_1:def 15; :: thesis: verum