def fx_c

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

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

174def fx_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.fx_cls(x, t) == SF.pickt(F.F64 & F.Exp, Bool.and(t, Bool.not(z)), (SF.qnan(), F.Exp{False{}, 0n}), SF.pickt(F.F64 & F.Exp, Bool.or(Bool.and(t, z), SF.is_zero(x)), (x, F.Exp{False{}, 0n}), FIN(x))) : F.F64 & F.Exp}:
175  match t z:
176    case True{} True{}:
177      Equal.cong(Bool, F.F64 & F.Exp, b => (F.nan_or(x, Bool.not(b)), F.Exp{False{}, 0n}), X.is_zero(F.frac(x)), True{}, hz)
178    case True{} False{}:
179      Equal.cong(Bool, F.F64 & F.Exp, b => (F.nan_or(x, Bool.not(b)), F.Exp{False{}, 0n}), X.is_zero(F.frac(x)), False{}, hz)
180    case False{} _:
181      +e1 = Equal.cong(Bool, F.F64 & F.Exp, b => F.fx_z(x, b), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
182      Equal.trans(F.F64 & F.Exp, F.fx_z(x, F.is_zero(x)), F.fx_z(x, SF.is_zero(x)), SF.pickt(F.F64 & F.Exp, SF.is_zero(x), (x, F.Exp{False{}, 0n}), FIN(x)), e1, fxz_c(x, SF.is_zero(x)))