let P be Instruction-Sequence of SCMPDS; :: thesis: for I being halt-free Program of SCMPDS
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 SCMPDS; :: 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
A2: I is_closed_on s,P and
A3: 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 Element of NAT ;
XX: 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 XX, XBOOLE_1:1;
A5: P +* (stop I) halts_on Initialize s by A3, Def3;

now

A7: (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 A8: 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 A7
.= halt SCMPDS by A5, EXTPRO_1:def 15 ;
hence contradiction by A8, COMPOS_1:def 25; :: thesis: verum

end;

then A9: n >= card I by AFINSQ_1:66;
A10: 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 A2, Def2;
then n < (card I) + 1 by A10, 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 A9, XXREAL_0:1;
hence IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I ; :: thesis: verum