scheme :: SCMPDS_8:sch 1
WhileLHalt{ F1( State of SCMPDS) -> Nat, F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ State of SCMPDS] } :
( while<0 (F5(),F6(),F4()) is_closed_on F2(),F3() & while<0 (F5(),F6(),F4()) is_halting_on F2(),F3() )
provided
A1: for t being 0 -started State of SCMPDS st P1[t] & F1(t) = 0 holds
t . (DataLoc ((F2() . F5()),F6())) >= 0 and
A2: P1[F2()] and
A3: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) < 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] )