let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
let I, J be Program of SCMPDS; :: thesis:
let s be State of SCMPDS; :: thesis:
assume A1: I is_closed_on s,P ; :: thesis:
set pI = stop I;
set pIJ = stop (I ';' J);
set s1 = Initialize s;
set P1 = P +* (stop I);
set IL = NAT ;
defpred S₁[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies NPP (Comput ((P +* (stop I)),(Initialize s),$1)) = NPP (Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),$1)) );
assume I is_halting_on s,P ; :: thesis:
then A4: P +* (stop I) halts_on Initialize s by Def3;
A6: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

set JS = J ';' (Stop SCMPDS);
set S1 = Initialize s;
set S2 = Initialize (Initialize s);
set E1 = P +* (stop I);
set E2 = (P +* (stop I)) +* (stop (I ';' J));
let m be Element of NAT ; :: thesis:
assume A7: ( m <= LifeSpan ((P +* (stop I)),(Initialize s)) implies NPP (Comput ((P +* (stop I)),(Initialize s),m)) = NPP (Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),m)) ) ; :: thesis:
A8: stop (I ';' J) c= (P +* (stop I)) +* (stop (I ';' J)) by FUNCT_4:26;
A10: Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m)))),(Comput ((P +* (stop I)),(Initialize s),m))) ;
A11: stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS)
.= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30 ;
dom (I ';' (J ';' (Stop SCMPDS))) = dom (I +* (Shift ((J ';' (Stop SCMPDS)),(card I))))
.= (dom I) \/ (dom (Shift ((J ';' (Stop SCMPDS)),(card I)))) by FUNCT_4:def 1 ;
then A12: dom I c= dom (I ';' (J ';' (Stop SCMPDS))) by XBOOLE_1:7;
A14: Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),(m + 1)) = Following (((P +* (stop I)) +* (stop (I ';' J))),(Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),m))) by EXTPRO_1:4
.= Exec ((CurInstr (((P +* (stop I)) +* (stop (I ';' J))),(Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),m)))),(Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),m))) ;
A15: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I) by A1, Def2;
A16: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),(Initialize s),m))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by PBOOLE:158;
stop I c= P +* (stop I) by FUNCT_4:26;
then A18: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m))) = (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A15, A16, GRFUNC_1:8;
assume A19: m + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis:
then m < LifeSpan ((P +* (stop I)),(Initialize s)) by NAT_1:13;
then (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) <> halt SCMPDS by A4, A18, EXTPRO_1:def 14;
then A20: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom I by A15, SCMPDS_5:3;
A21: ((P +* (stop I)) +* (stop (I ';' J))) /. (IC (Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),m))) = ((P +* (stop I)) +* (stop (I ';' J))) . (IC (Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),m))) by PBOOLE:158;
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m))) = (I ';' (Stop SCMPDS)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A18
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A20, AFINSQ_1:def 4
.= (stop (I ';' J)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A20, A11, AFINSQ_1:def 4
.= ((P +* (stop I)) +* (stop (I ';' J))) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A8, A20, A11, A12, GRFUNC_1:8
.= CurInstr (((P +* (stop I)) +* (stop (I ';' J))),(Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),m))) by A7, A19, A21, COMPOS_1:230, NAT_1:13 ;
hence NPP (Comput ((P +* (stop I)),(Initialize s),(m + 1))) = NPP (Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize (Initialize s)),(m + 1))) by A7, A19, A10, A14, NAT_1:13, SCMPDS_4:15; :: thesis:

end;

( Comput ((P +* (stop I)),(Initialize s),0) = Initialize s & Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize s),0) = Initialize (Initialize s) ) by EXTPRO_1:3;
then A23: S₁[ 0 ] ;
A24: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A23, A6);
A25: (P +* (stop I)) +* (stop (I ';' J)) = P +* ((stop I) +* (stop (I ';' J))) by FUNCT_4:15
.= P +* (stop (I ';' J)) by SCMPDS_5:17 ;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume Z: k <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis:
NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) by A24, A25, Z;
hence IC (Comput ((P +* (stop I)),(Initialize s),k)) = IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) by COMPOS_1:230; :: thesis:

end;

NPP (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = NPP (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A25, A24;
hence DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by COMPOS_1:138; :: thesis: