# Generated by tools/generators/tree_map.py; edit algorithm definitions there.
import Base
import ./dynamic_array.bend as D
import ./types/dynamic_array.bend as DE

# Indexed CLRS red-black map. Keys and payloads are Data for this version.
# Comparator is a type index: changing comparator requires rebuilding a map.
# Node links are slot indices plus one; zero is the black NIL sentinel.
type Node<-K: Data> is Data:
  Free{next: Nat}
  N{red: Bool, left: Nat, right: Nat, parent: Nat, key: K}

# Node storage: one array per node field instead of one array of Node
# records. Reading a record out of an array hands back a shared copy that the
# runtime reference-counts and takes apart field by field; a field read out of
# its own array is a plain word. The store has the shape of a dynamic array
# of nodes: slots [0, used) are live, the capacity is 2^depth <= 2^limit, and
# it grows by doubling. A slot holds the encoding of its node by ntag (0 free,
# 1 black, 2 red), nleft (the free-list link of a free slot), nright, nparent
# and nkey (None when free); every other slot holds the encoding of Free{0},
# so each array is exactly its field of the node list, padded.
type NodeStore<-K: Data> is Type:
  NS{limit: Nat, depth: Nat, cap: Nat, used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>}

type TreeMap<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
  TM{size: Nat, root: Nat, first: Nat, last: Nat, free: Nat,
     nodes: NodeStore<K>, payloads: D.DynArray<&2, Maybe<&2, V>>}

type Entry<-K: Data, -V: Data> is Data:
  Entry{key: K, value: V}

type Error is Data:
  CapacityExceeded{}
  OutOfRange{}
  NoCurrent{}
  InvalidBounds{}

type Rejected<-K: Data, -V: Data> is Data:
  Rejected{error: Error, key: K, value: V}

type Search is Data:
  Search{found: Nat, parent: Nat, left: Bool}

type Fix is Data:
  Fix{node: Nat, more: Bool}

type Ascend is Data:
  Ascend{child: Nat, parent: Nat, done: Bool}

# A direct branch preserves scalar traversal state in native code. Passing
# these records through pick(-T: Type) erases their layout and boxes both arms.
type DeleteFix is Data:
  DF{node: Nat, parent: Nat, more: Bool}

type NavEnd is Data:
  NavBest{id: Nat}
  NavEqual{id: Nat}

type Bound<-K: Data> is Data:
  Unbounded{}
  Inclusive{key: K}
  Exclusive{key: K}

type View<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
  View{map: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, descending: Bool}

type InvalidView<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
  InvalidView{map: TreeMap<K, V, cmp>, error: Error}

type Cursor<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
  Cursor{map: TreeMap<K, V, cmp>, next: Nat, current: Nat,
         lower: Bound<K>, upper: Bound<K>, forward: Bool}

def ntag(~K: Data, n: Node<K>) -> Nat:
  match n:
    case Free{x}:
      0n
    case N{c, l, r, p, k}:
      match c:
        case True{}:
          2n
        case False{}:
          1n

def nleft(~K: Data, n: Node<K>) -> Nat:
  match n:
    case Free{x}:
      x
    case N{c, l, r, p, k}:
      l

def nright(~K: Data, n: Node<K>) -> Nat:
  match n:
    case Free{x}:
      0n
    case N{c, l, r, p, k}:
      r

def nparent(~K: Data, n: Node<K>) -> Nat:
  match n:
    case Free{x}:
      0n
    case N{c, l, r, p, k}:
      p

def nkey(~K: Data, n: Node<K>) -> Maybe<&2, K>:
  match n:
    case Free{x}:
      None{}
    case N{c, l, r, p, k}:
      Some{k}

def mk_node(~K: Data, +t: Nat, +l: Nat, +r: Nat, +p: Nat, k: Maybe<&2, K>) -> Node<K>:
  match t k:
    case 0n _:
      Free{l}
    case 1n+ +c Some{key}:
      N{Nat.is_eq(c, 1n), l, r, p, key}
    case 1n+ +c None{}:
      Free{l}

def ns_nats(+d: Nat) -> Array<Nat>:
  Array.new(Nat, d, 0n)

def ns_nokeys(~K: Data, +d: Nat) -> Array<Maybe<&2, K>>:
  Array.new(Maybe<&2, K>, d, None{})

def ns_length(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Nat:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, used)

# ---- reading a slot ----

def ns_tag_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
  (tags, +x) = q
  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)

def ns_left_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
  (lefts, +x) = q
  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)

def ns_right_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
  (rights, +x) = q
  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)

def ns_parent_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
  (parents, +x) = q
  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)

def ns_key_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, q: Array<Maybe<&2, K>> & Maybe<&2, K>) -> NodeStore<K> & Maybe<&2, K>:
  (keys, x) = q
  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)

def ns_red_tag(red: Bool) -> Nat:
  match red:
    case True{}:
      2n
    case False{}:
      1n

def ns_set_left_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>:
  match q:
    case Tuple{tags, 0n}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
    case Tuple{tags, 1n+c}:
      NS{limit, depth, cap, used, tags, Array.set(Nat, lefts, U32.from_nat(i), v), rights, parents, keys}

def ns_set_right_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>:
  match q:
    case Tuple{tags, 0n}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
    case Tuple{tags, 1n+c}:
      NS{limit, depth, cap, used, tags, lefts, Array.set(Nat, rights, U32.from_nat(i), v), parents, keys}

def ns_set_parent_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>:
  match q:
    case Tuple{tags, 0n}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
    case Tuple{tags, 1n+c}:
      NS{limit, depth, cap, used, tags, lefts, rights, Array.set(Nat, parents, U32.from_nat(i), v), keys}

def pick(-T: Type, b: Bool, yes: T, no: T) -> T:
  match b:
    case True{}:
      yes
    case False{}:
      no

def node_red(~K: Data, n: Node<K>) -> Bool:
  match n:
    case Free{x}:
      False{}
    case N{c, l, r, p, k}:
      c

def node_left(~K: Data, n: Node<K>) -> Nat:
  match n:
    case Free{x}:
      0n
    case N{c, l, r, p, k}:
      l

def node_right(~K: Data, n: Node<K>) -> Nat:
  match n:
    case Free{x}:
      0n
    case N{c, l, r, p, k}:
      r

def node_parent(~K: Data, n: Node<K>) -> Nat:
  match n:
    case Free{x}:
      0n
    case N{c, l, r, p, k}:
      p

def node_key(~K: Data, n: Node<K>) -> Maybe<&2, K>:
  match n:
    case Free{x}:
      None{}
    case N{c, l, r, p, k}:
      Some{k}

def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
  TM{+n, root, lo, hi, free, nodes, payloads} = m
  (TM{n, root, lo, hi, free, nodes, payloads}, n)

def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
  TM{n, +root, lo, hi, free, nodes, payloads} = m
  (TM{n, root, lo, hi, free, nodes, payloads}, root)

def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
  TM{n, root, +lo, hi, free, nodes, payloads} = m
  (TM{n, root, lo, hi, free, nodes, payloads}, lo)

def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
  TM{n, root, lo, +hi, free, nodes, payloads} = m
  (TM{n, root, lo, hi, free, nodes, payloads}, hi)

def read_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Node<K>:
  match r:
    case Tuple{nodes, Done{x}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, x)
    case Tuple{nodes, Fail{e}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, Free{0n})

def write_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp>:
  (nodes, status) = r
  TM{n, root, lo, hi, free, nodes, payloads}

def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +root: Nat) -> TreeMap<K, V, cmp>:
  TM{n, old, lo, hi, free, nodes, payloads} = m
  TM{n, root, lo, hi, free, nodes, payloads}

def probe_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & (Node<K> & Cmp):
  match r:
    case Tuple{m, Free{next}}:
      (m, (Free{next}, EQ{}))
    case Tuple{m, N{c, l, r, p, +key}}:
      (m, (N{c, l, r, p, key}, cmp(k, key)))

def search_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, r: NodeStore<K> & Maybe<&2, K>) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
  match r:
    case Tuple{nodes, None{}}:
      (nodes, (id, None{}))
    case Tuple{nodes, Some{key}}:
      (nodes, (id, Some{cmp(k, key)}))

def search_fin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Search) -> TreeMap<K, V, cmp> & Search:
  (nodes, s) = r
  (TM{n, root, lo, hi, free, nodes, payloads}, s)

