F64round.sticky: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round Lines 157-178 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&start_line=157&end_line=178 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/proofs/lib/lemmas/proofs/nat_algebra.bend as NA import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC # rounding m by K + D bits is rounding jam(m >> D, m mod 2^D) by K bits, K >= 2 def sticky(+i: Nat, +D: Nat, +m: Nat) -> {SF.rne(m, Nat.add(2n+i, D)) == SF.rne(SW.jam(C.high(D, m), C.low(D, m)), 2n+i) : Nat}: +eA = NA.add_comm(D, 2n+i) +qm = Equal.trans(Nat, C.high(Nat.add(2n+i, D), m), C.high(Nat.add(D, 2n+i), m), C.high(2n+i, C.high(D, m)), Equal.cong(Nat, Nat, z => C.high(z, m), Nat.add(2n+i, D), Nat.add(D, 2n+i), Equal.sym(Nat, Nat.add(D, 2n+i), Nat.add(2n+i, D), eA)), WW.high_comp(2n+i, D, m)) +rm = Equal.trans(Nat, C.low(Nat.add(2n+i, D), m), C.low(Nat.add(D, 2n+i), m), Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), Equal.cong(Nat, Nat, z => C.low(z, m), Nat.add(2n+i, D), Nat.add(D, 2n+i), Equal.sym(Nat, Nat.add(D, 2n+i), Nat.add(2n+i, D), eA)), FB.low_split(D, 2n+i, m)) +hm = Equal.trans(Nat, C.shift(Nat.add(1n+i, D), 1n), C.shift(Nat.add(D, 1n+i), 1n), C.shift(D, C.shift(1n+i, 1n)), Equal.cong(Nat, Nat, z => C.shift(z, 1n), Nat.add(1n+i, D), Nat.add(D, 1n+i), NA.add_comm(1n+i, D)), WW.shift_comp(D, 1n+i, 1n)) +c1 = Equal.trans(Cmp, Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(Nat.add(1n+i, D), 1n)), Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(D, C.shift(1n+i, 1n))), Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(Nat.add(1n+i, D), 1n)), C.low(Nat.add(2n+i, D), m), Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), rm), Equal.cong(Nat, Cmp, z => Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), z), C.shift(Nat.add(1n+i, D), 1n), C.shift(D, C.shift(1n+i, 1n)), hm)) +c2 = NC.cmp_limbs(D, C.low(D, m), C.low(2n+i, C.high(D, m)), 0n, C.shift(1n+i, 1n), WW.low_fits(D, m), fz(D)) +c3 = Equal.cong(Cmp, Cmp, z => NC.lex(z, Nat.cmp(C.low(D, m), 0n)), Nat.cmp(C.low(2n+i, C.high(D, m)), C.shift(1n+i, 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n)), NC.cmp_limbs(1n, C.bit(C.high(D, m)), C.low(1n+i, C.half(C.high(D, m))), 0n, C.shift(i, 1n), small(C.bit(C.high(D, m)), WW.bit_le1(C.high(D, m))), fz(1n))) +c4 = lex_assoc(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n), Nat.cmp(C.low(D, m), 0n)) +c5 = Equal.cong(Cmp, Cmp, z => NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), z), NC.lex(Nat.cmp(C.bit(C.high(D, m)), 0n), Nat.cmp(C.low(D, m), 0n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n), tl(C.bit(C.high(D, m)), C.low(D, m), WW.bit_le1(C.high(D, m)))) +cm = Equal.trans(Cmp, Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(D, C.shift(1n+i, 1n))), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c1, Equal.trans(Cmp, Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(D, C.shift(1n+i, 1n))), NC.lex(Nat.cmp(C.low(2n+i, C.high(D, m)), C.shift(1n+i, 1n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c2, Equal.trans(Cmp, NC.lex(Nat.cmp(C.low(2n+i, C.high(D, m)), C.shift(1n+i, 1n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c3, Equal.trans(Cmp, NC.lex(NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), NC.lex(Nat.cmp(C.bit(C.high(D, m)), 0n), Nat.cmp(C.low(D, m), 0n))), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c4, c5)))) +lhs = Equal.trans(Nat, SF.rne_up(C.high(Nat.add(2n+i, D), m), C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), rne_c(C.high(Nat.add(2n+i, D), m), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), rne_cmp(C.high(Nat.add(2n+i, D), m), C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), Equal.trans(Nat, rne_c(C.high(Nat.add(2n+i, D), m), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), rne_c(C.high(2n+i, C.high(D, m)), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), Equal.cong(Nat, Nat, z => rne_c(z, Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), C.high(Nat.add(2n+i, D), m), C.high(2n+i, C.high(D, m)), qm), Equal.cong(Cmp, Nat, z => rne_c(C.high(2n+i, C.high(D, m)), z), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), cm))) +jf = jam_form(C.high(D, m), C.low(D, m)) +hbt = max_le1(C.bit(C.high(D, m)), C.low(D, m), WW.bit_le1(C.high(D, m))) +hJ = Equal.trans(Nat, C.half(SW.jam(C.high(D, m), C.low(D, m))), C.half(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), C.half(C.high(D, m)), Equal.cong(Nat, Nat, z => C.half(z), SW.jam(C.high(D, m), C.low(D, m)), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m)))), jf), Equal.trans(Nat, C.half(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), Nat.add(C.half(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n))), C.half(C.high(D, m))), C.half(C.high(D, m)), WW.half_dbl(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), C.half(C.high(D, m))), Equal.cong(Nat, Nat, z => Nat.add(z, C.half(C.high(D, m))), C.half(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n))), 0n, half_small(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), hbt)))) +bJ = Equal.trans(Nat, C.bit(SW.jam(C.high(D, m), C.low(D, m))), C.bit(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Equal.cong(Nat, Nat, z => C.bit(z), SW.jam(C.high(D, m), C.low(D, m)), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m)))), jf), Equal.trans(Nat, C.bit(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), C.bit(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n))), Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), WW.bit_dbl(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), C.half(C.high(D, m))), bit_small(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), hbt))) +qJ = Equal.cong(Nat, Nat, z => C.high(1n+i, z), C.half(SW.jam(C.high(D, m), C.low(D, m))), C.half(C.high(D, m)), hJ) +lJ = Equal.trans(Nat, Nat.add(C.bit(SW.jam(C.high(D, m), C.low(D, m))), Nat.double(C.low(1n+i, C.half(SW.jam(C.high(D, m), C.low(D, m)))))), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(SW.jam(C.high(D, m), C.low(D, m)))))), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(C.high(D, m))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(C.low(1n+i, C.half(SW.jam(C.high(D, m), C.low(D, m)))))), C.bit(SW.jam(C.high(D, m), C.low(D, m))), Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), bJ), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, z))), C.half(SW.jam(C.high(D, m), C.low(D, m))), C.half(C.high(D, m)), hJ)) +cJ = Equal.trans(Cmp, Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), Nat.cmp(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(C.high(D, m))))), C.shift(1n+i, 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(1n+i, 1n)), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(C.high(D, m))))), lJ), NC.cmp_limbs(1n, Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), C.low(1n+i, C.half(C.high(D, m))), 0n, C.shift(i, 1n), small(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), hbt), fz(1n))) +rhs = Equal.trans(Nat, SF.rne_up(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), rne_c(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), rne_cmp(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), Equal.trans(Nat, rne_c(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), rne_c(C.high(2n+i, C.high(D, m)), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), Equal.cong(Nat, Nat, z => rne_c(z, Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.high(2n+i, C.high(D, m)), qJ), Equal.cong(Cmp, Nat, z => rne_c(C.high(2n+i, C.high(D, m)), z), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), cJ))) Equal.trans(Nat, SF.rne_up(C.high(Nat.add(2n+i, D), m), C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), SF.rne_up(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), lhs, Equal.sym(Nat, SF.rne_up(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), rhs)) Uses (38): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.max https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=low_split https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=bit_small https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=fz https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=half_small https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=jam_form https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=lex_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=max_le1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=rne_c https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=rne_cmp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=small https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=tl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=cmp_limbs https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=lex https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_dbl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_le1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=half_dbl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_comp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=bit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=half https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=rne https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=rne_up https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=jam