def INV

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64clz.bend:79

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

79def INV(+k: Nat, +n: Nat, st: Nat & U32) -> Type:
80  {M.bit_length(n) == Nat.add(P1(st), M.bit_length(v(P2(st)))) : Nat} & {C.fits(k, v(P2(st))) == True{} : Bool}