let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free Program of
for J being Program of 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 0 -started State of SCMPDS; :: thesis: for I being halt-free Program of
for J being Program of 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 ; :: thesis: for J being Program of 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 ; :: 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 P1 = P +* (stop I);
set m = (LifeSpan ((P +* (stop I)),s)) + 1;
set G = Goto ((card J) + 1);
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))
Initialize s = s by MEMSTR_0:44;
then A3: P +* (stop I) halts_on s by A2;
( P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on s & LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + 1 ) by A1, A2, Lm3;
then A4: Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1)) by EXTPRO_1:23;
then DataPart (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s)) = DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by A1, A2, Lm3;
then A5: DataPart (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s)) = DataPart (Result ((P +* (stop I)),s)) by A3, EXTPRO_1:23
.= DataPart ((Result ((P +* (stop I)),s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))) by MEMSTR_0:79 ;
IC (Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s)) = ((card I) + (card J)) + 1 by A1, A2, A4, Lm3
.= IC ((Result ((P +* (stop I)),s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))) by FUNCT_4:113 ;
then A6: Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = (Result ((P +* (stop I)),s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS)) by A5, MEMSTR_0:78;
thus IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = Result ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s)
.= (Result ((P +* (stop I)),s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS)) by A6
.= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS)) ; :: thesis: verum