def exchange_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  match r:
    case Tuple{payloads, Done{old}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, old)
    case Tuple{payloads, Fail{e}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, None{})

def append_rollback(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  (nodes, dropped) = r
  (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})

def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +free: Nat) -> TreeMap<K, V, cmp>:
  TM{n, root, lo, hi, old, nodes, payloads} = m
  TM{n, root, lo, hi, free, nodes, payloads}

def reuse_slot_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  (m1, old) = pair_result
  (m1, Done{id})

def put_replaced(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  (m, old) = r
  (m, Done{old})

def get_id_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  match r:
    case Tuple{payloads, Done{x}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, x)
    case Tuple{payloads, Fail{e}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, None{})

def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool:
  (m, Search{id, p, left}) = r
  (m, Nat.is_lt(0n, id))

def ascend_choice(x: Nat, p: Nat, q: Nat, found: Bool) -> Ascend:
  match found:
    case True{}:
      Ascend{0n, p, True{}}
    case False{}:
      Ascend{x, q, False{}}

def neighbor_slots_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Nat) -> TreeMap<K, V, cmp> & Nat:
  (nodes, id) = r
  (TM{n, root, lo, hi, free, nodes, payloads}, id)

def move_successor_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +source: Nat, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Nat:
  (m3, old) = pair_result
  (m3, source)

def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
  TM{n, root, lo, hi, free, nodes, payloads} = m
  TM{Nat.sub(n, 1n), root, lo, hi, id, nodes, payloads}

def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lo: Nat, +hi: Nat) -> TreeMap<K, V, cmp>:
  TM{n, root, oldlo, oldhi, free, nodes, payloads} = m
  TM{n, root, lo, hi, free, nodes, payloads}

def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool:
  (m1, +n) = pair_result
  (m1, Nat.is_eq(n, 0n))

def entry_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, k: Maybe<&2, K>, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match k r:
    case Some{key} Tuple{m, Some{v}}:
      (m, Some{Entry{key, v}})
    case _ Tuple{m, value}:
      (m, None{})

def snap_kv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, mk: Maybe<&2, K>, mv: Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match mk mv:
    case Some{key} Some{v}:
      (TM{n, root, lo, hi, free, nodes, payloads}, Some{Entry{key, v}})
    case _ _:
      (TM{n, root, lo, hi, free, nodes, payloads}, None{})

def default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fallback: V, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & V:
  match r:
    case Tuple{m, None{}}:
      (m, fallback)
    case Tuple{m, Some{v}}:
      (m, v)

def ordering_ok(order: Cmp, inclusive: Bool) -> Bool:
  match order:
    case LT{}:
      True{}
    case EQ{}:
      inclusive
    case GT{}:
      False{}

def view_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> Result<&1, &1, InvalidView<K, V, cmp>, View<K, V, cmp>>:
  match valid:
    case True{}:
      Done{View{m, lower, upper, descending}}
    case False{}:
      Fail{InvalidView{m, InvalidBounds{}}}

def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, upper: Bound<K>) -> View<K, V, cmp>:
  View{m, Unbounded{}, upper, False{}}

def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>) -> View<K, V, cmp>:
  View{m, lower, Unbounded{}, False{}}

def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> View<K, V, cmp>:
  View{m, Unbounded{}, Unbounded{}, True{}}

def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
  View{m, lower, upper, descending} = view
  View{m, lower, upper, Bool.not(descending)}

def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> TreeMap<K, V, cmp>:
  View{m, lower, upper, descending} = view
  m

def view_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +descending: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> View<K, V, cmp> & Maybe<&2, V>:
  (m, v) = r
  (View{m, lower, upper, descending}, v)

def view_put_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +descending: Bool, r: TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>) -> View<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  (m, status) = r
  (View{m, lower, upper, descending}, status)

def cursor_started(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Nat) -> Cursor<K, V, cmp>:
  (m, id) = r
  Cursor{m, id, 0n, lower, upper, forward}

def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> TreeMap<K, V, cmp>:
  Cursor{m, next, current, lower, upper, forward} = cursor
  m

def iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> View<K, V, cmp>:
  Cursor{m, next, current, lower, upper, forward} = cursor
  View{m, lower, upper, Bool.not(forward)}

def iterator_yield(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, r: TreeMap<K, V, cmp> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (m, next) = r
  (Cursor{m, next, id, lower, upper, forward}, Some{entry})

def iterator_set_done(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Result<&2, &2, Error, V>:
  match r:
    case Tuple{m, Some{old}}:
      (Cursor{m, next, current, lower, upper, forward}, Done{old})
    case Tuple{m, None{}}:
      (Cursor{m, next, current, lower, upper, forward}, Fail{NoCurrent{}})

def iterator_relocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +forward: Bool, removed: Maybe<&2, V>, r: TreeMap<K, V, cmp> & Search) -> Cursor<K, V, cmp> & Maybe<&2, V>:
  (m, Search{id, p, on_left}) = r
  (Cursor{m, id, 0n, lower, upper, forward}, removed)

def iterator_key_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> Cursor<K, V, cmp> & Maybe<&2, K>:
  match r:
    case Tuple{cursor, None{}}:
      (cursor, None{})
    case Tuple{cursor, Some{Entry{k, v}}}:
      (cursor, Some{k})

def iterator_value_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
  match r:
    case Tuple{cursor, None{}}:
      (cursor, None{})
    case Tuple{cursor, Some{Entry{k, v}}}:
      (cursor, Some{v})

def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool:
  match r:
    case Tuple{m, None{}}:
      (m, False{})
    case Tuple{m, Some{old}}:
      (m, True{})

def view_contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: View<K, V, cmp> & Maybe<&2, V>) -> View<K, V, cmp> & Bool:
  match r:
    case Tuple{view, None{}}:
      (view, False{})
    case Tuple{view, Some{x}}:
      (view, True{})

def view_entry_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, +descending: Bool, entry: Entry<K, V>, +valid: Bool) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match valid:
    case True{}:
      (View{m, lower, upper, descending}, Some{entry})
    case False{}:
      (View{m, lower, upper, descending}, None{})

def ns_empty(~K: Data, +limit: Nat) -> NodeStore<K>:
  NS{limit, 0n, 1n, 0n, ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nokeys(~K, 0n)}

def ns_rk(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, +t: Nat, +l: Nat, +r: Nat, +p: Nat, q: Array<Maybe<&2, K>> & Maybe<&2, K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  (keys, k) = q
  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Done{mk_node(~K, t, l, r, p, k)})

def ns_tag_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
  match ok:
    case True{}:
      ns_tag_fin(~K, limit, depth, cap, used, lefts, rights, parents, keys, Array.get(Nat, tags, U32.from_nat(i)))
    case False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)

def ns_left_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
  match ok:
    case True{}:
      ns_left_fin(~K, limit, depth, cap, used, tags, rights, parents, keys, Array.get(Nat, lefts, U32.from_nat(i)))
    case False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)

def ns_right_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
  match ok:
    case True{}:
      ns_right_fin(~K, limit, depth, cap, used, tags, lefts, parents, keys, Array.get(Nat, rights, U32.from_nat(i)))
    case False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)

def ns_parent_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
  match ok:
    case True{}:
      ns_parent_fin(~K, limit, depth, cap, used, tags, lefts, rights, keys, Array.get(Nat, parents, U32.from_nat(i)))
    case False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)

def ns_key_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Maybe<&2, K>:
  match ok:
    case True{}:
      ns_key_fin(~K, limit, depth, cap, used, tags, lefts, rights, parents, Array.get(Maybe<&2, K>, keys, U32.from_nat(i)))
    case False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, None{})

def ns_set_left_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>:
  match ok:
    case True{}:
      ns_set_left_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
    case False{}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}

def ns_set_right_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>:
  match ok:
    case True{}:
      ns_set_right_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
    case False{}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}

def ns_set_parent_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>:
  match ok:
    case True{}:
      ns_set_parent_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
    case False{}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}

def ns_set_red_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Bool, q: Array<Nat> & Nat) -> NodeStore<K>:
  match q:
    case Tuple{tags, 0n}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
    case Tuple{tags, 1n+c}:
      NS{limit, depth, cap, used, Array.set(Nat, tags, U32.from_nat(i), ns_red_tag(v)), lefts, rights, parents, keys}

