def ld_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:244

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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

244def ld_c(+x: F.F64, +neg: Bool, +k: Nat, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.ld_cls(x, F.Exp{neg, k}, t) == SF.pick(F.F64, Bool.and(t, Bool.not(z)), SF.qnan(), SF.pick(F.F64, Bool.or(Bool.and(t, z), SF.is_zero(x)), x, LD(x, neg, k))) : F.F64}:
245  match t z:
246    case True{} True{}:
247      Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), True{}, hz)
248    case True{} False{}:
249      Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), False{}, hz)
250    case False{} _:
251      +e1 = Equal.cong(Bool, F.F64, b => F.ld_z(x, F.Exp{neg, k}, b), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
252      Equal.trans(F.F64, F.ld_z(x, F.Exp{neg, k}, F.is_zero(x)), F.ld_z(x, F.Exp{neg, k}, SF.is_zero(x)), SF.pick(F.F64, SF.is_zero(x), x, LD(x, neg, k)), e1, ldz_c(x, neg, k, SF.is_zero(x)))