def dbl_inv

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

import Base

719# the invariant of cap_dbl: whichever way it ends (n <= p found, or the fuel out and cap_pair's answer), the second
720# component is 2^(first) and is >= n
721def dbl_inv(f: Nat, ok: Bool, +n: Nat, +d: Nat, +p: Nat, e: {ok == Nat.is_le(n, p) : Bool}, i1: {p == pow2(d) : Nat}) -> {snd_nat(cap_dbl(f, ok, n, d, p)) == pow2(fst_nat(cap_dbl(f, ok, n, d, p))) : Nat} & {True{} == leb(n, snd_nat(cap_dbl(f, ok, n, d, p))) : Bool}:
722  match f ok:
723    case _ True{}:
724      (i1, leb_of(n, p, e))
725    case 0n False{}:
726      cap_inv(n)
727    case 1n+g False{}:
728      dbl_inv(g, Nat.is_le(n, Nat.add(p, p)), n, 1n+d, Nat.add(p, p), {==}, step_eq(d, p, i1))