def pko_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:535

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/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/f64bits.bend as FB

535def pko_c(+s: Bool, +q: Nat, +u: Nat, +EF: Nat, +hEF: {Nat.add(EF, 1926n) == u : Nat}, +f53: Bool, +h52: {C.fits(52n, q) == False{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, f53, 1n, 2n)), 2047n) == False{} : Bool}) -> {SF.pick(F.F64, f53, SF.pick(F.F64, C.fits(52n, q), 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)) == SF.inf(s) : F.F64}:
536  match f53:
537    case True{}:
538      +e1 = efv(u, EF, hEF)
539      +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(u, 1075n), SF.zb())), Nat.is_le(2047n, 1n+EF), True{}, 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)), True{}, FB.le_nlt(2047n, 1n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(1n+EF, 2047n), False{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == False{} : 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))))
540      +p0 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), C.fits(52n, q), False{}, h52)
541      Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.pick(F.F64, C.fits(52n, q), 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)), SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.inf(s), pk_t(F.F64, SF.pick(F.F64, C.fits(52n, q), 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)), Equal.trans(F.F64, SF.pick(F.F64, C.fits(52n, q), 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(u, 1075n), SF.zb()), C.low(52n, q)), SF.inf(s), p0, 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())), True{}, hle)))
542    case False{}:
543      +e1 = ef2v(u, EF, hEF)
544      +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), Nat.is_le(2047n, 2n+EF), True{}, 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)), True{}, FB.le_nlt(2047n, 2n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(2n+EF, 2047n), False{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == False{} : 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))))
545      Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.pick(F.F64, C.fits(52n, q), 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)), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), SF.inf(s), pk_f(F.F64, SF.pick(F.F64, C.fits(52n, q), 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)), 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())), True{}, hle))