let s be State of ; :: thesis: for I being shiftable No-StopCode Program of
for a being Int_position
for i being Integer
for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( for t being State of st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let I be shiftable No-StopCode Program of ; :: thesis: for a being Int_position
for i being Integer
for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( for t being State of st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let a be Int_position ; :: thesis: for i being Integer
for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( for t being State of st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let i be Integer; :: thesis: for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( for t being State of st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let X be set ; :: thesis: ( s . (DataLoc (s . a),i) < 0 & card I > 0 & ( for t being State of st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) implies IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s) )
set b = DataLoc (s . a),i;
set WHL = while<0 a,i,I;
set iWHL = Initialized (stop (while<0 a,i,I));
set iI = Initialized (stop I);
set s1 = s +* (Initialized (stop (while<0 a,i,I)));
set ps = s | NAT ;
set i1 = a,i >=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume A1: s . (DataLoc (s . a),i) < 0 ; :: thesis: ( not card I > 0 or ex t being State of st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 & not ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) or IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s) )
set Es = IExec I,s;
set bj = DataLoc ((IExec I,s) . a),i;
set sI = s +* (Initialized (stop I));
set m1 = (LifeSpan (s +* (Initialized (stop I)))) + 2;
set s2 = (IExec I,s) +* (Initialized (stop (while<0 a,i,I)));
set m2 = LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I))));
assume A2: card I > 0 ; :: thesis: ( ex t being State of st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 & not ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) or IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s) )
assume A3: for t being State of st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ; :: thesis: IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
then while<0 a,i,I is_halting_on s by A2, Th15;
then A4: ProgramPart (s +* (Initialized (stop (while<0 a,i,I)))) halts_on s +* (Initialized (stop (while<0 a,i,I))) by SCMPDS_6:def 3;
A5: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
A6: for x being Int_position st x in X holds
s . x = s . x ;
then I is_halting_on s by A1, A3;
then A7: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
s +* (Initialized (stop I)) = (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A5, FUNCT_4:79;
then ProgramPart ((s +* (Initialized (stop I))) +* (Initialized (stop I))) halts_on (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A5, FUNCT_4:79, A7;
then A8: I is_halting_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
A9: (IExec I,s) . a = s . a by A1, A3, A6;

now

let t be State of ; :: thesis: ( ( for x being Int_position st x in X holds
t . x = (IExec I,s) . x ) & t . a = (IExec I,s) . a & t . (DataLoc ((IExec I,s) . a),i) < 0 implies ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,s) . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) )
assume that
A10: for x being Int_position st x in X holds
t . x = (IExec I,s) . x and
A11: ( t . a = (IExec I,s) . a & t . (DataLoc ((IExec I,s) . a),i) < 0 ) ; :: thesis: ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,s) . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) )

A12: now

let x be Int_position ; :: thesis: ( x in X implies t . x = s . x )
assume A13: x in X ; :: thesis: t . x = s . x
hence t . x = (IExec I,s) . x by A10
.= s . x by A1, A3, A6, A13 ;
:: thesis: verum

end;

hence (IExec I,t) . a = t . a by A3, A9, A11; :: thesis: ( (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,s) . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) )
thus (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,s) . a),i) by A3, A9, A11, A12; :: thesis: ( I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) )
thus ( I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) by A3, A9, A11, A12; :: thesis: verum

end;

