let P be Instruction-Sequence of SCMPDS; :: thesis: for I being halt-free Program of
for s being State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
let I be halt-free Program of ; :: thesis: for s being State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
let s be State of SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I )
set s1 = Initialize s;
set P1 = P +* (stop I);
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis: IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
set Css = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
reconsider n = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) as Nat ;
A3: stop I c= P +* (stop I) by FUNCT_4:25;
I c= stop I by AFINSQ_1:74;
then A4: I c= P +* (stop I) by A3, XBOOLE_1:1;
A5: P +* (stop I) halts_on Initialize s by A2;

now :: thesis: not IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom I

A6: (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:143;
assume A7: IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom I ; :: thesis: contradiction
then 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 A4, GRFUNC_1:2
.= CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A6
.= halt SCMPDS by A5, EXTPRO_1:def 15 ;
hence contradiction by A7, COMPOS_1:def 27; :: thesis: verum

end;

then A8: n >= card I by AFINSQ_1:66;
A9: card (stop I) = (card I) + 1 by COMPOS_1:55;
IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom (stop I) by A1;
then n < (card I) + 1 by A9, AFINSQ_1:66;
then n <= card I by NAT_1:13;
then IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I by A8, XXREAL_0:1;
hence IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I ; :: thesis: verum