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 & I is_halting_on s holds
IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (IExec I,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 & I is_halting_on s holds
IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )
let J be Program of SCMPDS ; :: thesis: ( I is_closed_on s & I is_halting_on s implies IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 1),SCMPDS ) )
set s1 = (Initialize s) +* (stop I);
set m = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1;
set G = Goto ((card J) + 1);
set s2 = (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set l = ((card I) + (card J)) + 1;
assume that
A1: I is_closed_on s and
A2: I is_halting_on s ; :: thesis: IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )
A3: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A2, Def3;
( ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) halts_on (Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) & LifeSpan (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 ) by A1, A2, Lm2;
then A4: Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))) = Comput (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) by AMI_1:122;
then DataPart (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A1, A2, Lm2;
then A5: DataPart (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = DataPart (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by A3, AMI_1:122
.= DataPart ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )) by Th7 ;
IC (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = ((card I) + (card J)) + 1 by A1, A2, A4, Lm2
.= IC ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )) by FUNCT_4:121 ;
then A6: Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (Start-At (((card I) + (card J)) + 1),SCMPDS ) equal_outside NAT by A5, Th4;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then A7: (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) +* (s | NAT ) = ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )) +* (s | NAT ) by A6, FUNCT_7:108;
A8: dom (ProgramPart s) misses dom (Start-At (((card I) + (card J)) + 1),SCMPDS ) by Th10;
thus IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (Result (ProgramPart ((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((Initialize s) +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) +* (s | NAT )
.= (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* ((Start-At (((card I) + (card J)) + 1),SCMPDS ) +* (s | NAT )) by A7, FUNCT_4:15
.= (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* ((s | NAT ) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )) by A8, FUNCT_4:36
.= ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (s | NAT )) +* (Start-At (((card I) + (card J)) + 1),SCMPDS ) by FUNCT_4:15
.= (IExec I,s) +* (Start-At (((card I) + (card J)) + 1),SCMPDS ) ; :: thesis: verum