def iif_c

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

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/spec/math/w64.bend as SW
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/f64tools.bend as T

158def iif_c(+x: F.F64, +c: Bool) -> {F.ii_fin(x, c) == Bool.or(c, LZ(x)) : Bool}:
159  match c:
160    case True{}:
161      {==}
162    case False{}:
163      +k = Nat.sub(3000n, F.dexp(x))
164      +e1 = iik_c(F.dmant(x), k, Nat.is_lt(k, 64n), {==})
165      +e2 = Equal.cong(Nat, Bool, t => Nat.is_eq(C.low(k, t), 0n), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
166      +e3 = Equal.cong(Nat, Bool, t => Nat.is_eq(C.low(Nat.sub(3000n, t), SF.mant(x)), 0n), F.dexp(x), SF.xexp(x), T.dexp_value(x))
167      Equal.trans(Bool, F.ii_k(F.dmant(x), k, Nat.is_lt(k, 64n)), Nat.is_eq(C.low(k, SW.value(F.dmant(x))), 0n), LZ(x), e1, Equal.trans(Bool, Nat.is_eq(C.low(k, SW.value(F.dmant(x))), 0n), Nat.is_eq(C.low(k, SF.mant(x)), 0n), LZ(x), e2, e3))