let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS holds
IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I

let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS holds
IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I

let I, J be Program of ; :: thesis: ( I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS implies IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I )
set ss = Initialize s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),());
set s0 = Initialize s;
set P0 = P +* J;
set s1 = Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())));
set s2 = Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())));
set P1 = P +* J;
set P2 = P +* (stop I);
set Ik = IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))));
assume that
A1: I c= J and
A2: I is_closed_on s,P and
A3: I is_halting_on s,P ; :: thesis: ( CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS or IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I )
A4: dom I c= dom J by ;
reconsider n = IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))) as Nat ;
A5: stop I c= P +* (stop I) by FUNCT_4:25;
A6: P +* (stop I) halts_on Initialize s by ;
A7: IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))) in dom (stop I) by ;
card (stop I) = (card I) + 1 by COMPOS_1:55;
then n < (card I) + 1 by ;
then A8: n <= card I by INT_1:7;
A9: IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))) by A1, A2, A3, Th18;
now :: thesis: ( ( n < card I & halt SCMPDS = CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) ) or ( n = card I & IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I ) )
per cases ( n < card I or n = card I ) by ;
case n < card I ; :: thesis: halt SCMPDS = CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))))
then A10: n in dom I by AFINSQ_1:66;
thus halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))) by
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))) by PBOOLE:143
.= (stop I) . (IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))) by
.= I . (IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))) by
.= J . (IC (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),()))))) by
.= (P +* J) . (IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) by
.= CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) by PBOOLE:143 ; :: thesis: verum
end;
case n = card I ; :: thesis: IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I
hence IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I by A1, A2, A3, Th18; :: thesis: verum
end;
end;
end;
hence ( CurInstr ((P +* J),(Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),()))))) = halt SCMPDS or IC (Comput ((P +* J),(),(LifeSpan ((P +* (stop I)),())))) = card I ) ; :: thesis: verum