let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I, J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being Element of 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 SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being Element of 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 SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( ( for k being Element of 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 Element of 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)))) ) )
I: Initialize s = s by MEMSTR_0:44;
set pI = stop I;
set pIJ = stop (I ';' J);
set P1 = P +* (stop I);
defpred S₁[ Element of 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 Element of 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 A4: P +* (stop I) halts_on s by Def3, I;
A6: for m being Element of 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 Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A7: ( 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]
A8: stop (I ';' J) c= (P +* (stop I)) +* (stop (I ';' J)) by FUNCT_4:25;
A10: Comput ((P +* (stop I)),s,(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) by EXTPRO_1:3;
A11: 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 A12: dom I c= dom (I ';' (J ';' (Stop SCMPDS))) by XBOOLE_1:7;
A14: 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;
A15: IC (Comput ((P +* (stop I)),s,m)) in dom (stop I) by A1, Def2, I;
A16: (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 A18: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) = (stop I) . (IC (Comput ((P +* (stop I)),s,m))) by A15, A16, GRFUNC_1:2;
assume A19: 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 A4, A18, EXTPRO_1:def 15;
then A20: IC (Comput ((P +* (stop I)),s,m)) in dom I by A15, COMPOS_1:51;
A21: ((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 A18
.= I . (IC (Comput ((P +* (stop I)),s,m))) by A20, AFINSQ_1:def 3
.= (stop (I ';' J)) . (IC (Comput ((P +* (stop I)),s,m))) by A20, A11, AFINSQ_1:def 3
.= ((P +* (stop I)) +* (stop (I ';' J))) . (IC (Comput ((P +* (stop I)),s,m))) by A8, A20, A11, A12, GRFUNC_1:2
.= CurInstr (((P +* (stop I)) +* (stop (I ';' J))),(Comput (((P +* (stop I)) +* (stop (I ';' J))),s,m))) by A7, A19, A21, NAT_1:13 ;
hence Comput ((P +* (stop I)),s,(m + 1)) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(m + 1)) by A7, A19, A10, A14, 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 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:14
.= P +* (stop (I ';' J)) by SCMPDS_5:14 ;
thus for k being Element of 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 A24, A25; :: 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 A25, A24;
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