def ov_c

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
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
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U

712# the overflow test of roundPackToF64 against the spec's exponent field
713def ov_c(+EF: Nat, +f: Bool) -> {Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), Bool.not(f))) == Bool.not(Nat.is_lt(Nat.add(EF, SF.pick(Nat, f, 1n, 2n)), 2047n)) : Bool}:
714  match f:
715    case True{}:
716      +l1 = Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), False{})), Bool.or(Nat.is_lt(2045n, EF), False{}), Nat.is_lt(2045n, EF), Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, EF), t), Bool.and(Nat.is_eq(EF, 2045n), False{}), False{}, and_f(Nat.is_eq(EF, 2045n))), or_f(Nat.is_lt(2045n, EF)))
717      +r1 = Equal.trans(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 1n), 2047n)), Bool.not(Nat.is_lt(EF, 2046n)), Nat.is_lt(2045n, EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(Nat.add(EF, 1n), 2047n), Nat.is_lt(EF, 2046n), WW.lt_cancel_r(EF, 2046n, 1n)), Equal.trans(Bool, Bool.not(Nat.is_lt(EF, 2046n)), Nat.is_le(2046n, EF), Nat.is_lt(2045n, EF), Equal.sym(Bool, Nat.is_le(2046n, EF), Bool.not(Nat.is_lt(EF, 2046n)), FB.le_nlt(2046n, EF)), le_succ_lt(2045n, EF)))
718      Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), False{})), Nat.is_lt(2045n, EF), Bool.not(Nat.is_lt(Nat.add(EF, 1n), 2047n)), l1, Equal.sym(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 1n), 2047n)), Nat.is_lt(2045n, EF), r1))
719    case False{}:
720      +l1 = Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), True{})), Bool.or(Nat.is_lt(2045n, EF), Nat.is_eq(EF, 2045n)), Nat.is_le(2045n, EF), Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, EF), t), Bool.and(Nat.is_eq(EF, 2045n), True{}), Nat.is_eq(EF, 2045n), U.and_true(Nat.is_eq(EF, 2045n))), ge_or(2045n, EF))
721      +r1 = Equal.trans(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 2n), 2047n)), Bool.not(Nat.is_lt(EF, 2045n)), Nat.is_le(2045n, EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(Nat.add(EF, 2n), 2047n), Nat.is_lt(EF, 2045n), WW.lt_cancel_r(EF, 2045n, 2n)), Equal.sym(Bool, Nat.is_le(2045n, EF), Bool.not(Nat.is_lt(EF, 2045n)), FB.le_nlt(2045n, EF)))
722      Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), True{})), Nat.is_le(2045n, EF), Bool.not(Nat.is_lt(Nat.add(EF, 2n), 2047n)), l1, Equal.sym(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 2n), 2047n)), Nat.is_le(2045n, EF), r1))