def offset_lt

bendtorch-core@0.1.0.0 · src/storage/api.bend:211

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

211def offset_lt(+d: Nat, +path: Model.Path(d)) -> {Nat.is_lt(Model.offset(d, path), Model.capacity(d)) == True{} : Bool}:
212  match d:
213    case 0n:
214      {==}
215    case 1n+p:
216      Model.Step{+b, +rest} = path
217      match b:
218        case False{}:
219          Arith.lt_le_trans(Model.offset(p, rest), Model.capacity(p), Nat.add(Model.capacity(p), Model.capacity(p)),
220            offset_lt(p, rest), le_add_right(Model.capacity(p), Model.capacity(p)))
221        case True{}:
222          lt_add_left(Model.capacity(p), Model.offset(p, rest), Model.capacity(p), offset_lt(p, rest))