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
IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
let s be State of SCM+FSA; :: thesis: ( I is_closed_on Initialized s & I is_halting_on Initialized s implies IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) )
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)));
assume that
A1: I is_closed_on Initialized s and
A2: I is_halting_on Initialized s ; :: thesis: IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
s +* (Initialized I) = (Initialized s) +* (I +* (Start-At (0,SCM+FSA))) by Th13;
then A3: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by A2, SCMFSA7B:def 8;
( 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 A1, A2, Lm6;
then A4: Result ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))) = 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 EXTPRO_1:23;
then DataPart (Result ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) by A1, A2, Lm6;
then A5: DataPart (Result ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) = DataPart (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) by A3, EXTPRO_1:23
.= DataPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) by Th10 ;
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)))))) = ((card I) + (card J)) + 1 by A1, A2, A4, Lm6
.= IC ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) by FUNCT_4:121 ;
then A6: Result ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) equal_outside NAT by A5, Th6;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then A7: (Result ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) +* (s | NAT) = ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) +* (s | NAT) by A6, FUNCT_7:108;
A8: dom (ProgramPart s) misses dom (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by Th12;
thus IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),s) = (Result ((ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* ((Start-At ((((card I) + (card J)) + 1),SCM+FSA)) +* (s | NAT)) by A7, FUNCT_4:15
.= (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* ((s | NAT) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) by A8, FUNCT_4:36
.= ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by FUNCT_4:15
.= (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by SCMFSA6B:def 1 ; :: thesis: verum