Bits.wand: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend as Bits
Lines 77-91 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend&start_line=77&end_line=91

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR

# THEOREM: Word.and is and_bits on the values
def wand(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.to_nat(n, Word.and(n, a, b)) == SR.and_bits(n, Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}:
  match n a b:
    case 0n WNil{} WNil{}:
      {==}
    case 1n+p WCon{+x, +t} WCon{+y, +u}:
      +e1 = to_nat_con(p, Bool.and(x, y), Word.and(p, t, u))
      +e2 = Equal.cong(Nat, Nat, z => Nat.add(bv(Bool.and(x, y)), Nat.double(z)), Word.to_nat(p, Word.and(p, t, u)), SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)), wand(p, t, u))
      +e3 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), bv(Bool.and(x, y)), Nat.mul(bv(x), bv(y)), bv_and(x, y))
      +e4 = Equal.sym(Nat, SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), Nat.add(Nat.mul(bv(x), bv(y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), and_step(p, bv(x), Word.to_nat(p, t), bv(y), Word.to_nat(p, u), bv_le(x), bv_le(y)))
      %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, t}), Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), to_nat_con(p, x, t)) : {Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}) == SR.and_bits(1n+p, _, Word.to_nat(1n+p, WCon{y, u})) : Nat}
      %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, u}), Nat.add(bv(y), Nat.double(Word.to_nat(p, u))), to_nat_con(p, y, u)) : {Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}) == SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), _) : Nat}
      Equal.trans(Nat, Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}), Nat.add(bv(Bool.and(x, y)), Nat.double(Word.to_nat(p, Word.and(p, t, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e1,
        Equal.trans(Nat, Nat.add(bv(Bool.and(x, y)), Nat.double(Word.to_nat(p, Word.and(p, t, u)))), Nat.add(bv(Bool.and(x, y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e2,
          Equal.trans(Nat, Nat.add(bv(Bool.and(x, y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), Nat.add(Nat.mul(bv(x), bv(y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e3, e4)))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend&name=and_step
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend&name=bv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend&name=bv_and
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend&name=bv_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend&name=to_nat_con
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend&name=and_bits