src/containers/balanced_search_tree.bend source

src/containers/balanced_search_tree.bend on the hub · documented module

# Generated by tools/generators/tree_map.py; edit algorithm definitions there.import Baseimport ./dynamic_array.bend as Dimport ./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}type TreeMap<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:  TM{size: Nat, root: Nat, first: Nat, last: Nat, free: Nat,     nodes: D.DynArray<&2, Node<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 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 pick(-T: Type, b: Bool, yes: T, no: T) -> T:  match b:    case True{}:      yes    case False{}:      nodef node_red(~K: Data, n: Node<K>) -> Bool:  match n:    case Free{x}:      False{}    case N{c, l, r, p, k}:      cdef node_left(~K: Data, n: Node<K>) -> Nat:  match n:    case Free{x}:      0n    case N{c, l, r, p, k}:      ldef node_right(~K: Data, n: Node<K>) -> Nat:  match n:    case Free{x}:      0n    case N{c, l, r, p, k}:      rdef node_parent(~K: Data, n: Node<K>) -> Nat:  match n:    case Free{x}:      0n    case N{c, l, r, p, k}:      pdef 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 new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> TreeMap<K, V, cmp>:  TM{0n, 0n, 0n, 0n, 0n, D.new_at(~Node<K>), D.new_at(~Maybe<&2, V>)}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: D.DynArray<&2, Node<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: D.DynArray<&2, Node<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 exchange_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<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: D.DynArray<&2, Node<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: D.DynArray<&2, Node<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 node_slot_done(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Array<Maybe<&2, Node<K>>> & Maybe<&2, Node<K>>) -> Array<Maybe<&2, Node<K>>> & Node<K>:  match r:    case Tuple{nodes, None{}}:      (nodes, Free{0n})    case Tuple{nodes, Some{node}}:      (nodes, node)def neighbor_slots_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: Array<Maybe<&2, Node<K>>> & Nat) -> TreeMap<K, V, cmp> & Nat:  (nodes, id) = r  (TM{n, root, lo, hi, free, D.DA{limit, depth, cap, used, 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 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, D.clear_at(~Node<K>, nodes), D.clear_at(~Maybe<&2, V>, 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 with_limit(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +limit: Nat) -> TreeMap<K, V, cmp>:  TM{0n, 0n, 0n, 0n, 0n, D.with_limit_at(~Node<K>, limit), D.with_limit_at(~Maybe<&2, V>, limit)}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  mdef 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  mdef 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 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 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, D.get_at(~Node<K>, nodes, i))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, D.set_at(~Node<K>, nodes, i, node))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 append_values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<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, D.pop_at(~Node<K>, nodes))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 node_slot_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +i: Nat, +valid: Bool) -> Array<Maybe<&2, Node<K>>> & Node<K>:  match valid:    case False{}:      (nodes, Free{0n})    case True{}:      node_slot_done(~K, ~V, ~cmp, Array.get(Maybe<&2, Node<K>>, nodes, U32.from_nat(i)))def ascend_slots_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, r: Array<Maybe<&2, Node<K>>> & Node<K>) -> Array<Maybe<&2, Node<K>>> & Ascend:  match r:    case Tuple{nodes, Free{next}}:      (nodes, Ascend{0n, 0n, True{}})    case Tuple{nodes, N{c, l, r, q, key}}:      (nodes, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))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 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 set_left_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:  match node:    case Free{next}:      m    case N{c, l, r, p, k}:      write(~K, ~V, ~cmp, m, id, N{c, v, r, p, k})def set_right_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:  match node:    case Free{next}:      m    case N{c, l, r, p, k}:      write(~K, ~V, ~cmp, m, id, N{c, l, v, p, k})def set_parent_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:  match node:    case Free{next}:      m    case N{c, l, r, p, k}:      write(~K, ~V, ~cmp, m, id, N{c, l, r, v, k})def set_red_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool, +node: Node<K>) -> TreeMap<K, V, cmp>:  match node:    case Free{next}:      m    case N{c, l, r, p, k}:      write(~K, ~V, ~cmp, m, id, N{v, l, r, p, k})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 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: D.DynArray<&2, Node<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 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 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 extreme_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:  (m, node) = r  (m, child(~K, node, forward))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 node_slot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +used: Nat, +id: Nat) -> Array<Maybe<&2, Node<K>>> & Node<K>:  match id:    case 0n:      (nodes, Free{0n})    case 1n+ +i:      node_slot_checked(~K, ~V, ~cmp, nodes, i, Nat.is_lt(i, used))def extreme_slots_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: Array<Maybe<&2, Node<K>>> & Node<K>) -> Array<Maybe<&2, Node<K>>> & Nat:  (nodes, node) = r  (nodes, child(~K, node, forward))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 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 entry_snapshot_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, id: Nat, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:  (m, node) = r  entry_value(~K, ~V, ~cmp, node_key(~K, node), 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 set_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:  (m1, +node) = pair_result  set_left_node(~K, ~V, ~cmp, m1, id, v, node)def set_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:  (m1, +node) = pair_result  set_right_node(~K, ~V, ~cmp, m1, id, v, node)def set_parent_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:  (m1, +node) = pair_result  set_parent_node(~K, ~V, ~cmp, m1, id, v, node)def set_red_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Bool, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:  (m1, +node) = pair_result  set_red_node(~K, ~V, ~cmp, m1, id, v, node)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_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: D.DynArray<&2, Node<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, D.push_at(~Node<K>, nodes, N{True{}, 0n, 0n, p, k}))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 extreme_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:  match fuel st:    case 0n Tuple{m, next}:      (m, id)    case 1n+p Tuple{m, 0n}:      (m, id)    case 1n+p Tuple{m, 1n+ +j}:      extreme_loop(~K, ~V, ~cmp, p, forward, 1n+j, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, m, 1n+j)))def ascend_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +used: Nat, +forward: Bool, st: Array<Maybe<&2, Node<K>>> & Ascend) -> Array<Maybe<&2, Node<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, used, forward, ascend_slots_step(~K, ~V, ~cmp, x, p, forward, node_slot(~K, ~V, ~cmp, nodes, used, p)))def extreme_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +used: Nat, +forward: Bool, +id: Nat, st: Array<Maybe<&2, Node<K>>> & Nat) -> Array<Maybe<&2, Node<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, used, forward, 1n+j, extreme_slots_probe(~K, ~V, ~cmp, forward, node_slot(~K, ~V, ~cmp, nodes, used, 1n+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 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 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  entry_snapshot_value(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))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 set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:  set_left_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:  set_right_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:  set_parent_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool) -> TreeMap<K, V, cmp>:  set_red_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))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_loop(~K, ~V, ~cmp, 1n+n, k, root, 0n, False{}, probe(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, root, k))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, D.length(Node<K>, nodes))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  extreme_loop(~K, ~V, ~cmp, 1n+n, forward, id, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id)))def neighbor_slots(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +n: Nat, +used: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> Array<Maybe<&2, Node<K>>> & Nat:  match c:    case 0n:      ascend_slots_loop(~K, ~V, ~cmp, 1n+n, used, forward, (nodes, Ascend{id, p, False{}}))    case 1n+ +j:      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, used, Bool.not(forward), 1n+j, extreme_slots_probe(~K, ~V, ~cmp, Bool.not(forward), node_slot(~K, ~V, ~cmp, nodes, used, 1n+j)))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 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 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 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 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 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 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 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 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, D.DA{limit, depth, cap, +used, nodes}, payloads}, +node) = r  neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, limit, depth, cap, used, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, used, id, node_parent(~K, node), forward, child(~K, node, forward)))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_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 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 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 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 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 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 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_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 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 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 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 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_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 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 iterator_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: 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{}:      iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor(~K, ~V, ~cmp, m, id, forward))    case False{}:      (Cursor{m, 0n, current, lower, upper, forward}, None{})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 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 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 iterator_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:  match r:    case Tuple{m, None{}}:      (Cursor{m, 0n, current, lower, upper, forward}, None{})    case Tuple{m, Some{Entry{+k, v}}}:      iterator_checked(~K, ~V, ~cmp, m, id, current, lower, upper, forward, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))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 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 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 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_loop(~K, ~V, ~cmp, 1n+n, k, higher, inclusive, root, 0n, probe(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, root, k))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  iterator_read(~K, ~V, ~cmp, next, current, lower, upper, forward, entry_snapshot(~K, ~V, ~cmp, (m, next)))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 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 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 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_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_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 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 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 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_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_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 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 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 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 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_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 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_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 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_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 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 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 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 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})))