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

IExec ((while<0 (F₅(),F₆(),F₄())),F₃(),F₂()) = IExec ((while<0 (F₅(),F₆(),F₄())),F₃(),(Initialize (IExec (F₄(),F₃(),F₂()))))

provided

A1: F₂() . (DataLoc ((F₂() . F₅()),F₆())) < 0 and
A2: for t being 0 -started State of SCMPDS st P₁[t] & F₁(t) = 0 holds
t . (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₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Initialize (IExec (F₄(),Q,t)))) < F₁(t) & P₁[ Initialize (IExec (F₄(),Q,t))] )