def ns_put(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +node: Node<K>) -> NodeStore<K>:
  NS{limit, depth, cap, used, Array.set(Nat, tags, i, ntag(~K, node)), Array.set(Nat, lefts, i, nleft(~K, node)), Array.set(Nat, rights, i, nright(~K, node)), Array.set(Nat, parents, i, nparent(~K, node)), Array.set(Maybe<&2, K>, keys, i, nkey(~K, node))}

def ns_grow_nats(+depth: Nat, a: Array<Nat>) -> Array<Nat>:
  ANode{a, ns_nats(depth)}

def ns_grow_keys(~K: Data, +depth: Nat, a: Array<Maybe<&2, K>>) -> Array<Maybe<&2, K>>:
  ANode{a, ns_nokeys(~K, depth)}

def child(~K: Data, +n: Node<K>, forward: Bool) -> Nat:
  pick(Nat, forward, node_right(~K, n), node_left(~K, n))

# All links reference live slots. Free slots contain no key and no value.

def exchange(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, value: Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  match m id:
    case mm 0n:
      (mm, None{})
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.swap_at(~Maybe<&2, V>, payloads, i, value))

def insert_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +p: Nat, +on_left: Bool) -> TreeMap<K, V, cmp>:
  TM{+n, root, +lo, +hi, free, nodes, payloads} = m
  TM{1n+n, root, pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(on_left, Nat.is_eq(p, lo))), id, lo), pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(on_left), Nat.is_eq(p, hi))), id, hi), free, nodes, payloads}

def get_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  match m id:
    case mm 0n:
      (mm, None{})
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.get_at(~Maybe<&2, V>, payloads, i))

def ascend_step_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Ascend:
  match r:
    case Tuple{m, Free{next}}:
      (m, Ascend{0n, 0n, True{}})
    case Tuple{m, N{c, l, r, q, key}}:
      (m, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))

def ascend_par(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +s: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
  (nodes, +q) = r
  (nodes, ascend_choice(p, p, q, Nat.is_eq(x, s)))

def refresh_ends_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
  (m3, +hi) = pair_result
  set_ends(~K, ~V, ~cmp, m3, lo, hi)

def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Bool:
  is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))

def key_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  (m, node) = r
  (m, node_key(~K, node))

def snap_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, mv: Maybe<&2, V>, r: NodeStore<K> & Maybe<&2, K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (nodes, mk) = r
  snap_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, mk, mv)

def above_lower(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
  match bound:
    case Unbounded{}:
      True{}
    case Inclusive{lo}:
      ordering_ok(cmp(lo, k), True{})
    case Exclusive{lo}:
      ordering_ok(cmp(lo, k), False{})

def below_upper(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
  match bound:
    case Unbounded{}:
      True{}
    case Inclusive{hi}:
      ordering_ok(cmp(k, hi), True{})
    case Exclusive{hi}:
      ordering_ok(cmp(k, hi), False{})

def bounds_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>) -> Bool:
  match lower upper:
    case Unbounded{} _:
      True{}
    case _ Unbounded{}:
      True{}
    case Inclusive{lo} Inclusive{hi}:
      ordering_ok(cmp(lo, hi), True{})
    case Inclusive{lo} Exclusive{hi}:
      ordering_ok(cmp(lo, hi), True{})
    case Exclusive{lo} Inclusive{hi}:
      ordering_ok(cmp(lo, hi), True{})
    case Exclusive{lo} Exclusive{hi}:
      ordering_ok(cmp(lo, hi), True{})

def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
  match forward:
    case True{}:
      first_id(~K, ~V, ~cmp, m)
    case False{}:
      last_id(~K, ~V, ~cmp, m)

def iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))

def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))

def ns_new(~K: Data) -> NodeStore<K>:
  ns_empty(~K, D.max_depth())

def ns_with_limit(~K: Data, +k: Nat) -> NodeStore<K>:
  ns_empty(~K, D.clamp_limit(k, Nat.is_lt(k, D.max_depth())))

def ns_rp(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, +l: Nat, +r: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  (parents, +p) = q
  ns_rk(~K, limit, depth, cap, used, tags, lefts, rights, parents, t, l, r, p, Array.get(Maybe<&2, K>, keys, i))

def ns_tag_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_tag_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))

def ns_left_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))

def ns_right_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))

def ns_parent_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))

def ns_key_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Maybe<&2, K>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_key_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))

# ---- writing one field of a live slot (free slots and ids past the length unchanged) ----

def ns_set_left(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_set_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))

def ns_set_right(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_set_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))

def ns_set_parent(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_set_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))

def ns_set_red_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Bool, ok: Bool) -> NodeStore<K>:
  match ok:
    case True{}:
      ns_set_red_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
    case False{}:
      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}

def ns_set_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +node: Node<K>, ok: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
  match ok:
    case True{}:
      (ns_put(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, U32.from_nat(i), node), Done{Unit{}})
    case False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})

def ns_push_room(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +node: Node<K>, room: Bool, grow: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
  match room grow:
    case True{} _:
      (ns_put(~K, limit, depth, cap, 1n+used, tags, lefts, rights, parents, keys, U32.from_nat(used), node), Done{Unit{}})
    case False{} True{}:
      (ns_put(~K, limit, 1n+depth, Nat.double(cap), 1n+used, ns_grow_nats(depth, tags), ns_grow_nats(depth, lefts), ns_grow_nats(depth, rights), ns_grow_nats(depth, parents), ns_grow_keys(~K, depth, keys), U32.from_nat(used), node), Done{Unit{}})
    case False{} False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.CapacityExceeded{}})

def ns_drop(~K: Data, s: NodeStore<K>, +m: Nat) -> NodeStore<K>:
  NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} = s
  ns_put(~K, limit, depth, cap, m, tags, lefts, rights, parents, keys, U32.from_nat(m), Free{0n})

def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  (m, Search{id, p, on_left}) = r
  get_id(~K, ~V, ~cmp, m, id)

def replace_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +v: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  match r:
    case Tuple{m, Search{0n, p, on_left}}:
      (m, None{})
    case Tuple{m, Search{1n+i, p, on_left}}:
      exchange(~K, ~V, ~cmp, m, 1n+i, Some{v})

def in_range(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, lower: Bound<K>, upper: Bound<K>) -> Bool:
  Bool.and(above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper))

def sub_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lower: Bound<K>, +upper: Bound<K>) -> Result<&1, &1, InvalidView<K, V, cmp>, View<K, V, cmp>>:
  view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, bounds_valid(~K, ~V, ~cmp, lower, upper))

def iterator_set_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>, +v: V) -> Cursor<K, V, cmp> & Result<&2, &2, Error, V>:
  match cursor:
    case Cursor{m, next, 0n, lower, upper, forward}:
      (Cursor{m, next, 0n, lower, upper, forward}, Fail{NoCurrent{}})
    case Cursor{m, next, 1n+ +id, lower, upper, forward}:
      iterator_set_done(~K, ~V, ~cmp, next, 1n+id, lower, upper, forward, exchange(~K, ~V, ~cmp, m, 1n+id, Some{v}))

def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
  iterator(~K, ~V, ~cmp, m)

def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
  iterator(~K, ~V, ~cmp, m)

def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
  iterator(~K, ~V, ~cmp, m)

def replace_if_apply(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +replacement: V, +equal: Bool) -> TreeMap<K, V, cmp> & Bool:
  match equal:
    case False{}:
      (m, False{})
    case True{}:
      changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))

def ns_rr(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, +l: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  (rights, +r) = q
  ns_rp(~K, limit, depth, cap, used, tags, lefts, rights, keys, i, t, l, r, Array.get(Nat, parents, i))

def ns_set_red(~K: Data, s: NodeStore<K>, +i: Nat, +v: Bool) -> NodeStore<K>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_set_red_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))

# ---- writing a slot: the encoding of the node in all five arrays ----

def ns_set(~K: Data, s: NodeStore<K>, +i: Nat, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_set_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, node, Nat.is_lt(i, used))

# ---- appending a slot ----

