law complete_token

bend-kit-scheduler@0.4.1.0 · queue_laws.bend:300

import Base
import bend-kit-collections@0.1.4.1/heap.bend as H
import bend-kit-scheduler@0.4.1.0/queue.bend as Q

300law complete_token:
301  for -A: Data
302  for +i: Nat
303  for old: Nat
304  for x: A
305  for n: Nat
306  for h: H.Heap<Q.Ticket<A>>
307  for r: List<&2, Q.Ticket<A>>
308  {selected(A, Q.complete(A, i, Q.State{n, h, Q.Ticket{i, old, x} <> r}))
309   == Some{Q.Ticket{i, old, x}} : Maybe<&2, Q.Ticket<A>>}