def badv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:502

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

502def 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}:
503  +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))
504  +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))
505  +U = Bool.or(SF.is_nan(x), SF.is_nan(y))
506  +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)))
507  +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))
508  +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))
509  +b1 = Bool.or(Bool.or(Bool.or(SF.is_nan(x), F.is_nan(y)), F.is_inf(x)), F.is_zero(y))
510  +b2 = Bool.or(Bool.or(U, F.is_inf(x)), F.is_zero(y))
511  +b3 = Bool.or(Bool.or(Bool.not(Bool.not(U)), F.is_inf(x)), F.is_zero(y))
512  +b4 = Bool.or(Bool.or(Bool.not(Bool.not(U)), SF.is_inf(x)), F.is_zero(y))
513  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))))