def clz_t

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

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/nat.bend as N
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/math/typed/f64round.bend as FR

49def clz_t(+fa: WU.U64, +Fr: Nat, +hfa: {SW.value(fa) == Fr : Nat}, +hb: {Nat.is_le(M.bit_length(Fr), 52n) == True{} : Bool}) -> {Nat.sub(X.clz(fa), 11n) == Nat.sub(53n, M.bit_length(Fr)) : Nat}:
50  +ec = Equal.trans(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), Nat.sub(64n, M.bit_length(Fr)), CLZ.clz_value(fa), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(fa), Fr, hfa))
51  +hb53 = N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==})
52  +e1 = Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec)
53  +e2 = Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), Nat.sub(64n, M.bit_length(Fr)), Nat.add(11n, Nat.sub(53n, M.bit_length(Fr))), FR.sub_add_a(11n, 53n, M.bit_length(Fr), hb53))
54  Equal.trans(Nat, Nat.sub(X.clz(fa), 11n), Nat.sub(Nat.sub(64n, M.bit_length(Fr)), 11n), Nat.sub(53n, M.bit_length(Fr)), e1, Equal.trans(Nat, Nat.sub(Nat.sub(64n, M.bit_length(Fr)), 11n), Nat.sub(Nat.add(11n, Nat.sub(53n, M.bit_length(Fr))), 11n), Nat.sub(53n, M.bit_length(Fr)), e2, N.add_sub_cancel(11n, Nat.sub(53n, M.bit_length(Fr)))))