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) + 1),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) + 1),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) + 1),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) + 1),SCMPDS ) )
set b = DataLoc (s . a),k1;
assume A1: 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) + 1),SCMPDS ) )
set i = a,k1 <>0_goto ((card I) + 1);
set IF = if=0 a,k1,I;
set pI = stop I;
set pIF = stop (if=0 a,k1,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;
I1: (Initialize s) +* (stop (if=0 a,k1,I)) = s +* (Initialize (stop (if=0 a,k1,I))) by SCMPDS_4:5;
I2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
A2: IC ((Initialize s) +* (stop (if=0 a,k1,I))) = 0 by I1, FUNCT_4:26, SCMPDS_5:18;
A3: not DataLoc (s . a),k1 in dom (Initialize (stop (if=0 a,k1,I))) by SCMPDS_4:31;
A4: 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 ((card I) + 1)),((Initialize s) +* (stop (if=0 a,k1,I))) by Th22, I1 ;
not a in dom (Initialize (stop (if=0 a,k1,I))) by SCMPDS_4:31;
then ((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 I1, FUNCT_4:12
.= 0 by A1, A3, I1, FUNCT_4:12 ;
then A5: IC (Comput (ProgramPart ((Initialize s) +* (stop (if=0 a,k1,I)))),((Initialize s) +* (stop (if=0 a,k1,I))),1) = succ (IC ((Initialize s) +* (stop (if=0 a,k1,I)))) by A4, SCMPDS_2:67
.= 0 + 1 by A2 ;
A6: 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 A6, SCMPDS_4:23
.= (Comput (ProgramPart ((Initialize s) +* (stop (if=0 a,k1,I)))),((Initialize s) +* (stop (if=0 a,k1,I))),1) . a by A4, SCMPDS_2:67 ; :: thesis: verum

end;

then A7: 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 A8: 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) + 1),SCMPDS ) )
then A9: I is_closed_on (Initialize s) +* (stop I) by Th38;
set SAl = Start-At ((card I) + 1),SCMPDS ;
A10: dom (ProgramPart s) = NAT by COMPOS_1:34;
A11: ( Initialize (stop I) c= (Initialize s) +* (stop I) & Shift (stop I),1 c= Comput (ProgramPart ((Initialize s) +* (stop (if=0 a,k1,I)))),((Initialize s) +* (stop (if=0 a,k1,I))),1 ) by Lm5, I2, FUNCT_4:26;
assume A12: I is_halting_on s ; :: thesis: IExec (if=0 a,k1,I),s = (IExec I,s) +* (Start-At ((card I) + 1),SCMPDS )
then A13: 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;
A14: 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 A9, A11, A5, A7, Th45, TX4, TX2
.= halt SCMPDS by A13, AMI_1:def 46 ;
then A15: ProgramPart ((Initialize s) +* (stop (if=0 a,k1,I))) halts_on (Initialize s) +* (stop (if=0 a,k1,I)) by AMI_1:146;
A16: CurInstr (ProgramPart ((Initialize s) +* (stop (if=0 a,k1,I)))),((Initialize s) +* (stop (if=0 a,k1,I))) = a,k1 <>0_goto ((card I) + 1) by Th22, I1;

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 A17: 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 A16, Th29; :: 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
A18: l = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A19: n < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) by A17, A18, XREAL_1:8;
assume A20: 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;
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;
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;
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 A9, A11, A5, A7, Th45, TX4, TX2
.= halt SCMPDS by A18, A20, x, T ;
hence contradiction by A13, A19, 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 A21: 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 A14, A15, 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;
A22: 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 A13, 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 A9, A11, A5, A7, 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 A15, A21, AMI_1:122 ;

A23: 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) + 1),SCMPDS )) . b₁ )
A26: dom (Start-At ((card I) + 1),SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
assume A27: 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) + 1),SCMPDS )) . b₁

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

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

then x <> IC SCMPDS by SCMPDS_2:52;
then A29: not x in dom (Start-At ((card I) + 1),SCMPDS ) by A26, TARSKI:def 1;
A30: not x in dom (s | NAT ) by A10, A28, 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 A22, A28, SCMPDS_4:23
.= (IExec I,s) . x by A30, FUNCT_4:12
.= ((IExec I,s) +* (Start-At ((card I) + 1),SCMPDS )) . x by A29, FUNCT_4:12 ;
:: thesis: verum

end;

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

A32: not x in dom (s | NAT ) by A10, A31, COMPOS_1:3;
then A33: IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) = IC (IExec I,s) by A31, FUNCT_4:12
.= card I by A8, A12, Th48 ;
A34: x in dom (Start-At ((card I) + 1),SCMPDS ) by A26, A31, 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 A32, 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 A15, A21, 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 A31, AMI_1:51
.= (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) + 1 by A9, A11, A5, A7, Th45, T
.= (IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1 by A13, AMI_1:122
.= (Start-At ((card I) + 1),SCMPDS ) . (IC SCMPDS ) by A33, FUNCOP_1:87
.= ((IExec I,s) +* (Start-At ((card I) + 1),SCMPDS )) . x by A31, A34, 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) + 1),SCMPDS )) . b₁

hence (IExec (if=0 a,k1,I),s) . x = ((IExec I,s) +* (Start-At ((card I) + 1),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) + 1),SCMPDS )) by PARTFUN1:def 4 ;
hence IExec (if=0 a,k1,I),s = (IExec I,s) +* (Start-At ((card I) + 1),SCMPDS ) by A23, FUNCT_1:9; :: thesis: verum