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
IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (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 IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 1))) )
set s1 = s +* (Initialized I);
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: IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 1)))
A2: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by Th13;
A3: dom (s | NAT ) = NAT by Th3;
A4: s +* (Initialized I) is halting by A1, A2, SCMFSA7B:def 8;
( 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 A1, Lm6;
then A5: Result (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) = Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2) by AMI_1:122;
then DataPart (Result (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))))) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) by A1, Lm6;
then A6: DataPart (Result (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))))) = DataPart (Result (s +* (Initialized I))) by A4, AMI_1:122
.= DataPart ((Result (s +* (Initialized I))) +* (Start-At (insloc (((card I) + (card J)) + 1)))) by Th10 ;
IC (Result (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))))) = insloc (((card I) + (card J)) + 1) by A1, A5, Lm6
.= IC ((Result (s +* (Initialized I))) +* (Start-At (insloc (((card I) + (card J)) + 1)))) by AMI_1:111 ;
then Result (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),(Result (s +* (Initialized I))) +* (Start-At (insloc (((card I) + (card J)) + 1))) equal_outside NAT by A6, Th6;
then A7: (Result (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))))) +* (s | NAT ) = ((Result (s +* (Initialized I))) +* (Start-At (insloc (((card I) + (card J)) + 1)))) +* (s | NAT ) by A3, FUNCT_7:108;
A8: dom (s | NAT ) misses dom (Start-At (insloc (((card I) + (card J)) + 1))) by Th12;
thus IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )),s = (Result (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Result (s +* (Initialized I))) +* ((Start-At (insloc (((card I) + (card J)) + 1))) +* (s | NAT )) by A7, FUNCT_4:15
.= (Result (s +* (Initialized I))) +* ((s | NAT ) +* (Start-At (insloc (((card I) + (card J)) + 1)))) by A8, FUNCT_4:36
.= ((Result (s +* (Initialized I))) +* (s | NAT )) +* (Start-At (insloc (((card I) + (card J)) + 1))) by FUNCT_4:15
.= (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 1))) by SCMFSA6B:def 1 ; :: thesis: verum