W64mul.split16: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64mul
Lines 88-96 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&start_line=88&end_line=96

import Base
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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD

# v(x) == lo + 2^16 hi
def split16(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}) -> {v(x) == Nat.add(lo16(x, m), WD.sc(16n, hi16(x, c))) : Nat}:
  +em = dm16(one, h1, x, c, pc)
  +ea = PD.and32(16n, x, m, pm)
  +bm = L.subst(Nat, z => {Nat.is_lt(v(U32.mod(x, c)), z) == True{} : Bool}, v(c), WD.sc(16n, one), h16(one, h1, c, pc), PD.dm_l(x, c, nz16(c, pc)))
  +ex = Equal.trans(Nat, Nat.add(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), v(x), Nat.add(lo16(x, m), WD.sc(16n, PD.hp32(16n, x))), Equal.trans(Nat, Nat.add(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), v(x), N.add_comm(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), em), ea)
  +er = WD.uniq(16n, one, h1, v(U32.mod(x, c)), lo16(x, m), hi16(x, c), PD.hp32(16n, x), ex, bm, lo16_lt(one, h1, x, m, pm))
  %er : {v(x) == Nat.add(_, WD.sc(16n, hi16(x, c))) : Nat}
  Equal.trans(Nat, v(x), Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), Nat.add(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), Equal.sym(Nat, Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), v(x), em), N.add_comm(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))))

Uses (24):
  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=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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=uniq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=dm16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=h16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=hi16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=lo16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=lo16_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=nz16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=and32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=dm_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=hp32