let s be State of SCMPDS ; :: thesis:
let I be halt-free shiftable Program of SCMPDS ; :: thesis:
let J be shiftable Program of SCMPDS ; :: thesis:
let a be Int_position ; :: thesis:
let k1 be Integer; :: thesis:
set b = DataLoc (s . a),k1;
set G = Goto ((card J) + 1);
set I2 = (I ';' (Goto ((card J) + 1))) ';' J;
set IF = if>0 a,k1,I,J;
set IsIF = Initialized (stop (if>0 a,k1,I,J));
set pI2 = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set II2 = Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set s2 = s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' 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 SAl = Start-At (((card I) + (card J)) + 2),SCMPDS ;
A1: IC (s +* (Initialized (stop (if>0 a,k1,I,J)))) = 0 by FUNCT_4:26, SCMPDS_5:18;
A2: 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 A3: (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 A2, FUNCT_4:12 ;
A4: dom (ProgramPart s) = NAT by AMI_1:143;
A5: 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 ;
then A6: Shift (stop ((I ';' (Goto ((card J) + 1))) ';' J)),1 c= Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),1 by Lm5;
A7: 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 A5, Th22 ;
assume s . (DataLoc (s . a),k1) > 0 ; :: thesis:
then A8: IC (Comput (ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J))))),(s +* (Initialized (stop (if>0 a,k1,I,J)))),1) = succ (IC (s +* (Initialized (stop (if>0 a,k1,I,J))))) by A7, A3, SCMPDS_2:68
.= 0 + 1 by A1 ;
A9: DataPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' J)))) . a = (s +* (Initialized (stop (if>0 a,k1,I,J)))) . a by A9, 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 A7, SCMPDS_2:68 ; :: thesis:

end;

now

let l be Element of NAT ; :: thesis:
assume A18: l < (LifeSpan (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' 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;

A24: now

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

per cases by A28, SCMPDS_4:20;

suppose A29: x is Int_position ; :: thesis:

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

end;

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

end;

suppose x is Element of NAT ; :: thesis:

hence (IExec (if>0 a,k1,I,J),s) . x = ((IExec ((I ';' (Goto ((card J) + 1))) ';' 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 ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS )) by PARTFUN1:def 4 ;
hence IExec (if>0 a,k1,I,J),s = (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ) by A24, FUNCT_1:9
.= ((IExec I,s) +* (Start-At (((card I) + (card J)) + 1),SCMPDS )) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ) by A11, A12, Th47
.= (IExec I,s) +* (Start-At (((card I) + (card J)) + 2),SCMPDS ) by Th14 ;
:: thesis: