def rj2
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:198
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as F64rtools
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/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
198def rj2(+s: Bool, +d: Nat, +m: Nat, +x: Nat, +hb: {Nat.is_le(Nat.add(d, 55n), M.bit_length(m)) == True{} : Bool}, +hz: {Nat.is_eq(m, 0n) == False{} : Bool}, +e: Nat, +fh0: {C.fits(e, C.high(d, m)) == False{} : Bool}, +fh1: {C.fits(1n+e, C.high(d, m)) == True{} : Bool}, +eB: {Nat.add(d, 1n+e) == M.bit_length(m) : Nat}) -> {SF.round(s, m, x) == SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)) : F.F64}:
199 +ejf = FR.jam_form(C.high(d, m), C.low(d, m))
200 +hhb = WW.le_add_r(C.bit(C.high(d, m)), Nat.max(C.bit(C.high(d, m)), Nat.min(C.low(d, m), 1n)), Nat.double(C.half(C.high(d, m))), max_ge_l(C.bit(C.high(d, m)), Nat.min(C.low(d, m), 1n)))
201 +hhJ = L.subst(Nat, z => {Nat.is_le(z, SW.jam(C.high(d, m), C.low(d, m))) == True{} : Bool}, Nat.add(C.bit(C.high(d, m)), Nat.double(C.half(C.high(d, m)))), C.high(d, m), Equal.sym(Nat, C.high(d, m), Nat.add(C.bit(C.high(d, m)), Nat.double(C.half(C.high(d, m)))), WW.hb(C.high(d, m))), L.subst(Nat, z => {Nat.is_le(Nat.add(C.bit(C.high(d, m)), Nat.double(C.half(C.high(d, m)))), z) == True{} : Bool}, 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)))), SW.jam(C.high(d, m), C.low(d, m)), Equal.sym(Nat, 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)))), ejf), hhb))
202 +nfJ = FR.nfit(e, C.high(d, m), SW.jam(C.high(d, m), C.low(d, m)), hhJ, fh0)
203 +fJ1 = Equal.trans(Bool, C.fits(1n+e, SW.jam(C.high(d, m), C.low(d, m))), C.fits(1n+e, C.high(d, m)), True{}, jam_fits(e, C.high(d, m), C.low(d, m)), fh1)
204 +eblJ = FR.bl_c(e, SW.jam(C.high(d, m), C.low(d, m)), nfJ, fJ1, Nat.cmp(M.bit_length(SW.jam(C.high(d, m), C.low(d, m))), 1n+e), {==})
205 +hzJ = FR.nz_of(e, SW.jam(C.high(d, m), C.low(d, m)), nfJ)
206 +ea = Equal.trans(Nat, Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), Nat.add(Nat.add(x, d), 1n+e), Nat.add(x, M.bit_length(m)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, d), z), M.bit_length(SW.jam(C.high(d, m), C.low(d, m))), 1n+e, eblJ), Equal.trans(Nat, Nat.add(Nat.add(x, d), 1n+e), Nat.add(x, Nat.add(d, 1n+e)), Nat.add(x, M.bit_length(m)), NA.add_assoc(x, d, 1n+e), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(d, 1n+e), M.bit_length(m), eB)))
207 +eU = Equal.cong(Nat, Nat, z => Nat.max(Nat.sub(z, 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), Nat.add(x, M.bit_length(m)), ea)
208 +ed55 = Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), 53n), Nat.add(x, Nat.add(Nat.add(d, 2n), 53n)), Nat.add(x, Nat.add(d, 55n)), NA.add_assoc(x, Nat.add(d, 2n), 53n), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(Nat.add(d, 2n), 53n), Nat.add(d, 55n), NA.add_assoc(d, 2n, 53n)))
209 +a0 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(x, M.bit_length(m))) == True{} : Bool}, Nat.add(x, Nat.add(d, 55n)), Nat.add(Nat.add(x, Nat.add(d, 2n)), 53n), Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), 53n), Nat.add(x, Nat.add(d, 55n)), ed55), N.le_add_left(Nat.add(d, 55n), M.bit_length(m), x, hb))
210 +hu = N.le_trans(Nat.add(x, Nat.add(d, 2n)), Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), le_sub(Nat.add(x, Nat.add(d, 2n)), 53n, Nat.add(x, M.bit_length(m)), a0), max_ge_l(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))
211 +i = Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, Nat.add(d, 2n)))
212 +eu = N.sub_add(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, Nat.add(d, 2n)), hu)
213 +k1 = Equal.trans(Nat, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x), Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), x), Nat.add(2n+i, d), Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), eu)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), x), Nat.sub(Nat.add(x, Nat.add(Nat.add(d, 2n), i)), x), Nat.add(2n+i, d), Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.add(x, Nat.add(Nat.add(d, 2n), i)), NA.add_assoc(x, Nat.add(d, 2n), i)), Equal.trans(Nat, Nat.sub(Nat.add(x, Nat.add(Nat.add(d, 2n), i)), x), Nat.add(Nat.add(d, 2n), i), Nat.add(2n+i, d), N.add_sub_cancel(x, Nat.add(Nat.add(d, 2n), i)), Equal.trans(Nat, Nat.add(Nat.add(d, 2n), i), Nat.add(d, 2n+i), Nat.add(2n+i, d), NA.add_assoc(d, 2n, i), NA.add_comm(d, 2n+i)))))
214 +k2 = Equal.trans(Nat, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d)), Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.add(x, d)), 2n+i, Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(x, d)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), eu)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.add(x, d)), Nat.sub(Nat.add(Nat.add(Nat.add(x, d), 2n), i), Nat.add(x, d)), 2n+i, Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, i), Nat.add(x, d)), Nat.add(x, Nat.add(d, 2n)), Nat.add(Nat.add(x, d), 2n), Equal.sym(Nat, Nat.add(Nat.add(x, d), 2n), Nat.add(x, Nat.add(d, 2n)), NA.add_assoc(x, d, 2n))), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(Nat.add(x, d), 2n), i), Nat.add(x, d)), Nat.sub(Nat.add(Nat.add(x, d), 2n+i), Nat.add(x, d)), 2n+i, Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(x, d)), Nat.add(Nat.add(Nat.add(x, d), 2n), i), Nat.add(Nat.add(x, d), 2n+i), NA.add_assoc(Nat.add(x, d), 2n, i)), N.add_sub_cancel(Nat.add(x, d), 2n+i))))
215 +hle1 = N.le_trans(x, Nat.add(x, Nat.add(d, 2n)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), N.le_add_right(x, Nat.add(d, 2n)), hu)
216 +hle2 = N.le_trans(Nat.add(x, d), Nat.add(x, Nat.add(d, 2n)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), N.le_add_left(d, Nat.add(d, 2n), x, N.le_add_right(d, 2n)), hu)
217 +l1 = Equal.cong(Bool, F.F64, z => SF.pick(F.F64, z, SF.zero(s), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(m, 0n), False{}, hz)
218 +l2 = Equal.cong(Bool, F.F64, z => SF.pack(s, SF.pick(Nat, z, SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), C.shift(Nat.sub(x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), m)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.is_le(x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), True{}, hle1)
219 +l3 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(m, z), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x), Nat.add(2n+i, d), k1)
220 +l4 = Equal.cong(Nat, F.F64, z => SF.pack(s, z, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(m, Nat.add(2n+i, d)), SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), FR.sticky(i, d, m))
221 +r1 = Equal.cong(Bool, F.F64, z => SF.pick(F.F64, z, SF.zero(s), SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(SW.jam(C.high(d, m), C.low(d, m)), 0n), False{}, hzJ)
222 +r2 = Equal.cong(Nat, F.F64, z => SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), z), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), eU)
223 +r3 = Equal.cong(Bool, F.F64, z => SF.pack(s, SF.pick(Nat, z, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d))), C.shift(Nat.sub(Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SW.jam(C.high(d, m), C.low(d, m)))), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.is_le(Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), True{}, hle2)
224 +r4 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), z), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d)), 2n+i, k2)
225 +lhs = Equal.trans(F.F64, SF.round(s, m, x), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), l1, Equal.trans(F.F64, SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), l2, Equal.trans(F.F64, SF.pack(s, SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(m, Nat.add(2n+i, d)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), l3, l4)))
226 +rhs = Equal.trans(F.F64, SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)), SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), r1, Equal.trans(F.F64, SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), r2, Equal.trans(F.F64, SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d))), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), r3, r4)))
227 Equal.trans(F.F64, SF.round(s, m, x), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)), lhs, Equal.sym(F.F64, SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), rhs))