F64cmp.hw: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as F64cmp
Lines 334-340 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&start_line=334&end_line=340

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

# the high words are equal when sign and the low 31 bits are
def 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}:
  +e1 = LW.eq_nat(xh, yh)
  +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))))
  +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))))
  +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))))
  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)))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=bit_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=half0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=eq_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=eq_limbs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=b2n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=sign
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64