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) ";" ()),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) ";" ()),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) ";" ()),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) ";" ()),P,s)) = ((card I) + (card J)) + 1 )
set s2 = Initialized s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ());
assume A1: I is_halting_on Initialized s,P ; :: thesis: IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s)) = ((card I) + (card J)) + 1
then ( P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ()) halts_on Initialized s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),()) = (LifeSpan ((P +* I),())) + 2 ) by Lm6;
then IC (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),())) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(),((LifeSpan ((P +* I),())) + 2))) by EXTPRO_1:23
.= ((card I) + (card J)) + 1 by ;
hence IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s)) = ((card I) + (card J)) + 1 by SCMFSA6B:def 1; :: thesis: verum