PROOFDiv.wd.bs: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_div.bend as PROOFDiv
Lines 395-398 of bend-osdev-word64@0.1.1.0/PROOF_div.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&start_line=395&end_line=398

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-word64@0.1.1.0/word64.bend as W

def wd.bs(+p: Nat, +x: Bool, +hi: Word(p), +b: W.W64, +q: W.W64, +r: W.W64, +hb: {Nat.is_lt(W.W64.to_nat(b), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, +hX: {Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, ih: {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))) == Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r))))) == Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}:
  (+e, +l) = ih
  %Equal.sym(W.W64 & W.W64, W.W64.div.bits(p, hi, b, (q, r)), (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))), wd.eta(W.W64.div.bits(p, hi, b, (q, r)))) : {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, _))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, _)))) == Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, _))), W.W64.to_nat(b)) == True{} : Bool}
  (Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b), wd.st(x, b, W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))), l, hb, Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Equal.sym(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), U.U32Nat.bit(x)), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), e), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi)))), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), wr.d8(p, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), Word.to_nat(p, hi), U.U32Nat.bit(x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), zz), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), Word.to_nat(1n+p, WCon{x, hi}), Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, hi}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), wd.wv(p, x, hi)))), {==}))))), hX))), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), U.U32Nat.bit(x)), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), e), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi)))), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), wr.d8(p, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), Word.to_nat(p, hi), U.U32Nat.bit(x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), zz), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), Word.to_nat(1n+p, WCon{x, hi}), Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, hi}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), wd.wv(p, x, hi)))), {==}))), wd.p2(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b), wd.st(x, b, W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))), l, hb, Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Equal.sym(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), U.U32Nat.bit(x)), Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), e), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), Equal.trans(Nat, Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi))), U.U32Nat.bit(x)), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi)))), Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), Word.to_nat(1n+p, WCon{x, hi})), wr.d8(p, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), Word.to_nat(p, hi), U.U32Nat.bit(x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), zz), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), Word.to_nat(1n+p, WCon{x, hi}), Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, hi}), Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, hi))), wd.wv(p, x, hi)))), {==}))))), hX))))

Uses (28):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wd.eta
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wd.p1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wd.p2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wd.st
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wd.wv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_div.bend&name=wr.d8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.div.bits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.div.step
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.fst
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.snd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat