def fmax_ny_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:97

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

97def fmax_ny_c(+x: F.F64, +y: F.F64, +hx: {SF.is_nan(x) == False{} : Bool}, +b: Bool, +hb: {SF.is_nan(y) == b : Bool}) -> {F.fmax_ny(x, y, b) == SF.pick(F.F64, b, x, SF.pick(F.F64, Bool.and(SF.is_zero(x), SF.is_zero(y)), SF.zero(Bool.and(SF.sign(x), SF.sign(y))), SF.pick(F.F64, Cmp.is_lt(SF.ord(y, x)), x, y))) : F.F64}:
98  match b:
99    case True{}:
100      {==}
101    case False{}:
102      +R = SF.pick(F.F64, Bool.and(SF.is_zero(x), SF.is_zero(y)), SF.zero(Bool.and(SF.sign(x), SF.sign(y))), SF.pick(F.F64, Cmp.is_lt(SF.ord(y, x)), x, y))
103      +e1 = Equal.cong(Bool, F.F64, t => F.fmax_z(x, y, t), F.zeros(x, y), Bool.and(SF.is_zero(x), SF.is_zero(y)), zeros_v(x, y))
104      Equal.trans(F.F64, F.fmax_z(x, y, F.zeros(x, y)), F.fmax_z(x, y, Bool.and(SF.is_zero(x), SF.is_zero(y))), R, e1, fmax_z_c(x, y, hx, hb, Bool.and(SF.is_zero(x), SF.is_zero(y))))