let s be State of ; :: thesis: for I being shiftable No-StopCode Program of
for J being shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) > 0 & I is_closed_on s & I is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
let I be shiftable No-StopCode Program of ; :: thesis: for J being shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) > 0 & I is_closed_on s & I is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
let J be shiftable Program of ; :: thesis: for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) > 0 & I is_closed_on s & I is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec I,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 & I is_closed_on s & I is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
let k1 be Integer; :: thesis: ( s . (DataLoc (s . a),k1) > 0 & I is_closed_on s & I is_halting_on s implies IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) )
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 = Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1;
set i = a,k1 <=0_goto ((card I) + 2);
set SAl = Start-At (inspos (((card I) + (card J)) + 2));
A1: IC (s +* (Initialized (stop (if>0 a,k1,I,J)))) = inspos 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 (s | NAT ) = NAT by Th1;
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= Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1 by Lm5;
A7: 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 A5, Th22 ;
assume s . (DataLoc (s . a),k1) > 0 ; :: thesis: ( not I is_closed_on s or not I is_halting_on s or IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) )
then A8: IC (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) = Next (IC (s +* (Initialized (stop (if>0 a,k1,I,J))))) by A7, A3, SCMPDS_2:68
.= inspos (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: (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) . a = (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) . a
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
.= (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) . a by A7, SCMPDS_2:68 ; :: thesis: verum

end;

then A10: DataPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = DataPart (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1) by SCMPDS_4:23;
assume A11: I is_closed_on s ; :: thesis: ( not I is_halting_on s or IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) )
assume A12: I is_halting_on s ; :: thesis: IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))
then (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s by A11, Th44;
then A13: ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by Def3;
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on s by A11, A12, Th44;
then A14: ( Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) ) by Th38, FUNCT_4:26;
A15: CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),((LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1)) = CurInstr (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) by AMI_1:51
.= CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) by A14, A6, A8, A10, Th45
.= halt SCMPDS by A13, AMI_1:def 46 ;
then A16: ProgramPart (s +* (Initialized (stop (if>0 a,k1,I,J)))) halts_on s +* (Initialized (stop (if>0 a,k1,I,J))) by AMI_1:146;
A17: CurInstr (s +* (Initialized (stop (if>0 a,k1,I,J)))) = a,k1 <=0_goto ((card I) + 2) by A5, Th22;

now

let l be Element of NAT ; :: thesis: ( l < (LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1 implies CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),b₁) <> halt SCMPDS )
assume A18: l < (LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' 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 A17, 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
A19: l = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A20: n < LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) by A18, A19, XREAL_1:8;
assume A21: CurInstr (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),l) = halt SCMPDS ; :: thesis: contradiction
CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),n) = CurInstr (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),n) by A14, A6, A8, A10, Th45
.= halt SCMPDS by A19, A21, AMI_1:51 ;
hence contradiction by A13, A20, 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 ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1 <= l ;
then A22: LifeSpan (s +* (Initialized (stop (if>0 a,k1,I,J)))) = (LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1 by A15, A16, AMI_1:def 46;
A23: DataPart (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) = DataPart (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) by A13, AMI_1:122
.= DataPart (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) by A14, A6, A8, A10, Th45
.= DataPart (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),((LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1)) by AMI_1:51
.= DataPart (Result (s +* (Initialized (stop (if>0 a,k1,I,J))))) by A16, A22, AMI_1:122 ;

A24: 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 ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . b₁ )
A25: 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;
A26: 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;
A27: dom (Start-At (inspos (((card I) + (card J)) + 2))) = {(IC SCMPDS )} by FUNCOP_1:19;
assume A28: x in dom (IExec (if>0 a,k1,I,J),s) ; :: thesis: (IExec (if>0 a,k1,I,J),s) . b₁ = ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . b₁

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

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

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

A31: now

assume x in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = x as Instruction-Location of SCMPDS by A4, AMI_1:def 4;
l = x ;
hence contradiction by A29, 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 A26, FUNCT_4:12
.= (Result (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 (inspos (((card I) + (card J)) + 2)))) . x by A30, FUNCT_4:12 ;
:: thesis: verum

end;

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

A33: now

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

end;

then A34: IC (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) = IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) by A25, A32, FUNCT_4:12
.= inspos (((card I) + (card J)) + 1) by A11, A12, Th46 ;
A35: x in dom (Start-At (inspos (((card I) + (card J)) + 2))) by A27, A32, TARSKI:def 1;
thus (IExec (if>0 a,k1,I,J),s) . x = (Result (s +* (Initialized (stop (if>0 a,k1,I,J))))) . x by A26, A33, FUNCT_4:12
.= (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),((LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1)) . x by A16, A22, AMI_1:122
.= IC (Computation (Computation (s +* (Initialized (stop (if>0 a,k1,I,J)))),1),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) by A32, AMI_1:51
.= (IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))))) + 1 by A14, A6, A8, A10, Th45
.= (IC (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))))) + 1 by A13, AMI_1:122
.= (Start-At ((inspos (((card I) + (card J)) + 1)) + 1)) . (IC SCMPDS ) by A34, FUNCOP_1:87
.= ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . x by A32, A35, FUNCT_4:14 ; :: thesis: verum

end;

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

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

end;

end;

end;

dom (IExec (if>0 a,k1,I,J),s) = the carrier of SCMPDS by AMI_1:79
.= dom ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) by AMI_1:79 ;
hence IExec (if>0 a,k1,I,J),s = (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2))) by A24, FUNCT_1:9
.= ((IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 1)))) +* (Start-At (inspos (((card I) + (card J)) + 2))) by A11, A12, Th47
.= (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) by Th14 ;
:: thesis: verum