PROOF.ud.k: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 1682-1698 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=1682&end_line=1698

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws

# r' + g b = 2 r + a, r' < b: the remainder after one step, at a width N
def ud.k(+N: Nat, +S: Nat, +B: Nat, +R: Nat, +A: Nat, +R1: Nat, +T: Bool, +L: Bool, +g: Bool, +eput: {Nat.add(S, U.U32Nat.dbl(N, U.U32Nat.bit(T))) == Nat.add(A, Nat.double(R)) : Nat}, +eL: {Nat.is_lt(S, B) == L : Bool}, +eg: {Bool.or(T, Bool.not(L)) == g : Bool}, +er1: {Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)) == Nat.add(S, U.U32Nat.dbl(N, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(L)))) : Nat}, +hA: {Nat.is_le(A, 1n) == True{} : Bool}, +hR: {Nat.is_lt(R, B) == True{} : Bool}, +hB: {Nat.is_lt(B, U.U32Nat.dbl(N, 1n)) == True{} : Bool}) -> {Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}:
  match T L g:
    case True{} True{} True{}:
      (Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 1n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 1n))), Nat.add(S, U.U32Nat.dbl(N, 1n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 1n), 1n, ur.r21())), eput), Equal.trans(Bool, Nat.is_lt(R1, B), Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), True{}, Equal.sym(Bool, Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.is_lt(R1, B), Equal.cong(Nat, Bool, zz => Nat.is_lt(R1, zz), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Laws.nat_add_cancel(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(B), Nat.add(B, B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Nat.double(B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(R1, Nat.mul(1n, B))), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), ur.r29(B, Nat.sub(B, 1n+R), Nat.sub(1n, A), R1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), zz), Nat.add(R1, Nat.mul(1n, B)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 1n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 1n))), Nat.add(S, U.U32Nat.dbl(N, 1n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 1n), 1n, ur.r21())), eput))), ur.r30(Nat.sub(B, 1n+R), Nat.sub(1n, A), A, R)), Equal.cong(Nat, Nat, zz => Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), zz), Nat.add(Nat.sub(1n, A), A), 1n, Laws.nat_le_witness(A, 1n, hA))), ur.r7(Nat.sub(B, 1n+R), R)), Equal.cong(Nat, Nat, zz => Nat.double(zz), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, Laws.nat_lt_witness(R, B, hR))), ur.r31(B))))), Laws.nat_lt_add(R1, Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)))))
    case True{} False{} True{}:
      Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(True{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, Laws.nat_succ_add_absurd(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(S, U.U32Nat.dbl(N, 1n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(S, Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Nat.add(S, U.U32Nat.dbl(N, 1n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.sub(S, B), B), Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Nat.add(S, Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(B)), Nat.add(Nat.add(Nat.sub(S, B), B), Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R))), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(B)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), 1n), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), Nat.add(Nat.sub(1n, A), A)), Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), 1n), ur.r26(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), Nat.sub(B, 1n+R), Nat.sub(1n, A), A, R), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), zz), Nat.add(Nat.sub(1n, A), A), 1n, Laws.nat_le_witness(A, 1n, hA))), ur.r27(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), Nat.sub(B, 1n+R), R)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(zz)), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, Laws.nat_lt_witness(R, B, hR))), ur.r28(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), B)), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Nat.add(Nat.sub(S, B), B), S, Laws.nat_le_witness(B, S, un.nlt_le(S, B, eL)))), Equal.cong(Nat, Nat, zz => Nat.add(S, zz), Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B), U.U32Nat.dbl(N, 1n), Laws.nat_lt_witness(B, U.U32Nat.dbl(N, 1n), hB))), eput)))
    case False{} False{} True{}:
      (Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 0n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 0n))), Nat.add(S, U.U32Nat.dbl(N, 0n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 0n), 0n, ur.r22())), eput), Equal.trans(Bool, Nat.is_lt(R1, B), Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), True{}, Equal.sym(Bool, Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.is_lt(R1, B), Equal.cong(Nat, Bool, zz => Nat.is_lt(R1, zz), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Laws.nat_add_cancel(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(B), Nat.add(B, B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Nat.double(B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(R1, Nat.mul(1n, B))), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), ur.r29(B, Nat.sub(B, 1n+R), Nat.sub(1n, A), R1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), zz), Nat.add(R1, Nat.mul(1n, B)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 0n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 0n))), Nat.add(S, U.U32Nat.dbl(N, 0n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 0n), 0n, ur.r22())), eput))), ur.r30(Nat.sub(B, 1n+R), Nat.sub(1n, A), A, R)), Equal.cong(Nat, Nat, zz => Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), zz), Nat.add(Nat.sub(1n, A), A), 1n, Laws.nat_le_witness(A, 1n, hA))), ur.r7(Nat.sub(B, 1n+R), R)), Equal.cong(Nat, Nat, zz => Nat.double(zz), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, Laws.nat_lt_witness(R, B, hR))), ur.r31(B))))), Laws.nat_lt_add(R1, Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)))))
    case False{} True{} False{}:
      (Equal.trans(Nat, Nat.add(R1, Nat.mul(0n, B)), Nat.add(S, U.U32Nat.dbl(N, 0n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(0n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(0n, 1n))), Nat.add(S, U.U32Nat.dbl(N, 0n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(0n, 1n), 0n, ur.r23())), eput), Equal.trans(Bool, Nat.is_lt(R1, B), Nat.is_lt(S, B), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, B), R1, S, Equal.trans(Nat, R1, Nat.add(S, U.U32Nat.dbl(N, Nat.mul(0n, 1n))), S, Equal.trans(Nat, R1, Nat.add(R1, Nat.mul(0n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(0n, 1n))), ur.r24(R1, B), er1), ur.r25(S, N))), eL))
    case True{} _ False{}:
      Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(False{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, un.tf(eg))
    case False{} False{} False{}:
      Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(False{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, un.tf(eg))
    case False{} True{} True{}:
      Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(True{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, un.ft(eg))

Uses (38):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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.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_le
  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=Nat.sub
  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=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_witness
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_witness
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_succ_add_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.nlt_le
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.tf
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r21
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r22
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r23
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r24
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r25
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r26
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r27
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r28
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r29
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r30
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r31
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r7
  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