def fmax_nx_c

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

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

114def fmax_nx_c(+x: F.F64, +y: F.F64, +a: Bool, +ha: {SF.is_nan(x) == a : Bool}) -> {F.fmax_nx(x, y, a) == SF.pick(F.F64, a, SF.pick(F.F64, SF.is_nan(y), SF.qnan(), y), SF.pick(F.F64, SF.is_nan(y), 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}:
115  match a:
116    case True{}:
117      Equal.trans(F.F64, F.nan_or(y, F.is_nan(y)), F.nan_or(y, SF.is_nan(y)), SF.pick(F.F64, SF.is_nan(y), SF.qnan(), y), Equal.cong(Bool, F.F64, t => F.nan_or(y, t), F.is_nan(y), SF.is_nan(y), FB.is_nan_value(y)), non(y, SF.is_nan(y)))
118    case False{}:
119      +R = SF.pick(F.F64, SF.is_nan(y), 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)))
120      Equal.trans(F.F64, F.fmax_ny(x, y, F.is_nan(y)), F.fmax_ny(x, y, SF.is_nan(y)), R, Equal.cong(Bool, F.F64, t => F.fmax_ny(x, y, t), F.is_nan(y), SF.is_nan(y), FB.is_nan_value(y)), fmax_ny_c(x, y, ha, SF.is_nan(y), {==}))