def ns_push(~K: Data, s: NodeStore<K>, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
  NS{+limit, +depth, +cap, +used, tags, lefts, rights, parents, keys} = s
  ns_push_room(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, node, Nat.is_lt(used, cap), Nat.is_lt(depth, limit))

# ---- dropping slots: the dropped slots get the encoding of Free{0} back ----

def ns_pop_fin(~K: Data, +m: Nat, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  (s, x) = r
  (ns_drop(~K, s, m), x)

def ns_clear_go(~K: Data, k: Nat, s: NodeStore<K>) -> NodeStore<K>:
  match k:
    case 0n:
      s
    case 1n+ +m:
      ns_clear_go(~K, m, ns_drop(~K, s, m))

# O(used): resets the live slots top down and keeps the capacity.
def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> TreeMap<K, V, cmp>:
  TM{0n, 0n, 0n, 0n, 0n, ns_new(~K), D.new_at(~Maybe<&2, V>)}

def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
  match m id:
    case mm 0n:
      mm
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      TM{n, root, lo, hi, free, ns_set_left(~K, nodes, i, v), payloads}

def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
  match m id:
    case mm 0n:
      mm
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      TM{n, root, lo, hi, free, ns_set_right(~K, nodes, i, v), payloads}

def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
  match m id:
    case mm 0n:
      mm
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      TM{n, root, lo, hi, free, ns_set_parent(~K, nodes, i, v), payloads}

def search_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +id: Nat, +k: K) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
  match id:
    case 0n:
      (nodes, (0n, None{}))
    case 1n+ +i:
      search_key(~K, ~V, ~cmp, 1n+i, k, ns_key_at(~K, nodes, i))

def side_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +left: Bool, +i: Nat) -> NodeStore<K> & Nat:
  match left:
    case True{}:
      ns_left_at(~K, nodes, i)
    case False{}:
      ns_right_at(~K, nodes, i)

def ascend_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
  (nodes, +s) = r
  ascend_par(~K, ~V, ~cmp, x, p, s, ns_parent_at(~K, nodes, i))

def snap_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +i: Nat, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r
  snap_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, mv, ns_key_at(~K, nodes, i))

def with_limit(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +limit: Nat) -> TreeMap<K, V, cmp>:
  TM{0n, 0n, 0n, 0n, 0n, ns_with_limit(~K, limit), D.with_limit_at(~Maybe<&2, V>, limit)}

def replace_if_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +id: Nat, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool:
  match r:
    case Tuple{m, None{}}:
      (m, False{})
    case Tuple{m, Some{old}}:
      replace_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))

def iterator_has_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> Cursor<K, V, cmp> & Bool:
  match r:
    case Tuple{m, Free{free}}:
      (Cursor{m, next, current, lower, upper, forward}, False{})
    case Tuple{m, N{c, l, rr, p, key}}:
      (Cursor{m, next, current, lower, upper, forward}, in_range(~K, ~V, ~cmp, key, lower, upper))

def view_entry_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lower: Bound<K>, +upper: Bound<K>, +descending: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match r:
    case Tuple{m, None{}}:
      (View{m, lower, upper, descending}, None{})
    case Tuple{m, Some{Entry{+k, v}}}:
      view_entry_checked(~K, ~V, ~cmp, m, lower, upper, descending, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))

def ns_rl(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  (lefts, +l) = q
  ns_rr(~K, limit, depth, cap, used, tags, lefts, parents, keys, i, t, l, Array.get(Nat, rights, i))

def ns_clear(~K: Data, s: NodeStore<K>) -> NodeStore<K>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_clear_go(~K, used, NS{limit, depth, cap, used, tags, lefts, rights, parents, keys})


def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
  match m id:
    case mm 0n:
      mm
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_set(~K, nodes, i, node))

def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool) -> TreeMap<K, V, cmp>:
  match m id:
    case mm 0n:
      mm
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      TM{n, root, lo, hi, free, ns_set_red(~K, nodes, i, v), payloads}

def attach_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +x: Nat, +on_left: Bool) -> TreeMap<K, V, cmp>:
  match p on_left:
    case 0n _:
      set_root(~K, ~V, ~cmp, m, x)
    case 1n+q True{}:
      set_left(~K, ~V, ~cmp, m, 1n+q, x)
    case 1n+q False{}:
      set_right(~K, ~V, ~cmp, m, 1n+q, x)

def search_down2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, r: NodeStore<K> & Nat) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
  (nodes, +c) = r
  search_probe(~K, ~V, ~cmp, nodes, c, k)

def ascend_tag(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +i: Nat, +forward: Bool, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
  match r:
    case Tuple{nodes, 0n}:
      (nodes, Ascend{0n, 0n, True{}})
    case Tuple{nodes, 1n+c}:
      ascend_side(~K, ~V, ~cmp, x, p, i, side_at(~K, ~V, ~cmp, nodes, forward, i))

def extreme_tag(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Nat:
  match r:
    case Tuple{nodes, 0n}:
      (nodes, 0n)
    case Tuple{nodes, 1n+c}:
      side_at(~K, ~V, ~cmp, nodes, Bool.not(forward), i)

def snap_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match id:
    case 0n:
      (m, None{})
    case 1n+ +i:
      snap_value(~K, ~V, ~cmp, i, get_id(~K, ~V, ~cmp, m, 1n+i))

def replace_if_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool:
  (m, Search{+id, p, on_left}) = r
  replace_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))

def ns_rt(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  (tags, +t) = q
  ns_rl(~K, limit, depth, cap, used, tags, rights, parents, keys, i, t, Array.get(Nat, lefts, i))

def attach(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +x: Nat, +on_left: Bool) -> TreeMap<K, V, cmp>:
  set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)

def search_down(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +id: Nat, +left: Bool, +k: K) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
  match id:
    case 0n:
      (nodes, (0n, None{}))
    case 1n+ +i:
      search_down2(~K, ~V, ~cmp, k, side_at(~K, ~V, ~cmp, nodes, left, i))

def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
  (m1, +r) = pair_result
  set_red(~K, ~V, ~cmp, m1, r, False{})

def reuse_slot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +next: Nat, +p: Nat, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  reuse_slot_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, write(~K, ~V, ~cmp, free_header(~K, ~V, ~cmp, m, next), id, N{True{}, 0n, 0n, p, k}), id, Some{v}))

def ascend_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, nodes: NodeStore<K>) -> NodeStore<K> & Ascend:
  match p:
    case 0n:
      (nodes, Ascend{0n, 0n, True{}})
    case 1n+ +i:
      ascend_tag(~K, ~V, ~cmp, x, 1n+i, i, forward, ns_tag_at(~K, nodes, i))

def extreme_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, nodes: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
  extreme_tag(~K, ~V, ~cmp, forward, i, ns_tag_at(~K, nodes, i))

def set_key_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K, +node: Node<K>) -> TreeMap<K, V, cmp>:
  match node:
    case Free{next}:
      m
    case N{c, l, r, p, old}:
      write(~K, ~V, ~cmp, m, id, N{c, l, r, p, k})

def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
  TM{n, root, lo, hi, +free, nodes, payloads} = m
  release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, Free{free}), id)

def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
  TM{n, root, lo, hi, free, nodes, payloads} = m
  TM{0n, 0n, 0n, 0n, 0n, ns_clear(~K, nodes), D.clear_at(~Maybe<&2, V>, payloads)}

def entry_snapshot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (m, +id) = r
  snap_at(~K, ~V, ~cmp, id, m)

def ns_get_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  match ok:
    case True{}:
      ns_rt(~K, limit, depth, cap, used, lefts, rights, parents, keys, U32.from_nat(i), Array.get(Nat, tags, U32.from_nat(i)))
    case False{}:
      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})

def rotate_left_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, +yn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m3, +pn) = pair_result
  set_parent(~K, ~V, ~cmp, set_left(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, set_parent(~K, ~V, ~cmp, set_right(~K, ~V, ~cmp, m3, x, node_left(~K, yn)), node_left(~K, yn), x), node_parent(~K, xn), node_right(~K, xn), Nat.is_eq(node_left(~K, pn), x)), node_right(~K, xn), x), x, node_right(~K, xn))

def rotate_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, +yn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m3, +pn) = pair_result
  set_parent(~K, ~V, ~cmp, set_right(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, set_parent(~K, ~V, ~cmp, set_left(~K, ~V, ~cmp, m3, x, node_right(~K, yn)), node_right(~K, yn), x), node_parent(~K, xn), node_left(~K, xn), Nat.is_eq(node_left(~K, pn), x)), node_left(~K, xn), x), x, node_left(~K, xn))

def search_fast(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +p: Nat, +on_left: Bool, st: NodeStore<K> & (Nat & Maybe<&2, Cmp>)) -> NodeStore<K> & Search:
  match fuel st:
    case 0n Tuple{nodes, x}:
      (nodes, Search{0n, p, on_left})
    case 1n+f Tuple{nodes, Tuple{id, None{}}}:
      (nodes, Search{0n, p, on_left})
    case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}:
      search_fast(~K, ~V, ~cmp, f, k, id, True{}, search_down(~K, ~V, ~cmp, nodes, id, True{}, k))
    case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}:
      search_fast(~K, ~V, ~cmp, f, k, id, False{}, search_down(~K, ~V, ~cmp, nodes, id, False{}, k))
    case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}:
      (nodes, Search{id, p, on_left})

def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
  black_root_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))


def alloc_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +p: Nat, +k: K, +v: V, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  match r:
    case Tuple{m, Free{next}}:
      reuse_slot(~K, ~V, ~cmp, m, id, next, p, k, v)
    case Tuple{m, N{c, l, r, q, oldk}}:
      (m, Fail{Rejected{CapacityExceeded{}, k, v}})

def ascend_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: NodeStore<K> & Ascend) -> NodeStore<K> & Nat:
  match fuel st:
    case 0n Tuple{nodes, state}:
      (nodes, 0n)
    case 1n+f Tuple{nodes, Ascend{x, p, True{}}}:
      (nodes, p)
    case 1n+f Tuple{nodes, Ascend{+x, +p, False{}}}:
      ascend_slots_loop(~K, ~V, ~cmp, f, forward, ascend_at(~K, ~V, ~cmp, x, p, forward, nodes))

def extreme_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: NodeStore<K> & Nat) -> NodeStore<K> & Nat:
  match fuel st:
    case 0n Tuple{nodes, next}:
      (nodes, id)
    case 1n+f Tuple{nodes, 0n}:
      (nodes, id)
    case 1n+f Tuple{nodes, 1n+ +j}:
      extreme_slots_loop(~K, ~V, ~cmp, f, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))

def set_key_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m1, +node) = pair_result
  set_key_node(~K, ~V, ~cmp, m1, id, k, node)

def nav_fast(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +higher: Bool, +best: Nat, st: NodeStore<K> & (Nat & Maybe<&2, Cmp>)) -> NodeStore<K> & NavEnd:
  match fuel st:
    case 0n Tuple{nodes, x}:
      (nodes, NavBest{best})
    case 1n+f Tuple{nodes, Tuple{id, None{}}}:
      (nodes, NavBest{best})
    case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}:
      nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, id, best), search_down(~K, ~V, ~cmp, nodes, id, True{}, k))
    case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}:
      nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, best, id), search_down(~K, ~V, ~cmp, nodes, id, False{}, k))
    case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}:
      (nodes, NavEqual{id})

def first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))

def last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))

def ns_get(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
  ns_get_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))

# ---- reading one field of a slot (0, the encoding of Free{0}, past the length) ----

def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Search:
  TM{+n, +root, lo, hi, free, nodes, payloads} = m
  search_fin(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, search_fast(~K, ~V, ~cmp, 1n+n, k, 0n, False{}, search_probe(~K, ~V, ~cmp, nodes, root, k)))

def neighbor_slots(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +n: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> NodeStore<K> & Nat:
  match c:
    case 0n:
      ascend_slots_loop(~K, ~V, ~cmp, 1n+n, forward, (nodes, Ascend{id, p, False{}}))
    case 1n+ +j:
      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, Bool.not(forward), 1n+j, extreme_at(~K, ~V, ~cmp, Bool.not(forward), nodes, j))

def extreme_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +n: Nat, +id: Nat, +forward: Bool) -> NodeStore<K> & Nat:
  match id:
    case 0n:
      (nodes, 0n)
    case 1n+ +j:
      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))

def ns_pop_n(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  match used:
    case 0n:
      (NS{limit, depth, cap, 0n, tags, lefts, rights, parents, keys}, Fail{DE.EmptyArray{}})
    case 1n+ +m:
      ns_pop_fin(~K, m, ns_get(~K, NS{limit, depth, cap, 1n+m, tags, lefts, rights, parents, keys}, m))

def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Node<K>:
  match m id:
    case mm 0n:
      (mm, Free{0n})
    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
      read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_get(~K, nodes, i))

def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  get_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))

def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Bool:
  contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))


def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
  TM{+n, root, lo, hi, free, nodes, payloads} = m
  neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, extreme_start(~K, ~V, ~cmp, nodes, n, id, forward))

def neighbor_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:
  (TM{+n, root, lo, hi, free, nodes, payloads}, +node) = r
  neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, id, node_parent(~K, node), forward, child(~K, node, forward)))

def replace(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  replace_found(~K, ~V, ~cmp, v, search(~K, ~V, ~cmp, m, k))

def iter_child(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +id: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, +p: Nat, r: NodeStore<K> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (nodes, +c) = r
  iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, id, p, forward, c)))

def iterator_reseek(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, k: Maybe<&2, K>, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
  match k r:
    case None{} Tuple{m, removed}:
      (Cursor{m, 0n, 0n, lower, upper, forward}, removed)
    case Some{key} Tuple{m, removed}:
      iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, removed, search(~K, ~V, ~cmp, m, key))

def replace_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: TreeMap<K, V, cmp>, +k: K, +expected: V, +replacement: V) -> TreeMap<K, V, cmp> & Bool:
  replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))

def ns_pop(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
  NS{+limit, +depth, +cap, used, tags, lefts, rights, parents, keys} = s
  ns_pop_n(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys)

def rotate_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m2, +yn) = pair_result
  rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))

def rotate_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m2, +yn) = pair_result
  rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))

def probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp> & (Node<K> & Cmp):
  probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))

def ascend_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: TreeMap<K, V, cmp> & Ascend) -> TreeMap<K, V, cmp> & Nat:
  match fuel st:
    case 0n Tuple{m, state}:
      (m, 0n)
    case 1n+f Tuple{m, Ascend{x, p, True{}}}:
      (m, p)
    case 1n+f Tuple{m, Ascend{+x, +p, False{}}}:
      ascend_loop(~K, ~V, ~cmp, f, forward, ascend_step_node(~K, ~V, ~cmp, x, p, forward, read(~K, ~V, ~cmp, m, p)))

def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
  neighbor_node(~K, ~V, ~cmp, id, forward, read(~K, ~V, ~cmp, m, id))

def set_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp>:
  set_key_1(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))

def refresh_ends_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +r: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
  (m2, +lo) = pair_result
  refresh_ends_3(~K, ~V, ~cmp, lo, extreme(~K, ~V, ~cmp, m2, r, True{}))

def key_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  (m, id) = r
  key_finish(~K, ~V, ~cmp, read(~K, ~V, ~cmp, m, id))

def get_or_default(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +fallback: V) -> TreeMap<K, V, cmp> & V:
  default_value(~K, ~V, ~cmp, fallback, get(~K, ~V, ~cmp, m, k))


def view_get_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> View<K, V, cmp> & Maybe<&2, V>:
  match valid:
    case True{}:
      view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k))
    case False{}:
      (View{m, lower, upper, descending}, None{})

def iter_link(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +i: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, r: NodeStore<K> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (nodes, +p) = r
  iter_child(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, 1n+i, lower, upper, forward, entry, p, side_at(~K, ~V, ~cmp, nodes, Bool.not(forward), i))

def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Bool:
  Cursor{m, +next, current, lower, upper, forward} = cursor
  iterator_has_checked(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))

def rotate_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m1, +xn) = pair_result
  rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_right(~K, xn)))

def rotate_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m1, +xn) = pair_result
  rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_left(~K, xn)))

def search_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +id: Nat, +p: Nat, +on_left: Bool, st: TreeMap<K, V, cmp> & (Node<K> & Cmp)) -> TreeMap<K, V, cmp> & Search:
  match fuel st:
    case 0n Tuple{m, node}:
      (m, Search{0n, p, on_left})
    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
      (m, Search{0n, p, on_left})
    case 1n+f Tuple{m, Tuple{N{c, +l, r, p0, key}, LT{}}}:
      search_loop(~K, ~V, ~cmp, f, k, l, id, True{}, probe(~K, ~V, ~cmp, m, l, k))
    case 1n+f Tuple{m, Tuple{N{c, l, +r, p0, key}, GT{}}}:
      search_loop(~K, ~V, ~cmp, f, k, r, id, False{}, probe(~K, ~V, ~cmp, m, r, k))
    case 1n+f Tuple{m, Tuple{N{c, l, r, p0, key}, EQ{}}}:
      (m, Search{id, p, on_left})

