U64int.blsim: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend as U64int
Lines 386-399 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&start_line=386&end_line=399

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

def blsim(+f: Nat, +k: Nat, +n: WU.U64, +cz: Bool, +nn: Nat, +hcz: {I.u64_is(NM.IsZero{n}) == cz : Bool}, +hnn: {v(n) == nn : Nat}) -> {G.bit_length_go(~WU.U64, ~I.u64_op, ~I.u64_is, f, k, (n, cz)) == M.bit_length_go(f, nn, k) : Nat}:
  match f cz nn:
    case 0n _ _:
      {==}
    case 1n+g True{} 0n:
      {==}
    case 1n+g True{} 1n+np:
      Empty.absurd({G.bit_length_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, k, (n, True{})) == M.bit_length_go(1n+g, 1n+np, k) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u64_is(NM.IsZero{n}), False{}, Equal.sym(Bool, I.u64_is(NM.IsZero{n}), True{}, hcz), iz(n, 1n+np, hnn))))
    case 1n+g False{} 0n:
      Empty.absurd({G.bit_length_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, k, (n, False{})) == M.bit_length_go(1n+g, 0n, k) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u64_is(NM.IsZero{n}), False{}, Equal.sym(Bool, I.u64_is(NM.IsZero{n}), True{}, iz(n, 0n, hnn)), hcz)))
    case 1n+ +g False{} 1n+ +np:
      +h = I.u64_op(NM.Half{n})
      +eh = Equal.trans(Nat, v(h), Nat.div(v(n), 2n), Nat.div(1n+np, 2n), LW.ops_half(n), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(n), 1n+np, hnn))
      blsim(g, 1n+k, h, I.u64_is(NM.IsZero{h}), Nat.div(1n+np, 2n), {==}, eh)

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=iz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=true_ne_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend&name=ops_half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=bit_length_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u64_is
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u64_op
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=bit_length_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Test
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64