def tbn

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64nrp.bend:54

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/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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL

54def tbn(+k: Nat, +V: Nat, +K: Nat, +hz: {Nat.is_eq(V, 0n) == False{} : Bool}, +ek: {Nat.add(k, M.bit_length(V)) == 1n+K : Nat}) -> {C.fits(K, C.shift(k, V)) == False{} : Bool}:
55  +epb = N.sub_add(M.bit_length(V), 1n, BL.bl_pos(V, hz, M.bit_length(V), {==}))
56  +K2 = Nat.add(k, Nat.sub(M.bit_length(V), 1n))
57  +e2 = N.succ_inj(K2, K, Equal.trans(Nat, 1n+K2, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), 1n+K, Equal.sym(Nat, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), 1n+K2, N.add_succ(k, Nat.sub(M.bit_length(V), 1n))), Equal.trans(Nat, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), Nat.add(k, M.bit_length(V)), 1n+K, Equal.cong(Nat, Nat, z => Nat.add(k, z), 1n+Nat.sub(M.bit_length(V), 1n), M.bit_length(V), epb), ek)))
58  +hql = L.subst(Nat, z => {Nat.is_le(z, C.shift(k, V)) == True{} : Bool}, C.shift(k, C.pow2(Nat.sub(M.bit_length(V), 1n))), C.pow2(K2), WW.shift_pow2(k, Nat.sub(M.bit_length(V), 1n)), WW.shift_mono(k, C.pow2(Nat.sub(M.bit_length(V), 1n)), V, BL.lower(V, hz)))
59  +nf = Equal.trans(Bool, C.fits(K2, C.pow2(K2)), Nat.is_lt(C.pow2(K2), C.pow2(K2)), False{}, WW.fits_lt(K2, C.pow2(K2)), N.lt_irrefl(C.pow2(K2)))
60  L.subst(Nat, z => {C.fits(z, C.shift(k, V)) == False{} : Bool}, K2, K, e2, FR.nfit(K2, C.pow2(K2), C.shift(k, V), hql, nf))