let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer
for n being Nat st n > 0 & s . x >= (s . y) + c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
let s be 0 -started 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 Nat st n > 0 & s . x >= (s . y) + c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
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 Nat st n > 0 & s . x >= (s . y) + c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
let a, x, y be Int_position; :: thesis: for i, c being Integer
for n being Nat st n > 0 & s . x >= (s . y) + c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
let i, c be Integer; :: thesis: for n being Nat st n > 0 & s . x >= (s . y) + c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
let n be Nat; :: thesis: ( n > 0 & s . x >= (s . y) + c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) implies ( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P ) )
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 ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) or ( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P ) )
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: ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) or ( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P ) )
A3: S₁[s] by A2;
assume A4: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence 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)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ; :: thesis: ( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )

A5: now :: thesis: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st S₁[t] & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & S₁[ Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t))] )

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st S₁[t] & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & S₁[ Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t))] )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( S₁[t] & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 implies ( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & S₁[ Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t))] ) )
assume that
A6: S₁[t] and
A7: ( t . a = s . a & t . (DataLoc ((s . a),i)) > 0 ) ; :: thesis: ( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & S₁[ Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t))] )
consider v being State of SCMPDS such that
A8: v = t and
A9: v . x >= (v . y) + c by A6;
thus ( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q ) by A4, A7, A8, A9; :: thesis: S₁[ Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t))]
thus S₁[ Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t))] :: thesis: verum

proof

take v = Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)); :: thesis: ( v = Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) & v . x >= (v . y) + c )
thus v = Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) ; :: thesis: v . x >= (v . y) + c
v . x = (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x by SCMPDS_5:15;
then v . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c by A4, A7, A8, A9;
hence v . x >= (v . y) + c by SCMPDS_5:15; :: thesis: verum

end;

end;

( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P ) from SCPISORT:sch 1(A1, A3, A5);
hence ( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P ) ; :: thesis: verum