def rw_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64tools.bend:155

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
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

155def rw_c(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +x: Nat, +w: WU.U64, +hx: {Nat.is_le(63n, x) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(SW.value(w), 0n) == z : Bool}) -> {F.rw_z(s, x, w, z) == SF.round(s, SW.value(w), x) : F.F64}:
156  match z:
157    case True{}:
158      +e1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(s), SF.round_u(s, SW.value(w), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(SW.value(w))), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(SW.value(w), 0n), True{}, hz)
159      Equal.trans(F.F64, F.zero(s), SF.zero(s), SF.round(s, SW.value(w), x), zero_eq(s), Equal.sym(F.F64, SF.round(s, SW.value(w), x), SF.zero(s), e1))
160    case False{}:
161      +et = Equal.cong(Bool, F.F64, t => F.rw_top(s, x, w, t), X.le(WU.U64{0, 2147483648}, w), Bool.not(C.fits(63n, SW.value(w))), top_eq(one, h1, w, 2147483648, {==}))
162      Equal.trans(F.F64, F.rw_top(s, x, w, X.le(WU.U64{0, 2147483648}, w)), F.rw_top(s, x, w, Bool.not(C.fits(63n, SW.value(w)))), SF.round(s, SW.value(w), x), et, rw_f(one, h1, s, x, w, hx, hz, C.fits(63n, SW.value(w)), {==}))