def step_ok

bend-ml-tensor-array@0.1.19.0 · main.bend:691

import Base

691# one step: given the invariant for m, the invariant for 1+m holds whichever way the comparison goes
692def step_ok(ok: Bool, +d: Nat, +p: Nat, +m: Nat, +e: {ok == leb(1n+m, p) : Bool}, +i1: {p == pow2(d) : Nat}, +i2: {True{} == leb(m, p) : Bool}) -> {snd_nat(cap_pick(ok, d, p)) == pow2(fst_nat(cap_pick(ok, d, p))) : Nat} & {True{} == leb(1n+m, snd_nat(cap_pick(ok, d, p))) : Bool}:
693  match ok:
694    case True{}:
695      (i1, e)
696    case False{}:
697      (step_eq(d, p, i1), leb_add(1n, p, m, p, pos_p(d, p, i1), i2))