PROOFText.wsd.sd4b: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 309-310 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=309&end_line=310

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

def wsd.sd4b(+hh: U32, +ll: U32, +a1: {U32.to_nat(wsd.q(0, 0, U32.shrn(hh, 16n))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(0)), U32.to_nat(wsd.d(0, U32.shrn(hh, 16n)))) : Nat}, +a2: {U32.to_nat(wsd.q(wsd.q(0, 0, U32.shrn(hh, 16n)), wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(wsd.q(0, 0, U32.shrn(hh, 16n)))), U32.to_nat(wsd.d(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)))) : Nat}, +a3: {U32.to_nat(wsd.q(0, wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(0)), U32.to_nat(wsd.d(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)))) : Nat}, +b1: {Nat.add(Nat.mul(U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), 10n), U32.to_nat(wsd.m(0, U32.shrn(hh, 16n)))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(0)), U32.to_nat(U32.shrn(hh, 16n))) : Nat}, +b2: {Nat.add(Nat.mul(U32.to_nat(wsd.d(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535))), 10n), U32.to_nat(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(wsd.m(0, U32.shrn(hh, 16n)))), U32.to_nat(U32.and(hh, 65535))) : Nat}, +b3: {Nat.add(Nat.mul(U32.to_nat(wsd.d(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n))), 10n), U32.to_nat(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)))), U32.to_nat(U32.shrn(ll, 16n))) : Nat}, +a4: {U32.to_nat(wsd.q(wsd.q(0, wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(wsd.q(0, wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)))), U32.to_nat(wsd.d(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535)))) : Nat}, +b4: {Nat.add(Nat.mul(U32.to_nat(wsd.d(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535))), 10n), U32.to_nat(wsd.m(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535)))) == Nat.add(U.U32Nat.dbl(16n, U32.to_nat(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)))), U32.to_nat(U32.and(ll, 65535))) : Nat}, +m4: {Nat.is_lt(U32.to_nat(wsd.m(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535))), 10n) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.small.q(W.W64.small.divmod(W.W64{hh, ll}, 10))), 10n), U32.to_nat(W.W64.small.r(W.W64.small.divmod(W.W64{hh, ll}, 10)))) == W.W64.to_nat(W.W64{hh, ll}) : Nat} & {Nat.is_lt(U32.to_nat(W.W64.small.r(W.W64.small.divmod(W.W64{hh, ll}, 10))), 10n) == True{} : Bool}:
  (wsd.alg(U32.to_nat(hh), U32.to_nat(ll), U32.to_nat(0), U32.to_nat(U32.shrn(hh, 16n)), U32.to_nat(U32.and(hh, 65535)), U32.to_nat(U32.shrn(ll, 16n)), U32.to_nat(U32.and(ll, 65535)), U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), U32.to_nat(wsd.d(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535))), U32.to_nat(wsd.d(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n))), U32.to_nat(wsd.d(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535))), U32.to_nat(wsd.m(0, U32.shrn(hh, 16n))), U32.to_nat(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535))), U32.to_nat(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n))), U32.to_nat(wsd.m(wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535))), U32.to_nat(wsd.q(0, 0, U32.shrn(hh, 16n))), U32.to_nat(wsd.q(wsd.q(0, 0, U32.shrn(hh, 16n)), wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535))), U32.to_nat(wsd.q(0, wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n))), U32.to_nat(wsd.q(wsd.q(0, wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), wsd.m(wsd.m(wsd.m(0, U32.shrn(hh, 16n)), U32.and(hh, 65535)), U32.shrn(ll, 16n)), U32.and(ll, 65535))), {==}, a1, a2, a3, a4, b1, b2, b3, b4, UL.u32_shrn_value(hh, 16n), UL.u32_and_65535(hh), UL.u32_shrn_value(ll, 16n), UL.u32_and_65535(ll)), m4)

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  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=u32_and_65535
  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-word64@0.1.1.0/PROOF_text.bend&name=wsd.alg
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.d
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.m
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.q
  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.small.divmod
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.small.q
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.small.r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat