def ok_u

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

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/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC

522def ok_u(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}) -> {Bool.or(SF.is_nan(x), SF.is_nan(y)) == False{} : Bool}:
523  +h1 = FC.or_l(Bool.not(SF.ordered(x, y)), SF.is_inf(x), FC.or_l(Bool.or(Bool.not(SF.ordered(x, y)), SF.is_inf(x)), SF.is_zero(y), h))
524  FR.not_t(Bool.or(SF.is_nan(x), SF.is_nan(y)), FR.not_f(SF.ordered(x, y), h1))