let s be State of ; :: thesis:
let I be shiftable No-StopCode Program of ; :: thesis:
let a be Int_position ; :: thesis:
let i, c be Integer; :: thesis:
let X, Y be set ; :: thesis:
let f be Function of product the Object-Kind of SCMPDS , NAT ; :: thesis:
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:
set s4 = Computation (s +* (Initialized (stop (while>0 a,i,I)))),1;
A2: IC (s +* (Initialized (stop (while>0 a,i,I)))) = inspos 0 by SCMPDS_6:21;
A3: while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A4: 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 A3, SCMPDS_6:22 ;
set m0 = LifeSpan (s +* (Initialized (stop (while>0 a,i,I))));
A5: dom (s | NAT ) = NAT by SCMPDS_6:1;
A6: 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 Es = IExec I,s;
set bj = DataLoc ((IExec I,s) . a),i;
assume A7: card I > 0 ; :: thesis:
assume A8: for t being State of st f . (Dstate t) = 0 holds
t . (DataLoc (s . a),i) <= 0 ; :: thesis:
assume A9: for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc (s . a),i)) ; :: thesis:
assume A10: for t being State of st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in Y holds
(IExec I,t) . x = t . x ) ) ; :: thesis:
then while>0 a,i,I is_halting_on s by A7, A8, A9, Th24;
then A11: ProgramPart (s +* (Initialized (stop (while>0 a,i,I)))) halts_on s +* (Initialized (stop (while>0 a,i,I))) by SCMPDS_6:def 3;
A12: for x being Int_position st x in Y holds
s . x = s . x ;
then A13: DataLoc ((IExec I,s) . a),i = DataLoc (s . a),i by A1, A9, A10;
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))));
A14: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
A15: (IExec I,s) . a = s . a by A1, A9, A10, A12;

A16: now

let t be State of ; :: thesis:
assume that
A17: for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((IExec I,s) . a),i)) and
A18: for x being Int_position st x in Y holds
t . x = (IExec I,s) . x and
A19: t . a = (IExec I,s) . a and
A20: t . (DataLoc ((IExec I,s) . a),i) > 0 ; :: thesis:

A21: now

let x be Int_position ; :: thesis:
assume A22: x in Y ; :: thesis:
hence t . x = (IExec I,s) . x by A18
.= s . x by A1, A9, A10, A12, A22 ;
:: thesis:

end;

hence (IExec I,t) . a = t . a by A10, A15, A17, A19, A20; :: thesis:
A23: t . a = s . a by A1, A9, A10, A12, A19;
hence ( I is_closed_on t & I is_halting_on t ) by A10, A17, A19, A20, A21; :: thesis:
thus f . (Dstate (IExec I,t)) < f . (Dstate t) by A10, A17, A19, A20, A21, A23; :: thesis:
thus for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc ((IExec I,s) . a),i)) by A10, A15, A17, A19, A20, A21; :: thesis:
thus for x being Int_position st x in Y holds
(IExec I,t) . x = t . x by A10, A17, A19, A20, A21, A23; :: thesis:

end;

for x being Int_position st x in X holds
(IExec I,s) . x >= c + ((IExec I,s) . (DataLoc ((IExec I,s) . a),i)) by A1, A9, A10, A12, A15;
then while>0 a,i,I is_halting_on IExec I,s by A7, A8, A13, A16, Th24;
then A24: 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;
A25: 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:
thus (s +* (Initialized (stop I))) . a = (s +* (Initialized (stop (while>0 a,i,I)))) . a by A25, SCMPDS_4:23
.= (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1) . a by A4, SCMPDS_2:68 ; :: thesis:

end;

now

let x be Int_position ; :: thesis:
A43: not x in dom (Initialized (stop (while>0 a,i,I))) by SCMPDS_4:31;

A44: now

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

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 A42, SCMPDS_4:23
.= (Result (s +* (Initialized (stop I)))) . x by A31, AMI_1:122
.= (IExec I,s) . x by A28, A44, 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 A38, A40, SCMPDS_2:66
.= ((IExec I,s) +* (Initialized (stop (while>0 a,i,I)))) . x by A43, FUNCT_4:12 ;
:: thesis:

end;