let s be State of SCMPDS ; :: thesis: for I being halt-free Program of SCMPDS
for J being Program of SCMPDS st I is_closed_on s & I is_halting_on s holds
IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = ((card I) + (card J)) + 1
let I be halt-free Program of SCMPDS ; :: thesis: for J being Program of SCMPDS st I is_closed_on s & I is_halting_on s holds
IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = ((card I) + (card J)) + 1
let J be Program of SCMPDS ; :: thesis: ( I is_closed_on s & I is_halting_on s implies IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = ((card I) + (card J)) + 1 )
set m = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1;
set G = Goto ((card J) + 1);
set s2 = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J));
assume A1: ( I is_closed_on s & I is_halting_on s ) ; :: thesis: IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = ((card I) + (card J)) + 1
then ( ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) halts_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) & LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 ) by Lm2;
then IC (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = IC (Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by AMI_1:122
.= ((card I) + (card J)) + 1 by A1, Lm2 ;
hence IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = ((card I) + (card J)) + 1 by SCMPDS_5:22; :: thesis: verum