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

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

def merge_ordered(~A: Data, +fuel: Nat, +a: H.Heap<Q.Ticket<A>>, +b: H.Heap<Q.Ticket<A>>, +ea: L.ordered(A, a), +eb: L.ordered(A, b)) -> L.ordered(A, 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{L.Both{xal, xar}, L.Both{oal, oar}} = ea
          L.Both{L.Both{ybl, ybr}, L.Both{obl, obr}} = eb
          split(c => L.ordered(A, 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{L.Both{merge_all(~A, L.bound.ticket(A, x), f, ar, H.HNode{nb, y, bl, br}, xar, L.Both{e, L.Both{below_trans(A, bl, x, y, e, ybl), below_trans(A, br, x, y, e, ybr)}}), xal}, L.Both{merge_ordered(~A, f, ar, H.HNode{nb, y, bl, br}, oar, L.Both{L.Both{ybl, ybr}, L.Both{obl, obr}}), oal}},
            e => (
              +e = le_flip(A, x, y, e)
              L.Both{L.Both{merge_all(~A, L.bound.ticket(A, y), f, br, H.HNode{na, x, al, ar}, ybr, L.Both{e, L.Both{below_trans(A, al, y, x, e, xal), below_trans(A, ar, y, x, e, xar)}}), ybl}, L.Both{merge_ordered(~A, f, br, H.HNode{na, x, al, ar}, obr, L.Both{L.Both{xal, xar}, L.Both{oal, oar}}), obl}}))

Uses (15):
  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=bound.ticket
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=ordered
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=below_trans
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=le_flip
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=merge_all
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=split