let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of 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 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 ; :: 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 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: stop I c= P +* (stop I) by FUNCT_4:25;
then A2: P +* (stop I) halts_on s by SCMPDS_4:def 7;
reconsider n = IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) as Nat ;
A3: IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) in dom (stop I) by A1, SCMPDS_4:def 6;
A4: Initialize s = s by MEMSTR_0:44;
card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17;
then n < (card I) + 1 by A3, AFINSQ_1:66;
then A5: n <= card I by INT_1:7;
A6: stop I c= P +* (stop I) by FUNCT_4:25;
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 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 Th13, A4;

now :: thesis: ( ( n < card I & halt SCMPDS = CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) ) or ( n = card I & IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) )

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:66;
thus halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A2, A4, EXTPRO_1:def 15
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by PBOOLE:143
.= (stop I) . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A3, A6, GRFUNC_1:2
.= I . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A9, AFINSQ_1:def 3
.= P . (IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) by A7, A8, A9, GRFUNC_1:2
.= CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143 ; :: thesis: verum

end;

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

hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I by A7, Th13, A4; :: 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