def wsh.rd

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:354

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

354def 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>}:
355  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)))