def append_values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, +k: K, +v: V, +id: Nat, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  match r:
    case Tuple{payloads, Done{u}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, Done{id})
    case Tuple{payloads, Fail{e}}:
      append_rollback(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, ns_pop(~K, nodes))

def copy_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
  match node:
    case Free{next}:
      m
    case N{c, l, r, p, k}:
      set_key(~K, ~V, ~cmp, m, target, k)

def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
  (m1, +r) = pair_result
  refresh_ends_2(~K, ~V, ~cmp, r, extreme(~K, ~V, ~cmp, m1, r, False{}))

def nav_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +higher: Bool, +inclusive: Bool) -> TreeMap<K, V, cmp> & Nat:
  match inclusive:
    case True{}:
      (m, id)
    case False{}:
      neighbor(~K, ~V, ~cmp, m, id, higher)


def first_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))

def last_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))

def view_get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>:
  View{m, +lower, +upper, descending} = view
  view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))

def iter_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, +valid: Bool) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match valid:
    case True{}:
      iter_link(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, lower, upper, forward, entry, ns_parent_at(~K, nodes, i))
    case False{}:
      (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})

def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
  rotate_left_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))

def rotate_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
  rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))

def append_nodes(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +id: Nat, r: NodeStore<K> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  match r:
    case Tuple{nodes, Done{u}}:
      append_values(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, k, v, id, D.push_at(~Maybe<&2, V>, payloads, Some{v}))
    case Tuple{nodes, Fail{e}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})

def move_successor_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, +source_node: Node<K>, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Nat:
  (m2, value) = pair_result
  move_successor_3(~K, ~V, ~cmp, source, exchange(~K, ~V, ~cmp, copy_key(~K, ~V, ~cmp, m2, target, source_node), target, value))

def refresh_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
  refresh_ends_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))

def nav_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +higher: Bool, +inclusive: Bool, +id: Nat, +best: Nat, st: TreeMap<K, V, cmp> & (Node<K> & Cmp)) -> TreeMap<K, V, cmp> & Nat:
  match fuel st:
    case 0n Tuple{m, node}:
      (m, best)
    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
      (m, best)
    case 1n+f Tuple{m, Tuple{N{c, +l, r, p, key}, LT{}}}:
      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, l, pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, m, l, k))
    case 1n+f Tuple{m, Tuple{N{c, l, +r, p, key}, GT{}}}:
      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, r, pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, m, r, k))
    case 1n+f Tuple{m, Tuple{node, EQ{}}}:
      nav_equal(~K, ~V, ~cmp, m, id, higher, inclusive)

def nav_end(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +higher: Bool, +inclusive: Bool, r: NodeStore<K> & NavEnd) -> TreeMap<K, V, cmp> & Nat:
  match r:
    case Tuple{nodes, NavBest{b}}:
      (TM{n, root, lo, hi, free, nodes, payloads}, b)
    case Tuple{nodes, NavEqual{+id}}:
      nav_equal(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, higher, inclusive)

def iter_kv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, +i: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, mk: Maybe<&2, K>, mv: Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match mk mv:
    case Some{+key} Some{v}:
      iter_valid(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, i, current, lower, upper, forward, Entry{key, v}, in_range(~K, ~V, ~cmp, key, lower, upper))
    case _ _:
      (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})

def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Bool:
  view_contains_value(~K, ~V, ~cmp, view_get(~K, ~V, ~cmp, view, k))

def insert_black_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> TreeMap<K, V, cmp> & Fix:
  match triangle:
    case True{}:
      (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, m, p), z, False{}), g, True{}), g), Fix{0n, False{}})
    case False{}:
      (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})

def insert_black_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> TreeMap<K, V, cmp> & Fix:
  match triangle:
    case True{}:
      (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, m, p), z, False{}), g, True{}), g), Fix{0n, False{}})
    case False{}:
      (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})

def append_count(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +p: Nat, r: NodeStore<K> & Nat) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  (nodes, +used) = r
  append_nodes(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, 1n+used, ns_push(~K, nodes, N{True{}, 0n, 0n, p, k}))

def move_successor_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:
  (m1, +source_node) = pair_result
  move_successor_2(~K, ~V, ~cmp, target, source, source_node, exchange(~K, ~V, ~cmp, m1, source, None{}))

def delete_borrow_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, node_red(~K, pn)), p, False{}), node_right(~K, wn), False{}), p), DF{0n, 0n, False{}})

def delete_borrow_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, node_red(~K, pn)), p, False{}), node_left(~K, wn), False{}), p), DF{0n, 0n, False{}})

def navigate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +higher: Bool, +inclusive: Bool) -> TreeMap<K, V, cmp> & Nat:
  TM{+n, +root, lo, hi, free, nodes, payloads} = m
  nav_end(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, higher, inclusive, nav_fast(~K, ~V, ~cmp, 1n+n, k, higher, 0n, search_probe(~K, ~V, ~cmp, nodes, root, k)))

def iter_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, mv: Maybe<&2, V>, r: NodeStore<K> & Maybe<&2, K>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (nodes, mk) = r
  iter_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, i, current, lower, upper, forward, mk, mv)

def insert_uncle_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: Node<K>) -> TreeMap<K, V, cmp> & Fix:
  match uncle:
    case N{True{}, l, r, gp, k}:
      (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), Fix{g, True{}})
    case _:
      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)

def insert_uncle_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: Node<K>) -> TreeMap<K, V, cmp> & Fix:
  match uncle:
    case N{True{}, l, r, gp, k}:
      (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), Fix{g, True{}})
    case _:
      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)

def append(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V, +p: Nat) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  TM{n, root, lo, hi, free, nodes, payloads} = m
  append_count(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, p, ns_length(~K, nodes))

def move_successor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +target: Nat, +source: Nat) -> TreeMap<K, V, cmp> & Nat:
  move_successor_1(~K, ~V, ~cmp, target, source, read(~K, ~V, ~cmp, m, source))

def delete_borrow_read_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m2, +wn) = pair_result
  delete_borrow_left(~K, ~V, ~cmp, m2, p, node_right(~K, pn), pn, wn)

def delete_borrow_read_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m2, +wn) = pair_result
  delete_borrow_right(~K, ~V, ~cmp, m2, p, node_left(~K, pn), pn, wn)

def lower_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))

def floor_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))

def ceiling_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))

def higher_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))

def lower_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))

def floor_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))

def ceiling_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))

def higher_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, k: K) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))

def range_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, bound: Bound<K>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
  match bound:
    case Unbounded{}:
      range_unbounded(~K, ~V, ~cmp, m, forward)
    case Inclusive{k}:
      navigate(~K, ~V, ~cmp, m, k, forward, True{})
    case Exclusive{k}:
      navigate(~K, ~V, ~cmp, m, k, forward, False{})

def iter_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r
  iter_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, current, lower, upper, forward, mv, ns_key_at(~K, nodes, i))

def insert_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix:
  (m1, +un) = pair_result
  insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, node_right(~K, gn), Nat.is_eq(z, node_right(~K, pn)), un)

def insert_side_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix:
  (m1, +un) = pair_result
  insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, node_left(~K, gn), Nat.is_eq(z, node_left(~K, pn)), un)

def allocate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
  TM{n, root, lo, hi, free, nodes, payloads} = m
  match free:
    case 0n:
      append(~K, ~V, ~cmp, TM{n, root, lo, hi, 0n, nodes, payloads}, k, v, p)
    case 1n+ +f:
      alloc_read(~K, ~V, ~cmp, 1n+f, p, k, v, read(~K, ~V, ~cmp, TM{n, root, lo, hi, 1n+f, nodes, payloads}, 1n+f))

def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:
  (m, source) = r
  move_successor(~K, ~V, ~cmp, m, target, source)

def delete_borrow_read_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m1, +pn) = pair_result
  delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))

def delete_borrow_read_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m1, +pn) = pair_result
  delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))

def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> Cursor<K, V, cmp>:
  View{m, +lower, +upper, +descending} = view
  cursor_started(~K, ~V, ~cmp, lower, upper, Bool.not(descending), range_start(~K, ~V, ~cmp, m, pick(Bound<K>, descending, upper, lower), Bool.not(descending)))

