def hw

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

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/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

334# the high words are equal when sign and the low 31 bits are
335def hw(+xl: U32, +xh: U32, +yl: U32, +yh: U32) -> {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})))) : Bool}:
336  +e1 = LW.eq_nat(xh, yh)
337  +e2 = Equal.trans(Bool, Nat.is_eq(v(xh), v(yh)), Nat.is_eq(Nat.add(C.low(31n, v(xh)), C.shift(31n, C.high(31n, v(xh)))), v(yh)), Nat.is_eq(Nat.add(C.low(31n, v(xh)), C.shift(31n, C.high(31n, v(xh)))), Nat.add(C.low(31n, v(yh)), C.shift(31n, C.high(31n, v(yh))))), Equal.cong(Nat, Bool, t => Nat.is_eq(t, v(yh)), v(xh), Nat.add(C.low(31n, v(xh)), C.shift(31n, C.high(31n, v(xh)))), WW.low_high(31n, v(xh))), Equal.cong(Nat, Bool, t => Nat.is_eq(Nat.add(C.low(31n, v(xh)), C.shift(31n, C.high(31n, v(xh)))), t), v(yh), Nat.add(C.low(31n, v(yh)), C.shift(31n, C.high(31n, v(yh)))), WW.low_high(31n, v(yh))))
338  +e3 = Equal.sym(Bool, Bool.and(Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), Nat.is_eq(C.high(31n, v(xh)), C.high(31n, v(yh)))), Nat.is_eq(Nat.add(C.low(31n, v(xh)), C.shift(31n, C.high(31n, v(xh)))), Nat.add(C.low(31n, v(yh)), C.shift(31n, C.high(31n, v(yh))))), WW.eq_limbs(31n, C.low(31n, v(xh)), C.high(31n, v(xh)), C.low(31n, v(yh)), C.high(31n, v(yh)), WW.low_fits(31n, v(xh)), WW.low_fits(31n, v(yh))))
339  +e4 = Equal.trans(Bool, Bool.and(Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), Nat.is_eq(C.high(31n, v(xh)), C.high(31n, v(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})), C.high(31n, v(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})))), Equal.cong(Nat, Bool, t => Bool.and(Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), Nat.is_eq(t, C.high(31n, v(yh)))), C.high(31n, v(xh)), SF.b2n(SF.sign(F.Bits{xl, xh})), FB.bit_c(C.high(31n, v(xh)), FB.half0(xh))), Equal.cong(Nat, Bool, t => 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})), t)), C.high(31n, v(yh)), SF.b2n(SF.sign(F.Bits{yl, yh})), FB.bit_c(C.high(31n, v(yh)), FB.half0(yh))))
340  Equal.trans(Bool, U32.is_eq(xh, yh), Nat.is_eq(v(xh), v(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})))), e1, Equal.trans(Bool, Nat.is_eq(v(xh), v(yh)), Nat.is_eq(Nat.add(C.low(31n, v(xh)), C.shift(31n, C.high(31n, v(xh)))), Nat.add(C.low(31n, v(yh)), C.shift(31n, C.high(31n, v(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})))), e2, Equal.trans(Bool, Nat.is_eq(Nat.add(C.low(31n, v(xh)), C.shift(31n, C.high(31n, v(xh)))), Nat.add(C.low(31n, v(yh)), C.shift(31n, C.high(31n, v(yh))))), Bool.and(Nat.is_eq(C.low(31n, v(xh)), C.low(31n, v(yh))), Nat.is_eq(C.high(31n, v(xh)), C.high(31n, v(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})))), e3, e4)))