def pm_one

bend-collections-laws-math@1.0.0.0 · proofs/math/random/uint64n.bend:75

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/random/rand.bend as SR
import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as LE

75# pow2mod through a symbolic one (2^64 is never a closed term)
76def pm_one(+w: Nat, +m: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {SR.pow2mod(w, 1n+m) == Nat.mod(C.shift(w, one), 1n+m) : Nat}:
77  %Equal.sym(Nat, one, 1n, h1) : {SR.pow2mod(w, 1n+m) == Nat.mod(C.shift(w, _), 1n+m) : Nat}
78  LE.pm(w, m)