def lt_s_case

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:441

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/random/rand.bend as R
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/f64.bend as F
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/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as WC

441def lt_s_case(+x: WU.U64, +np: Nat, +hv: {SW.value(mm(x)) == 1n+np : Nat}) -> {F.lt(R.to_float(x), F.one()) == True{} : Bool}:
442  +hl = hl_of(x, 1n+np, hv)
443  +hf = Equal.trans(Bool, C.fits(53n, 1n+np), C.fits(53n, C.low(53n, SW.value(x))), True{}, Equal.cong(Nat, Bool, z => C.fits(53n, z), 1n+np, C.low(53n, SW.value(x)), Equal.sym(Nat, C.low(53n, SW.value(x)), 1n+np, hl)), WW.low_fits(53n, SW.value(x)))
444  +j = J(np)
445  +Q = X.shl(mm(x), Nat.sub(52n, j))
446  +hE = Equal.trans(Bool, Nat.is_lt(Nat.add(j, 970n), 1023n), Nat.is_lt(j, 53n), True{}, WW.lt_cancel_r(j, 53n, 970n), N.le_lt_succ(j, 52n, j52(np, hf)))
447  %Equal.sym(Bool, X.is_zero(mm(x)), Nat.is_eq(1n+np, 0n), iz(mm(x), 1n+np, hv)) : {F.lt(R.f53_z(mm(x), _), F.one()) == True{} : Bool}
448  %Equal.sym(F.F64, R.f53(mm(x), X.clz(mm(x))), bits(Q, Nat.add(j, 970n)), impl_eq(mm(x), np, hv, j, j52(np, hf), WC.bl_succ(np))) : {F.lt(_, F.one()) == True{} : Bool}
449  below_one(X.lo(Q), X.hi(Q), Nat.add(j, 970n), 1072693248, 1023, 1023n, hE, {==}, {==}, {==}, {==}, {==}, {==})