law absent_selected

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

import Base
import bend-kit-scheduler@0.4.1.0/queue.bend as Q

204law absent_selected:
205  for ~A: Data
206  for now: Nat
207  for +i: Nat
208  for +s: Q.State<A>
209  for eh: absent.heap(A, Q.pending(A, s), i)
210  for t: Q.Ticket<A>
211  for e: {selected(A, Q.select(~A, now, s)) == Some{t} : Maybe<&2, Q.Ticket<A>>}
212  {Nat.is_eq(Q.id(A, t), i) == False{} : Bool}