PROOFText.wsh.rd: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 354-355 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=354&end_line=355

import Base
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 wsh.rd(+r: U32, +acc: String, +x: Nat, +hr: {Nat.is_lt(U32.to_nat(r), 10n) == True{} : Bool}) -> {Nat.read.go(SCon{W.W64.digit(r), acc}, x) == Nat.read.go(acc, Nat.add(Nat.mul(x, 10n), U32.to_nat(r))) : Maybe<&2, Nat>}:
  Equal.trans(Maybe<&2, Nat>, Nat.read.if(acc, x, U32.sub(U32.add(48, r), 48), U32.is_lt(U32.sub(U32.add(48, r), 48), 10)), Nat.read.if(acc, x, r, U32.is_lt(r, 10)), Nat.read.go(acc, Nat.add(Nat.mul(x, 10n), U32.to_nat(r))), Equal.cong(U32, Maybe<&2, Nat>, zz => Nat.read.if(acc, x, zz, U32.is_lt(zz, 10)), U32.sub(U32.add(48, r), 48), r, wsh.ed(r, hr)), Equal.cong(Bool, Maybe<&2, Nat>, zz => Nat.read.if(acc, x, r, zz), U32.is_lt(r, 10), True{}, Equal.trans(Bool, U32.is_lt(r, 10), Nat.is_lt(U32.to_nat(r), U32.to_nat(10)), True{}, UL.u32_lt_value(r, 10), hr)))

Uses (19):
  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.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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=Nat.read.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.read.if
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  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_lt_value
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.ed
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.digit