merge — Mathlib

Lean4
/-- O(log(m + n)). Concatenate two trees that are ordered with respect to each other.

     merge {1, 2} {3, 4} = {1, 2, 3, 4}
     merge {3, 4} {1, 2} = precondition violation -/
def merge (l : Ordnode α) : Ordnode α → Ordnode α :=
  (Ordnode.recOn (motive := fun _ => Ordnode α → Ordnode α) l fun r => r) fun ls ll lx lr _ IHlr r =>
    (Ordnode.recOn (motive := fun _ => Ordnode α) r (node ls ll lx lr)) fun rs rl rx rr IHrl _ =>
      if delta * ls < rs then balanceL IHrl rx rr
      else
        if delta * rs < ls then balanceR ll lx (IHlr <| node rs rl rx rr)
        else glue (node ls ll lx lr) (node rs rl rx rr)
Похожие утверждения