let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
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;
set ps = ProgramPart s;
set P1 = P +* (stop (while>0 (a,i,I)));
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume A2: s . (DataLoc ((s . a),i)) > 0 ; :: thesis:
set s4 = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1);
set P4 = P +* (stop (while>0 (a,i,I)));
A3: IC (Initialize s) = 0 by COMPOS_1:def 16;
A4: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A5: Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(0 + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),0))) by EXTPRO_1:4
.= Following ((P +* (stop (while>0 (a,i,I)))),(Initialize s)) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 2)),(Initialize s)) by A4, SCMPDS_6:22 ;
set m0 = LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize s));
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,P,s);
set bj = DataLoc (((IExec (I,P,s)) . a),i);
set EP = P;
assume 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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis:
then while>0 (a,i,I) is_halting_on s,P by A9, A10, Th24;
then A12: P +* (stop (while>0 (a,i,I))) halts_on Initialize s 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,P,s)) . a),i) = DataLoc ((s . a),i) by A2, A10, A11;
set sI = Initialize s;
set PI = P +* (stop I);
set m1 = (LifeSpan ((P +* (stop I)),(Initialize s))) + 2;
set s2 = Initialize (IExec (I,P,s));
set P2 = P +* (stop (while>0 (a,i,I)));
set m2 = LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))));
A17: stop I c= P +* (stop I) by FUNCT_4:26;
B17: Start-At (0,SCMPDS) c= Initialize s by FUNCT_4:26;
A18: (IExec (I,P,s)) . a = s . a by A2, A10, A11, A13;

A19: now

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

A24: now

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

end;

hence (IExec (I,Q,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,Q & I is_halting_on t,Q ) by A11, A20, A22, A23, A24; :: thesis:
thus f . (Dstate (IExec (I,Q,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,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((IExec (I,P,s)) . a),i))) by A11, A18, A20, A22, A23, A24; :: thesis:
thus for x being Int_position st x in Y holds
(IExec (I,Q,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,P,s)) . x >= c + ((IExec (I,P,s)) . (DataLoc (((IExec (I,P,s)) . a),i))) by A2, A10, A11, A13, A18;
then while>0 (a,i,I) is_halting_on IExec (I,P,s),P by A9, A14, A19, Th24;
then A27: P +* (stop (while>0 (a,i,I))) halts_on Initialize (IExec (I,P,s)) by SCMPDS_6:def 3;

now

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

end;

now

let x be Int_position ; :: thesis:
A49: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
A50: not x in dom (s | NAT) by A6, SCMPDS_2:53;
(Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) . x = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) . x by A48, SCMPDS_4:23
.= (Result ((P +* (stop I)),(Initialize s))) . x by A34, EXTPRO_1:23
.= (IExec (I,P,s)) . x by A31, A50, FUNCT_4:12 ;
hence (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))) . x = (IExec (I,P,s)) . x by A43, A46, SCMPDS_2:66
.= (Initialize (IExec (I,P,s))) . x by A49, FUNCT_4:12 ;
:: thesis:

end;