QueueProof.requeue_absent: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/queue_proof.bend as QueueProof
Lines 258-263 of bend-kit-scheduler@0.4.1.0/queue_proof.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&start_line=258&end_line=263

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

def requeue_absent(~A: Data, +i: Nat, d: Nat, +s: Q.State<A>, e: {Q.find.list(A, Q.running(A, s), i) == None{} : Maybe<&2, Q.Ticket<A>>}) -> {L.requeued(A, Q.requeue(~A, i, d, s)) == False{} : Bool}:
  match s:
    case Q.State{n, h, r}:
      %Equal.sym(Q.State<A> & Bool, Q.requeue(~A, i, d, Q.State{n, h, r}), L.requeue.reference(~A, i, d, Q.State{n, h, r}), L.requeue_equivalent(~A, i, d, Q.State{n, h, r})) : {L.requeued(A, _) == False{} : Bool}
      %Equal.sym(Maybe<&2, Q.Ticket<A>>, Q.find.list(A, r, i), None{}, e) : {L.requeued(A, Q.requeue.completed(~A, (Q.State{n, h, Q.remove.list(A, r, i)}, _), d)) == False{} : Bool}
      {==}

Uses (16):
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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-kit-scheduler@0.4.1.0/queue.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=Ticket
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=find.list
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=remove.list
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=requeue
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=requeue.completed
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=running
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue.reference
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue_equivalent
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeued