Float.lt_s_case: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float Lines 441-449 of bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&start_line=441&end_line=449 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 def 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}: +hl = hl_of(x, 1n+np, hv) +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))) +j = J(np) +Q = X.shl(mm(x), Nat.sub(52n, j)) +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))) %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} %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} below_one(X.lo(Q), X.hi(Q), Nat.add(j, 970n), 1072693248, 1023, 1023n, hE, {==}, {==}, {==}, {==}, {==}, {==}) Uses (36): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_lt_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=J https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=below_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=hl_of https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=impl_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=iz https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=j52 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&name=mm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend&name=bl_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_cancel_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=f53 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=f53_z https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend&name=to_float https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=clz https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=hi https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=is_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=lo https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shl