def step_pair_ok

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

import Base

700# the invariant for cap_step on a pair, opened
701def step_pair_ok(+m: Nat, r: Nat & Nat, i1: {snd_nat(r) == pow2(fst_nat(r)) : Nat}, i2: {True{} == leb(m, snd_nat(r)) : Bool}) -> {snd_nat(cap_step(r, 1n+m)) == pow2(fst_nat(cap_step(r, 1n+m))) : Nat} & {True{} == leb(1n+m, snd_nat(cap_step(r, 1n+m))) : Bool}:
702  match r:
703    case Tuple{+d, +p}:
704      step_ok(leb(1n+m, p), d, p, m, {==}, i1, i2)