scheme :: SCPISORT:sch 1
ForDownHalt{ P₁[ set ], F₁() -> 0 -started State of SCMPDS, F₂() -> Instruction-Sequence of SCMPDS, F₃() -> halt-free shiftable Program of SCMPDS, F₄() -> Int_position, F₅() -> Integer, F₆() -> Nat } :

( for-down (F₄(),F₅(),F₆(),F₃()) is_closed_on F₁(),F₂() & for-down (F₄(),F₅(),F₆(),F₃()) is_halting_on F₁(),F₂() )

provided

A1: F₆() > 0 and
A2: P₁[F₁()] and
A3: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P₁[t] & t . F₄() = F₁() . F₄() & t . (DataLoc ((F₁() . F₄()),F₅())) > 0 holds
( (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . F₄() = t . F₄() & (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . (DataLoc ((F₁() . F₄()),F₅())) = (t . (DataLoc ((F₁() . F₄()),F₅()))) - F₆() & F₃() is_closed_on t,Q & F₃() is_halting_on t,Q & P₁[ Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t))] )