def hlf_bit

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32half.bend:46

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

46def hlf_bit(+b: Bool, +q: Nat) -> {hlf(Nat.add(S.bit_value(b), Nat.double(q))) == q : Nat}:
47  match b:
48    case False{}:
49      hlf_double(q)
50    case True{}:
51      hlf_double_succ(q)