def pkg_c
bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:184
import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
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
184def 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}:
185 match f53 f52:
186 case True{} True{}:
187 +e0 = N.eq_from_is_eq(EF, 0n, h0)
188 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)))
189 case True{} False{}:
190 +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)
191 +e1 = efv(u, EF, hEF)
192 +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)))
193 +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))))
194 +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)
195 +p2 = enc_bits(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))
196 +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))))))
197 +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)
198 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))
199 case False{} _:
200 +e1 = ef2v(u, EF, hEF)
201 +eq = top_q(one, h1, q, hq, h53)
202 +two = Nat.double(one)
203 +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)))
204 +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))))
205 +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)
206 +p2 = enc_bits(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)
207 +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))))
208 +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)
209 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))