def rp_nc

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:879

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/u64.bend as WU

879def rp_nc(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +u: Nat, +hEF: {Nat.add(Nat.sub(e, F.off()), 1926n) == u : Nat}, +o: Bool, +ho: {Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)) == o : Bool}) -> {F.rp_over(s, e, sig, o) == SF.pack(s, SF.rne(SW.value(sig), 10n), u) : F.F64}:
880  match o:
881    case True{}:
882      +hovF = not_t(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n), ho)
883      Equal.trans(F.F64, F.inf(s), SF.inf(s), SF.pack(s, SF.rne(SW.value(sig), 10n), u), inf_v(s), Equal.sym(F.F64, SF.pack(s, SF.rne(SW.value(sig), 10n), u), SF.inf(s), pko(s, SF.rne(SW.value(sig), 10n), u, Nat.sub(e, F.off()), hEF, rne_norm(SW.value(sig), h62), hovF)))
884    case False{}:
885      +hovT = not_f(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n), ho)
886      +hz = rne_norm(SW.value(sig), h62)
887      +hq = rne_top(one, h1, SW.value(sig), h63)
888      +i1 = rpfE(s, Nat.sub(e, F.off()), sig, h63, ef11(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n), hovT), hz, qfit(one, h1, SF.rne(SW.value(sig), 10n), Nat.sub(e, F.off()), hq, hz, hovT))
889      +h0 = Equal.cong(Bool, Bool, t => Bool.or(Bool.not(t), Nat.is_eq(Nat.sub(e, F.off()), 0n)), C.fits(52n, SF.rne(SW.value(sig), 10n)), False{}, hz)
890      +sp = pkg(one, h1, s, SF.rne(SW.value(sig), 10n), u, Nat.sub(e, F.off()), hEF, hq, h0, hovT)
891      Equal.trans(F.F64, F.rp_fin(s, Nat.sub(e, F.off()), sig), bits(s, Nat.add(SF.rne(SW.value(sig), 10n), C.shift(52n, Nat.sub(e, F.off())))), SF.pack(s, SF.rne(SW.value(sig), 10n), u), i1, Equal.sym(F.F64, SF.pack(s, SF.rne(SW.value(sig), 10n), u), bits(s, Nat.add(SF.rne(SW.value(sig), 10n), C.shift(52n, Nat.sub(e, F.off())))), sp))