let s be State of ; :: thesis: for I being No-StopCode Program of
for J being Program of 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 (inspos (((card I) + (card J)) + 1)))
let I be No-StopCode Program of ; :: thesis: for J being Program of 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 (inspos (((card I) + (card J)) + 1)))
let J be Program of ; :: 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 (inspos (((card I) + (card J)) + 1))) )
set s1 = s +* (Initialized (stop I));
set m = (LifeSpan (s +* (Initialized (stop I)))) + 1;
set G = Goto ((card J) + 1);
set s2 = s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)));
set l = inspos (((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 (inspos (((card I) + (card J)) + 1)))
A3: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by A2, Def3;
( ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 ) by A1, A2, Lm2;
then A4: Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) by AMI_1:122;
then DataPart (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) = DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by A1, A2, Lm2;
then A5: DataPart (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) = DataPart (Result (s +* (Initialized (stop I)))) by A3, AMI_1:122
.= DataPart ((Result (s +* (Initialized (stop I)))) +* (Start-At (inspos (((card I) + (card J)) + 1)))) by Th7 ;
IC (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) = inspos (((card I) + (card J)) + 1) by A1, A2, A4, Lm2
.= IC ((Result (s +* (Initialized (stop I)))) +* (Start-At (inspos (((card I) + (card J)) + 1)))) by AMI_1:111 ;
then A6: Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(Result (s +* (Initialized (stop I)))) +* (Start-At (inspos (((card I) + (card J)) + 1))) equal_outside NAT by A5, Th4;
dom (s | NAT ) = NAT by Th1;
then A7: (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) +* (s | NAT ) = ((Result (s +* (Initialized (stop I)))) +* (Start-At (inspos (((card I) + (card J)) + 1)))) +* (s | NAT ) by A6, FUNCT_7:108;
A8: dom (s | NAT ) misses dom (Start-At (inspos (((card I) + (card J)) + 1))) by Th10;
thus IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) +* (s | NAT ) by SCMPDS_4:def 8
.= (Result (s +* (Initialized (stop I)))) +* ((Start-At (inspos (((card I) + (card J)) + 1))) +* (s | NAT )) by A7, FUNCT_4:15
.= (Result (s +* (Initialized (stop I)))) +* ((s | NAT ) +* (Start-At (inspos (((card I) + (card J)) + 1)))) by A8, FUNCT_4:36
.= ((Result (s +* (Initialized (stop I)))) +* (s | NAT )) +* (Start-At (inspos (((card I) + (card J)) + 1))) by FUNCT_4:15
.= (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 1))) by SCMPDS_4:def 8 ; :: thesis: verum