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