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 AMI_1:122
.= ((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