let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS
for I being halt-free Program of st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (I,P,(Initialize s))) = card I
let s be State of SCMPDS; :: thesis: for I being halt-free Program of st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (I,P,(Initialize s))) = card I
let I be halt-free Program of ; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies IC (IExec (I,P,(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 (IExec (I,P,(Initialize s))) = card I
A3: P +* (stop I) halts_on Initialize s by A2;
thus IC (IExec (I,P,(Initialize s))) = IC (Result ((P +* (stop I)),(Initialize s)))
.= IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A3, EXTPRO_1:23
.= card I by A1, A2, Th20 ; :: thesis: verum