def wsd.e

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

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

343def wsd.e(+a: W.W64, pr: {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}) -> {Nat.add(Nat.mul(W.W64.to_nat(wsh.q(a)), 10n), U32.to_nat(wsh.r(a))) == W.W64.to_nat(a) : Nat}:
344  (+u, +w) = pr
345  u