~/jendhub

def cap_inv

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

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

711# the invariant of cap_pair: the second component is 2^(first) and is >= n
712def cap_inv(n: Nat) -> {snd_nat(cap_pair(n)) == pow2(fst_nat(cap_pair(n))) : Nat} & {True{} == leb(n, snd_nat(cap_pair(n))) : Bool}:
713  match n:
714    case 0n:
715      ({==}, {==})
716    case 1n++m:
717      cap_succ(m, cap_inv(m))

Uses (10)

Used by (1)