def round_jam

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.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/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/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/lib/logic.bend as L
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/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as FO

229# round(s, m, x) = round(s, jam(m >> d, m mod 2^d), x + d) when m has d + 55 bits
230def round_jam(+s: Bool, +d: Nat, +m: Nat, +x: Nat, +hb: {Nat.is_le(Nat.add(d, 55n), M.bit_length(m)) == True{} : Bool}) -> {SF.round(s, m, x) == SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)) : F.F64}:
231  +hb1 = L.subst(Nat, z => {Nat.is_le(z, M.bit_length(m)) == True{} : Bool}, Nat.add(d, 55n), 1n+Nat.add(d, 54n), Equal.trans(Nat, Nat.add(d, 55n), 1n+Nat.add(d, 54n), 1n+Nat.add(d, 54n), N.add_succ(d, 54n), {==}), hb)
232  +hz = nz_bl(m, Nat.add(d, 54n), hb1, Nat.is_eq(m, 0n), {==})
233  +j = Nat.sub(M.bit_length(m), 1n)
234  +ej = N.sub_add(M.bit_length(m), 1n, FO.bl_pos(m, hz, M.bit_length(m), {==}))
235  +hdj = N.le_trans(d, Nat.add(d, 54n), j, N.le_add_right(d, 54n), N.lt_succ_le(Nat.add(d, 54n), j, N.succ_le_lt(Nat.add(d, 54n), 1n+j, L.subst(Nat, z => {Nat.is_le(1n+Nat.add(d, 54n), z) == True{} : Bool}, M.bit_length(m), 1n+j, Equal.sym(Nat, 1n+j, M.bit_length(m), ej), hb1))))
236  +e = Nat.sub(j, d)
237  +eje = Equal.trans(Nat, Nat.add(e, d), Nat.add(d, e), j, NA.add_comm(e, d), N.sub_add(j, d, hdj))
238  +h = C.high(d, m)
239  +eB = Equal.trans(Nat, Nat.add(d, 1n+e), 1n+Nat.add(d, e), M.bit_length(m), N.add_succ(d, e), Equal.trans(Nat, 1n+Nat.add(d, e), 1n+j, M.bit_length(m), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(d, e), j, N.sub_add(j, d, hdj)), ej))
240  +fB = L.subst(Nat, z => {C.fits(z, m) == True{} : Bool}, M.bit_length(m), Nat.add(d, 1n+e), Equal.sym(Nat, Nat.add(d, 1n+e), M.bit_length(m), eB), bl_fit(m))
241  +fh1 = Equal.trans(Bool, C.fits(1n+e, h), C.fits(Nat.add(d, 1n+e), m), True{}, Equal.sym(Bool, C.fits(Nat.add(d, 1n+e), m), C.fits(1n+e, h), FR.fits_hc(d, 1n+e, m)), fB)
242  +nj = L.subst(Nat, z => {C.fits(z, m) == False{} : Bool}, j, Nat.add(d, e), Equal.sym(Nat, Nat.add(d, e), j, N.sub_add(j, d, hdj)), bl_nfit(m, hz))
243  +fh0 = Equal.trans(Bool, C.fits(e, h), C.fits(Nat.add(d, e), m), False{}, Equal.sym(Bool, C.fits(Nat.add(d, e), m), C.fits(e, h), FR.fits_hc(d, e, m)), nj)
244  rj2(s, d, m, x, hb, hz, e, fh0, fh1, eB)