then while<0 a,i,I is_halting_on IExec I,s by A2, Th15;
then A14: ProgramPart ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) halts_on (IExec I,s) +* (Initialized (stop (while<0 a,i,I))) by SCMPDS_6:def 3;
set m0 = LifeSpan (s +* (Initialized (stop (while<0 a,i,I))));
A15: dom (s | NAT ) = NAT by SCMPDS_6:1;
A16: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= (({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) /\ NAT by SCMPDS_4:19
.= NAT by XBOOLE_1:21 ;
set s4 = Computation (s +* (Initialized (stop (while<0 a,i,I)))),1;
A17: IC (s +* (Initialized (stop (while<0 a,i,I)))) = inspos 0 by SCMPDS_6:21;
A18: while<0 a,i,I = (a,i >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A19: Computation (s +* (Initialized (stop (while<0 a,i,I)))),(0 + 1) = Following (Computation (s +* (Initialized (stop (while<0 a,i,I)))),0 ) by AMI_1:14
.= Following (s +* (Initialized (stop (while<0 a,i,I)))) by AMI_1:13
.= Exec (a,i >=0_goto ((card I) + 2)),(s +* (Initialized (stop (while<0 a,i,I)))) by A18, SCMPDS_6:22 ;
A20: (IExec I,s) | NAT = ((Result (s +* (Initialized (stop I)))) +* (s | NAT )) | NAT by SCMPDS_4:def 8
.= s | NAT by A16, FUNCT_4:24 ;
A21: not DataLoc (s . a),i in dom (Initialized (stop (while<0 a,i,I))) by SCMPDS_4:31;
not a in dom (Initialized (stop (while<0 a,i,I))) by SCMPDS_4:31;
then (s +* (Initialized (stop (while<0 a,i,I)))) . (DataLoc ((s +* (Initialized (stop (while<0 a,i,I)))) . a),i) = (s +* (Initialized (stop (while<0 a,i,I)))) . (DataLoc (s . a),i) by FUNCT_4:12
.= s . (DataLoc (s . a),i) by A21, FUNCT_4:12 ;
then A22: IC (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1) = Next (IC (s +* (Initialized (stop (while<0 a,i,I))))) by A1, A19, SCMPDS_2:69
.= inspos (0 + 1) by A17 ;
set mI = LifeSpan (s +* (Initialized (stop I)));
set s5 = Computation (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))));
set l1 = inspos ((card I) + 1);
A23: DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (while<0 a,i,I)))) by SCMPDS_4:24, SCMPDS_4:36;

now

let a be Int_position ; :: thesis: (s +* (Initialized (stop I))) . a = (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1) . a
thus (s +* (Initialized (stop I))) . a = (s +* (Initialized (stop (while<0 a,i,I)))) . a by A23, SCMPDS_4:23
.= (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1) . a by A19, SCMPDS_2:69 ; :: thesis: verum

end;

then A24: DataPart (s +* (Initialized (stop I))) = DataPart (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1) by SCMPDS_4:23;
set m3 = (LifeSpan (s +* (Initialized (stop I)))) + 1;
set s6 = Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1);
(card I) + 1 < (card I) + 2 by XREAL_1:8;
then A25: inspos ((card I) + 1) in dom (while<0 a,i,I) by Th7;
set s7 = Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1);
A26: IExec I,s = (Result (s +* (Initialized (stop I)))) +* (s | NAT ) by SCMPDS_4:def 8;
( while<0 a,i,I c= Initialized (stop (while<0 a,i,I)) & Initialized (stop (while<0 a,i,I)) c= s +* (Initialized (stop (while<0 a,i,I))) ) by FUNCT_4:26, SCMPDS_6:17;
then A27: while<0 a,i,I c= s +* (Initialized (stop (while<0 a,i,I))) by XBOOLE_1:1;
Shift I,1 c= while<0 a,i,I by Lm2;
then Shift I,1 c= s +* (Initialized (stop (while<0 a,i,I))) by A27, XBOOLE_1:1;
then A28: Shift I,1 c= Computation (s +* (Initialized (stop (while<0 a,i,I)))),1 by AMI_1:81;
I is_closed_on s by A1, A3, A6;
then A29: I is_closed_on s +* (Initialized (stop I)) by SCMPDS_6:38;
then A30: IC (Computation (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = inspos ((card I) + 1) by A2, A5, A8, A22, A24, A28, SCMPDS_7:36;
A31: Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Computation (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:51;
then A32: CurInstr (Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (Computation (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . (inspos ((card I) + 1)) by A2, A5, A8, A29, A22, A24, A28, SCMPDS_7:36
.= (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1) . (inspos ((card I) + 1)) by AMI_1:54
.= (s +* (Initialized (stop (while<0 a,i,I)))) . (inspos ((card I) + 1)) by AMI_1:54
.= (while<0 a,i,I) . (inspos ((card I) + 1)) by A25, A27, GRFUNC_1:8
.= goto (- ((card I) + 1)) by Th8 ;
A33: Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) = Following (Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 1))),(Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by A32 ;
then IC (Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) = ICplusConst (Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)),(0 - ((card I) + 1)) by SCMPDS_2:66
.= inspos 0 by A30, A31, SCMPDS_7:1 ;
then A34: IC ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) = IC (Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 2)) by SCMPDS_6:21;
A35: DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) by A2, A5, A8, A29, A22, A24, A28, SCMPDS_7:36;

