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_Values_of SCMPDS)),NAT such that
A1: 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 Th3;
deffunc H₁( State of SCMPDS) -> Element of NAT = f . $1;
A2: for t being 0 -started State of SCMPDS st S₁[t] & H₁(t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 by A1;
assume A3: for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ; :: thesis:
A4: S₁[s] by A3;
assume A5: 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:

A6: now :: thesis:

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A7: S₁[t] and
A8: t . a = s . a and
A9: 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
A10: v = t and
A11: for x being Int_position st x in X holds
v . x >= c + (v . (DataLoc ((s . a),i))) and
A12: for x being Int_position st x in Y holds
v . x = s . x by A7;
thus ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q ) by A5, A8, A9, A10, A12, A11; :: thesis:
thus H₁( Initialize (IExec (I,Q,t))) < H₁(t) :: thesis:

proof

A13: H₁(t) = t . (DataLoc ((s . a),i)) by A1, A9;
assume A14: 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 A1, A9, A13, A14
.= (IExec (I,Q,t)) . (DataLoc ((s . a),i)) by SCMPDS_5:15 ;
hence contradiction by A5, A8, A9, A7, A14, A13; :: 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 A5, A8, A9, A7;
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 A15: x in Y ; :: thesis:
then (IExec (I,Q,t)) . x = t . x by A5, A8, A9, A7;
then (Initialize (IExec (I,Q,t))) . x = t . x by SCMPDS_5:15;
hence (Initialize (IExec (I,Q,t))) . x = s . x by A10, A12, A15; :: 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(A2, A4, A6);
hence ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) ; :: thesis:
assume A16: 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(A16, A2, A4, A6);
hence IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ; :: thesis: