let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS holds
( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )
let s be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS holds
( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )
let I be parahalting Program of SCMPDS; :: thesis: ( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )
set ss = s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),s);
set s1 = Comput (P,s,(LifeSpan ((P +* (stop I)),s)));
set s2 = Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))));
set Ik = IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))));
A1: P +* (stop I) halts_on s by FUNCT_4:26, SCMPDS_4:def 10;
reconsider n = IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) as Element of NAT ;
A2: stop I c= P +* (stop I) by FUNCT_4:26;
A3: IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) in dom (stop I) by FUNCT_4:26, SCMPDS_4:def 9;
X: Initialize s = s by COMPOS_1:78;
A4: (P +* (stop I)) +* (stop I) = P +* (stop I) by A2, FUNCT_4:104;
card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:20;
then n < (card I) + 1 by A3, AFINSQ_1:70;
then A5: n <= card I by INT_1:20;
A6: stop I c= P +* (stop I) by FUNCT_4:26;
assume A7: I c= P ; :: thesis: ( CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )
then NPP (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = NPP (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) by A4, Th29, X;
then A8: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) by COMPOS_1:230;

now

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

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

then A9: n in dom I by AFINSQ_1:70;
thus halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A4, A1, EXTPRO_1:def 14, X
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by PBOOLE:158
.= (stop I) . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A3, A6, GRFUNC_1:8
.= I . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A9, AFINSQ_1:def 4
.= P . (IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) by A7, A8, A9, GRFUNC_1:8
.= CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:158 ; :: thesis: verum

end;

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

NPP (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = NPP (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) by A7, A4, Th29, X;
hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I by C, COMPOS_1:230; :: thesis: verum

end;

end;

end;

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