def bit_bvd

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/xor.bend:22

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

22# the low bit and the rest of bv(b) + 2 u
23def bit_bvd(+b: Bool, +u: Nat) -> {C.bit(Nat.add(S.bit_value(b), Nat.double(u))) == S.bit_value(b) : Nat}:
24  match b:
25    case True{}:
26      WW.bit_dbl(1n, u)
27    case False{}:
28      WW.bit_dbl(0n, u)