Float.main_g: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float Lines 271-293 of bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&start_line=271&end_line=293 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/spec/math/f64.bend as SF 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/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/math/typed/width.bend as WW import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as FR def main_g(+one: Nat, +h1: {one == 1n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}, +m: WU.U64, +np: Nat, +hM: {SW.value(m) == 1n+np : Nat}, +j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {bits(X.shl(m, Nat.sub(52n, j)), Nat.add(j, 970n)) == SF.round(False{}, 1n+np, xv) : F.F64}: +r = Nat.sub(52n, j) +q = C.shift(r, 1n+np) +e1 = N.sub_add(52n, j, hj) +bq = Equal.trans(Nat, M.bit_length(q), Nat.add(M.bit_length(1n+np), r), 53n, FR.bl_shift(r, 1n+np, {==}), Equal.trans(Nat, Nat.add(M.bit_length(1n+np), r), Nat.add(1n+j, r), 53n, Equal.cong(Nat, Nat, z => Nat.add(z, r), M.bit_length(1n+np), 1n+j, hbl), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, r), 52n, e1))) +hzq = WW.shift_eq0(r, 1n+np) +f53 = L.subst(Nat, z => {C.fits(z, q) == True{} : Bool}, M.bit_length(q), 53n, bq, FR.bl_fit(q)) +n52 = L.subst(Nat, z => {C.fits(z, q) == False{} : Bool}, Nat.sub(M.bit_length(q), 1n), 52n, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), M.bit_length(q), 53n, bq), FR.bl_nfit(q, hzq)) sv = SH.shl_value(m, r, r52(j, hj)) +hq = Equal.trans(Nat, SW.value(X.shl(m, r)), C.low(64n, C.shift(r, SW.value(m))), q, sv, Equal.trans(Nat, C.low(64n, C.shift(r, SW.value(m))), C.low(64n, q), q, Equal.cong(Nat, Nat, z => C.low(64n, C.shift(r, z)), SW.value(m), 1n+np, hM), WW.low_fit(64n, q, fits_up(53n, 11n, q, f53)))) +he = L.subst(Nat, z => {Nat.is_lt(z, 2048n) == True{} : Bool}, Nat.add(970n, j), Nat.add(j, 970n), N.add_comm(970n, j), N.le_lt_trans(j, 52n, 1078n, hj, {==})) +l52 = C.low(52n, q) +c1 = enc(one, h1, X.shl(m, r), Nat.add(j, 970n), he, q, hq, f53) +c2 = pack_q(one, h1, q, j, hj, f53, n52) +c3 = round_q(q, j, bq, hzq) +c4 = FR.round_shift(False{}, r, 1n+np, Nat.add(j, 2895n)) +c5 = Equal.cong(Nat, F.F64, z => SF.round(False{}, 1n+np, z), Nat.add(Nat.add(j, 2895n), r), xv, Equal.trans(Nat, Nat.add(Nat.add(j, 2895n), r), x0(), xv, ex(j, hj), hx)) +s3 = Equal.trans(F.F64, SF.round(False{}, q, Nat.add(j, 2895n)), SF.pack(False{}, q, Nat.add(j, 2895n)), SF.encode(False{}, Nat.add(j, 970n), l52), c3, c2) +s4 = Equal.trans(F.F64, SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), SF.round(False{}, q, Nat.add(j, 2895n)), SF.encode(False{}, Nat.add(j, 970n), l52), Equal.sym(F.F64, SF.round(False{}, q, Nat.add(j, 2895n)), SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), c4), s3) +sp = Equal.trans(F.F64, SF.round(False{}, 1n+np, xv), SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), SF.encode(False{}, Nat.add(j, 970n), l52), Equal.sym(F.F64, SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), SF.round(False{}, 1n+np, xv), c5), s4) Equal.trans(F.F64, bits(X.shl(m, r), Nat.add(j, 970n)), SF.encode(False{}, Nat.add(j, 970n), l52), SF.round(False{}, 1n+np, xv), c1, Equal.sym(F.F64, SF.round(False{}, 1n+np, xv), SF.encode(False{}, Nat.add(j, 970n), l52), sp)) Uses (40): 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.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/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_comm 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=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=enc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=ex https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=fits_up https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=pack_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=r52 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=round_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=x0 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=bl_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=bl_nfit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=bl_shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=round_shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=shl_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_eq0 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=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/f64.bend&name=encode https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pack https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=zb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=bit_length https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shl