let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st 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 be really-closed Program of SCM+FSA; :: thesis: for J being Program of SCM+FSA
for s being State of SCM+FSA st 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 J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st 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_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 = Initialized s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
assume A1: 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 Initialized s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s)) = (LifeSpan ((P +* I),(Initialized s))) + 2 ) by Lm6;
then IC (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 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 SCMFSA6B:def 1; :: thesis: verum