let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free Program of
for J being Program of st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free Program of
for J being Program of st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1
let I be halt-free Program of ; :: thesis: for J being Program of st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1
let J be Program of ; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1 )
set m = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1;
set G = Goto ((card J) + 1);
set P2 = P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J));
A1: Initialize s = s by MEMSTR_0:44;
assume A2: ( I is_closed_on s,P & I is_halting_on s,P ) ; :: thesis: IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1
then ( P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on s & LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 ) by Lm3, A1;
then IC (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s)) = IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) by EXTPRO_1:23
.= ((card I) + (card J)) + 1 by A2, Lm3, A1 ;
hence IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1 ; :: thesis: verum