def ordered

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

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

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