let s be State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of SCMPDS; :: 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 pWHL = stop (while>0 (a,i,I));
set s1 = (Initialize s) +* (stop (while>0 (a,i,I)));
set ps = ProgramPart s;
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
I1: (Initialize s) +* (stop (while>0 (a,i,I))) = s +* (Initialize (stop (while>0 (a,i,I)))) by COMPOS_1:125;
assume A1: s . (DataLoc ((s . a),i)) > 0 ; :: thesis:
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),1);
A2: IC ((Initialize s) +* (stop (while>0 (a,i,I)))) = 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: Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),(0 + 1)) = Following ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I))))) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 2)),((Initialize s) +* (stop (while>0 (a,i,I))))) by A3, I1, SCMPDS_6:22 ;
set m0 = LifeSpan ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))));
A5: dom (ProgramPart s) = NAT by COMPOS_1:34;
A6: dom (ProgramPart s) = (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 SCMPDS 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 SCMPDS 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 ((Initialize s) +* (stop (while>0 (a,i,I)))) halts_on (Initialize s) +* (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 = (Initialize s) +* (stop I);
set m1 = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2;
set s2 = (Initialize (IExec (I,s))) +* (stop (while>0 (a,i,I)));
set m2 = LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while>0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while>0 (a,i,I)))));
I2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by COMPOS_1:125;
I3: (Initialize (IExec (I,s))) +* (stop (while>0 (a,i,I))) = (IExec (I,s)) +* (Initialize (stop (while>0 (a,i,I)))) by COMPOS_1:125;
A14: Initialize (stop I) c= (Initialize s) +* (stop I) by I2, FUNCT_4:26;
A15: (IExec (I,s)) . a = s . a by A1, A9, A10, A12;

A16: now

let t be State of SCMPDS; :: 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 ((Initialize (IExec (I,s))) +* (stop (while>0 (a,i,I)))) halts_on (Initialize (IExec (I,s))) +* (stop (while>0 (a,i,I))) by SCMPDS_6:def 3;
A25: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (while>0 (a,i,I)))) by COMPOS_1:138, FUNCT_7:134;

now

let a be Int_position ; :: thesis:
thus ((Initialize s) +* (stop I)) . a = ((Initialize s) +* (stop (while>0 (a,i,I)))) . a by A25, SCMPDS_4:23
.= (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),1)) . a by A4, SCMPDS_2:68 ; :: thesis:

end;

now

end;