let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS
for J being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
let I be Program of SCMPDS ; :: thesis: for J being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
let J be shiftable No-StopCode Program of SCMPDS ; :: thesis: for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
let a be Int_position ; :: thesis: for k1 being Integer st s . (DataLoc (s . a),k1) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
let k1 be Integer; :: thesis: ( s . (DataLoc (s . a),k1) <= 0 & J is_closed_on s & J is_halting_on s implies IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) )
set b = DataLoc (s . a),k1;
assume A1: s . (DataLoc (s . a),k1) <= 0 ; :: thesis: ( not J is_closed_on s or not J is_halting_on s or IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) )
assume A2: J is_closed_on s ; :: thesis: ( not J is_halting_on s or IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) )
assume A3: J is_halting_on s ; :: thesis: IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
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 = Computation (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 (inspos (((card I) + (card J)) + 2));
A4: Initialized (stop J) c= s +* (Initialized (stop J)) by FUNCT_4:26;
A5: s +* (Initialized (stop J)) is halting by A3, Def3;
A6: J is_closed_on s +* (Initialized (stop J)) by A2, Th38;
A7: 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 ;
A8: IC (s +* (Initialized (stop (if>0 a,k1,I,J)))) = inspos 0 by FUNCT_4:26, SCMPDS_5:18;
A9: CurInstr (s +* (Initialized (stop (if>0 a,k1,I,J)))) = a,k1 <=0_goto ((card I) + 2) by A7, Th22;
A10: Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),(0 + 1) = Following (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),0 ) by AMI_1:14
.= Following (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 A7, Th22 ;
A11: card (((a,k1 <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) = (card ((a,k1 <=0_goto ((card I) + 2)) ';' I)) + (card (Goto ((card J) + 1))) by SCMPDS_4:45
.= (card ((a,k1 <=0_goto ((card I) + 2)) ';' I)) + 1 by SCMPDS_5:6
.= ((card I) + 1) + 1 by Th15
.= (card I) + (1 + 1) ;
A12: dom (s | NAT ) = NAT by Th1;
A13: ( not a in dom (Initialized (stop (if>0 a,k1,I,J))) & a in dom s ) by SCMPDS_2:49, SCMPDS_4:31;
A14: ( not DataLoc (s . a),k1 in dom (Initialized (stop (if>0 a,k1,I,J))) & DataLoc (s . a),k1 in dom s ) by SCMPDS_2:49, SCMPDS_4:31;
A15: (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 A13, FUNCT_4:12
.= s . (DataLoc (s . a),k1) by A14, FUNCT_4:12 ;
A16: Shift (stop J),((card I) + 2) c= stop (if>0 a,k1,I,J) by A11, Th24;
stop (if>0 a,k1,I,J) c= s +* (Initialized (stop (if>0 a,k1,I,J))) by FUNCT_4:26, SCMPDS_4:57;
then Shift (stop J),((card I) + 2) c= s +* (Initialized (stop (if>0 a,k1,I,J))) by A16, XBOOLE_1:1;
then A17: Shift (stop J),((card I) + 2) c= Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1 by AMI_1:81;
A18: IC (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) = ICplusConst (s +* (Initialized (stop (if>0 a,k1,I,J)))),((card I) + 2) by A1, A10, A15, SCMPDS_2:68
.= inspos (0 + ((card I) + 2)) by A8, Th23 ;
A19: 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: (s +* (Initialized (stop J))) . a = (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) . a
thus (s +* (Initialized (stop J))) . a = (s +* (Initialized (stop (if>0 a,k1,I,J)))) . a by A19, SCMPDS_4:23
.= (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) . a by A10, SCMPDS_2:68 ; :: thesis: verum

end;

then A20: DataPart (s +* (Initialized (stop J))) = DataPart (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) by SCMPDS_4:23;
A21: CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),((LifeSpan (s +* (Initialized (stop J)))) + 1)) = CurInstr (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),(LifeSpan (s +* (Initialized (stop J))))) by AMI_1:51
.= CurInstr (Computation (s +* (Initialized (stop J))),(LifeSpan (s +* (Initialized (stop J))))) by A4, A6, A17, A18, A20, Th45
.= halt SCMPDS by A5, AMI_1:def 46 ;
then A22: s +* (Initialized (stop (if>0 a,k1,I,J))) is halting by AMI_1:def 20;

now

let l be Element of NAT ; :: thesis: ( l < (LifeSpan (s +* (Initialized (stop J)))) + 1 implies CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),b₁) <> halt SCMPDS )
assume A23: l < (LifeSpan (s +* (Initialized (stop J)))) + 1 ; :: thesis: CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),b₁) <> halt SCMPDS

per cases ( l = 0 or l <> 0 ) ;

suppose l = 0 ; :: thesis: CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),b₁) <> halt SCMPDS

then CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),l) = CurInstr (s +* (Initialized (stop (if>0 a,k1,I,J)))) by AMI_1:13;
hence CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),l) <> halt SCMPDS by A9, Th30; :: thesis: verum

end;

suppose l <> 0 ; :: thesis: not CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),b₁) = halt SCMPDS

