def wsd.sd1b
bend-osdev-word64@0.1.1.0 · PROOF_text.bend:330
import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
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
330def wsd.sd1b(+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}, +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}, +m1: {Nat.is_lt(U32.to_nat(wsd.m(0, U32.shrn(hh, 16n))), 10n) == True{} : Bool}, +d1: {Nat.is_lt(U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), U.U32Nat.dbl(16n, 1n)) == 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}:
331 wsd.sd2(hh, ll, a1, b1, wsd.step(wsd.m(0, U32.shrn(hh, 16n)), wsd.q(0, 0, U32.shrn(hh, 16n)), U32.and(hh, 65535), m1, Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.and(hh, 65535)), U.U32Nat.dbl(16n, 1n)), Nat.is_lt(U.U32Nat.low(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.and(hh, 65535)), U.U32Nat.low(16n, U32.to_nat(hh)), Equal.sym(Nat, U.U32Nat.low(16n, U32.to_nat(hh)), U32.to_nat(U32.and(hh, 65535)), Equal.sym(Nat, U32.to_nat(U32.and(hh, 65535)), U.U32Nat.low(16n, U32.to_nat(hh)), UL.u32_and_65535(hh)))), UL.low_lt(16n, U32.to_nat(hh))), Equal.trans(Bool, Nat.is_lt(U32.to_nat(wsd.q(0, 0, U32.shrn(hh, 16n))), U.U32Nat.dbl(16n, 1n)), Nat.is_lt(U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), U.U32Nat.dbl(16n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(16n, 1n)), U32.to_nat(wsd.q(0, 0, U32.shrn(hh, 16n))), U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), Equal.sym(Nat, U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), U32.to_nat(wsd.q(0, 0, U32.shrn(hh, 16n))), Equal.sym(Nat, U32.to_nat(wsd.q(0, 0, U32.shrn(hh, 16n))), U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), Equal.trans(Nat, 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)))), U32.to_nat(wsd.d(0, U32.shrn(hh, 16n))), a1, {==})))), d1)))