let I, J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_closed_on Initialized s & I is_halting_on Initialized s holds
IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s)) = ((card I) + (card J)) + 1
let s be State of SCM+FSA; :: thesis: ( I is_closed_on Initialized s & I is_halting_on Initialized s implies IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s)) = ((card I) + (card J)) + 1 )
set s2 = s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)));
assume A1: ( I is_closed_on Initialized s & I is_halting_on Initialized s ) ; :: thesis: IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s)) = ((card I) + (card J)) + 1
then ( ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))) halts_on s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))) & LifeSpan ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))) = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 2 ) by Lm6;
then IC (Result ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) = IC (Comput ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 2))) by EXTPRO_1:23
.= ((card I) + (card J)) + 1 by A1, Lm6 ;
hence IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s)) = ((card I) + (card J)) + 1 by Th7; :: thesis: verum