def fmax_z_c

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

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

77def fmax_z_c(+x: F.F64, +y: F.F64, +hx: {SF.is_nan(x) == False{} : Bool}, +hy: {SF.is_nan(y) == False{} : Bool}, +zz: Bool) -> {F.fmax_z(x, y, zz) == SF.pick(F.F64, zz, 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}:
78  match zz:
79    case True{}:
80      +e1 = T.zero_v(Bool.and(F.signbit(x), F.signbit(y)))
81      +e2 = Equal.cong(Bool, F.F64, t => SF.zero(Bool.and(t, F.signbit(y))), F.signbit(x), SF.sign(x), FB.signbit_value(x))
82      +e3 = Equal.cong(Bool, F.F64, t => SF.zero(Bool.and(SF.sign(x), t)), F.signbit(y), SF.sign(y), FB.signbit_value(y))
83      Equal.trans(F.F64, F.zero(Bool.and(F.signbit(x), F.signbit(y))), SF.zero(Bool.and(F.signbit(x), F.signbit(y))), SF.zero(Bool.and(SF.sign(x), SF.sign(y))), e1, Equal.trans(F.F64, SF.zero(Bool.and(F.signbit(x), F.signbit(y))), SF.zero(Bool.and(SF.sign(x), F.signbit(y))), SF.zero(Bool.and(SF.sign(x), SF.sign(y))), e2, e3))
84    case False{}:
85      +e1 = Equal.cong(Bool, F.F64, b => F.fpick(x, y, b), F.lt(y, x), Cmp.is_lt(SF.ord(y, x)), ltc(y, x, or_ff(SF.is_nan(y), SF.is_nan(x), hy, hx)))
86      Equal.trans(F.F64, F.fpick(x, y, F.lt(y, x)), F.fpick(x, y, Cmp.is_lt(SF.ord(y, x))), SF.pick(F.F64, Cmp.is_lt(SF.ord(y, x)), x, y), e1, fpk(x, y, Cmp.is_lt(SF.ord(y, x))))