let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started 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:
set b = DataLoc ((s . a),i);
defpred S₁[ State of SCMPDS] means ( ( for x being Int_position st x in X holds
$1 . x >= c + ($1 . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
$1 . x = s . x ) );
consider f being Function of (product the Object-Kind of SCMPDS),NAT such that
A2: for s being State of SCMPDS holds
( ( s . (DataLoc ((s . a),i)) <= 0 implies f . s = 0 ) & ( s . (DataLoc ((s . a),i)) > 0 implies f . s = s . (DataLoc ((s . a),i)) ) ) by Th5;
deffunc H₁( State of SCMPDS) -> Element of NAT = f . $1;
A5: for t being 0 -started State of SCMPDS st S₁[t] & H₁(t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 by A2;
assume A6: for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ; :: thesis:
A7: S₁[s] by A6;
assume A8: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( 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:

A9: now

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A10: S₁[t] and
A11: t . a = s . a and
A12: t . (DataLoc ((s . a),i)) > 0 ; :: thesis:
set It = IExec (I,Q,t);
set t2 = Initialize (IExec (I,Q,t));
set t1 = t;
consider v being State of SCMPDS such that
A13: v = t and
A14: for x being Int_position st x in X holds
v . x >= c + (v . (DataLoc ((s . a),i))) and
A15: for x being Int_position st x in Y holds
v . x = s . x by A10;
thus ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q ) by A8, A11, A12, A13, A15, A14; :: thesis:
thus H₁( Initialize (IExec (I,Q,t))) < H₁(t) :: thesis:

proof

A18: H₁(t) = t . (DataLoc ((s . a),i)) by A2, A12;
assume A19: H₁( Initialize (IExec (I,Q,t))) >= H₁(t) ; :: thesis:
H₁( Initialize (IExec (I,Q,t))) = (Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i)) by A2, A12, A18, A19
.= (IExec (I,Q,t)) . (DataLoc ((s . a),i)) by SCMPDS_5:15 ;
hence contradiction by A8, A11, A12, A10, A19, A18; :: thesis:

end;

thus S₁[ Initialize (IExec (I,Q,t))] :: thesis:

proof

set v = Initialize (IExec (I,Q,t));

hereby :: thesis:

let x be Int_position ; :: thesis:
assume x in X ; :: thesis:
then (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) by A8, A11, A12, A10;
then (Initialize (IExec (I,Q,t))) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) by SCMPDS_5:15;
hence (Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc ((s . a),i))) by SCMPDS_5:15; :: thesis:

end;

hereby :: thesis:

let x be Int_position ; :: thesis:
assume A20: x in Y ; :: thesis:
then (IExec (I,Q,t)) . x = t . x by A8, A11, A12, A10;
then (Initialize (IExec (I,Q,t))) . x = t . x by SCMPDS_5:15;
hence (Initialize (IExec (I,Q,t))) . x = s . x by A13, A15, A20; :: thesis:

end;

( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) from SCMPDS_8:sch 3(A5, A7, A9);
hence ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) ; :: thesis:
assume A21: s . (DataLoc ((s . a),i)) > 0 ; :: thesis:
IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) from SCMPDS_8:sch 4(A21, A5, A7, A9);
hence IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ; :: thesis: