PROOFText.wsd.sd: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 337-341 of bend-osdev-word64@0.1.1.0/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&start_line=337&end_line=341

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 UL
import bend-osdev-word64@0.1.1.0/word64.bend as W

# a = 10 q + r with r < 10, for q and r from W64.small.divmod(a, 10)
def wsd.sd(+a: W.W64) -> {Nat.add(Nat.mul(W.W64.to_nat(wsh.q(a)), 10n), U32.to_nat(wsh.r(a))) == W.W64.to_nat(a) : Nat} & {Nat.is_lt(U32.to_nat(wsh.r(a)), 10n) == True{} : Bool}:
  match a:
    case W.W64{+hh, +ll}:
      wsd.sd1(hh, ll, wsd.step(0, 0, U32.shrn(hh, 16n), {==}, Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.shrn(hh, 16n)), U.U32Nat.dbl(16n, 1n)), Nat.is_lt(U.U32Nat.high(16n, U32.to_nat(hh)), U.U32Nat.dbl(16n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(16n, 1n)), U32.to_nat(U32.shrn(hh, 16n)), U.U32Nat.high(16n, U32.to_nat(hh)), Equal.sym(Nat, U.U32Nat.high(16n, U32.to_nat(hh)), U32.to_nat(U32.shrn(hh, 16n)), Equal.sym(Nat, U32.to_nat(U32.shrn(hh, 16n)), U.U32Nat.high(16n, U32.to_nat(hh)), UL.u32_shrn_value(hh, 16n)))), UL.high_lt(16n, 16n, 32n, U32.to_nat(hh), {==}, wu.lt(hh))), {==}))

Uses (22):
  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.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=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=high_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_shrn_value
  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-u32@0.1.0.0/u32.bend&name=U32Nat.high
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.sd1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.step
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.q
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wu.lt
  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.to_nat