let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1
let I, J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1
let s be State of SCM+FSA; :: thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1 )
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set P2 = P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA));
assume A1: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P ) ; :: thesis: IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1
then ( P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 ) by Lm6;
then IC (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 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)),P,s)) = ((card I) + (card J)) + 1 by Th7; :: thesis: verum