def iter_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  match next:
    case 0n:
      (Cursor{m, 0n, current, lower, upper, forward}, None{})
    case 1n+ +i:
      iter_value(~K, ~V, ~cmp, i, current, lower, upper, forward, get_id(~K, ~V, ~cmp, m, 1n+i))

def view_nav_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, lower: Bound<K>, upper: Bound<K>, +higher: Bool, +inclusive: Bool, +within: Bool) -> TreeMap<K, V, cmp> & Nat:
  match within:
    case True{}:
      navigate(~K, ~V, ~cmp, m, k, higher, inclusive)
    case False{}:
      range_start(~K, ~V, ~cmp, m, pick(Bound<K>, higher, lower, upper), higher)

def view_extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +first: Bool) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  View{m, +lower, +upper, +descending} = view
  +up = pick(Bool, descending, Bool.not(first), first)
  view_entry_result(~K, ~V, ~cmp, lower, upper, descending, entry_snapshot(~K, ~V, ~cmp, range_start(~K, ~V, ~cmp, m, pick(Bound<K>, up, lower, upper), up)))

def insert_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>) -> TreeMap<K, V, cmp> & Fix:
  insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_right(~K, gn)))

def insert_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>) -> TreeMap<K, V, cmp> & Fix:
  insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_left(~K, gn)))

def delete_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:
  match r:
    case Tuple{m, N{c, 1n+l, 1n+r, p, k}}:
      successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, m, 1n+r, False{}))
    case Tuple{m, node}:
      (m, id)


def delete_borrow_read_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
  delete_borrow_read_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

def delete_borrow_read_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
  delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  Cursor{m, +next, current, lower, upper, forward} = cursor
  iter_at(~K, ~V, ~cmp, next, current, lower, upper, forward, m)

def view_nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K, +higher: Bool, +inclusive: Bool) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  View{m, +lower, +upper, +descending} = view
  +up = pick(Bool, descending, Bool.not(higher), higher)
  view_entry_result(~K, ~V, ~cmp, lower, upper, descending, entry_snapshot(~K, ~V, ~cmp, view_nav_start(~K, ~V, ~cmp, m, k, lower, upper, up, inclusive, pick(Bool, up, above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper)))))

def view_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  view_extreme(~K, ~V, ~cmp, view, True{})

def view_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  view_extreme(~K, ~V, ~cmp, view, False{})

def insert_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +g: Nat, +pn: Node<K>, +gn: Node<K>, +on_left: Bool) -> TreeMap<K, V, cmp> & Fix:
  match on_left:
    case True{}:
      insert_side_left(~K, ~V, ~cmp, m, z, p, g, pn, gn)
    case False{}:
      insert_side_right(~K, ~V, ~cmp, m, z, p, g, pn, gn)

def delete_far_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match far_red:
    case True{}:
      delete_borrow_left(~K, ~V, ~cmp, m, p, w, pn, wn)
    case False{}:
      delete_borrow_read_left(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, node_left(~K, wn), False{}), w, True{}), w), p)

def delete_far_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match far_red:
    case True{}:
      delete_borrow_right(~K, ~V, ~cmp, m, p, w, pn, wn)
    case False{}:
      delete_borrow_read_right(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, node_right(~K, wn), False{}), w, True{}), w), p)

def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, K>:
  iterator_key_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))

def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
  iterator_value_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))

def contains_value_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +fuel: Nat, +wanted: V, +found: Bool, st: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> TreeMap<K, V, cmp> & Bool:
  match fuel found st:
    case _ True{} Tuple{cursor, item}:
      (iterator_finish(~K, ~V, ~cmp, cursor), True{})
    case 0n False{} Tuple{cursor, item}:
      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
    case 1n+f False{} Tuple{cursor, None{}}:
      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
    case 1n+f False{} Tuple{cursor, Some{Entry{k, v}}}:
      contains_value_loop(~K, ~V, ~cmp, ~eq, f, wanted, eq(v, wanted), iterator_next(~K, ~V, ~cmp, cursor))

def view_lower_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, False{}, False{})

def view_floor_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, False{}, True{})

def view_ceiling_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, True{}, True{})

def view_higher_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, True{}, False{})

def view_count_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +count: Nat, st: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> View<K, V, cmp> & Nat:
  match fuel st:
    case 0n Tuple{cursor, item}:
      (iterator_view(~K, ~V, ~cmp, cursor), count)
    case 1n+f Tuple{cursor, None{}}:
      (iterator_view(~K, ~V, ~cmp, cursor), count)
    case 1n+f Tuple{cursor, Some{item}}:
      view_count_loop(~K, ~V, ~cmp, f, 1n+count, iterator_next(~K, ~V, ~cmp, cursor))

def view_clear_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Cursor<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (cursor, removed) = r
  iterator_next(~K, ~V, ~cmp, cursor)

def insert_grand_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix:
  (m1, +gn) = pair_result
  insert_side(~K, ~V, ~cmp, m1, z, p, node_parent(~K, pn), pn, gn, Nat.is_eq(p, node_left(~K, gn)))

def delete_children_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +near_red: Bool, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match near_red far_red:
    case False{} False{}:
      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
    case _ _:
      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)

def delete_children_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +pn: Node<K>, +wn: Node<K>, +near_red: Bool, +far_red: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match near_red far_red:
    case False{} False{}:
      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
    case _ _:
      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)

def contains_value_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +wanted: V, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool:
  (m, n) = r
  contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+n, wanted, False{}, iterator_next(~K, ~V, ~cmp, iterator(~K, ~V, ~cmp, m)))

def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Nat:
  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
  view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, View{TM{n, root, lo, hi, free, nodes, payloads}, lower, upper, descending})))

def insert_grand(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +pn: Node<K>) -> TreeMap<K, V, cmp> & Fix:
  insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, node_parent(~K, pn)))

def delete_sibling_left_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, +near_node: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m4, +far_node) = pair_result
  delete_children_left(~K, ~V, ~cmp, m4, p, node_right(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))

def delete_sibling_right_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, +near_node: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m4, +far_node) = pair_result
  delete_children_right(~K, ~V, ~cmp, m4, p, node_left(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))

def contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: TreeMap<K, V, cmp>, +wanted: V) -> TreeMap<K, V, cmp> & Bool:
  contains_value_start(~K, ~V, ~cmp, ~eq, wanted, size(~K, ~V, ~cmp, m))

def insert_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat, +p: Nat, +pn: Node<K>, +is_red: Bool) -> TreeMap<K, V, cmp> & Fix:
  match is_red:
    case False{}:
      (m, Fix{0n, False{}})
    case True{}:
      insert_grand(~K, ~V, ~cmp, m, z, p, pn)

def delete_sibling_left_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m3, +near_node) = pair_result
  delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_right(~K, wn)))

def delete_sibling_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, +wn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m3, +near_node) = pair_result
  delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_left(~K, wn)))

def insert_fix_step_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +zn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix:
  (m2, +pn) = pair_result
  insert_parent(~K, ~V, ~cmp, m2, z, node_parent(~K, zn), pn, node_red(~K, pn))

def delete_sibling_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m2, +wn) = pair_result
  delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_left(~K, wn)))

def delete_sibling_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m2, +wn) = pair_result
  delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_right(~K, wn)))

def insert_fix_step_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Fix:
  (m1, +zn) = pair_result
  insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, node_parent(~K, zn)))

def delete_sibling_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m1, +pn) = pair_result
  delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))

def delete_sibling_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m1, +pn) = pair_result
  delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))

def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat) -> TreeMap<K, V, cmp> & Fix:
  insert_fix_step_1(~K, ~V, ~cmp, z, read(~K, ~V, ~cmp, m, z))

def delete_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
  delete_sibling_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

def delete_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
  delete_sibling_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

def insert_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & Fix) -> TreeMap<K, V, cmp>:
  match fuel st:
    case 0n Tuple{m, f}:
      black_root(~K, ~V, ~cmp, m)
    case 1n+p Tuple{m, Fix{z, False{}}}:
      black_root(~K, ~V, ~cmp, m)
    case 1n+p Tuple{m, Fix{z, True{}}}:
      insert_fix_loop(~K, ~V, ~cmp, p, insert_fix_step(~K, ~V, ~cmp, m, z))

def delete_red_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +red_sibling: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match red_sibling:
    case True{}:
      delete_sibling_left(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, False{}), p, True{}), p), p)
    case False{}:
      delete_sibling_left(~K, ~V, ~cmp, m, p)

