def step_room

bend-ml-llama@0.2.1.0 · main.bend:573

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

573# For callers that walk the positions with a counter of steps left (fuel), keeping t + fuel = cap: with 1 + p steps
574# left, position t is below the capacity (step_room), and after the step t + 1 + p = cap still holds (step_inv).
575def step_room(+t: Nat, +p: Nat, -cap: Nat, e: {Nat.add(t, 1n+p) == cap : Nat}) -> {True{} == TA.leb(1n+t, cap) : Bool}:
576  %e : {True{} == TA.leb(1n+t, _) : Bool}
577  %add_succ(t, p) : {True{} == TA.leb(1n+t, _) : Bool}
578  TA.leb_up(t, t, p, TA.leb_refl(t))