let s be State of ; :: thesis: for I being No-StopCode Program of
for J being Program of st I is_closed_on s & I is_halting_on s holds
IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = inspos (((card I) + (card J)) + 1)
let I be No-StopCode Program of ; :: thesis: for J being Program of st I is_closed_on s & I is_halting_on s holds
IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = inspos (((card I) + (card J)) + 1)
let J be Program of ; :: thesis: ( I is_closed_on s & I is_halting_on s implies IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = inspos (((card I) + (card J)) + 1) )
set m = (LifeSpan (s +* (Initialized (stop I)))) + 1;
set G = Goto ((card J) + 1);
set s2 = s +* (Initialized (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) = inspos (((card I) + (card J)) + 1)
then ( ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 ) by Lm2;
then IC (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) = IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:122
.= inspos (((card I) + (card J)) + 1) by A1, Lm2 ;
hence IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = inspos (((card I) + (card J)) + 1) by SCMPDS_5:22; :: thesis: verum