def sa_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mexp.bend:30

import Base
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/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/src/math/natural.bend as M
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/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as CLZ
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as NM

30def sa_le(+ea: Nat, +fa: WU.U64) -> {Nat.is_le(NM.sa(ea, fa), 53n) == True{} : Bool}:
31  match ea:
32    case 0n:
33      +hc = L.subst(Nat, z => {Nat.is_le(z, 64n) == True{} : Bool}, Nat.sub(64n, M.bit_length(SW.value(fa))), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), CLZ.clz_value(fa)), UH.sub_le(64n, M.bit_length(SW.value(fa))))
34      NF.sub_mono_l(X.clz(fa), 64n, 11n, hc)
35    case 1n+ +p:
36      {==}