let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I, J being Program of st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) )
let s be 0 -started State of SCMPDS; :: thesis: for I, J being Program of st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) )
let I, J be Program of ; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( ( for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) ) )
assume A1: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or ( ( for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) ) )
A2: Initialize s = s by MEMSTR_0:44;
set pI = stop I;
set pIJ = stop (I ';' J);
set P1 = P +* (stop I);
defpred S₁[ Nat] means ( $1 <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,$1) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,$1) );
assume I is_halting_on s,P ; :: thesis: ( ( for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) )
then A3: P +* (stop I) halts_on s by A2;
A4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

set JS = J ';' (Stop SCMPDS);
set E2 = (P +* (stop I)) +* (stop (I ';' J));
let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: ( m <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,m) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,m) ) ; :: thesis: S₁[m + 1]
A6: stop (I ';' J) c= (P +* (stop I)) +* (stop (I ';' J)) by FUNCT_4:25;
A7: Comput ((P +* (stop I)),s,(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) by EXTPRO_1:3;
A8: stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS)
.= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27 ;
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 A9: dom I c= dom (I ';' (J ';' (Stop SCMPDS))) by XBOOLE_1:7;
A10: Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(m + 1)) = Following (((P +* (stop I)) +* (stop (I ';' J))),(Comput (((P +* (stop I)) +* (stop (I ';' J))),s,m))) by EXTPRO_1:3;
A11: IC (Comput ((P +* (stop I)),s,m)) in dom (stop I) by A1, A2;
A12: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),s,m))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,m))) by PBOOLE:143;
stop I c= P +* (stop I) by FUNCT_4:25;
then A13: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) = (stop I) . (IC (Comput ((P +* (stop I)),s,m))) by A11, A12, GRFUNC_1:2;
assume A14: m + 1 <= LifeSpan ((P +* (stop I)),s) ; :: thesis: Comput ((P +* (stop I)),s,(m + 1)) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(m + 1))
then m < LifeSpan ((P +* (stop I)),s) by NAT_1:13;
then (stop I) . (IC (Comput ((P +* (stop I)),s,m))) <> halt SCMPDS by A3, A13, EXTPRO_1:def 15;
then A15: IC (Comput ((P +* (stop I)),s,m)) in dom I by A11, COMPOS_1:51;
A16: ((P +* (stop I)) +* (stop (I ';' J))) /. (IC (Comput (((P +* (stop I)) +* (stop (I ';' J))),s,m))) = ((P +* (stop I)) +* (stop (I ';' J))) . (IC (Comput (((P +* (stop I)) +* (stop (I ';' J))),s,m))) by PBOOLE:143;
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) = (I ';' (Stop SCMPDS)) . (IC (Comput ((P +* (stop I)),s,m))) by A13
.= I . (IC (Comput ((P +* (stop I)),s,m))) by A15, AFINSQ_1:def 3
.= (stop (I ';' J)) . (IC (Comput ((P +* (stop I)),s,m))) by A15, A8, AFINSQ_1:def 3
.= ((P +* (stop I)) +* (stop (I ';' J))) . (IC (Comput ((P +* (stop I)),s,m))) by A6, A15, A8, A9, GRFUNC_1:2
.= CurInstr (((P +* (stop I)) +* (stop (I ';' J))),(Comput (((P +* (stop I)) +* (stop (I ';' J))),s,m))) by A5, A14, A16, NAT_1:13 ;
hence Comput ((P +* (stop I)),s,(m + 1)) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(m + 1)) by A5, A14, A7, A10, NAT_1:13; :: thesis: verum

end;

( Comput ((P +* (stop I)),s,0) = s & Comput (((P +* (stop I)) +* (stop (I ';' J))),s,0) = s ) by EXTPRO_1:2;
then A17: S₁[ 0 ] ;
A18: for m being Nat holds S₁[m] from NAT_1:sch 2(A17, A4);
A19: (P +* (stop I)) +* (stop (I ';' J)) = P +* ((stop I) +* (stop (I ';' J))) by FUNCT_4:14
.= P +* (stop (I ';' J)) by SCMPDS_5:14 ;
thus for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) by A18, A19; :: thesis: DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s))))
Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) = Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s))) by A19, A18;
hence DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) ; :: thesis: verum