def threshold

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64.bend:88

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

88def threshold() -> {S.sign_threshold(63n) == W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n)) : Word(64n)}:
89  {==}