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:
set b = DataLoc (s . a),i;
assume A1: card I > 0 ; :: thesis:
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;
A3: for t being State of SCMPDS holds
( H₁( Dstate t) = 0 iff t . (DataLoc (s . a),i) <= 0 )

let t be State of SCMPDS ; :: thesis:
thus ( H₁( Dstate t) = 0 implies t . (DataLoc (s . a),i) <= 0 ) :: thesis:

end;

assume t . (DataLoc (s . a),i) <= 0 ; :: thesis:
then (Dstate t) . (DataLoc (s . a),i) <= 0 by Th4;
hence H₁( Dstate t) = 0 by A2; :: thesis:

end;

set t = Dstate s;

let x be Int_position ; :: thesis:
assume x in X ; :: thesis:
then s . x >= c + (s . (DataLoc (s . a),i)) by A6;
then (Dstate s) . x >= c + (s . (DataLoc (s . a),i)) by Th4;
hence (Dstate s) . x >= c + ((Dstate s) . (DataLoc (s . a),i)) by Th4; :: thesis:

end;

end;

assume A8: 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 & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( 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:

let t be State of SCMPDS ; :: thesis:
assume that
A10: S₁[ Dstate t] and
A11: t . a = s . a and
A12: t . (DataLoc (s . a),i) > 0 ; :: thesis:
set It = IExec I,t;
set t2 = Dstate (IExec I,t);
set t1 = Dstate t;
consider v being State of SCMPDS such that
A13: v = Dstate 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;

A16: now

end;

A17: now

let x be Int_position ; :: thesis:
assume x in X ; :: thesis:
then v . x >= c + (v . (DataLoc (s . a),i)) by A14;
then t . x >= c + (v . (DataLoc (s . a),i)) by A13, Th4;
hence t . x >= c + (t . (DataLoc (s . a),i)) by A13, Th4; :: thesis:

end;

(Dstate t) . (DataLoc (s . a),i) > 0 by A12, Th4;
then A18: H₁( Dstate t) = (Dstate t) . (DataLoc (s . a),i) by A2
.= t . (DataLoc (s . a),i) by Th4 ;
assume A19: H₁( Dstate (IExec I,t)) >= H₁( Dstate t) ; :: thesis:
then (IExec I,t) . (DataLoc (s . a),i) > 0 by A3, A12, A18;
then (Dstate (IExec I,t)) . (DataLoc (s . a),i) > 0 by Th4;
then H₁( Dstate (IExec I,t)) = (Dstate (IExec I,t)) . (DataLoc (s . a),i) by A2
.= (IExec I,t) . (DataLoc (s . a),i) by Th4 ;
hence contradiction by A8, A11, A12, A17, A16, A19, A18; :: thesis:

end;

set v = Dstate (IExec I,t);

let x be Int_position ; :: thesis:
assume x in X ; :: thesis:
then (IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) by A8, A11, A12, A17, A16;
then (Dstate (IExec I,t)) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) by Th4;
hence (Dstate (IExec I,t)) . x >= c + ((Dstate (IExec I,t)) . (DataLoc (s . a),i)) by Th4; :: thesis:

end;

end;