def smb1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addb.bend:64

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/proofs/lib/nat.bend as N
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/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as AA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend as AP
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend as AS

64# subMags, larger exponent el, smaller exponent es = 1 + p
65def smb1(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +el: Nat, +fl: WU.U64, +p: Nat, +fs: WU.U64, +Fl: Nat, +Fs: Nat, +hfl: {SW.value(fl) == Fl : Nat}, +hfs: {SW.value(fs) == Fs : Nat}, +hFl: {C.fits(52n, Fl) == True{} : Bool}, +hFs: {C.fits(52n, Fs) == True{} : Bool}, +hlt: {Nat.is_lt(1n+p, el) == True{} : Bool}) -> {F.norm_round_pack(s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(1n+p, X.shl(fs, 10n)), Nat.sub(el, 1n+p)))) == SF.round(s, Nat.sub(C.shift(Nat.sub(el, 1n+p), Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one))), Nat.add(1925n, 1n+p)) : F.F64}:
66  +d = Nat.sub(el, 1n+p)
67  +sw = X.add(X.shl(fs, 10n), WU.U64{0, 1073741824})
68  +et = top10(one, h1, fl, Fl, hfl, hFl, 1073741824, {==})
69  +es = top10(one, h1, fs, Fs, hfs, hFs, 1073741824, {==})
70  +eld = N.sub_add(el, 1n+p, N.lt_le(1n+p, el, hlt))
71  +hd1 = FR.lt_sub_pos(1n+p, el, hlt)
72  +hS = f63s(one, h1, 10n, Fs, hFs, {==})
73  +hT63 = f63s(one, h1, 10n, Fl, hFl, {==})
74  +hT62 = Equal.trans(Bool, C.fits(Nat.add(10n, 52n), C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.fits(52n, Nat.add(Fl, C.shift(52n, one))), False{}, RT.fits_sh(10n, 52n, Nat.add(Fl, C.shift(52n, one))), AA.n52(one, h1, Fl))
75  +hle = hlt2(one, h1, C.shift(9n, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one)), d, hd1, hS, hT62)
76  +hsig = subv(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), sw, C.shift(9n, Nat.add(Fl, C.shift(52n, one))), C.shift(10n, Nat.add(Fs, C.shift(52n, one))), d, et, es, hle)
77  +el1 = N.sub_add(el, 1n, N.le_trans(1n, 1n+p, el, N.zero_le(p), N.lt_le(1n+p, el, hlt)))
78  +he = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(1915n, 1n+p), d), 2180n), Nat.add(Nat.add(1915n, Nat.add(1n+p, d)), 2180n), Nat.add(F.off(), Nat.sub(el, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, 2180n), Nat.add(Nat.add(1915n, 1n+p), d), Nat.add(1915n, Nat.add(1n+p, d)), NA.add_assoc(1915n, 1n+p, d)), Equal.trans(Nat, Nat.add(Nat.add(1915n, Nat.add(1n+p, d)), 2180n), Nat.add(Nat.add(1915n, el), 2180n), Nat.add(F.off(), Nat.sub(el, 1n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1915n, z), 2180n), Nat.add(1n+p, d), el, eld), Equal.trans(Nat, Nat.add(Nat.add(1915n, el), 2180n), Nat.add(Nat.add(1915n, Nat.add(1n, Nat.sub(el, 1n))), 2180n), Nat.add(F.off(), Nat.sub(el, 1n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1915n, z), 2180n), el, Nat.add(1n, Nat.sub(el, 1n)), Equal.sym(Nat, Nat.add(1n, Nat.sub(el, 1n)), el, el1)), Equal.trans(Nat, Nat.add(Nat.add(1915n, Nat.add(1n, Nat.sub(el, 1n))), 2180n), Nat.add(1915n, Nat.add(Nat.add(1n, Nat.sub(el, 1n)), 2180n)), Nat.add(F.off(), Nat.sub(el, 1n)), NA.add_assoc(1915n, Nat.add(1n, Nat.sub(el, 1n)), 2180n), Equal.cong(Nat, Nat, z => Nat.add(1915n, z), Nat.add(Nat.add(1n, Nat.sub(el, 1n)), 2180n), Nat.add(2181n, Nat.sub(el, 1n)), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(Nat.sub(el, 1n), 2180n), Nat.add(2180n, Nat.sub(el, 1n)), NA.add_comm(Nat.sub(el, 1n), 2180n)))))))
79  +hx63 = N.le_trans(63n, Nat.add(1915n, 1n+p), Nat.add(Nat.add(1915n, 1n+p), d), {==}, N.le_add_right(Nat.add(1915n, 1n+p), d))
80  +r1 = AS.smb_c(one, h1, s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(1n+p, X.shl(fs, 10n)), Nat.sub(el, 1n+p))), C.shift(9n, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one)), d, Nat.add(1915n, 1n+p), hsig, he, hx63, hd1, hS, hT62, hT63, Nat.is_eq(C.low(d, C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), 0n), {==})
81  +r1b = Equal.trans(F.F64, F.norm_round_pack(s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(1n+p, X.shl(fs, 10n)), Nat.sub(el, 1n+p)))), SF.round(s, Nat.sub(C.shift(d, Nat.double(C.shift(9n, Nat.add(Fl, C.shift(52n, one))))), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), Nat.add(1915n, 1n+p)), SF.round(s, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), Nat.add(1915n, 1n+p)), r1, Equal.cong(Nat, F.F64, zz_ => SF.round(s, Nat.sub(C.shift(d, zz_), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), Nat.add(1915n, 1n+p)), Nat.double(C.shift(9n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fl, C.shift(52n, one))), {==}))
82  +hmd = ms_le(one, h1, Fl, Nat.add(Fs, C.shift(52n, one)), d, AA.f53(one, h1, Fs, hFs), hd1)
83  +eW = Equal.trans(Nat, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), Nat.sub(C.shift(10n, C.shift(d, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), C.shift(10n, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one)))), Equal.cong(Nat, Nat, z => Nat.sub(z, C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, C.shift(d, Nat.add(Fl, C.shift(52n, one)))), AA.shc(d, 10n, Nat.add(Fl, C.shift(52n, one)))), AP.sub_shift(10n, C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one)), hmd))
84  +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(1915n, 1n+p)), Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), C.shift(10n, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one)))), eW)
85  +r3 = RT.round_shift(s, 10n, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one))), Nat.add(1915n, 1n+p))
86  +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one))), z), Nat.add(Nat.add(1915n, 1n+p), 10n), Nat.add(1925n, 1n+p), Equal.cong(Nat, Nat, z => 1916n+z, Nat.add(p, 10n), Nat.add(10n, p), NA.add_comm(p, 10n)))
87  Equal.trans(F.F64, F.norm_round_pack(s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(1n+p, X.shl(fs, 10n)), Nat.sub(el, 1n+p)))), SF.round(s, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), Nat.add(1915n, 1n+p)), SF.round(s, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one))), Nat.add(1925n, 1n+p)), r1b, Equal.trans(F.F64, SF.round(s, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fs, C.shift(52n, one)))), Nat.add(1915n, 1n+p)), SF.round(s, C.shift(10n, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one)))), Nat.add(1915n, 1n+p)), SF.round(s, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one))), Nat.add(1925n, 1n+p)), r2, Equal.trans(F.F64, SF.round(s, C.shift(10n, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one)))), Nat.add(1915n, 1n+p)), SF.round(s, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one))), Nat.add(Nat.add(1915n, 1n+p), 10n)), SF.round(s, Nat.sub(C.shift(d, Nat.add(Fl, C.shift(52n, one))), Nat.add(Fs, C.shift(52n, one))), Nat.add(1925n, 1n+p)), r3, r4)))