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));
A1: (Initialize s) +* (stop (while>0 (a,i,I))) = s +* (Initialize (stop (while>0 (a,i,I)))) by COMPOS_1:125;
assume A2: 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);
A3: IC ((Initialize s) +* (stop (while>0 (a,i,I)))) = 0 by SCMPDS_6:21;
A4: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A5: 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 A4, A1, SCMPDS_6:22 ;
set m0 = LifeSpan ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))));
A6: dom (ProgramPart s) = NAT by COMPOS_1:34;
A7: dom (ProgramPart s) = (dom s) /\ NAT by RELAT_1:90
.= (({(IC )} \/ 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 A8: card I > 0 ; :: thesis:
assume A9: for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 ; :: thesis:
assume A10: for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ; :: thesis:
assume A11: 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 A8, A9, A10, Th24;
then A12: ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I)))) halts_on (Initialize s) +* (stop (while>0 (a,i,I))) by SCMPDS_6:def 3;
A13: for x being Int_position st x in Y holds
s . x = s . x ;
then A14: DataLoc (((IExec (I,s)) . a),i) = DataLoc ((s . a),i) by A2, A10, A11;
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)))));
A15: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by COMPOS_1:125;
A16: (Initialize (IExec (I,s))) +* (stop (while>0 (a,i,I))) = (IExec (I,s)) +* (Initialize (stop (while>0 (a,i,I)))) by COMPOS_1:125;
A17: Initialize (stop I) c= (Initialize s) +* (stop I) by A15, FUNCT_4:26;
A18: (IExec (I,s)) . a = s . a by A2, A10, A11, A13;

A19: now

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

A24: now

let x be Int_position ; :: thesis:
assume A25: x in Y ; :: thesis:
hence t . x = (IExec (I,s)) . x by A21
.= s . x by A2, A10, A11, A13, A25 ;
:: thesis:

end;

hence (IExec (I,t)) . a = t . a by A11, A18, A20, A22, A23; :: thesis:
A26: t . a = s . a by A2, A10, A11, A13, A22;
hence ( I is_closed_on t & I is_halting_on t ) by A11, A20, A22, A23, A24; :: thesis:
thus f . (Dstate (IExec (I,t))) < f . (Dstate t) by A11, A20, A22, A23, A24, A26; :: 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 A11, A18, A20, A22, A23, A24; :: thesis:
thus for x being Int_position st x in Y holds
(IExec (I,t)) . x = t . x by A11, A20, A22, A23, A24, A26; :: 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 A2, A10, A11, A13, A18;
then while>0 (a,i,I) is_halting_on IExec (I,s) by A8, A9, A14, A19, Th24;
then A27: 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;
A28: 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 A28, SCMPDS_4:23
.= (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),1)) . a by A5, SCMPDS_2:68 ; :: thesis:

end;

now

end;