def ov_eq

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

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/spec/math/w64.bend as SW
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/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/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

867def ov_eq(+one: Nat, +h1: {one == 1n : Nat}, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hge: {Nat.is_le(1916n, x) == True{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0})))) == Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)) : Bool}:
868  +he = L.subst(Nat, z => {Nat.is_le(F.off(), z) == True{} : Bool}, Nat.add(x, 2180n), e, hx, Equal.trans(Bool, Nat.is_le(Nat.add(1916n, 2180n), Nat.add(x, 2180n)), Nat.is_le(1916n, x), True{}, le_cancel_r(1916n, x, 2180n), hge))
869  +ee = Equal.trans(Nat, e, Nat.add(4096n, Nat.sub(e, F.off())), Nat.add(Nat.sub(e, F.off()), 4096n), Equal.sym(Nat, Nat.add(4096n, Nat.sub(e, F.off())), e, N.sub_add(e, 4096n, he)), NA.add_comm(4096n, Nat.sub(e, F.off())))
870  +a1 = Equal.trans(Bool, Nat.is_lt(6141n, e), Nat.is_lt(6141n, Nat.add(Nat.sub(e, F.off()), 4096n)), Nat.is_lt(2045n, Nat.sub(e, F.off())), Equal.cong(Nat, Bool, z => Nat.is_lt(6141n, z), e, Nat.add(Nat.sub(e, F.off()), 4096n), ee), WW.lt_cancel_r(2045n, Nat.sub(e, F.off()), 4096n))
871  +a2 = Equal.trans(Bool, Nat.is_eq(e, 6141n), Nat.is_eq(Nat.add(Nat.sub(e, F.off()), 4096n), 6141n), Nat.is_eq(Nat.sub(e, F.off()), 2045n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 6141n), e, Nat.add(Nat.sub(e, F.off()), 4096n), ee), eq_cancel_r(Nat.sub(e, F.off()), 2045n, 4096n))
872  +a3 = Equal.trans(Bool, X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0})), Bool.not(C.fits(63n, Nat.add(SW.value(sig), 512n))), Bool.not(C.fits(53n, SF.rne(SW.value(sig), 10n))), ovle(one, h1, sig, h63, 2147483648, {==}), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(63n, Nat.add(SW.value(sig), 512n)), C.fits(53n, SF.rne(SW.value(sig), 10n)), Equal.sym(Bool, C.fits(53n, SF.rne(SW.value(sig), 10n)), C.fits(63n, Nat.add(SW.value(sig), 512n)), p2(one, h1, SW.value(sig), h63))))
873  +LE = X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0}))
874  +c1 = Equal.cong(Bool, Bool, t => Bool.or(t, Bool.and(Nat.is_eq(e, 6141n), LE)), Nat.is_lt(6141n, e), Nat.is_lt(2045n, Nat.sub(e, F.off())), a1)
875  +c2 = Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(t, LE)), Nat.is_eq(e, 6141n), Nat.is_eq(Nat.sub(e, F.off()), 2045n), a2)
876  +c3 = Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), t)), LE, Bool.not(C.fits(53n, SF.rne(SW.value(sig), 10n))), a3)
877  Equal.trans(Bool, Bool.or(Nat.is_lt(6141n, e), Bool.and(Nat.is_eq(e, 6141n), LE)), Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(e, 6141n), LE)), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), c1, Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(e, 6141n), LE)), Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), LE)), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), c2, Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), LE)), Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), Bool.not(C.fits(53n, SF.rne(SW.value(sig), 10n))))), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), c3, ov_c(Nat.sub(e, F.off()), C.fits(53n, SF.rne(SW.value(sig), 10n))))))