def bv_and

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/bits.bend:60

import Base

60def bv_and(+x: Bool, +y: Bool) -> {bv(Bool.and(x, y)) == Nat.mul(bv(x), bv(y)) : Nat}:
61  match x y:
62    case True{} True{}:
63      {==}
64    case True{} False{}:
65      {==}
66    case False{} _:
67      {==}