F64addp.jsub: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend as F64addp Lines 69-97 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend&start_line=69&end_line=97 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/w64.bend as SW 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/lib/u32alg.bend as A import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR # T - jam(h, l) is the jam of T * 2^d - (l + h * 2^d) when 0 < l < 2^d, h < T, T even def jsub(+t: Nat, +d: Nat, +h: Nat, +l: Nat, +hl0: {Nat.is_eq(l, 0n) == False{} : Bool}, +hld: {C.fits(d, l) == True{} : Bool}, +hh: {Nat.is_lt(h, Nat.double(t)) == True{} : Bool}) -> {Nat.sub(Nat.double(t), SW.jam(h, l)) == SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))) : Nat}: +hTh = N.lt_le(h, Nat.double(t), hh) +h1 = FR.lt_sub_pos(h, Nat.double(t), hh) +eg1 = N.sub_add(Nat.sub(Nat.double(t), h), 1n, h1) +ehg = Equal.trans(Nat, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(h, Nat.sub(Nat.double(t), h)), Nat.double(t), Equal.cong(Nat, Nat, z => Nat.add(h, z), 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.sub(Nat.double(t), h), eg1), N.sub_add(Nat.double(t), h, hTh)) +hl1 = WW.lt_one(d, 1n, {==}, l, hld) +er = N.sub_add(C.shift(d, 1n), l, N.lt_le(l, C.shift(d, 1n), hl1)) +hr = L.subst(Nat, z => {Nat.is_lt(Nat.sub(C.shift(d, 1n), l), z) == True{} : Bool}, Nat.add(l, Nat.sub(C.shift(d, 1n), l)), C.shift(d, 1n), er, lt_add_l(l, Nat.sub(C.shift(d, 1n), l), hl0)) +fr = WW.fits_one(d, 1n, {==}, Nat.sub(C.shift(d, 1n), l), hr) +rnz = rnz_c(l, Nat.sub(C.shift(d, 1n), l), C.shift(d, 1n), er, hl1, Nat.is_eq(Nat.sub(C.shift(d, 1n), l), 0n), {==}) +sh = C.shift(d, h) +sg = C.shift(d, Nat.sub(Nat.sub(Nat.double(t), h), 1n)) +eW0 = Equal.trans(Nat, C.shift(d, Nat.double(t)), C.shift(d, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => C.shift(d, z), Nat.double(t), Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Equal.sym(Nat, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.double(t), ehg)), Equal.trans(Nat, C.shift(d, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(sh, C.shift(d, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), WW.shift_add(d, h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Equal.trans(Nat, Nat.add(sh, C.shift(d, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(sh, Nat.add(C.shift(d, 1n), sg)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => Nat.add(sh, z), C.shift(d, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(C.shift(d, 1n), sg), WW.shift_add(d, 1n, Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Equal.trans(Nat, Nat.add(sh, Nat.add(C.shift(d, 1n), sg)), Nat.add(sh, Nat.add(Nat.add(l, Nat.sub(C.shift(d, 1n), l)), sg)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => Nat.add(sh, Nat.add(z, sg)), C.shift(d, 1n), Nat.add(l, Nat.sub(C.shift(d, 1n), l)), Equal.sym(Nat, Nat.add(l, Nat.sub(C.shift(d, 1n), l)), C.shift(d, 1n), er)), Equal.trans(Nat, Nat.add(sh, Nat.add(Nat.add(l, Nat.sub(C.shift(d, 1n), l)), sg)), Nat.add(sh, Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => Nat.add(sh, z), Nat.add(Nat.add(l, Nat.sub(C.shift(d, 1n), l)), sg), Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), NA.add_assoc(l, Nat.sub(C.shift(d, 1n), l), sg)), Equal.trans(Nat, Nat.add(sh, Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), Nat.add(Nat.add(sh, l), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.sym(Nat, Nat.add(Nat.add(sh, l), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(sh, Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), NA.add_assoc(sh, l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(sh, l), Nat.add(l, sh), NA.add_comm(sh, l)))))))) +eW = Equal.trans(Nat, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))), Nat.sub(Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(l, sh)), Nat.add(Nat.sub(C.shift(d, 1n), l), sg), Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(l, sh)), C.shift(d, Nat.double(t)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), eW0), N.add_sub_cancel(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg))) +eH = Equal.trans(Nat, C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.high(d, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.sub(Nat.sub(Nat.double(t), h), 1n), Equal.cong(Nat, Nat, z => C.high(d, z), Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))), Nat.add(Nat.sub(C.shift(d, 1n), l), sg), eW), WW.high_u(d, Nat.sub(C.shift(d, 1n), l), Nat.sub(Nat.sub(Nat.double(t), h), 1n), fr)) +eL = Equal.trans(Nat, C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.sub(C.shift(d, 1n), l), Equal.cong(Nat, Nat, z => C.low(d, z), Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))), Nat.add(Nat.sub(C.shift(d, 1n), l), sg), eW), WW.low_u(d, Nat.sub(C.shift(d, 1n), l), Nat.sub(Nat.sub(Nat.double(t), h), 1n), fr)) +rhs = Equal.trans(Nat, SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), 1n+Nat.double(C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Equal.cong(Nat, Nat, z => SW.jam(z, C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), Nat.sub(Nat.sub(Nat.double(t), h), 1n), eH), Equal.trans(Nat, SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.sub(C.shift(d, 1n), l)), 1n+Nat.double(C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Equal.cong(Nat, Nat, z => SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), z), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), Nat.sub(C.shift(d, 1n), l), eL), jam_nz(Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.sub(C.shift(d, 1n), l), rnz))) +ehk = WW.hb(h) +hdk = N.le_lt_trans(Nat.double(C.half(h)), h, Nat.double(t), L.subst(Nat, z => {Nat.is_le(Nat.double(C.half(h)), z) == True{} : Bool}, Nat.add(Nat.double(C.half(h)), C.bit(h)), h, Equal.trans(Nat, Nat.add(Nat.double(C.half(h)), C.bit(h)), Nat.add(C.bit(h), Nat.double(C.half(h))), h, NA.add_comm(Nat.double(C.half(h)), C.bit(h)), Equal.sym(Nat, h, Nat.add(C.bit(h), Nat.double(C.half(h))), ehk)), N.le_add_right(Nat.double(C.half(h)), C.bit(h))), hh) +hk = half_lt(C.half(h), t, hdk) +et = N.sub_add(t, 1n+C.half(h), N.lt_succ_le_succ(C.half(h), t, hk)) +eT = Equal.trans(Nat, Nat.double(t), Nat.double(Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h)))), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Equal.cong(Nat, Nat, z => Nat.double(z), t, Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h))), Equal.sym(Nat, Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h))), t, et)), Equal.trans(Nat, Nat.double(Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h)))), Nat.add(2n+Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), NA.double_add(1n+C.half(h), Nat.sub(t, 1n+C.half(h))), Equal.cong(Nat, Nat, z => 1n+z, 1n+Nat.add(Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Equal.sym(Nat, Nat.add(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), 1n+Nat.add(Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h)))), N.add_succ(Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h)))))))) +lhs = Equal.trans(Nat, Nat.sub(Nat.double(t), SW.jam(h, l)), Nat.sub(Nat.double(t), 1n+Nat.double(C.half(h))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Equal.cong(Nat, Nat, z => Nat.sub(Nat.double(t), z), SW.jam(h, l), 1n+Nat.double(C.half(h)), jam_nz(h, l, hl0)), Equal.trans(Nat, Nat.sub(Nat.double(t), 1n+Nat.double(C.half(h))), Nat.sub(Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), 1n+Nat.double(C.half(h))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n+Nat.double(C.half(h))), Nat.double(t), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), eT), N.add_sub_cancel(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))))) +b = C.bit(h) +e1 = Equal.trans(Nat, Nat.add(Nat.add(b, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.double(C.half(h))), Nat.add(Nat.add(b, Nat.double(C.half(h))), 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), A.add_rot(b, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.double(C.half(h))), Equal.trans(Nat, Nat.add(Nat.add(b, Nat.double(C.half(h))), 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), Equal.cong(Nat, Nat, z => Nat.add(z, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(b, Nat.double(C.half(h))), h, Equal.sym(Nat, h, Nat.add(b, Nat.double(C.half(h))), ehk)), Equal.trans(Nat, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.double(t), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), ehg, Equal.trans(Nat, Nat.double(t), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), eT, Equal.cong(Nat, Nat, z => 1n+z, Nat.add(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Nat.double(C.half(h))), NA.add_comm(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))))))))) +e2 = A.add_cancel_r(Nat.add(b, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h)), e1) +ehalf = hg_c(Nat.sub(t, 1n+C.half(h)), Nat.sub(Nat.sub(Nat.double(t), h), 1n), b, e2, WW.bit_le1(h)) Equal.trans(Nat, Nat.sub(Nat.double(t), SW.jam(h, l)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), lhs, Equal.sym(Nat, SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Equal.trans(Nat, SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), 1n+Nat.double(C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), rhs, Equal.cong(Nat, Nat, z => 1n+Nat.double(z), C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.sub(t, 1n+C.half(h)), ehalf)))) Uses (44): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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_eq 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=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_add 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=add_sub_cancel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans 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_succ_le_succ 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/lib/u32alg.bend&name=add_cancel_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=add_rot https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend&name=half_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend&name=hg_c https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend&name=jam_nz https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend&name=lt_add_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend&name=rnz_c https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=lt_sub_pos https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_le1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=fits_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=hb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_u https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_u https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=bit 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=half https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=jam