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

( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁())) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁()))] )

provided

A1: F₆() > 0 and
A2: P₁[F₁()] and
A3: for Q being Instruction-Sequence of SCMPDS
for t being 0 -started State 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))] )