Bits.and_join: 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 98-117 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=98&end_line=117

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/random/rand.bend as SR
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WI

# THEOREM: and on two limbs, (a1 + 2^k b1) & (a2 + 2^k b2) = a1 & a2 + 2^k (b1 & b2)
def and_join(+k: Nat, +j: Nat, +a1: Nat, +b1: Nat, +a2: Nat, +b2: Nat, +h1: {C.fits(k, a1) == True{} : Bool}, +h2: {C.fits(k, a2) == True{} : Bool}) -> {SR.and_bits(Nat.add(k, j), Nat.add(a1, C.shift(k, b1)), Nat.add(a2, C.shift(k, b2))) == Nat.add(SR.and_bits(k, a1, a2), C.shift(k, SR.and_bits(j, b1, b2))) : Nat}:
  match k:
    case 0n:
      %Equal.sym(Nat, a1, 0n, N.eq_from_is_eq(a1, 0n, h1)) : {SR.and_bits(j, Nat.add(_, b1), Nat.add(a2, b2)) == Nat.add(SR.and_bits(0n, _, a2), SR.and_bits(j, b1, b2)) : Nat}
      %Equal.sym(Nat, a2, 0n, N.eq_from_is_eq(a2, 0n, h2)) : {SR.and_bits(j, b1, Nat.add(_, b2)) == Nat.add(SR.and_bits(0n, 0n, _), SR.and_bits(j, b1, b2)) : Nat}
      {==}
    case 1n+p:
      +S1 = C.shift(p, b1)
      +S2 = C.shift(p, b2)
      +X = SR.and_bits(j, b1, b2)
      +B = Nat.mul(C.bit(a1), C.bit(a2))
      +Ih = and_join(p, j, C.half(a1), b1, C.half(a2), b2, h1, h2)
      %Equal.sym(Nat, C.bit(Nat.add(a1, Nat.double(S1))), C.bit(a1), WI.bit_dbl(a1, S1)) : {Nat.add(Nat.mul(_, C.bit(Nat.add(a2, Nat.double(S2)))), Nat.double(SR.and_bits(Nat.add(p, j), C.half(Nat.add(a1, Nat.double(S1))), C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
      %Equal.sym(Nat, C.bit(Nat.add(a2, Nat.double(S2))), C.bit(a2), WI.bit_dbl(a2, S2)) : {Nat.add(Nat.mul(C.bit(a1), _), Nat.double(SR.and_bits(Nat.add(p, j), C.half(Nat.add(a1, Nat.double(S1))), C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
      %Equal.sym(Nat, C.half(Nat.add(a1, Nat.double(S1))), Nat.add(C.half(a1), S1), WI.half_dbl(a1, S1)) : {Nat.add(B, Nat.double(SR.and_bits(Nat.add(p, j), _, C.half(Nat.add(a2, Nat.double(S2)))))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
      %Equal.sym(Nat, C.half(Nat.add(a2, Nat.double(S2))), Nat.add(C.half(a2), S2), WI.half_dbl(a2, S2)) : {Nat.add(B, Nat.double(SR.and_bits(Nat.add(p, j), Nat.add(C.half(a1), S1), _))) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
      %Equal.sym(Nat, SR.and_bits(Nat.add(p, j), Nat.add(C.half(a1), S1), Nat.add(C.half(a2), S2)), Nat.add(SR.and_bits(p, C.half(a1), C.half(a2)), C.shift(p, X)), Ih) : {Nat.add(B, Nat.double(_)) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
      %N.add_double(SR.and_bits(p, C.half(a1), C.half(a2)), C.shift(p, X)) : {Nat.add(B, _) == Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))) : Nat}
      Equal.sym(Nat, Nat.add(Nat.add(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2)))), Nat.double(C.shift(p, X))), Nat.add(B, Nat.add(Nat.double(SR.and_bits(p, C.half(a1), C.half(a2))), Nat.double(C.shift(p, X)))), N.add_assoc(B, Nat.double(SR.and_bits(p, C.half(a1), C.half(a2))), Nat.double(C.shift(p, X))))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_double
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=eq_from_is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=half_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=half
  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