QueueLaws.ordered: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/queue_laws.bend as QueueLaws
Lines 87-99 of bend-kit-scheduler@0.4.1.0/queue_laws.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&start_line=87&end_line=99

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

# The root must bound both subtrees recursively, not just its direct children.
# No law takes the desired selection result as an assumption.
# Cached sizes are a separate construction invariant of collections' heap:
# new/push/merge build them and remove.heap recomputes each retained size.
# ordered deliberately concerns ordering only. The order/absence merge lemmas
# hold even for malformed sizes; they do not claim element conservation for
# forged HNode values whose merge fuel can run out early.
def ordered(-A: Data, h: H.Heap<Q.Ticket<A>>) -> Data:
  match h:
    case H.HLeaf{}:
      Unit
    case H.HNode{n, +t, +l, +r}:
      Both<Both<below(A, l, t), below(A, r, t)>, Both<ordered(A, l), ordered(A, r)>>

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/heap.bend&name=Heap
  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_laws.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=below