def delete_red_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +w: Nat, +red_sibling: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match red_sibling:
    case True{}:
      delete_sibling_right(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, False{}), p, True{}), p), p)
    case False{}:
      delete_sibling_right(~K, ~V, ~cmp, m, p)

def insert_fixed(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
  (m, n) = r
  insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, Fix{id, True{}}))

def delete_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m1, +wn) = pair_result
  delete_red_sibling_left(~K, ~V, ~cmp, m1, p, node_right(~K, pn), node_red(~K, wn))

def delete_side_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m1, +wn) = pair_result
  delete_red_sibling_right(~K, ~V, ~cmp, m1, p, node_left(~K, pn), node_red(~K, wn))

def put_allocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +on_left: Bool, r: TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  match r:
    case Tuple{m, Done{+id}}:
      (insert_fixed(~K, ~V, ~cmp, id, size(~K, ~V, ~cmp, insert_header(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, m, p, id, on_left), id, p, on_left))), Done{None{}})
    case Tuple{m, Fail{e}}:
      (m, Fail{e})

def delete_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +pn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_right(~K, pn)))

def delete_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat, +pn: Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_left(~K, pn)))

def put_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  match r:
    case Tuple{m, Search{0n, +p, +on_left}}:
      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
    case Tuple{m, Search{1n+i, p, on_left}}:
      put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, 1n+i, Some{v}))

def delete_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat, +pn: Node<K>, +on_left: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match on_left:
    case True{}:
      delete_side_left(~K, ~V, ~cmp, m, p, pn)
    case False{}:
      delete_side_right(~K, ~V, ~cmp, m, p, pn)

def put_absent_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  match r:
    case Tuple{m, Search{0n, +p, +on_left}}:
      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
    case Tuple{m, Search{1n+i, p, on_left}}:
      put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, m, 1n+i))

def put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  put_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))

def delete_stop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat, +pn: Node<K>, +stop: Bool) -> TreeMap<K, V, cmp> & DeleteFix:
  match stop:
    case True{}:
      (set_red(~K, ~V, ~cmp, m, x, False{}), DF{0n, 0n, False{}})
    case False{}:
      delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, node_left(~K, pn)))

def put_if_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  put_absent_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))

def delete_fix_step_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +root_node: Nat, +xn: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m3, +pn) = pair_result
  delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), node_red(~K, xn)))

def view_put_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, +v: V, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> View<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  match valid:
    case True{}:
      view_put_finish(~K, ~V, ~cmp, lower, upper, descending, put(~K, ~V, ~cmp, m, k, v))
    case False{}:
      (View{m, lower, upper, descending}, Fail{Rejected{OutOfRange{}, k, v}})

def delete_fix_step_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +root_node: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & DeleteFix:
  (m2, +xn) = pair_result
  delete_fix_step_3(~K, ~V, ~cmp, x, p, root_node, xn, read(~K, ~V, ~cmp, m2, p))

def view_put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K, +v: V) -> View<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>:
  View{m, +lower, +upper, descending} = view
  view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))

def delete_fix_step_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & DeleteFix:
  (m1, +root_node) = pair_result
  delete_fix_step_2(~K, ~V, ~cmp, x, p, root_node, read(~K, ~V, ~cmp, m1, x))

def delete_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
  delete_fix_step_1(~K, ~V, ~cmp, x, p, root_id(~K, ~V, ~cmp, m))

def delete_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & DeleteFix) -> TreeMap<K, V, cmp>:
  match fuel st:
    case 0n Tuple{m, fix}:
      black_root(~K, ~V, ~cmp, m)
    case 1n+f Tuple{m, DF{x, p, False{}}}:
      black_root(~K, ~V, ~cmp, m)
    case 1n+f Tuple{m, DF{x, p, True{}}}:
      delete_fix_loop(~K, ~V, ~cmp, f, delete_fix_step(~K, ~V, ~cmp, m, x, p))

def delete_repair(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat, +p: Nat, +was_red: Bool) -> TreeMap<K, V, cmp>:
  TM{+n, root, lo, hi, free, nodes, payloads} = m
  delete_fix_loop(~K, ~V, ~cmp, 1n+n, (TM{n, root, lo, hi, free, nodes, payloads}, DF{x, p, Bool.not(was_red)}))

def unlink_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +node: Node<K>, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m2, +pn) = pair_result
  delete_repair(~K, ~V, ~cmp, recycle(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, m2, node_parent(~K, node), pick(Nat, Nat.is_lt(0n, node_left(~K, node)), node_left(~K, node), node_right(~K, node)), Nat.is_eq(id, node_left(~K, pn))), id), pick(Nat, Nat.is_lt(0n, node_left(~K, node)), node_left(~K, node), node_right(~K, node)), node_parent(~K, node), node_red(~K, node))

def unlink_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
  (m1, +node) = pair_result
  unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, node_parent(~K, node)))

def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
  unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))

def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
  (m, id) = r
  refresh_ends(~K, ~V, ~cmp, unlink(~K, ~V, ~cmp, m, id))

def remove_present_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  (m1, value) = pair_result
  (unlink_target(~K, ~V, ~cmp, delete_target(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m1, id))), value)

def remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  remove_present_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, m, id, None{}))

def remove_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  match id:
    case 0n:
      (m, None{})
    case 1n+i:
      remove_present(~K, ~V, ~cmp, m, 1n+i)

def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  (m, Search{id, p, on_left}) = r
  remove_id(~K, ~V, ~cmp, m, id)

def remove_entry_id_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (m1, +node) = pair_result
  entry_value(~K, ~V, ~cmp, node_key(~K, node), remove_id(~K, ~V, ~cmp, m1, id))

def iterator_delete_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, pair_result: TreeMap<K, V, cmp> & Node<K>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
  (m1, +node) = pair_result
  iterator_reseek(~K, ~V, ~cmp, node_key(~K, node), lower, upper, forward, remove_id(~K, ~V, ~cmp, m1, current))

def remove_if_apply(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +replacement: V, +equal: Bool) -> TreeMap<K, V, cmp> & Bool:
  match equal:
    case False{}:
      (m, False{})
    case True{}:
      changed_value(~K, ~V, ~cmp, remove_id(~K, ~V, ~cmp, m, id))

def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
  remove_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))

def remove_entry_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  remove_entry_id_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))

def iterator_delete(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +next: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool) -> Cursor<K, V, cmp> & Maybe<&2, V>:
  iterator_delete_1(~K, ~V, ~cmp, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))

def remove_if_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +id: Nat, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool:
  match r:
    case Tuple{m, None{}}:
      (m, False{})
    case Tuple{m, Some{old}}:
      remove_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))

def poll_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  (m, id) = r
  remove_entry_id(~K, ~V, ~cmp, m, id)

def view_remove_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K, lower: Bound<K>, upper: Bound<K>, +descending: Bool, +valid: Bool) -> View<K, V, cmp> & Maybe<&2, V>:
  match valid:
    case True{}:
      view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k))
    case False{}:
      (View{m, lower, upper, descending}, None{})

def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
  Cursor{m, next, current, lower, upper, forward} = cursor
  iterator_delete(~K, ~V, ~cmp, m, next, current, lower, upper, forward)

def remove_if_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +expected: V, +replacement: V, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool:
  (m, Search{+id, p, on_left}) = r
  remove_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))

def poll_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  poll_ready(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))

def poll_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
  poll_ready(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))

def view_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Maybe<&2, V>:
  View{m, +lower, +upper, descending} = view
  view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))

def remove_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: TreeMap<K, V, cmp>, +k: K, +expected: V) -> TreeMap<K, V, cmp> & Bool:
  remove_if_found(~K, ~V, ~cmp, ~eq, expected, expected, search(~K, ~V, ~cmp, m, k))

def view_clear_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> View<K, V, cmp>:
  match fuel st:
    case 0n Tuple{cursor, item}:
      iterator_view(~K, ~V, ~cmp, cursor)
    case 1n+f Tuple{cursor, None{}}:
      iterator_view(~K, ~V, ~cmp, cursor)
    case 1n+f Tuple{cursor, Some{item}}:
      view_clear_loop(~K, ~V, ~cmp, f, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, cursor)))

def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
  view_clear_loop(~K, ~V, ~cmp, 1n+n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, View{TM{n, root, lo, hi, free, nodes, payloads}, lower, upper, descending})))