let s be State of SCMPDS ; :: thesis:
let I be Program of SCMPDS ; :: thesis:
let J be shiftable No-StopCode Program of SCMPDS ; :: thesis:
let a be Int_position ; :: thesis:
let k1 be Integer; :: thesis:
set b = DataLoc (s . a),k1;
set pJ = stop J;
set IsJ = Initialized (stop J);
set s1 = s +* (Initialized (stop J));
set IF = if<0 a,k1,I,J;
set pIF = stop (if<0 a,k1,I,J);
set IsIF = Initialized (stop (if<0 a,k1,I,J));
set s3 = s +* (Initialized (stop (if<0 a,k1,I,J)));
set s4 = Comput (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(s +* (Initialized (stop (if<0 a,k1,I,J)))),1;
set i = a,k1 >=0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
set iG = ((a,k1 >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1));
set SAl = Start-At (((card I) + (card J)) + 2),SCMPDS ;
A1: if<0 a,k1,I,J = ((a,k1 >=0_goto ((card I) + 2)) ';' (I ';' (Goto ((card J) + 1)))) ';' J by SCMPDS_4:50
.= (a,k1 >=0_goto ((card I) + 2)) ';' ((I ';' (Goto ((card J) + 1))) ';' J) by SCMPDS_4:50 ;
A2: Comput (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(s +* (Initialized (stop (if<0 a,k1,I,J)))),(0 + 1) = Following (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(Comput (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(s +* (Initialized (stop (if<0 a,k1,I,J)))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(s +* (Initialized (stop (if<0 a,k1,I,J)))) by AMI_1:13
.= Exec (a,k1 >=0_goto ((card I) + 2)),(s +* (Initialized (stop (if<0 a,k1,I,J)))) by A1, Th22 ;
A3: not DataLoc (s . a),k1 in dom (Initialized (stop (if<0 a,k1,I,J))) by SCMPDS_4:31;
not a in dom (Initialized (stop (if<0 a,k1,I,J))) by SCMPDS_4:31;
then A4: (s +* (Initialized (stop (if<0 a,k1,I,J)))) . (DataLoc ((s +* (Initialized (stop (if<0 a,k1,I,J)))) . a),k1) = (s +* (Initialized (stop (if<0 a,k1,I,J)))) . (DataLoc (s . a),k1) by FUNCT_4:12
.= s . (DataLoc (s . a),k1) by A3, FUNCT_4:12 ;
A5: IC (s +* (Initialized (stop (if<0 a,k1,I,J)))) = 0 by FUNCT_4:26, SCMPDS_5:18;
A6: dom (s | NAT ) = NAT by Th1;
assume s . (DataLoc (s . a),k1) >= 0 ; :: thesis:
then A7: IC (Comput (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(s +* (Initialized (stop (if<0 a,k1,I,J)))),1) = ICplusConst (s +* (Initialized (stop (if<0 a,k1,I,J)))),((card I) + 2) by A2, A4, SCMPDS_2:69
.= 0 + ((card I) + 2) by A5, Th23 ;
A8: DataPart (s +* (Initialized (stop J))) = DataPart (s +* (Initialized (stop (if<0 a,k1,I,J)))) by SCMPDS_4:24, SCMPDS_4:36;

now

let a be Int_position ; :: thesis:
thus (s +* (Initialized (stop J))) . a = (s +* (Initialized (stop (if<0 a,k1,I,J)))) . a by A8, SCMPDS_4:23
.= (Comput (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(s +* (Initialized (stop (if<0 a,k1,I,J)))),1) . a by A2, SCMPDS_2:69 ; :: thesis:

end;

now

let l be Element of NAT ; :: thesis:
assume A19: l < (LifeSpan (s +* (Initialized (stop J)))) + 1 ; :: thesis:
u: Comput (ProgramPart (s +* (Initialized (stop (if<0 a,k1,I,J))))),(s +* (Initialized (stop (if<0 a,k1,I,J)))),0 = s +* (Initialized (stop (if<0 a,k1,I,J))) by AMI_1:13;

per cases ;

suppose l = 0 ; :: thesis:

end;

suppose l <> 0 ; :: thesis:

end;

A25: now

let x be set ; :: thesis:
A26: IExec J,s = (Result (s +* (Initialized (stop J)))) +* (s | NAT ) by SCMPDS_4:def 8;
A27: IExec (if<0 a,k1,I,J),s = (Result (s +* (Initialized (stop (if<0 a,k1,I,J))))) +* (s | NAT ) by SCMPDS_4:def 8;
A28: dom (Start-At (((card I) + (card J)) + 2),SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
assume A29: x in dom (IExec (if<0 a,k1,I,J),s) ; :: thesis:

per cases by A29, SCMPDS_4:20;

suppose A30: x is Int_position ; :: thesis:

then x <> IC SCMPDS by SCMPDS_2:52;
then A31: not x in dom (Start-At (((card I) + (card J)) + 2),SCMPDS ) by A28, TARSKI:def 1;
A32: not x in dom (s | NAT ) by A6, A30, SCMPDS_2:53;
hence (IExec (if<0 a,k1,I,J),s) . x = (Result (s +* (Initialized (stop (if<0 a,k1,I,J))))) . x by A27, FUNCT_4:12
.= (Result (s +* (Initialized (stop J)))) . x by A24, A30, SCMPDS_4:23
.= (IExec J,s) . x by A26, A32, FUNCT_4:12
.= ((IExec J,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . x by A31, FUNCT_4:12 ;
:: thesis:

end;

suppose A33: x = IC SCMPDS ; :: thesis:

end;

suppose x is Element of NAT ; :: thesis:

hence (IExec (if<0 a,k1,I,J),s) . x = ((IExec J,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) . x by Th26; :: thesis:

end;

dom (IExec (if<0 a,k1,I,J),s) = the carrier of SCMPDS by PARTFUN1:def 4
.= dom ((IExec J,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) by PARTFUN1:def 4 ;
hence IExec (if<0 a,k1,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ) by A25, FUNCT_1:9; :: thesis: