def last_acc

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

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/src/math/u64.bend as WU

156def last_acc(~S: Data, ~next: S -> WU.U64 & S, +h: Nat, +ok: Bool, +x: Nat, +n: Nat, +s: S, +hh: {h == C.high(64n, Nat.mul(x, n)) : Nat}) -> {SR.below_go(~S, ~next, 0n, n, SR.accept(h, ok), x, s) == (h, s) : Nat & S}:
157  match ok:
158    case True{}:
159      {==}
160    case False{}:
161      %Equal.sym(Nat, h, C.high(64n, Nat.mul(x, n)), hh) : {(C.high(64n, Nat.mul(x, n)), s) == (_, s) : Nat & S}
162      {==}