def tu_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:178

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/src/math/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

178def tu_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {SF.rv64(F.tu_cls(x, t)) == TNR(Bool.and(t, Bool.not(z)), Bool.and(t, z), Bool.and(SF.sign(x), Bool.not(Nat.is_eq(SF.int_part(x), 0n))), SF.int_part(x), C.fits(64n, SF.int_part(x))) : Result<&2, &2, NE.NumError, Nat>}:
179  match t z:
180    case True{} True{}:
181      Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.rv64(F.tu_top(Bool.not(b))), X.is_zero(F.frac(x)), True{}, hz)
182    case True{} False{}:
183      Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.rv64(F.tu_top(Bool.not(b))), X.is_zero(F.frac(x)), False{}, hz)
184    case False{} _:
185      +e1 = tu_fin_c(x, Nat.is_le(3000n, F.dexp(x)), {==})
186      +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, u => TN(SF.sign(x), IPc(x, Nat.is_le(3000n, u))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
187      Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_fin(x, Nat.is_le(3000n, F.dexp(x)))), TN(SF.sign(x), IPc(x, Nat.is_le(3000n, F.dexp(x)))), TN(SF.sign(x), SF.int_part(x)), e1, e2)