def nrp_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64nrp.bend:147

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

147def nrp_c(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hz: {Nat.is_eq(SW.value(sig), 0n) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hx63: {Nat.is_le(63n, x) == True{} : Bool}, +d: Bool, +hd: {Bool.and(Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)))) == d : Bool}) -> {F.nrp_pick(s, e, sig, Nat.sub(X.clz(sig), 1n), d) == SF.round(s, SW.value(sig), x) : F.F64}:
148  match d:
149    case True{}:
150      +ha = and_l(Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n))), hd)
151      +hb = and_r(Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n))), hd)
152      nrp_d(one, h1, s, e, sig, x, hx, hz, h63, hx63, ha, and_l(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)), hb), and_r(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)), hb))
153    case False{}:
154      nrp_r(one, h1, s, e, sig, x, hx, hz, h63, hx63)