let s be State of SCMPDS ; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer
for n being Element of NAT st n > 0 & s . x >= (s . y) + c & s . (DataLoc (s . a),i) > 0 & ( for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let I be halt-free shiftable Program of SCMPDS ; :: thesis: for a, x, y being Int_position
for i, c being Integer
for n being Element of NAT st n > 0 & s . x >= (s . y) + c & s . (DataLoc (s . a),i) > 0 & ( for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let a, x, y be Int_position ; :: thesis: for i, c being Integer
for n being Element of NAT st n > 0 & s . x >= (s . y) + c & s . (DataLoc (s . a),i) > 0 & ( for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let i, c be Integer; :: thesis: for n being Element of NAT st n > 0 & s . x >= (s . y) + c & s . (DataLoc (s . a),i) > 0 & ( for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
let n be Element of NAT ; :: thesis: ( n > 0 & s . x >= (s . y) + c & s . (DataLoc (s . a),i) > 0 & ( for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) implies IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
set b = DataLoc (s . a),i;
set J = I ';' (AddTo a,i,(- n));
assume A1: n > 0 ; :: thesis: ( not s . x >= (s . y) + c or not s . (DataLoc (s . a),i) > 0 or ex t being State of SCMPDS st
( t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 & not ( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
defpred S₁[ set ] means ex t being State of SCMPDS st
( t = $1 & t . x >= (t . y) + c );
assume A2: s . x >= (s . y) + c ; :: thesis: ( not s . (DataLoc (s . a),i) > 0 or ex t being State of SCMPDS st
( t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 & not ( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
A3: S₁[ Dstate s]

proof

take t = Dstate s; :: thesis: ( t = Dstate s & t . x >= (t . y) + c )
thus t = Dstate s ; :: thesis: t . x >= (t . y) + c
t . x >= (s . y) + c by A2, SCMPDS_8:4;
hence t . x >= (t . y) + c by SCMPDS_8:4; :: thesis: verum

end;

assume A4: s . (DataLoc (s . a),i) > 0 ; :: thesis: ( ex t being State of SCMPDS st
( t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 & not ( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) or IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) )
assume A5: for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ; :: thesis: IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)

A6: now

let t be State of SCMPDS ; :: thesis: ( S₁[ Dstate t] & t . a = s . a & t . (DataLoc (s . a),i) > 0 implies ( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & S₁[ Dstate (IExec (I ';' (AddTo a,i,(- n))),t)] ) )
assume that
A7: S₁[ Dstate t] and
A8: ( t . a = s . a & t . (DataLoc (s . a),i) > 0 ) ; :: thesis: ( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & S₁[ Dstate (IExec (I ';' (AddTo a,i,(- n))),t)] )
consider v being State of SCMPDS such that
A9: v = Dstate t and
A10: v . x >= (v . y) + c by A7;
t . x = v . x by A9, SCMPDS_8:4;
then A11: t . x >= (t . y) + c by A9, A10, SCMPDS_8:4;
hence ( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t ) by A5, A8; :: thesis: S₁[ Dstate (IExec (I ';' (AddTo a,i,(- n))),t)]
thus S₁[ Dstate (IExec (I ';' (AddTo a,i,(- n))),t)] :: thesis: verum

proof

take v = Dstate (IExec (I ';' (AddTo a,i,(- n))),t); :: thesis: ( v = Dstate (IExec (I ';' (AddTo a,i,(- n))),t) & v . x >= (v . y) + c )
thus v = Dstate (IExec (I ';' (AddTo a,i,(- n))),t) ; :: thesis: v . x >= (v . y) + c
v . x = (IExec (I ';' (AddTo a,i,(- n))),t) . x by SCMPDS_8:4;
then v . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c by A5, A8, A11;
hence v . x >= (v . y) + c by SCMPDS_8:4; :: thesis: verum

end;

end;

( ( S₁[s] or not S₁[s] ) & IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) ) from SCPISORT:sch 2(A1, A4, A3, A6);
hence IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s) ; :: thesis: verum