scheme :: SCPISORT:sch 2
ForDownExec{ 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 } :

IExec ((for-down (F₄(),F₅(),F₆(),F₃())),F₂(),F₁()) = IExec ((for-down (F₄(),F₅(),F₆(),F₃())),F₂(),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))))

provided

A1: F₆() > 0 and
A2: F₁() . (DataLoc ((F₁() . F₄()),F₅())) > 0 and
A3: P₁[F₁()] and
A4: 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))] )