F64adds.wbig: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend as F64adds Lines 47-57 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend&start_line=47&end_line=57 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/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 import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT # W = 2^d T - S is at least 2^d * 2^61 when d >= 2, T >= 2^62, S < 2^63 def wbig(+one: Nat, +h1: {one == 1n : Nat}, +t: Nat, +S: Nat, +d: Nat, +hd: {Nat.is_le(2n, d) == True{} : Bool}, +hT: {C.fits(62n, Nat.double(t)) == False{} : Bool}, +hS: {C.fits(63n, S) == True{} : Bool}) -> {C.fits(Nat.add(d, 61n), Nat.sub(C.shift(d, Nat.double(t)), S)) == False{} : Bool}: +A = C.shift(d, C.shift(61n, one)) +hTge = N.not_lt_le(Nat.double(t), C.shift(62n, one), Equal.trans(Bool, Nat.is_lt(Nat.double(t), C.shift(62n, one)), C.fits(62n, Nat.double(t)), False{}, FR.lt_fit(62n, one, h1, Nat.double(t)), hT)) +h2A = L.subst(Nat, z => {Nat.is_le(z, C.shift(d, Nat.double(t))) == True{} : Bool}, C.shift(d, Nat.double(C.shift(61n, one))), Nat.add(A, A), Equal.trans(Nat, C.shift(d, Nat.double(C.shift(61n, one))), Nat.double(A), Nat.add(A, A), WW.shift_dbl(d, C.shift(61n, one)), NA.double_self(A)), WW.shift_mono(d, Nat.double(C.shift(61n, one)), Nat.double(t), hTge)) +ed = N.sub_add(d, 2n, hd) +hSA0 = N.lt_le_trans(S, C.shift(63n, one), C.shift(2n, C.shift(61n, one)), Equal.trans(Bool, Nat.is_lt(S, C.shift(63n, one)), C.fits(63n, S), True{}, FR.lt_fit(63n, one, h1, S), hS), L.subst(Nat, z => {Nat.is_le(C.shift(63n, one), z) == True{} : Bool}, C.shift(Nat.add(2n, 61n), one), C.shift(2n, C.shift(61n, one)), WW.shift_comp(2n, 61n, one), N.le_refl(C.shift(63n, one)))) +hSA = N.lt_le(S, A, N.lt_le_trans(S, C.shift(2n, C.shift(61n, one)), A, hSA0, shmk(2n, d, C.shift(61n, one), hd))) +hWA = RT.le_sub(A, S, C.shift(d, Nat.double(t)), N.le_trans(Nat.add(A, S), Nat.add(A, A), C.shift(d, Nat.double(t)), N.le_add_left(S, A, A, hSA), h2A)) +nfA = Equal.trans(Bool, C.fits(Nat.add(d, 61n), A), C.fits(61n, C.shift(61n, one)), False{}, RT.fits_sh(d, 61n, C.shift(61n, one)), Equal.trans(Bool, C.fits(61n, C.shift(61n, one)), Nat.is_lt(C.shift(61n, one), C.shift(61n, one)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(61n, one), C.shift(61n, one)), C.fits(61n, C.shift(61n, one)), FR.lt_fit(61n, one, h1, C.shift(61n, one))), N.lt_irrefl(C.shift(61n, one)))) FR.nfit(Nat.add(d, 61n), A, Nat.sub(C.shift(d, Nat.double(t)), S), hWA, nfA) Uses (29): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_refl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_irrefl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend&name=shmk https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=lt_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=nfit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=fits_sh https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=le_sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_dbl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_mono https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift