let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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:8;
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:26;
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 SCMPDS_5:7;
then n < (card I) + 1 by A9, AFINSQ_1:70;
then A10: n <= card I by INT_1:20;
NPP (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = NPP (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A2, A3, A4, Th39;
then 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 COMPOS_1:230;

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:70;
A13: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:158;
A14: (P +* J) /. (IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = (P +* J) . (IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:158;
thus halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A8, EXTPRO_1:def 14
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A13
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A9, A7, GRFUNC_1:8
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A12, AFINSQ_1:def 4
.= J . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A2, A12, GRFUNC_1:8
.= (P +* J) . (IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A5, A11, A12, FUNCT_4:14
.= CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A14 ; :: thesis: verum

end;

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

NPP (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = NPP (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A2, A3, A4, Th39;
hence IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I by C, COMPOS_1:230; :: 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