def sub_val

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64norm.bend:81

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/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/nat.bend as N
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/lib/u32half.bend as UH
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/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL

81def sub_val(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hz: {Nat.is_eq(Fr, 0n) == False{} : Bool}) -> {SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))) == C.shift(Nat.sub(X.clz(fa), 11n), Fr) : Nat}:
82  +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
83  +et = clz_t(fa, Fr, hfa, hb)
84  +hk = N.le_lt_trans(Nat.sub(X.clz(fa), 11n), 53n, 64n, L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, Nat.sub(53n, M.bit_length(Fr)), Nat.sub(X.clz(fa), 11n), Equal.sym(Nat, Nat.sub(X.clz(fa), 11n), Nat.sub(53n, M.bit_length(Fr)), et), UH.sub_le(53n, M.bit_length(Fr))), {==})
85  sv = SH.shl_value(fa, Nat.sub(X.clz(fa), 11n), hk)
86  Equal.trans(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), SW.value(fa))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sv, Equal.trans(Nat, C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), SW.value(fa))), C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr)), C.shift(Nat.sub(X.clz(fa), 11n), Fr), Equal.cong(Nat, Nat, z => C.low(64n, C.shift(Nat.sub(X.clz(fa), 11n), z)), SW.value(fa), Fr, hfa), WW.low_fit(64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SH.fits_mono(53n, 64n, C.shift(Nat.sub(X.clz(fa), 11n), Fr), {==}, sub_fit(fa, Fr, hfa, hF, hz)))))