Uint64n.last_acc: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
Lines 156-162 of bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend&start_line=156&end_line=162

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

def 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}:
  match ok:
    case True{}:
      {==}
    case False{}:
      %Equal.sym(Nat, h, C.high(64n, Nat.mul(x, n)), hh) : {(C.high(64n, Nat.mul(x, n)), s) == (_, s) : Nat & S}
      {==}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend&name=accept
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend&name=below_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64