F64fmod.badv: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as F64fmod
Lines 502-513 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend&start_line=502&end_line=513

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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

def badv(+x: F.F64, +y: F.F64) -> {Bool.or(Bool.or(F.unordered(x, y), F.is_inf(x)), F.is_zero(y)) == SF.rbad(x, y) : Bool}:
  +e1 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.or(t, F.is_nan(y)), F.is_inf(x)), F.is_zero(y)), F.is_nan(x), SF.is_nan(x), FB.is_nan_value(x))
  +e2 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.or(SF.is_nan(x), t), F.is_inf(x)), F.is_zero(y)), F.is_nan(y), SF.is_nan(y), FB.is_nan_value(y))
  +U = Bool.or(SF.is_nan(x), SF.is_nan(y))
  +e3 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(t, F.is_inf(x)), F.is_zero(y)), U, Bool.not(Bool.not(U)), Equal.sym(Bool, Bool.not(Bool.not(U)), U, nn(U)))
  +e4 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.not(Bool.not(U)), t), F.is_zero(y)), F.is_inf(x), SF.is_inf(x), FB.is_inf_value(x))
  +e5 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.not(Bool.not(U)), SF.is_inf(x)), t), F.is_zero(y), SF.is_zero(y), FB.is_zero_value(y))
  +b1 = Bool.or(Bool.or(Bool.or(SF.is_nan(x), F.is_nan(y)), F.is_inf(x)), F.is_zero(y))
  +b2 = Bool.or(Bool.or(U, F.is_inf(x)), F.is_zero(y))
  +b3 = Bool.or(Bool.or(Bool.not(Bool.not(U)), F.is_inf(x)), F.is_zero(y))
  +b4 = Bool.or(Bool.or(Bool.not(Bool.not(U)), SF.is_inf(x)), F.is_zero(y))
  Equal.trans(Bool, Bool.or(Bool.or(F.unordered(x, y), F.is_inf(x)), F.is_zero(y)), b1, SF.rbad(x, y), e1, Equal.trans(Bool, b1, b2, SF.rbad(x, y), e2, Equal.trans(Bool, b2, b3, SF.rbad(x, y), e3, Equal.trans(Bool, b3, b4, SF.rbad(x, y), e4, e5))))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=is_inf_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=is_nan_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=is_zero_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend&name=nn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=is_nan
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=rbad
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=is_nan
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=unordered