let s be State of SCMPDS ; :: thesis: for I being halt-free shiftable Program of SCMPDS
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),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )
let I be halt-free shiftable Program of SCMPDS ; :: 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),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )
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),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )
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),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS ) )
set b = DataLoc (s . a),k1;
set IF = if>=0 a,k1,I;
set pIF = stop (if>=0 a,k1,I);
set pI = stop I;
set s2 = (Initialize s) +* (stop I);
set s3 = (Initialize s) +* (stop (if>=0 a,k1,I));
set s4 = Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1;
set i = a,k1 >=0_goto 2;
set j = goto ((card I) + 1);
set SAl = Start-At ((card I) + 2),SCMPDS ;
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by SCMPDS_4:5;
I2: s +* (Initialize (stop (if>=0 a,k1,I))) = (Initialize s) +* (stop (if>=0 a,k1,I)) by SCMPDS_4:5;
A1: if>=0 a,k1,I = (a,k1 >=0_goto 2) ';' ((goto ((card I) + 1)) ';' I) by SCMPDS_4:52;
A2: Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),(0 + 1) = Following (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))) by AMI_1:13
.= Exec (a,k1 >=0_goto 2),((Initialize s) +* (stop (if>=0 a,k1,I))) by A1, Th22, I2 ;
A3: not DataLoc (s . a),k1 in dom (Initialize (stop (if>=0 a,k1,I))) by SCMPDS_4:31;
not a in dom (Initialize (stop (if>=0 a,k1,I))) by SCMPDS_4:31;
then A4: ((Initialize s) +* (stop (if>=0 a,k1,I))) . (DataLoc (((Initialize s) +* (stop (if>=0 a,k1,I))) . a),k1) = ((Initialize s) +* (stop (if>=0 a,k1,I))) . (DataLoc (s . a),k1) by I2, FUNCT_4:12
.= s . (DataLoc (s . a),k1) by A3, I2, FUNCT_4:12 ;
A5: IC ((Initialize s) +* (stop (if>=0 a,k1,I))) = 0 by I2, FUNCT_4:26, SCMPDS_5:18;
A6: ( Initialize (stop I) c= (Initialize s) +* (stop I) & Shift (stop I),2 c= Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1 ) by Lm6, I1, FUNCT_4:26;
A7: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (if>=0 a,k1,I))) by FUNCT_7:134, SCMPDS_4:24;

now

let a be Int_position ; :: thesis: ((Initialize s) +* (stop I)) . a = (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) . a
thus ((Initialize s) +* (stop I)) . a = ((Initialize s) +* (stop (if>=0 a,k1,I))) . a by A7, SCMPDS_4:23
.= (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) . a by A2, SCMPDS_2:69 ; :: thesis: verum

end;

then A8: DataPart ((Initialize s) +* (stop I)) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) by SCMPDS_4:23;
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),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS ) )
then A9: IC (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) = ICplusConst ((Initialize s) +* (stop (if>=0 a,k1,I))),2 by A2, A4, SCMPDS_2:69
.= 0 + 2 by A5, Th23 ;
A10: dom (ProgramPart s) = NAT by COMPOS_1:34;
assume A11: I is_closed_on s ; :: thesis: ( not I is_halting_on s or IExec (if>=0 a,k1,I),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS ) )
then A12: I is_closed_on (Initialize s) +* (stop I) by Th38;
assume A13: I is_halting_on s ; :: thesis: IExec (if>=0 a,k1,I),s = (IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )
then A14: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by Def3;
T: ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) by AMI_1:123;
x: Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) = Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by AMI_1:51;
TX4: ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by AMI_1:123;
TX2: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by AMI_1:123;
A15: CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) = CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1)),(Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by x, T
.= CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A12, A6, A9, A8, Th45, TX2, TX4
.= halt SCMPDS by A14, AMI_1:def 46 ;
then A16: ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I))) halts_on (Initialize s) +* (stop (if>=0 a,k1,I)) by AMI_1:146;
A17: CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))) = a,k1 >=0_goto 2 by A1, Th22, I2;

now

let l be Element of NAT ; :: thesis: ( l < (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 implies CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),b₁) <> halt SCMPDS )
assume A18: l < (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 ; :: thesis: CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),b₁) <> halt SCMPDS
u: Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),0 = (Initialize s) +* (stop (if>=0 a,k1,I)) by AMI_1:13;

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

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

then CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),l) = CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))) by u;
hence CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),l) <> halt SCMPDS by A17, Th31; :: thesis: verum

end;

suppose l <> 0 ; :: thesis: not CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),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 (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) by A18, A19, XREAL_1:8;
assume A21: CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),l) = halt SCMPDS ; :: thesis: contradiction
T: ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) by AMI_1:123;
x: Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),(n + 1) = Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),n by AMI_1:51;
TX2: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) by AMI_1:123;
TX4: ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),n) by AMI_1:123;
CurInstr (ProgramPart ((Initialize s) +* (stop I))),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n) = CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1)),(Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),n) by A12, A6, A9, A8, Th45, TX2, TX4
.= halt SCMPDS by A19, A21, x, T ;
hence contradiction by A14, A20, AMI_1:def 46; :: thesis: verum

end;

end;

end;

then for l being Element of NAT st CurInstr (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),l) = halt SCMPDS holds
(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 <= l ;
then A22: LifeSpan (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1 by A15, A16, AMI_1:def 46;
T: ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) by AMI_1:123;
A23: DataPart (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A14, AMI_1:122
.= DataPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A12, A6, A9, A8, Th45, T
.= DataPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by AMI_1:51
.= DataPart (Result (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I)))) by A16, A22, AMI_1:122 ;

A24: now

let x be set ; :: thesis: ( x in dom (IExec (if>=0 a,k1,I),s) implies (IExec (if>=0 a,k1,I),s) . b₁ = ((IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )) . b₁ )
A27: dom (Start-At ((card I) + 2),SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
assume A28: x in dom (IExec (if>=0 a,k1,I),s) ; :: thesis: (IExec (if>=0 a,k1,I),s) . b₁ = ((IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )) . b₁

per cases ( x is Int_position or x = IC SCMPDS or x is Element of NAT ) by A28, SCMPDS_4:20;

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

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

end;

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

A33: not x in dom (s | NAT ) by A10, A32, COMPOS_1:3;
then A34: IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) = IC (IExec I,s) by A32, FUNCT_4:12
.= card I by A11, A13, Th48 ;
A35: x in dom (Start-At ((card I) + 2),SCMPDS ) by A27, A32, TARSKI:def 1;
T: ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1) by AMI_1:123;
thus (IExec (if>=0 a,k1,I),s) . x = (Result (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I)))) . x by A33, FUNCT_4:12
.= (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) . x by A16, A22, AMI_1:122
.= IC (Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (if>=0 a,k1,I)))),((Initialize s) +* (stop (if>=0 a,k1,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A32, AMI_1:51
.= (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) + 2 by A12, A6, A9, A8, Th45, T
.= (IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2 by A14, AMI_1:122
.= (Start-At ((card I) + 2),SCMPDS ) . (IC SCMPDS ) by A34, FUNCOP_1:87
.= ((IExec I,s) +* (Start-At ((card I) + 2),SCMPDS )) . x by A32, A35, FUNCT_4:14 ; :: thesis: verum

end;

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

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

end;

end;

end;

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