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

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend as SR
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

# THEOREM: the 64-bit and of rand.bend is and_bits on the values
def and64_value(+a: WU.U64, +b: WU.U64) -> {SW.value(R.and64(a, b)) == SR.and_bits(64n, SW.value(a), SW.value(b)) : Nat}:
  match a b:
    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
      %Equal.sym(Nat, U32.to_nat(U32.and(al, bl)), SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), uand(al, bl)) : {Nat.add(_, C.shift(32n, U32.to_nat(U32.and(ah, bh)))) == SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}
      %Equal.sym(Nat, U32.to_nat(U32.and(ah, bh)), SR.and_bits(32n, U32.to_nat(ah), U32.to_nat(bh)), uand(ah, bh)) : {Nat.add(SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), C.shift(32n, _)) == SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}
      Equal.sym(Nat, SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), Nat.add(SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), C.shift(32n, SR.and_bits(32n, U32.to_nat(ah), U32.to_nat(bh)))), and_join(32n, 32n, U32.to_nat(al), U32.to_nat(ah), U32.to_nat(bl), U32.to_nat(bh), WA.vb(al), WA.vb(bl)))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend&name=and_join
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend&name=uand
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=vb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend&name=and_bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=and64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64