QueueProof.merge_all: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/queue_proof.bend as QueueProof
Lines 102-121 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=102&end_line=121

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
import bend-kit-scheduler@0.4.1.0/queue_laws.bend as L

# Merging cannot introduce an element that violates any predicate P. Fuel zero
# returns the left heap, so this lemma does not trust cached heap sizes.
def merge_all(~A: Data, -P: Q.Ticket<A> -> Data, +fuel: Nat, +a: H.Heap<Q.Ticket<A>>, +b: H.Heap<Q.Ticket<A>>, +ea: L.all.heap(A, P, a), +eb: L.all.heap(A, P, b)) -> L.all.heap(A, P, H.Heap.merge.go(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), fuel, a, b)):
  match fuel:
    case 0n:
      ea
    case 1n+f:
      match a b:
        case H.HLeaf{} H.HLeaf{}:
          Unit{}
        case H.HLeaf{} H.HNode{nb, y, bl, br}:
          eb
        case H.HNode{na, x, al, ar} H.HLeaf{}:
          ea
        case H.HNode{na, x, al, ar} H.HNode{nb, y, bl, br}:
          L.Both{ex, L.Both{eal, ear}} = ea
          L.Both{ey, L.Both{ebl, ebr}} = eb
          split(c => L.all.heap(A, P, H.HNode{Nat.add(na, nb), Bool.pick(Q.Ticket<A>, c, x, y), H.Heap.merge.go(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), f, Bool.pick(H.Heap<Q.Ticket<A>>, c, ar, br), Bool.pick(H.Heap<Q.Ticket<A>>, c, H.HNode{nb, y, bl, br}, H.HNode{na, x, al, ar})), Bool.pick(H.Heap<Q.Ticket<A>>, c, al, bl)}), Q.le(A, x, y),
            e => L.Both{ex, L.Both{merge_all(~A, P, f, ar, H.HNode{nb, y, bl, br}, ear, L.Both{ey, L.Both{ebl, ebr}}), eal}},
            e => L.Both{ey, L.Both{merge_all(~A, P, f, br, H.HNode{na, x, al, ar}, ebr, L.Both{ex, L.Both{eal, ear}}), ebl}})

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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-collections@0.1.4.1/heap.bend&name=Heap.merge.go
  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=le
  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=all.heap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=split