Fround.pkg_c: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround Lines 184-209 of bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&start_line=184&end_line=209 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/src/math/f64.bend as F 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/f64bits.bend as FB def pkg_c(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +q: Nat, +u: Nat, +EF: Nat, +hEF: {Nat.add(EF, 1926n) == u : Nat}, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +f53: Bool, +h53: {C.fits(53n, q) == f53 : Bool}, +f52: Bool, +h52: {C.fits(52n, q) == f52 : Bool}, +h0: {Bool.or(Bool.not(f52), Nat.is_eq(EF, 0n)) == True{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, f53, 1n, 2n)), 2047n) == True{} : Bool}) -> {SF.pick(F.F64, f53, SF.pick(F.F64, f52, SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)) == bits(s, Nat.add(q, C.shift(52n, EF))) : F.F64}: match f53 f52: case True{} True{}: +e0 = N.eq_from_is_eq(EF, 0n, h0) Equal.trans(F.F64, SF.encode(s, 0n, q), bits(s, Nat.add(q, C.shift(52n, 0n))), bits(s, Nat.add(q, C.shift(52n, EF))), enc_bits(s, 0n, q), Equal.cong(Nat, F.F64, z => bits(s, Nat.add(q, C.shift(52n, z))), 0n, EF, Equal.sym(Nat, EF, 0n, e0))) case True{} False{}: +eH = hi_one(C.high(52n, q), Equal.trans(Bool, Nat.is_eq(C.half(C.high(52n, q)), 0n), C.fits(53n, q), True{}, Equal.sym(Bool, C.fits(53n, q), Nat.is_eq(C.half(C.high(52n, q)), 0n), f53h(q)), h53), h52) +e1 = efv(u, EF, hEF) +eE = Equal.trans(Nat, Nat.sub(Nat.add(u, 1075n), SF.zb()), 1n+EF, Nat.add(C.high(52n, q), EF), e1, Equal.cong(Nat, Nat, z => Nat.add(z, EF), 1n, C.high(52n, q), Equal.sym(Nat, C.high(52n, q), 1n, eH))) +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(u, 1075n), SF.zb())), Nat.is_le(2047n, 1n+EF), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(2047n, z), Nat.sub(Nat.add(u, 1075n), SF.zb()), 1n+EF, e1), Equal.trans(Bool, Nat.is_le(2047n, 1n+EF), Bool.not(Nat.is_lt(1n+EF, 2047n)), False{}, FB.le_nlt(2047n, 1n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(1n+EF, 2047n), True{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(EF, 1n), 1n+EF, Equal.trans(Nat, Nat.add(EF, 1n), Nat.add(1n, EF), 1n+EF, NA.add_comm(EF, 1n), {==}), hov)))) +p1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.inf(s), SF.encode(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), Nat.is_le(2047n, Nat.sub(Nat.add(u, 1075n), SF.zb())), False{}, hle) +p2 = enc_bits(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)) +v1 = Equal.trans(Nat, Nat.add(C.low(52n, q), C.shift(52n, Nat.sub(Nat.add(u, 1075n), SF.zb()))), Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))), Nat.add(q, C.shift(52n, EF)), Equal.cong(Nat, Nat, z => Nat.add(C.low(52n, q), C.shift(52n, z)), Nat.sub(Nat.add(u, 1075n), SF.zb()), Nat.add(C.high(52n, q), EF), eE), Equal.trans(Nat, Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))), Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Nat.add(q, C.shift(52n, EF)), Equal.cong(Nat, Nat, z => Nat.add(C.low(52n, q), z), C.shift(52n, Nat.add(C.high(52n, q), EF)), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF)), WW.shift_add(52n, C.high(52n, q), EF)), Equal.trans(Nat, Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Nat.add(Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), C.shift(52n, EF)), Nat.add(q, C.shift(52n, EF)), Equal.sym(Nat, Nat.add(Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), C.shift(52n, EF)), Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), NA.add_assoc(C.low(52n, q), C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, EF)), Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), q, Equal.sym(Nat, q, Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), WW.low_high(52n, q)))))) +p3 = Equal.cong(Nat, F.F64, z => bits(s, z), Nat.add(C.low(52n, q), C.shift(52n, Nat.sub(Nat.add(u, 1075n), SF.zb()))), Nat.add(q, C.shift(52n, EF)), v1) Equal.trans(F.F64, SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)), SF.encode(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)), bits(s, Nat.add(q, C.shift(52n, EF))), p1, Equal.trans(F.F64, SF.encode(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)), bits(s, Nat.add(C.low(52n, q), C.shift(52n, Nat.sub(Nat.add(u, 1075n), SF.zb())))), bits(s, Nat.add(q, C.shift(52n, EF))), p2, p3)) case False{} _: +e1 = ef2v(u, EF, hEF) +eq = top_q(one, h1, q, hq, h53) +two = Nat.double(one) +eE = Equal.trans(Nat, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 2n+EF, Nat.add(two, EF), e1, Equal.cong(Nat, Nat, z => Nat.add(Nat.double(z), EF), 1n, one, Equal.sym(Nat, one, 1n, h1))) +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), Nat.is_le(2047n, 2n+EF), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(2047n, z), Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 2n+EF, e1), Equal.trans(Bool, Nat.is_le(2047n, 2n+EF), Bool.not(Nat.is_lt(2n+EF, 2047n)), False{}, FB.le_nlt(2047n, 2n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(2n+EF, 2047n), True{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(EF, 2n), 2n+EF, Equal.trans(Nat, Nat.add(EF, 2n), Nat.add(2n, EF), 2n+EF, NA.add_comm(EF, 2n), {==}), hov)))) +p1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.inf(s), SF.encode(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), Nat.is_le(2047n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), False{}, hle) +p2 = enc_bits(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n) +v1 = Equal.trans(Nat, C.shift(52n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), C.shift(52n, Nat.add(two, EF)), Nat.add(q, C.shift(52n, EF)), Equal.cong(Nat, Nat, z => C.shift(52n, z), Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), Nat.add(two, EF), eE), Equal.trans(Nat, C.shift(52n, Nat.add(two, EF)), Nat.add(C.shift(52n, two), C.shift(52n, EF)), Nat.add(q, C.shift(52n, EF)), WW.shift_add(52n, two, EF), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, EF)), C.shift(52n, two), q, Equal.sym(Nat, q, C.shift(52n, two), eq)))) +p3 = Equal.cong(Nat, F.F64, z => bits(s, z), C.shift(52n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), Nat.add(q, C.shift(52n, EF)), v1) Equal.trans(F.F64, SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), SF.encode(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), bits(s, Nat.add(q, C.shift(52n, EF))), p1, Equal.trans(F.F64, SF.encode(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), bits(s, Nat.add(0n, C.shift(52n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())))), bits(s, Nat.add(q, C.shift(52n, EF))), p2, p3)) Uses (38): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or 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/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=eq_from_is_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=ef2v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=efv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=enc_bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=f53h https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=hi_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=top_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=le_nlt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_high 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=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/f64.bend&name=encode https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=inf https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pack_e https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick 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/src/math/f64.bend&name=F64