def iik_c

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

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/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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL

146def iik_c(+w: WU.U64, +k: Nat, +b: Bool, +hb: {Nat.is_lt(k, 64n) == b : Bool}) -> {F.ii_k(w, k, b) == Nat.is_eq(C.low(k, SW.value(w)), 0n) : Bool}:
147  match b:
148    case True{}:
149      iik_t(w, k, hb)
150    case False{}:
151      +V = SW.value(w)
152      +el = WW.low_fit(k, V, SH.fits_mono(64n, k, V, N.not_lt_le(k, 64n, hb), FL.vb64(w)))
153      Equal.trans(Bool, X.is_zero(w), Nat.is_eq(V, 0n), Nat.is_eq(C.low(k, V), 0n), WA.is_zero_value(w), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), V, C.low(k, V), Equal.sym(Nat, C.low(k, V), V, el)))