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 be Integer; :: thesis:
let X be set ; :: 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 Es = IExec (I,P,s);
set bj = DataLoc (((IExec (I,P,s)) . a),i);
set EP = P;
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))));
assume card I > 0 ; :: thesis:
assume A6: 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 = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis:
then while<0 (a,i,I) is_halting_on s,P by Th15;
then A7: P +* (stop (while<0 (a,i,I))) halts_on Initialize s by SCMPDS_6:def 3;
A8: stop I c= P +* (stop I) by FUNCT_4:26;
B8: Start-At (0,SCMPDS) c= Initialize s by FUNCT_4:26;
A9: for x being Int_position st x in X holds
s . x = s . x ;
then I is_halting_on s,P by A2, A6;
then A10: P +* (stop I) halts_on Initialize s by SCMPDS_6:def 3;
P +* (stop I) = (P +* (stop I)) +* (stop I) by A8, FUNCT_4:104;
then (P +* (stop I)) +* (stop I) halts_on Initialize (Initialize s) by A10;
then A12: I is_halting_on Initialize s,P +* (stop I) by SCMPDS_6:def 3;
A13: (IExec (I,P,s)) . a = s . a by A2, A6, A9;

now

let t be State of SCMPDS; :: thesis:
let Q be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
assume that
A14: for x being Int_position st x in X holds
t . x = (IExec (I,P,s)) . x and
A15: ( t . a = (IExec (I,P,s)) . a & t . (DataLoc (((IExec (I,P,s)) . a),i)) < 0 ) ; :: thesis:

A16: now

let x be Int_position ; :: thesis:
assume A17: x in X ; :: thesis:
hence t . x = (IExec (I,P,s)) . x by A14
.= s . x by A2, A6, A9, A17 ;
:: thesis:

end;

hence (IExec (I,Q,t)) . a = t . a by A6, A13, A15; :: thesis:
thus (IExec (I,Q,t)) . (DataLoc (((IExec (I,P,s)) . a),i)) > t . (DataLoc (((IExec (I,P,s)) . a),i)) by A6, A13, A15, A16; :: thesis:
thus ( I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) by A6, A13, A15, A16; :: thesis:

end;

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 A23, SCMPDS_2:69 ; :: thesis:

end;

now

let x be Int_position ; :: thesis:
A42: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
A43: not x in dom (s | NAT) by A19, 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 A41, SCMPDS_4:23
.= (Result ((P +* (stop I)),(Initialize s))) . x by A10, EXTPRO_1:23
.= (IExec (I,P,s)) . x by A30, A43, 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 A36, A39, SCMPDS_2:66
.= (Initialize (IExec (I,P,s))) . x by A42, FUNCT_4:12 ;
:: thesis:

end;