now

let x be Int_position ; :: thesis: (Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . x = ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) . x
A36: not x in dom (Initialized (stop (while<0 a,i,I))) by SCMPDS_4:31;

A37: now

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

end;

(Computation (Computation (s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . x = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . x by A35, SCMPDS_4:23
.= (Result (s +* (Initialized (stop I)))) . x by A7, AMI_1:122
.= (IExec I,s) . x by A26, A37, FUNCT_4:12 ;
hence (Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . x = (IExec I,s) . x by A31, A33, SCMPDS_2:66
.= ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) . x by A36, FUNCT_4:12 ;
:: thesis: verum

end;

then A38: DataPart (Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) = DataPart ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) by SCMPDS_4:23;
((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) | NAT = (((Result (s +* (Initialized (stop I)))) +* (s | NAT )) +* (Initialized (stop (while<0 a,i,I)))) | NAT by SCMPDS_4:def 8
.= (((Result (s +* (Initialized (stop I)))) +* (s | NAT )) | NAT ) +* ((Initialized (stop (while<0 a,i,I))) | NAT ) by FUNCT_4:75
.= (s | NAT ) +* ((Initialized (stop (while<0 a,i,I))) | NAT ) by A16, FUNCT_4:24
.= (s +* (Initialized (stop (while<0 a,i,I)))) | NAT by FUNCT_4:75
.= (Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 2)) | NAT by SCMPDS_7:6 ;
then A39: Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 2) = (IExec I,s) +* (Initialized (stop (while<0 a,i,I))) by A38, A34, SCMPDS_7:7;
then CurInstr (Computation (s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 2)) = a,i >=0_goto ((card I) + 2) by A18, SCMPDS_6:22;
then LifeSpan (s +* (Initialized (stop (while<0 a,i,I)))) > (LifeSpan (s +* (Initialized (stop I)))) + 2 by A4, SCMPDS_6:2, SCMPDS_6:31;
then consider nn being Nat such that
A40: LifeSpan (s +* (Initialized (stop (while<0 a,i,I)))) = ((LifeSpan (s +* (Initialized (stop I)))) + 2) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 2) + (LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))))) = Computation ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))),(LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I))))) by A39, AMI_1:51;
then CurInstr (Computation (s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 2) + (LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I))))))) = halt SCMPDS by A14, AMI_1:def 46;
then ((LifeSpan (s +* (Initialized (stop I)))) + 2) + (LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I))))) >= LifeSpan (s +* (Initialized (stop (while<0 a,i,I)))) by A4, AMI_1:def 46;
then A41: LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) >= nn by A40, XREAL_1:8;
A42: Computation (s +* (Initialized (stop (while<0 a,i,I)))),(LifeSpan (s +* (Initialized (stop (while<0 a,i,I))))) = Computation ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))),nn by A39, A40, AMI_1:51;
then CurInstr (Computation ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))),nn) = halt SCMPDS by A4, AMI_1:def 46;
then nn >= LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) by A14, AMI_1:def 46;
then nn = LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) by A41, XXREAL_0:1;
then Result (s +* (Initialized (stop (while<0 a,i,I)))) = Computation ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))),(LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I))))) by A4, A42, AMI_1:122;
hence IExec (while<0 a,i,I),s = (Computation ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))),(LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))))) +* (s | NAT ) by SCMPDS_4:def 8
.= (Result ((IExec I,s) +* (Initialized (stop (while<0 a,i,I))))) +* ((IExec I,s) | NAT ) by A14, A20, AMI_1:122
.= IExec (while<0 a,i,I),(IExec I,s) by SCMPDS_4:def 8 ;
:: thesis: verum