let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being State of SCMPDS
for I being halt-free Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (I,P,s)) = card I
let s be State of SCMPDS; :: thesis: for I being halt-free Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (I,P,s)) = card I
let I be halt-free Program of SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies IC (IExec (I,P,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 (IExec (I,P,s)) = card I
A4: P +* (stop I) halts_on Initialize s by A3, Def3;
thus IC (IExec (I,P,s)) = IC (Result ((P +* (stop I)),(Initialize s))) by SCMPDS_5:22
.= IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A4, EXTPRO_1:23
.= card I by A2, A3, Th43 ; :: thesis: verum