let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of SCMPDS st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS holds
IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of SCMPDS st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS holds
IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
let I, J be Program of SCMPDS; :: thesis: ( I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS implies IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I )
set ss = Initialize s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),(Initialize s));
set s0 = Initialize s;
set P0 = P +* J;
set s1 = Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set s2 = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set P1 = P +* J;
set P2 = P +* (stop I);
set Ik = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))));
assume that
A2: I c= J and
A3: I is_closed_on s,P and
A4: I is_halting_on s,P ; :: thesis: ( CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS or IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I )
A5: dom I c= dom J by A2, GRFUNC_1:2;
reconsider n = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) as Element of NAT ;
A7: stop I c= P +* (stop I) by FUNCT_4:25;
A8: P +* (stop I) halts_on Initialize s by A4, SCMPDS_6:def 3;
A9: IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom (stop I) by A3, SCMPDS_6:def 2;
card (stop I) = (card I) + 1 by COMPOS_1:55;
then n < (card I) + 1 by A9, AFINSQ_1:66;
then A10: n <= card I by INT_1:7;
A11: IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A2, A3, A4, Th39;

now

per cases ( n < card I or n = card I ) by A10, XXREAL_0:1;

case n < card I ; :: thesis: halt SCMPDS = CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))

then A12: n in dom I by AFINSQ_1:66;
thus halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A8, EXTPRO_1:def 15
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:143
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A9, A7, GRFUNC_1:2
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A12, AFINSQ_1:def 3
.= J . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A2, A12, GRFUNC_1:2
.= (P +* J) . (IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A5, A11, A12, FUNCT_4:13
.= CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:143 ; :: thesis: verum

end;

case n = card I ; :: thesis: IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I

hence IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I by A2, A3, A4, Th39; :: thesis: verum

end;

end;

end;

hence ( CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS or IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I ) ; :: thesis: verum