let P, P2, P1 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
let I be halt-free Program of SCMPDS; :: thesis:
let J be shiftable Program of SCMPDS; :: thesis:
let s, s1, s2 be State of SCMPDS; :: thesis:
set spJ = stop J;
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set m1 = LifeSpan (P1,s1);
set sm = Comput (P1,s1,(LifeSpan (P1,s1)));
set s3 = Initialize (Comput (P1,s1,(LifeSpan (P1,s1))));
set P3 = P1 +* (stop J);
set m3 = LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))));
set sE = IExec (I,P,s);
SS: Start-At (0,SCMPDS) c= Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))) by FUNCT_4:26;
assume that
A2: I is_closed_on s,P and
A3: I is_halting_on s,P and
A4: J is_closed_on IExec (I,P,s),P and
A5: J is_halting_on IExec (I,P,s),P and
A6: s2 = Initialize s and
A7: s1 = Initialize s and
B6: P2 = P +* (stop (I ';' J)) and
B7: P1 = P +* (stop I) ; :: thesis:
A9: DataPart (Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))) = DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) by COMPOS_1:80;
set s4 = Comput (P2,s2,(LifeSpan (P1,s1)));
set P4 = P2;
thus A10: IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = card I by A2, A3, A6, A7, Th17, Th44, B6, B7; :: thesis:
A17: stop J c= P1 +* (stop J) by FUNCT_4:26;
A18: DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))) by A9;
XX: I ';' (J ';' (Stop SCMPDS)) = stop (I ';' J) by AFINSQ_1:30;
s2 = Initialize s by A6;
then Comput (P2,s2,(LifeSpan (P1,s1))) = Comput ((P +* (I ';' (J ';' (Stop SCMPDS)))),(Initialize s),(LifeSpan (P1,s1))) by XX, B6;
then NPP (Comput (P1,s1,(LifeSpan (P1,s1)))) = NPP (Comput (P2,s2,(LifeSpan (P1,s1)))) by A2, A3, A7, Th38, B7;
hence A19: DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) = DataPart (Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))) by A18, COMPOS_1:138; :: thesis:
reconsider m = (LifeSpan (P1,s1)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))))) as Element of NAT ;
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30
.= I +* (Shift ((stop J),(card I))) ;
then A21: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:26;
stop (I ';' J) c= P2 by B6, FUNCT_4:26;
then Shift ((stop J),(card I)) c= P2 by A21, XBOOLE_1:1;
hence A22: Shift ((stop J),(card I)) c= P2 ; :: thesis:
J is_halting_on Comput (P1,s1,(LifeSpan (P1,s1))),P1 by A3, A4, A5, A7, Th42, B7;
then A23: P1 +* (stop J) halts_on Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))) by SCMPDS_6:def 3;
A25: Comput (P2,s2,((LifeSpan (P1,s1)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))))))) = Comput (P2,(Comput (P2,s2,(LifeSpan (P1,s1)))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))))))) by EXTPRO_1:5;
J is_closed_on Comput (P1,s1,(LifeSpan (P1,s1))),P1 by A3, A4, A5, A7, Th42, B7;
then A28: J is_closed_on Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))),P1 +* (stop J) by SCMPDS_6:38;
then CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))))))))) = CurInstr (P2,(Comput (P2,(Comput (P2,s2,(LifeSpan (P1,s1)))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))))))))) by A17, A10, A19, A22, SCMPDS_6:45, SS;
then CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))))))))) = CurInstr (P2,(Comput (P2,s2,((LifeSpan (P1,s1)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))))))))) by A25;
then A29: CurInstr (P2,(Comput (P2,s2,m))) = halt SCMPDS by A23, EXTPRO_1:def 14;

A30: now

let k be Element of NAT ; :: thesis:
assume (LifeSpan (P1,s1)) + k < m ; :: thesis:
then A31: k < LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1)))))) by XREAL_1:8;
assume A32: CurInstr (P2,(Comput (P2,s2,((LifeSpan (P1,s1)) + k)))) = halt SCMPDS ; :: thesis:
A36: Comput (P2,s2,((LifeSpan (P1,s1)) + k)) = Comput (P2,(Comput (P2,s2,(LifeSpan (P1,s1)))),k) by EXTPRO_1:5;
CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s1,(LifeSpan (P1,s1))))),k))) = CurInstr (P2,(Comput (P2,(Comput (P2,s2,(LifeSpan (P1,s1)))),k))) by A17, A28, A10, A19, A22, SCMPDS_6:45, SS
.= halt SCMPDS by A32, A36 ;
hence contradiction by A23, A31, EXTPRO_1:def 14; :: thesis:

end;

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

suppose k < LifeSpan (P1,s1) ; :: thesis:

hence CurInstr (P2,(Comput (P2,s2,k))) <> halt SCMPDS by A2, A3, A6, A7, Th46, B6, B7; :: thesis:

end;

suppose LifeSpan (P1,s1) <= k ; :: thesis:

then consider kk being Nat such that
A39: (LifeSpan (P1,s1)) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
(LifeSpan (P1,s1)) + kk = k by A39;
hence CurInstr (P2,(Comput (P2,s2,k))) <> halt SCMPDS by A30, A37; :: thesis:

end;

end;

end;

then A40: for k being Element of NAT st CurInstr (P2,(Comput (P2,s2,k))) = halt SCMPDS holds
m <= k ;
A41: P1 halts_on s1 by A3, A7, SCMPDS_6:def 3, B7;
A42: Result (P1,s1) = Comput (P1,s1,(LifeSpan (P1,s1))) by A41, EXTPRO_1:23;
I ';' J is_halting_on s,P by A2, A3, A4, A5, Th43;
then P2 halts_on s2 by A6, SCMPDS_6:def 3, B6;
then LifeSpan (P2,s2) = m by A29, A40, EXTPRO_1:def 14;
hence LifeSpan (P2,s2) = (LifeSpan (P1,s1)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s1))))) by A42; :: thesis: