def rt_sub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:229

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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64exp.bend as EX

229def rt_sub(+s: Bool, +Fr: Nat, +hF: {C.fits(52n, Fr) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(Fr, 0n) == z : Bool}) -> {SF.round(s, Fr, 1926n) == SF.encode(s, 0n, Fr) : F.F64}:
230  match z:
231    case True{}:
232      +e0 = N.eq_from_is_eq(Fr, 0n, hz)
233      +ea = Equal.cong(Nat, F.F64, t => SF.round(s, t, 1926n), Fr, 0n, e0)
234      +eb = Equal.trans(F.F64, SF.encode(s, 0n, 0n), FR.bits(s, 0n), SF.zero(s), FR.enc_bits(s, 0n, 0n), EX.bz(s))
235      +ec = Equal.cong(Nat, F.F64, t => SF.encode(s, 0n, t), 0n, Fr, Equal.sym(Nat, Fr, 0n, N.eq_from_is_eq(Fr, 0n, hz)))
236      Equal.trans(F.F64, SF.round(s, Fr, 1926n), SF.zero(s), SF.encode(s, 0n, Fr), ea, Equal.trans(F.F64, SF.zero(s), SF.encode(s, 0n, 0n), SF.encode(s, 0n, Fr), Equal.sym(F.F64, SF.encode(s, 0n, 0n), SF.zero(s), eb), ec))
237    case False{}:
238      +B = M.bit_length(Fr)
239      +A = Nat.sub(Nat.add(1926n, B), 53n)
240      +hB = BL.bl_le(52n, Fr, hF, Nat.is_le(B, 52n), {==})
241      +emax = EX.max_le(A, 1926n, N.le_trans(B, 52n, 53n, hB, {==}))
242      +e1 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, Fr, 1926n, Nat.max(A, Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(Fr, 0n), False{}, hz)
243      +e2 = Equal.cong(Nat, F.F64, u => SF.round_u(s, Fr, 1926n, u), Nat.max(A, 1926n), 1926n, emax)
244      +r1 = SF.round_u(s, Fr, 1926n, Nat.max(A, 1926n))
245      +r2 = SF.round_u(s, Fr, 1926n, 1926n)
246      Equal.trans(F.F64, SF.round(s, Fr, 1926n), r1, SF.encode(s, 0n, Fr), e1, Equal.trans(F.F64, r1, r2, SF.encode(s, 0n, Fr), e2, ru_self(s, Fr, 1926n, hF)))