then consider n being Nat such that
A24: l = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A25: n < LifeSpan (s +* (Initialized (stop J))) by A23, A24, XREAL_1:8;
assume A26: CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),l) = halt SCMPDS ; :: thesis: contradiction
CurInstr (Computation (s +* (Initialized (stop J))),n) = CurInstr (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),n) by A4, A6, A17, A18, A20, Th45
.= halt SCMPDS by A24, A26, AMI_1:51 ;
hence contradiction by A5, A25, AMI_1:def 46; :: thesis: verum

end;

end;

end;

then for l being Element of NAT st CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),l) = halt SCMPDS holds
(LifeSpan (s +* (Initialized (stop J)))) + 1 <= l ;
then A27: LifeSpan (s +* (Initialized (stop (if>0 a,k1,I,J)))) = (LifeSpan (s +* (Initialized (stop J)))) + 1 by A21, A22, AMI_1:def 46;
A28: DataPart (Result (s +* (Initialized (stop J)))) = DataPart (Computation (s +* (Initialized (stop J))),(LifeSpan (s +* (Initialized (stop J))))) by A5, AMI_1:122
.= DataPart (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),(LifeSpan (s +* (Initialized (stop J))))) by A4, A6, A17, A18, A20, Th45
.= DataPart (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),((LifeSpan (s +* (Initialized (stop J)))) + 1)) by AMI_1:51
.= DataPart (Result (s +* (Initialized (stop (if>0 a,k1,I,J))))) by A22, A27, AMI_1:122 ;
A29: dom (IExec (if>0 a,k1,I,J),s) = the carrier of SCMPDS by AMI_1:79
.= dom ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) by AMI_1:79 ;

now

let x be set ; :: thesis: ( x in dom (IExec (if>0 a,k1,I,J),s) implies (IExec (if>0 a,k1,I,J),s) . b₁ = ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . b₁ )
A30: IExec J,s = (Result (s +* (Initialized (stop J)))) +* (s | NAT ) by SCMPDS_4:def 8;
A31: 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;
assume A32: x in dom (IExec (if>0 a,k1,I,J),s) ; :: thesis: (IExec (if>0 a,k1,I,J),s) . b₁ = ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . b₁
A33: dom (Start-At (inspos (((card I) + (card J)) + 2))) = {(IC SCMPDS )} by FUNCOP_1:19;

per cases ( x is Int_position or x = IC SCMPDS or x is Instruction-Location of SCMPDS ) by A32, SCMPDS_4:20;

suppose A34: x is Int_position ; :: thesis: (IExec (if>0 a,k1,I,J),s) . b₁ = ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . b₁

then x <> IC SCMPDS by SCMPDS_2:52;
then A35: not x in dom (Start-At (inspos (((card I) + (card J)) + 2))) by A33, TARSKI:def 1;

A36: now

assume x in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = x as Instruction-Location of SCMPDS by A12, AMI_1:def 4;
l = x ;
hence contradiction by A34, SCMPDS_2:53; :: thesis: verum

end;

hence (IExec (if>0 a,k1,I,J),s) . x = (Result (s +* (Initialized (stop (if>0 a,k1,I,J))))) . x by A31, FUNCT_4:12
.= (Result (s +* (Initialized (stop J)))) . x by A28, A34, SCMPDS_4:23
.= (IExec J,s) . x by A30, A36, FUNCT_4:12
.= ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . x by A35, FUNCT_4:12 ;
:: thesis: verum

end;

suppose A37: x = IC SCMPDS ; :: thesis: (IExec (if>0 a,k1,I,J),s) . b₁ = ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . b₁

then A38: x in dom (Start-At (inspos (((card I) + (card J)) + 2))) by A33, TARSKI:def 1;

A39: now

assume x in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = x as Instruction-Location of SCMPDS by A12, AMI_1:def 4;
l = x ;
hence contradiction by A37, AMI_1:48; :: thesis: verum

end;

then A40: IC (Result (s +* (Initialized (stop J)))) = IC (IExec J,s) by A30, A37, FUNCT_4:12
.= inspos (card J) by A2, A3, Th48 ;
thus (IExec (if>0 a,k1,I,J),s) . x = (Result (s +* (Initialized (stop (if>0 a,k1,I,J))))) . x by A31, A39, FUNCT_4:12
.= (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),((LifeSpan (s +* (Initialized (stop J)))) + 1)) . x by A22, A27, AMI_1:122
.= IC (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),(LifeSpan (s +* (Initialized (stop J))))) by A37, AMI_1:51
.= (IC (Computation (s +* (Initialized (stop J))),(LifeSpan (s +* (Initialized (stop J)))))) + ((card I) + 2) by A4, A6, A17, A18, A20, Th45
.= (IC (Result (s +* (Initialized (stop J))))) + ((card I) + 2) by A5, AMI_1:122
.= (Start-At ((inspos (card J)) + ((card I) + 2))) . (IC SCMPDS ) by A40, FUNCOP_1:87
.= ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . x by A37, A38, FUNCT_4:14 ; :: thesis: verum

end;

suppose x is Instruction-Location of SCMPDS ; :: thesis: (IExec (if>0 a,k1,I,J),s) . b₁ = ((IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . b₁

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

end;

end;

end;

hence IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) by A29, FUNCT_1:9; :: thesis: verum