def eq_gen

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:342

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/math/typed/u32laws.bend as LW

342def eq_gen(+one: Nat, +h1: {one == 1n : Nat}, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +bad: Bool, +hbad: {Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})) == bad : Bool}, +z: Bool) -> {F.eq_z(F.Bits{xl, xh}, F.Bits{yl, yh}, bad, z) == Bool.and(Bool.not(bad), Cmp.is_eq(SF.pick(Cmp, z, EQ{}, SF.pick(Cmp, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), SF.flip(SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), LT{}, GT{}))))) : Bool}:
343  match bad z:
344    case True{} _:
345      {==}
346    case False{} True{}:
347      {==}
348    case False{} False{}:
349      +nx = or_l(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh}), hbad)
350      +ny = or_r(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh}), hbad)
351      +e1 = Equal.trans(Bool, Bool.and(U32.is_eq(xl, yl), U32.is_eq(xh, yh)), Bool.and(Nat.is_eq(v(xl), v(yl)), U32.is_eq(xh, yh)), Bool.and(Nat.is_eq(v(xl), v(yl)), Bool.and(Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), Nat.is_eq(SF.b2n(SF.sign(F.Bits{xl, xh})), SF.b2n(SF.sign(F.Bits{yl, yh}))))), Equal.cong(Bool, Bool, t => Bool.and(t, U32.is_eq(xh, yh)), U32.is_eq(xl, yl), Nat.is_eq(v(xl), v(yl)), LW.eq_nat(xl, yl)), Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(v(xl), v(yl)), t), U32.is_eq(xh, yh), Bool.and(Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), Nat.is_eq(SF.b2n(SF.sign(F.Bits{xl, xh})), SF.b2n(SF.sign(F.Bits{yl, yh})))), hw(xl, xh, yl, yh)))
352      Equal.trans(Bool, Bool.and(U32.is_eq(xl, yl), U32.is_eq(xh, yh)), Bool.and(Nat.is_eq(v(xl), v(yl)), Bool.and(Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), Nat.is_eq(SF.b2n(SF.sign(F.Bits{xl, xh})), SF.b2n(SF.sign(F.Bits{yl, yh}))))), Cmp.is_eq(SF.pick(Cmp, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), SF.flip(SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), LT{}, GT{}))), e1, eqs(Nat.is_eq(v(xl), v(yl)), Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh}), hq(one, h1, xl, xh, yl, yh, nx, ny)))