let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being State of SCMPDS
for I being halt-free Program of SCMPDS
for J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))
let s be State of SCMPDS; :: thesis: for I being halt-free Program of SCMPDS
for J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))
let I be halt-free Program of SCMPDS; :: thesis: for J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))
let J be Program of SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS)) )
set s1 = Initialize s;
set P1 = P +* (stop I);
set m = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1;
set G = Goto ((card J) + 1);
set s2 = Initialize s;
set P2 = P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set l = ((card I) + (card J)) + 1;
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis: IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))
A3: P +* (stop I) halts_on Initialize s by A2, Def3;
( P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on Initialize s & LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s)) = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 ) by A1, A2, Lm3;
then A4: Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s)) = Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)) by EXTPRO_1:23;
then DataPart (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s))) = DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A1, A2, Lm3;
then A5: DataPart (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s))) = DataPart (Result ((P +* (stop I)),(Initialize s))) by A3, EXTPRO_1:23
.= DataPart ((Result ((P +* (stop I)),(Initialize s))) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))) by Th7 ;
IC (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s))) = ((card I) + (card J)) + 1 by A1, A2, A4, Lm3
.= IC ((Result ((P +* (stop I)),(Initialize s))) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))) by FUNCT_4:121 ;
then A6: NPP (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s))) = NPP ((Result ((P +* (stop I)),(Initialize s))) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))) by A5, Th4;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then A7: (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s))) +* (s | NAT) = ((Result ((P +* (stop I)),(Initialize s))) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))) +* (s | NAT) by A6, COMPOS_1:238;
A8: dom (s | NAT) misses dom (Start-At ((((card I) + (card J)) + 1),SCMPDS)) by COMPOS_1:130;
thus IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s))) +* (s | NAT)
.= (Result ((P +* (stop I)),(Initialize s))) +* ((Start-At ((((card I) + (card J)) + 1),SCMPDS)) +* (s | NAT)) by A7, FUNCT_4:15
.= (Result ((P +* (stop I)),(Initialize s))) +* ((s | NAT) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))) by A8, FUNCT_4:36
.= ((Result ((P +* (stop I)),(Initialize s))) +* (s | NAT)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS)) by FUNCT_4:15
.= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS)) ; :: thesis: verum