def st_c

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

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/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/logic.bend as L
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

295def st_c(+x: F.F64, +hn: {SF.is_nan(x) == False{} : Bool}, +hz: {SF.is_zero(x) == False{} : Bool}, +up: Bool) -> {F.na_step(x, up) == SF.of_pat(SF.sign(x), SF.pick(Nat, up, Nat.add(SF.pat(x), 1n), Nat.sub(SF.pat(x), 1n))) : F.F64}:
296  match up:
297    case True{}:
298      +P = SF.pat(x)
299      +M = F.mag(x)
300      +W = X.add(M, WU.U64{1, 0})
301      +h63 = p1_c(1n, {==}, x, hn, Nat.is_eq(SF.efield(x), 2047n), {==})
302      +h64 = SH.fits_mono(63n, 64n, Nat.add(P, 1n), {==}, p1_c(1n, {==}, x, hn, Nat.is_eq(SF.efield(x), 2047n), {==}))
303      +ev = Equal.trans(Nat, SW.value(W), C.low(64n, Nat.add(SW.value(M), 1n)), Nat.add(P, 1n), WA.add_value(M, WU.U64{1, 0}), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(M), 1n)), C.low(64n, Nat.add(P, 1n)), Nat.add(P, 1n), Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(t, 1n)), SW.value(M), P, magval(x)), WW.low_fit(64n, Nat.add(P, 1n), h64)))
304      step_fin(x, W, Nat.add(P, 1n), ev, h63)
305    case False{}:
306      +P = SF.pat(x)
307      +M = F.mag(x)
308      +W = X.sub(M, WU.U64{1, 0})
309      +hP = FL.nz_le(P, Equal.trans(Bool, Nat.is_eq(P, 0n), SF.is_zero(x), False{}, patz(x), hz))
310      +hM = L.subst(Nat, t => {Nat.is_le(1n, t) == True{} : Bool}, P, SW.value(M), Equal.sym(Nat, SW.value(M), P, magval(x)), hP)
311      +ev = Equal.trans(Nat, SW.value(W), Nat.sub(SW.value(M), 1n), Nat.sub(P, 1n), WA.sub_value(M, WU.U64{1, 0}, hM), Equal.cong(Nat, Nat, t => Nat.sub(t, 1n), SW.value(M), P, magval(x)))
312      +h63 = SH.fits_lek(63n, Nat.sub(P, 1n), P, sub_le_self(P, 1n), patfit(x))
313      step_fin(x, W, Nat.sub(P, 1n), ev, h63)