Bitcount.go: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend as Bitcount
Lines 29-41 of bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend&start_line=29&end_line=41

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/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

# the loop adds the ones of its fuel's worth of bits
def go(+f: Nat, +n: Nat, +acc: Nat) -> {NB.bit_count_go(f, n, acc) == Nat.add(acc, SN.ones(f, n)) : Nat}:
  match f n:
    case 0n _:
      Equal.sym(Nat, Nat.add(acc, 0n), acc, A.add_zero(acc))
    case 1n+ +g 0n:
      %Equal.sym(Nat, SN.ones(g, 0n), 0n, ones_zero(g)) : {acc == Nat.add(acc, _) : Nat}
      Equal.sym(Nat, Nat.add(acc, 0n), acc, A.add_zero(acc))
    case 1n+ +g 1n+ +np:
      %Equal.sym(Nat, C.bit(1n+np), Nat.mod(1n+np, 2n), WW.bit_mod(1n+np)) : {NB.bit_count_go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n))) == Nat.add(acc, Nat.add(_, SN.ones(g, C.half(1n+np)))) : Nat}
      %Equal.sym(Nat, C.half(1n+np), Nat.div(1n+np, 2n), half_div2(1n+np)) : {NB.bit_count_go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n))) == Nat.add(acc, Nat.add(Nat.mod(1n+np, 2n), SN.ones(g, _))) : Nat}
      %A.add_assoc(acc, Nat.mod(1n+np, 2n), SN.ones(g, Nat.div(1n+np, 2n))) : {NB.bit_count_go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n))) == _ : Nat}
      go(g, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n)))

Uses (14):
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend&name=half_div2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend&name=ones_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_mod
  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=half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/number.bend&name=ones
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/number.bend&name=bit_count_go