~/bend-docscommunity

proofs/containers/balanced_search_tree/mirror.bend source

proofs/containers/balanced_search_tree/mirror.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../../spec/lib/common.bend as SCimport ../../../src/containers/balanced_search_tree.bend as Mimport ./state.bend as STimport ./prim.bend as PR# The TreeMap's mirror over its shadow (generated by# tools/generators/tm_mirror.py from src/containers/balanced_search_tree.bend;# the array-level primitives come from tools/generators/tm_hand).# Every mirror function is its implementation function with the map# replaced by the shadow, whose node and payload arrays are item lists.type MCursor<-K: Data, -V: Data> is Data:  MC{sh: ST.Sh<K, V>, next: Nat, current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, forward: Bool}type MView<-K: Data, -V: Data> is Data:  MV{sh: ST.Sh<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, descending: Bool}type MInvalid<-K: Data, -V: Data> is Data:  MI{sh: ST.Sh<K, V>, error: M.Error}# ---- realizations ----def rc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: MCursor<K, V>) -> M.Cursor<K, V, cmp>:  match c:    case MC{s, next, current, lower, upper, forward}:      M.Cursor{ST.real(~K, ~V, ~cmp, s), next, current, lower, upper, forward}def rv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MView<K, V>) -> M.View<K, V, cmp>:  match w:    case MV{s, lower, upper, descending}:      M.View{ST.real(~K, ~V, ~cmp, s), lower, upper, descending}def ri(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MInvalid<K, V>) -> M.InvalidView<K, V, cmp>:  match w:    case MI{s, e}:      M.InvalidView{ST.real(~K, ~V, ~cmp, s), e}def rr(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Result<&1, &1, MInvalid<K, V>, MView<K, V>>) -> Result<&1, &1, M.InvalidView<K, V, cmp>, M.View<K, V, cmp>>:  match r:    case Done{w}:      Done{rv(~K, ~V, ~cmp, w)}    case Fail{w}:      Fail{ri(~K, ~V, ~cmp, w)}def rp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Type, p: ST.Sh<K, V> & X) -> M.TreeMap<K, V, cmp> & X:  match p:    case Tuple{s, x}:      (ST.real(~K, ~V, ~cmp, s), x)def rcp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Type, p: MCursor<K, V> & X) -> M.Cursor<K, V, cmp> & X:  match p:    case Tuple{c, x}:      (rc(~K, ~V, ~cmp, c), x)def rvp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Type, p: MView<K, V> & X) -> M.View<K, V, cmp> & X:  match p:    case Tuple{w, x}:      (rv(~K, ~V, ~cmp, w), x)# ---- the arrays' layout ----def dg(-K: Data, -V: Data, s: ST.Sh<K, V>) -> Bool:  match s:    case ST.SH{n, root, lo, hi, free, +l, +d, +nl, +pl, t, fl}:      Bool.and(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)), Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)))))def dgc(-K: Data, -V: Data, c: MCursor<K, V>) -> Bool:  match c:    case MC{s, next, current, lower, upper, forward}:      dg(K, V, s)def dgv(-K: Data, -V: Data, w: MView<K, V>) -> Bool:  match w:    case MV{s, lower, upper, descending}:      dg(K, V, s)def dgi(-K: Data, -V: Data, w: MInvalid<K, V>) -> Bool:  match w:    case MI{s, e}:      dg(K, V, s)def dgr(-K: Data, -V: Data, r: Result<&1, &1, MInvalid<K, V>, MView<K, V>>) -> Bool:  match r:    case Done{w}:      dgv(K, V, w)    case Fail{w}:      dgi(K, V, w)def dgp(-K: Data, -V: Data, -X: Type, p: ST.Sh<K, V> & X) -> Bool:  match p:    case Tuple{s, x}:      dg(K, V, s)def dgcp(-K: Data, -V: Data, -X: Type, p: MCursor<K, V> & X) -> Bool:  match p:    case Tuple{c, x}:      dgc(K, V, c)def dgvp(-K: Data, -V: Data, -X: Type, p: MView<K, V> & X) -> Bool:  match p:    case Tuple{w, x}:      dgv(K, V, w)# ---- field access ----def nl_of(-K: Data, -V: Data, s: ST.Sh<K, V>) -> List<&2, M.Node<K>>:  match s:    case ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}:      nldef pl_of(-K: Data, -V: Data, s: ST.Sh<K, V>) -> List<&2, Maybe<&2, V>>:  match s:    case ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}:      pl# ---- the array-level primitives ----def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> ST.Sh<K, V>:  ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & M.Node<K>:  match m:    case ST.SH{n, root, lo, hi, free, l, d, +nl, pl, t, fl}:      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, ST.nd(K, nl, id))def get_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & Maybe<&2, V>:  match m:    case ST.SH{n, root, lo, hi, free, l, d, nl, +pl, t, fl}:      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, ST.pv(V, pl, id))def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:  match m:    case ST.SH{n, root, lo, hi, free, l, d, +nl, pl, t, fl}:      ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, id, node), pl, t, fl}# ---- field writes (hand-written: the implementation writes one field array) ----def set_left_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:  match node:    case M.Free{px2}:      m    case M.N{px3, px4, px5, px6, px7}:      write(~K, ~V, ~cmp, m, id, M.N{px3, v, px5, px6, px7})def set_right_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:  match node:    case M.Free{px2}:      m    case M.N{px3, px4, px5, px6, px7}:      write(~K, ~V, ~cmp, m, id, M.N{px3, px4, v, px6, px7})def set_parent_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:  match node:    case M.Free{px2}:      m    case M.N{px3, px4, px5, px6, px7}:      write(~K, ~V, ~cmp, m, id, M.N{px3, px4, px5, v, px7})def set_red_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Bool, +node: M.Node<K>) -> ST.Sh<K, V>:  match node:    case M.Free{px2}:      m    case M.N{px3, px4, px5, px6, px7}:      write(~K, ~V, ~cmp, m, id, M.N{v, px4, px5, px6, px7})def set_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m1, +node) = pair_result  set_red_node(~K, ~V, ~cmp, m1, id, v, node)def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat) -> ST.Sh<K, V>:  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: ST.Sh<K, V>, +id: Nat, +v: Nat) -> ST.Sh<K, V>:  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: ST.Sh<K, V>, +id: Nat, +v: Nat) -> ST.Sh<K, V>:  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: ST.Sh<K, V>, +id: Nat, +v: Bool) -> ST.Sh<K, V>:  set_red_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))def exchange(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +value: Maybe<&2, V>) -> ST.Sh<K, V> & Maybe<&2, V>:  match m:    case ST.SH{n, root, lo, hi, free, l, d, nl, +pl, t, fl}:      (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, id, value), t, fl}, ST.pv(V, pl, id))def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V>:  match m:    case ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}:      ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, t, fl}def app_room(~K: Data, ~V: Data, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +k: K, +v: V, +p: Nat, +room: Bool, +grow: Bool) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:  match room grow:    case True{} _:      (ST.SH{n, root, lo, hi, free, l, d, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, p, k}), SC.snoc(Maybe<&2, V>, pl, Some{v}), t, fl}, Done{1n+SC.length(M.Node<K>, nl)})    case False{} True{}:      (ST.SH{n, root, lo, hi, free, l, 1n+d, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, p, k}), SC.snoc(Maybe<&2, V>, pl, Some{v}), t, fl}, Done{1n+SC.length(M.Node<K>, nl)})    case False{} False{}:      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})def append(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V, +p: Nat) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:      app_room(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, k, v, p, Nat.is_lt(SC.length(M.Node<K>, nl), SC.pow2(d)), Nat.is_lt(d, l))# the neighbour walks over the node listdef asc_step(-K: Data, +x: Nat, +p: Nat, +forward: Bool, node: M.Node<K>) -> M.Ascend:  match node:    case M.Free{next}:      M.Ascend{0n, 0n, True{}}    case M.N{c, +l, +r, +q, key}:      M.ascend_choice(p, p, q, Nat.is_eq(x, M.pick(Nat, forward, l, r)))def asc_loop(-K: Data, +fuel: Nat, +nl: List<&2, M.Node<K>>, +forward: Bool, st: M.Ascend) -> Nat:  match fuel st:    case 0n _:      0n    case 1n+f M.Ascend{x, p, True{}}:      p    case 1n+f M.Ascend{+x, +p, False{}}:      asc_loop(K, f, nl, forward, asc_step(K, x, p, forward, ST.nd(K, nl, p)))def ext_loop(~K: Data, +fuel: Nat, +nl: List<&2, M.Node<K>>, +forward: Bool, +id: Nat, +next: Nat) -> Nat:  match fuel next:    case 0n _:      id    case 1n+f 0n:      id    case 1n+f 1n+ +j:      ext_loop(~K, f, nl, forward, 1n+j, M.child(~K, ST.nd(K, nl, 1n+j), forward))def nbs(~K: Data, +nl: List<&2, M.Node<K>>, +n: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> Nat:  match c:    case 0n:      asc_loop(K, 1n+n, nl, forward, M.Ascend{id, p, False{}})    case 1n+ +j:      ext_loop(~K, 1n+n, nl, Bool.not(forward), 1n+j, M.child(~K, ST.nd(K, nl, 1n+j), Bool.not(forward)))def neighbor_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Nat:  match r:    case Tuple{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}, +node}:      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, nbs(~K, nl, n, id, M.node_parent(~K, node), forward, M.child(~K, node, forward)))# ---- generated mirrors ----def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, n)def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, root)def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, lo)def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, hi)def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +root: Nat) -> ST.Sh<K, V>:  match m:    case ST.SH{+n, +old, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}def probe_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & (M.Node<K> & Cmp):  match r:    case Tuple{px2, M.Free{px4}}:      (px2, (M.Free{px4}, EQ{}))    case Tuple{px2, M.N{px5, px6, px7, px8, +px9}}:      (px2, (M.N{px5, px6, px7, px8, px9}, cmp(k, px9)))def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +free: Nat) -> ST.Sh<K, V>:  match m:    case ST.SH{+n, +root, +lo, +hi, +old, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}def reuse_slot_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:  (m1, old) = pair_result  (m1, Done{id})def put_replaced(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:  (m, old) = r  (m, Done{old})def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Bool:  (m, M.Search{id, p, left}) = r  (m, Nat.is_lt(0n, id))def move_successor_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +source: Nat, pair_result: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Nat:  (m3, old) = pair_result  (m3, source)def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V>:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      ST.SH{Nat.sub(n, 1n), root, lo, hi, id, l_0, d_0, nl_0, pl_0, t_0, fl_0}def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +lo: Nat, +hi: Nat) -> ST.Sh<K, V>:  match m:    case ST.SH{+n, +root, +oldlo, +oldhi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & 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: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:  match k r:    case Some{px3} Tuple{px4, Some{px6}}:      (px4, Some{M.Entry{px3, px6}})    case None{} Tuple{px7, None{}}:      (px7, None{})    case None{} Tuple{px7, Some{px9}}:      (px7, None{})    case Some{px3} Tuple{px4, None{}}:      (px4, None{})def default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fallback: V, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & V:  match r:    case Tuple{px2, None{}}:      (px2, fallback)    case Tuple{px2, Some{px4}}:      (px2, px4)def view_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> Result<&1, &1, MInvalid<K, V>, MView<K, V>>:  match valid:    case True{}:      Done{MV{m, lower, upper, descending}}    case False{}:      Fail{MI{m, M.InvalidBounds{}}}def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, upper: M.Bound<K>) -> MView<K, V>:  MV{m, M.Unbounded{}, upper, False{}}def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, lower: M.Bound<K>) -> MView<K, V>:  MV{m, lower, M.Unbounded{}, False{}}def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MView<K, V>:  MV{m, M.Unbounded{}, M.Unbounded{}, True{}}def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V>:  MV{m, lower, upper, descending} = view  MV{m, lower, upper, Bool.not(descending)}def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> ST.Sh<K, V>:  MV{m, lower, upper, descending} = view  mdef view_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, r: ST.Sh<K, V> & Maybe<&2, V>) -> MView<K, V> & Maybe<&2, V>:  (m, v) = r  (MV{m, lower, upper, descending}, v)def view_put_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, r: ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>) -> MView<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:  (m, status) = r  (MV{m, lower, upper, descending}, status)def cursor_started(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & Nat) -> MCursor<K, V>:  (m, id) = r  MC{m, id, 0n, lower, upper, forward}def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> ST.Sh<K, V>:  MC{m, next, current, lower, upper, forward} = cursor  mdef iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MView<K, V>:  MC{m, next, current, lower, upper, forward} = cursor  MV{m, lower, upper, Bool.not(forward)}def iterator_yield(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, entry: M.Entry<K, V>, r: ST.Sh<K, V> & Nat) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:  (m, next) = r  (MC{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: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & Maybe<&2, V>) -> MCursor<K, V> & Result<&2, &2, M.Error, V>:  match r:    case Tuple{px2, Some{px4}}:      (MC{px2, next, current, lower, upper, forward}, Done{px4})    case Tuple{px2, None{}}:      (MC{px2, next, current, lower, upper, forward}, Fail{M.NoCurrent{}})def iterator_relocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, removed: Maybe<&2, V>, r: ST.Sh<K, V> & M.Search) -> MCursor<K, V> & Maybe<&2, V>:  (m, M.Search{id, p, on_left}) = r  (MC{m, id, 0n, lower, upper, forward}, removed)def iterator_key_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MCursor<K, V> & Maybe<&2, K>:  match r:    case Tuple{px2, None{}}:      (px2, None{})    case Tuple{px2, Some{M.Entry{px5, px6}}}:      (px2, Some{px5})def iterator_value_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MCursor<K, V> & Maybe<&2, V>:  match r:    case Tuple{px2, None{}}:      (px2, None{})    case Tuple{px2, Some{M.Entry{px5, px6}}}:      (px2, Some{px6})def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Bool:  match r:    case Tuple{px2, None{}}:      (px2, False{})    case Tuple{px2, Some{px4}}:      (px2, True{})def view_contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MView<K, V> & Maybe<&2, V>) -> MView<K, V> & Bool:  match r:    case Tuple{px2, None{}}:      (px2, False{})    case Tuple{px2, Some{px4}}:      (px2, True{})def view_entry_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, entry: M.Entry<K, V>, +valid: Bool) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:  match valid:    case True{}:      (MV{m, lower, upper, descending}, Some{entry})    case False{}:      (MV{m, lower, upper, descending}, None{})def insert_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +p: Nat, +on_left: Bool) -> ST.Sh<K, V>:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      ST.SH{1n+n, root, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(on_left, Nat.is_eq(p, lo))), id, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(on_left), Nat.is_eq(p, hi))), id, hi), free, l_0, d_0, nl_0, pl_0, t_0, fl_0}def ascend_step_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Ascend:  match r:    case Tuple{px2, M.Free{px4}}:      (px2, M.Ascend{0n, 0n, True{}})    case Tuple{px2, M.N{px5, px6, px7, px8, px9}}:      (px2, M.ascend_choice(p, p, px8, Nat.is_eq(x, M.pick(Nat, forward, px6, px7))))def refresh_ends_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: Nat, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:  (m3, +hi) = pair_result  set_ends(~K, ~V, ~cmp, m3, lo, hi)def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Bool:  is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))def key_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Maybe<&2, K>:  (m, node) = r  (m, M.node_key(~K, node))def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +forward: Bool) -> ST.Sh<K, V> & 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: ST.Sh<K, V>) -> MCursor<K, V>:  cursor_started(~K, ~V, ~cmp, M.Unbounded{}, M.Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:  cursor_started(~K, ~V, ~cmp, M.Unbounded{}, M.Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Maybe<&2, V>:  (m, 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: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Maybe<&2, V>:  match r:    case Tuple{px2, M.Search{0n, px5, px6}}:      (px2, None{})    case Tuple{px2, M.Search{1n+px7, px5, px6}}:      exchange(~K, ~V, ~cmp, px2, 1n+px7, Some{v})def sub_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +lower: M.Bound<K>, +upper: M.Bound<K>) -> Result<&1, &1, MInvalid<K, V>, MView<K, V>>:  view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, M.bounds_valid(~K, ~V, ~cmp, lower, upper))def iterator_set_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>, +v: V) -> MCursor<K, V> & Result<&2, &2, M.Error, V>:  match cursor:    case MC{px2, px3, 0n, px5, px6, px7}:      (MC{px2, px3, 0n, px5, px6, px7}, Fail{M.NoCurrent{}})    case MC{px2, px3, 1n+ +px8, px5, px6, px7}:      iterator_set_done(~K, ~V, ~cmp, px3, 1n+px8, px5, px6, px7, exchange(~K, ~V, ~cmp, px2, 1n+px8, Some{v}))def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:  iterator(~K, ~V, ~cmp, m)def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:  iterator(~K, ~V, ~cmp, m)def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:  iterator(~K, ~V, ~cmp, m)def replace_if_apply(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +replacement: V, +equal: Bool) -> ST.Sh<K, V> & Bool:  match equal:    case False{}:      (m, False{})    case True{}:      changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))def replace_if_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +id: Nat, +expected: V, +replacement: V, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Bool:  match r:    case Tuple{px2, None{}}:      (px2, False{})    case Tuple{px2, Some{px4}}:      replace_if_apply(~K, ~V, ~cmp, px2, id, replacement, eq(px4, expected))def iterator_has_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, +lower: M.Bound<K>, +upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> MCursor<K, V> & Bool:  match r:    case Tuple{px2, M.Free{px4}}:      (MC{px2, next, current, lower, upper, forward}, False{})    case Tuple{px2, M.N{px5, px6, px7, px8, px9}}:      (MC{px2, next, current, lower, upper, forward}, M.in_range(~K, ~V, ~cmp, px9, lower, upper))def view_entry_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lower: M.Bound<K>, +upper: M.Bound<K>, +descending: Bool, r: ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:  match r:    case Tuple{px2, None{}}:      (MV{px2, lower, upper, descending}, None{})    case Tuple{px2, Some{M.Entry{+px5, px6}}}:      view_entry_checked(~K, ~V, ~cmp, px2, lower, upper, descending, M.Entry{px5, px6}, M.in_range(~K, ~V, ~cmp, px5, lower, upper))def attach_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +x: Nat, +on_left: Bool) -> ST.Sh<K, V>:  match p on_left:    case 0n True{}:      set_root(~K, ~V, ~cmp, m, x)    case 0n False{}:      set_root(~K, ~V, ~cmp, m, x)    case 1n+px3 True{}:      set_left(~K, ~V, ~cmp, m, 1n+px3, x)    case 1n+px3 False{}:      set_right(~K, ~V, ~cmp, m, 1n+px3, x)def replace_if_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +expected: V, +replacement: V, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Bool:  (m, 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 attach(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +x: Nat, +on_left: Bool) -> ST.Sh<K, V>:  set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:  (m1, +r) = pair_result  set_red(~K, ~V, ~cmp, m1, r, False{})def reuse_slot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +next: Nat, +p: Nat, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.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, M.N{True{}, 0n, 0n, p, k}), id, Some{v}))def set_key_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +k: K, +node: M.Node<K>) -> ST.Sh<K, V>:  match node:    case M.Free{px2}:      m    case M.N{px3, px4, px5, px6, px7}:      write(~K, ~V, ~cmp, m, id, M.N{px3, px4, px5, px6, k})def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V>:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, id, M.Free{free}), id)# the mirror of entry_snapshot reads the whole node (the implementation reads# the key and the value; sim/entry_snapshot.part)def entry_snapshot_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, id: Nat, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:  (m, node) = r  entry_value(~K, ~V, ~cmp, M.node_key(~K, node), get_id(~K, ~V, ~cmp, m, id))def entry_snapshot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:  (m, +id) = r  entry_snapshot_value(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))def rotate_left_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, +yn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (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, M.node_left(~K, yn)), M.node_left(~K, yn), x), M.node_parent(~K, xn), M.node_right(~K, xn), Nat.is_eq(M.node_left(~K, pn), x)), M.node_right(~K, xn), x), x, M.node_right(~K, xn))def rotate_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, +yn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (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, M.node_right(~K, yn)), M.node_right(~K, yn), x), M.node_parent(~K, xn), M.node_left(~K, xn), Nat.is_eq(M.node_left(~K, pn), x)), M.node_left(~K, xn), x), x, M.node_left(~K, xn))def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V>:  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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:  match r:    case Tuple{px2, M.Free{px4}}:      reuse_slot(~K, ~V, ~cmp, px2, id, px4, p, k, v)    case Tuple{px2, M.N{px5, px6, px7, px8, px9}}:      (px2, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})def set_key_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m1, +node) = pair_result  set_key_node(~K, ~V, ~cmp, m1, id, k, node)def first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:  entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))def probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +k: K) -> ST.Sh<K, V> & (M.Node<K> & Cmp):  probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))def search_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +id: Nat, +p: Nat, +on_left: Bool, st: ST.Sh<K, V> & (M.Node<K> & Cmp)) -> ST.Sh<K, V> & M.Search:  match fuel st:    case 0n Tuple{px4, Tuple{M.Free{px8}, LT{}}}:      (px4, M.Search{0n, p, on_left})    case 0n Tuple{px4, Tuple{M.Free{px8}, EQ{}}}:      (px4, M.Search{0n, p, on_left})    case 0n Tuple{px4, Tuple{M.Free{px8}, GT{}}}:      (px4, M.Search{0n, p, on_left})    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, LT{}}}:      (px4, M.Search{0n, p, on_left})    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, EQ{}}}:      (px4, M.Search{0n, p, on_left})    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, GT{}}}:      (px4, M.Search{0n, p, on_left})    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, LT{}}}:      (px14, M.Search{0n, p, on_left})    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, EQ{}}}:      (px14, M.Search{0n, p, on_left})    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, GT{}}}:      (px14, M.Search{0n, p, on_left})    case 1n+px3 Tuple{px14, Tuple{M.N{px19, +px20, px21, px22, px23}, LT{}}}:      search_loop(~K, ~V, ~cmp, px3, k, px20, id, True{}, probe(~K, ~V, ~cmp, px14, px20, k))    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, +px21, px22, px23}, GT{}}}:      search_loop(~K, ~V, ~cmp, px3, k, px21, id, False{}, probe(~K, ~V, ~cmp, px14, px21, k))    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, px21, px22, px23}, EQ{}}}:      (px14, M.Search{id, p, on_left})# the mirror of search (the implementation reads two fields per level; sim/search.part)def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & M.Search:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      search_loop(~K, ~V, ~cmp, 1n+n, k, root, 0n, False{}, probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, root, k))def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Bool:  contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))# the mirror of extreme reads whole nodes (the implementation reads a tag and# one child per level; sim/extreme.part)def extreme_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Nat:  (m, node) = r  (m, M.child(~K, node, forward))def extreme_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Nat:  match fuel st:    case 0n Tuple{px4, 0n}:      (px4, id)    case 0n Tuple{px4, 1n+px6}:      (px4, id)    case 1n+px3 Tuple{px7, 0n}:      (px7, id)    case 1n+px3 Tuple{px7, 1n+ +px9}:      extreme_loop(~K, ~V, ~cmp, px3, forward, 1n+px9, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, px7, 1n+px9)))def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +forward: Bool) -> ST.Sh<K, V> & Nat:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      extreme_loop(~K, ~V, ~cmp, 1n+n, forward, id, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, id)))def replace(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V) -> ST.Sh<K, V> & 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: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & Maybe<&2, V>) -> MCursor<K, V> & Maybe<&2, V>:  match k r:    case None{} Tuple{px4, px5}:      (MC{px4, 0n, 0n, lower, upper, forward}, px5)    case Some{px3} Tuple{px6, px7}:      iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, px7, search(~K, ~V, ~cmp, px6, px3))def replace_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: ST.Sh<K, V>, +k: K, +expected: V, +replacement: V) -> ST.Sh<K, V> & Bool:  replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))def rotate_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m2, +yn) = pair_result  rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, M.node_parent(~K, xn)))def rotate_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m2, +yn) = pair_result  rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, M.node_parent(~K, xn)))def ascend_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: ST.Sh<K, V> & M.Ascend) -> ST.Sh<K, V> & Nat:  match fuel st:    case 0n Tuple{px4, px5}:      (px4, 0n)    case 1n+px3 Tuple{px6, M.Ascend{px8, px9, True{}}}:      (px6, px9)    case 1n+px3 Tuple{px6, M.Ascend{+px8, +px9, False{}}}:      ascend_loop(~K, ~V, ~cmp, px3, forward, ascend_step_node(~K, ~V, ~cmp, px8, px9, forward, read(~K, ~V, ~cmp, px6, px9)))def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +forward: Bool) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +id: Nat, +k: K) -> ST.Sh<K, V>:  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: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:  (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: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +k: K, +fallback: V) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +k: K, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> MView<K, V> & Maybe<&2, V>:  match valid:    case True{}:      view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k))    case False{}:      (MV{m, lower, upper, descending}, None{})def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Bool:  MC{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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m1, +xn) = pair_result  rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, M.node_right(~K, xn)))def rotate_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m1, +xn) = pair_result  rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, M.node_left(~K, xn)))def copy_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +target: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:  match node:    case M.Free{px2}:      m    case M.N{px3, px4, px5, px6, px7}:      set_key(~K, ~V, ~cmp, m, target, px7)def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:  (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: ST.Sh<K, V>, +id: Nat, +higher: Bool, +inclusive: Bool) -> ST.Sh<K, V> & 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: ST.Sh<K, V>) -> ST.Sh<K, V> & 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: ST.Sh<K, V>) -> ST.Sh<K, V> & 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: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, V>:  MV{m, +lower, +upper, descending} = view  view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, M.in_range(~K, ~V, ~cmp, k, lower, upper))def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat) -> ST.Sh<K, V>:  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: ST.Sh<K, V>, +x: Nat) -> ST.Sh<K, V>:  rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))def move_successor_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, +source_node: M.Node<K>, pair_result: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & 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: ST.Sh<K, V>) -> ST.Sh<K, V>:  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: ST.Sh<K, V> & (M.Node<K> & Cmp)) -> ST.Sh<K, V> & Nat:  match fuel st:    case 0n Tuple{px4, Tuple{M.Free{px8}, LT{}}}:      (px4, best)    case 0n Tuple{px4, Tuple{M.Free{px8}, EQ{}}}:      (px4, best)    case 0n Tuple{px4, Tuple{M.Free{px8}, GT{}}}:      (px4, best)    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, LT{}}}:      (px4, best)    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, EQ{}}}:      (px4, best)    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, GT{}}}:      (px4, best)    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, LT{}}}:      (px14, best)    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, EQ{}}}:      (px14, best)    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, GT{}}}:      (px14, best)    case 1n+px3 Tuple{px14, Tuple{M.N{px19, +px20, px21, px22, px23}, LT{}}}:      nav_loop(~K, ~V, ~cmp, px3, k, higher, inclusive, px20, M.pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, px14, px20, k))    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, +px21, px22, px23}, GT{}}}:      nav_loop(~K, ~V, ~cmp, px3, k, higher, inclusive, px21, M.pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, px14, px21, k))    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, px21, px22, px23}, EQ{}}}:      nav_equal(~K, ~V, ~cmp, px14, id, higher, inclusive)def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & 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: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> ST.Sh<K, V> & M.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), M.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), M.Fix{0n, False{}})def insert_black_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> ST.Sh<K, V> & M.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), M.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), M.Fix{0n, False{}})def move_successor_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, M.node_red(~K, pn)), p, False{}), M.node_right(~K, wn), False{}), p), M.DF{0n, 0n, False{}})def delete_borrow_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, M.node_red(~K, pn)), p, False{}), M.node_left(~K, wn), False{}), p), M.DF{0n, 0n, False{}})# the mirror of navigate (the implementation reads two fields per level; sim/navigate.part)def navigate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +higher: Bool, +inclusive: Bool) -> ST.Sh<K, V> & Nat:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      nav_loop(~K, ~V, ~cmp, 1n+n, k, higher, inclusive, root, 0n, probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, root, k))def insert_uncle_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: M.Node<K>) -> ST.Sh<K, V> & M.Fix:  match uncle:    case M.N{True{}, px4, px5, px6, px7}:      (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), M.Fix{g, True{}})    case M.Free{px2}:      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)    case M.N{False{}, px4, px5, px6, px7}:      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)def insert_uncle_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: M.Node<K>) -> ST.Sh<K, V> & M.Fix:  match uncle:    case M.N{True{}, px4, px5, px6, px7}:      (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), M.Fix{g, True{}})    case M.Free{px2}:      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)    case M.N{False{}, px4, px5, px6, px7}:      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)def move_successor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +target: Nat, +source: Nat) -> ST.Sh<K, V> & 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: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m2, +wn) = pair_result  delete_borrow_left(~K, ~V, ~cmp, m2, p, M.node_right(~K, pn), pn, wn)def delete_borrow_read_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m2, +wn) = pair_result  delete_borrow_right(~K, ~V, ~cmp, m2, p, M.node_left(~K, pn), pn, wn)def lower_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>, bound: M.Bound<K>, +forward: Bool) -> ST.Sh<K, V> & Nat:  match bound:    case M.Unbounded{}:      range_unbounded(~K, ~V, ~cmp, m, forward)    case M.Inclusive{px2}:      navigate(~K, ~V, ~cmp, m, px2, forward, True{})    case M.Exclusive{px3}:      navigate(~K, ~V, ~cmp, m, px3, forward, False{})def insert_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:  (m1, +un) = pair_result  insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, M.node_right(~K, gn), Nat.is_eq(z, M.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: M.Node<K>, +gn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:  (m1, +un) = pair_result  insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, M.node_left(~K, gn), Nat.is_eq(z, M.node_left(~K, pn)), un)def allocate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      match free:        case 0n:          append(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, 0n, l_0, d_0, nl_0, pl_0, t_0, fl_0}, k, v, p)        case 1n+ +px2:          alloc_read(~K, ~V, ~cmp, 1n+px2, p, k, v, read(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, 1n+px2, l_0, d_0, nl_0, pl_0, t_0, fl_0}, 1n+px2))def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & 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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m1, +pn) = pair_result  delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_right(~K, pn)))def delete_borrow_read_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m1, +pn) = pair_result  delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_left(~K, pn)))def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MCursor<K, V>:  MV{m, +lower, +upper, +descending} = view  cursor_started(~K, ~V, ~cmp, lower, upper, Bool.not(descending), range_start(~K, ~V, ~cmp, m, M.pick(M.Bound<K>, descending, upper, lower), Bool.not(descending)))def view_nav_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, lower: M.Bound<K>, upper: M.Bound<K>, +higher: Bool, +inclusive: Bool, +within: Bool) -> ST.Sh<K, V> & Nat:  match within:    case True{}:      navigate(~K, ~V, ~cmp, m, k, higher, inclusive)    case False{}:      range_start(~K, ~V, ~cmp, m, M.pick(M.Bound<K>, higher, lower, upper), higher)def view_extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +first: Bool) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:  MV{m, +lower, +upper, +descending} = view  +up = M.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, M.pick(M.Bound<K>, up, lower, upper), up)))def insert_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>) -> ST.Sh<K, V> & M.Fix:  insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, M.node_right(~K, gn)))def insert_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>) -> ST.Sh<K, V> & M.Fix:  insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, M.node_left(~K, gn)))def delete_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Nat:  match r:    case Tuple{px2, M.N{px5, 1n+px10, 1n+px11, px8, px9}}:      successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, px2, 1n+px11, False{}))    case Tuple{px2, M.Free{px4}}:      (px2, id)    case Tuple{px2, M.N{px5, 0n, 0n, px8, px9}}:      (px2, id)    case Tuple{px2, M.N{px5, 0n, 1n+px12, px8, px9}}:      (px2, id)    case Tuple{px2, M.N{px5, 1n+px10, 0n, px8, px9}}:      (px2, id)def delete_borrow_read_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.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: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.DeleteFix:  delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))# the mirror of iterator_next reads the whole node (the implementation reads# four fields; sim/iterator_next.part)def iterator_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, +node: M.Node<K>, entry: M.Entry<K, V>, +valid: Bool) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:  match valid:    case True{}:      iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor_node(~K, ~V, ~cmp, id, forward, (m, node)))    case False{}:      (MC{m, 0n, current, lower, upper, forward}, None{})def iterator_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +current: Nat, +lower: M.Bound<K>, +upper: M.Bound<K>, +forward: Bool, +node: M.Node<K>, r: ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:  match r:    case Tuple{px2, None{}}:      (MC{px2, 0n, current, lower, upper, forward}, None{})    case Tuple{px2, Some{M.Entry{+px5, px6}}}:      iterator_checked(~K, ~V, ~cmp, px2, id, current, lower, upper, forward, node, M.Entry{px5, px6}, M.in_range(~K, ~V, ~cmp, px5, lower, upper))def iterator_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:  (m, +node) = r  iterator_read(~K, ~V, ~cmp, id, current, lower, upper, forward, node, entry_value(~K, ~V, ~cmp, M.node_key(~K, node), get_id(~K, ~V, ~cmp, m, id)))def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:  MC{m, +next, current, lower, upper, forward} = cursor  iterator_node(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))def view_nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K, +higher: Bool, +inclusive: Bool) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:  MV{m, +lower, +upper, +descending} = view  +up = M.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, M.pick(Bool, up, M.above_lower(~K, ~V, ~cmp, k, lower), M.below_upper(~K, ~V, ~cmp, k, upper)))))def view_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:  view_extreme(~K, ~V, ~cmp, view, True{})def view_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:  view_extreme(~K, ~V, ~cmp, view, False{})def insert_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>, +on_left: Bool) -> ST.Sh<K, V> & M.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: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +far_red: Bool) -> ST.Sh<K, V> & M.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, M.node_left(~K, wn), False{}), w, True{}), w), p)def delete_far_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +far_red: Bool) -> ST.Sh<K, V> & M.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, M.node_right(~K, wn), False{}), w, True{}), w), p)def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & 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: MCursor<K, V>) -> MCursor<K, V> & 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: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> ST.Sh<K, V> & Bool:  match fuel found st:    case 0n True{} Tuple{px4, None{}}:      (iterator_finish(~K, ~V, ~cmp, px4), True{})    case 0n True{} Tuple{px4, Some{px7}}:      (iterator_finish(~K, ~V, ~cmp, px4), True{})    case 1n+px6 True{} Tuple{px4, None{}}:      (iterator_finish(~K, ~V, ~cmp, px4), True{})    case 1n+px6 True{} Tuple{px4, Some{px7}}:      (iterator_finish(~K, ~V, ~cmp, px4), True{})    case 0n False{} Tuple{px9, None{}}:      (iterator_finish(~K, ~V, ~cmp, px9), False{})    case 0n False{} Tuple{px9, Some{px11}}:      (iterator_finish(~K, ~V, ~cmp, px9), False{})    case 1n+px8 False{} Tuple{px12, None{}}:      (iterator_finish(~K, ~V, ~cmp, px12), False{})    case 1n+px8 False{} Tuple{px12, Some{M.Entry{px15, px16}}}:      contains_value_loop(~K, ~V, ~cmp, ~eq, px8, wanted, eq(px16, wanted), iterator_next(~K, ~V, ~cmp, px12))def view_lower_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.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: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.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: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.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: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.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: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MView<K, V> & Nat:  match fuel st:    case 0n Tuple{px4, None{}}:      (iterator_view(~K, ~V, ~cmp, px4), count)    case 0n Tuple{px4, Some{px6}}:      (iterator_view(~K, ~V, ~cmp, px4), count)    case 1n+px3 Tuple{px7, None{}}:      (iterator_view(~K, ~V, ~cmp, px7), count)    case 1n+px3 Tuple{px7, Some{px9}}:      view_count_loop(~K, ~V, ~cmp, px3, 1n+count, iterator_next(~K, ~V, ~cmp, px7))def view_clear_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MCursor<K, V> & Maybe<&2, V>) -> MCursor<K, V> & Maybe<&2, M.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: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:  (m1, +gn) = pair_result  insert_side(~K, ~V, ~cmp, m1, z, p, M.node_parent(~K, pn), pn, gn, Nat.is_eq(p, M.node_left(~K, gn)))def delete_children_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_red: Bool, +far_red: Bool) -> ST.Sh<K, V> & M.DeleteFix:  match near_red far_red:    case False{} False{}:      (set_red(~K, ~V, ~cmp, m, w, True{}), M.DF{p, M.node_parent(~K, pn), True{}})    case True{} True{}:      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)    case True{} False{}:      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)    case False{} True{}:      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: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_red: Bool, +far_red: Bool) -> ST.Sh<K, V> & M.DeleteFix:  match near_red far_red:    case False{} False{}:      (set_red(~K, ~V, ~cmp, m, w, True{}), M.DF{p, M.node_parent(~K, pn), True{}})    case True{} True{}:      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)    case True{} False{}:      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)    case False{} True{}:      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: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & 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: MView<K, V>) -> MView<K, V> & Nat:  match view:    case MV{ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}, lower, upper, descending}:      view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, MV{ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, lower, upper, descending})))def insert_grand(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +pn: M.Node<K>) -> ST.Sh<K, V> & M.Fix:  insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, M.node_parent(~K, pn)))def delete_sibling_left_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_node: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m4, +far_node) = pair_result  delete_children_left(~K, ~V, ~cmp, m4, p, M.node_right(~K, pn), pn, wn, M.node_red(~K, near_node), M.node_red(~K, far_node))def delete_sibling_right_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_node: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m4, +far_node) = pair_result  delete_children_right(~K, ~V, ~cmp, m4, p, M.node_left(~K, pn), pn, wn, M.node_red(~K, near_node), M.node_red(~K, far_node))def contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: ST.Sh<K, V>, +wanted: V) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +z: Nat, +p: Nat, +pn: M.Node<K>, +is_red: Bool) -> ST.Sh<K, V> & M.Fix:  match is_red:    case False{}:      (m, 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: M.Node<K>, +wn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m3, +near_node) = pair_result  delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, M.node_right(~K, wn)))def delete_sibling_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, +wn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m3, +near_node) = pair_result  delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, M.node_left(~K, wn)))def insert_fix_step_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +zn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:  (m2, +pn) = pair_result  insert_parent(~K, ~V, ~cmp, m2, z, M.node_parent(~K, zn), pn, M.node_red(~K, pn))def delete_sibling_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m2, +wn) = pair_result  delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, M.node_left(~K, wn)))def delete_sibling_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m2, +wn) = pair_result  delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, M.node_right(~K, wn)))def insert_fix_step_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:  (m1, +zn) = pair_result  insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, M.node_parent(~K, zn)))def delete_sibling_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m1, +pn) = pair_result  delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_right(~K, pn)))def delete_sibling_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m1, +pn) = pair_result  delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_left(~K, pn)))def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat) -> ST.Sh<K, V> & M.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: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.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: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.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: ST.Sh<K, V> & M.Fix) -> ST.Sh<K, V>:  match fuel st:    case 0n Tuple{px4, px5}:      black_root(~K, ~V, ~cmp, px4)    case 1n+px3 Tuple{px6, M.Fix{px8, False{}}}:      black_root(~K, ~V, ~cmp, px6)    case 1n+px3 Tuple{px6, M.Fix{px8, True{}}}:      insert_fix_loop(~K, ~V, ~cmp, px3, insert_fix_step(~K, ~V, ~cmp, px6, px8))def delete_red_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +red_sibling: Bool) -> ST.Sh<K, V> & M.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: ST.Sh<K, V>, +p: Nat, +w: Nat, +red_sibling: Bool) -> ST.Sh<K, V> & M.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: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:  (m, n) = r  insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, M.Fix{id, True{}}))def delete_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m1, +wn) = pair_result  delete_red_sibling_left(~K, ~V, ~cmp, m1, p, M.node_right(~K, pn), M.node_red(~K, wn))def delete_side_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m1, +wn) = pair_result  delete_red_sibling_right(~K, ~V, ~cmp, m1, p, M.node_left(~K, pn), M.node_red(~K, wn))def put_allocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +on_left: Bool, r: ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:  match r:    case Tuple{px2, Done{+px4}}:      (insert_fixed(~K, ~V, ~cmp, px4, size(~K, ~V, ~cmp, insert_header(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, px2, p, px4, on_left), px4, p, on_left))), Done{None{}})    case Tuple{px2, Fail{px5}}:      (px2, Fail{px5})def delete_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +pn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, M.node_right(~K, pn)))def delete_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +pn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, M.node_left(~K, pn)))def put_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:  match r:    case Tuple{px2, M.Search{0n, +px5, +px6}}:      put_allocated(~K, ~V, ~cmp, px5, px6, allocate(~K, ~V, ~cmp, px2, px5, k, v))    case Tuple{px2, M.Search{1n+px7, px5, px6}}:      put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, px2, 1n+px7, Some{v}))def delete_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat, +p: Nat, +pn: M.Node<K>, +on_left: Bool) -> ST.Sh<K, V> & M.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: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:  match r:    case Tuple{px2, M.Search{0n, +px5, +px6}}:      put_allocated(~K, ~V, ~cmp, px5, px6, allocate(~K, ~V, ~cmp, px2, px5, k, v))    case Tuple{px2, M.Search{1n+px7, px5, px6}}:      put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, px2, 1n+px7))def put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.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: ST.Sh<K, V>, +x: Nat, +p: Nat, +pn: M.Node<K>, +stop: Bool) -> ST.Sh<K, V> & M.DeleteFix:  match stop:    case True{}:      (set_red(~K, ~V, ~cmp, m, x, False{}), M.DF{0n, 0n, False{}})    case False{}:      delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, M.node_left(~K, pn)))def put_if_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.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: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:  (m3, +pn) = pair_result  delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), M.node_red(~K, xn)))def view_put_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> MView<K, V> & Result<&2, &2, M.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{}:      (MV{m, lower, upper, descending}, Fail{M.Rejected{M.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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.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: MView<K, V>, +k: K, +v: V) -> MView<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:  MV{m, +lower, +upper, descending} = view  view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, M.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: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & M.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: ST.Sh<K, V>, +x: Nat, +p: Nat) -> ST.Sh<K, V> & M.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: ST.Sh<K, V> & M.DeleteFix) -> ST.Sh<K, V>:  match fuel st:    case 0n Tuple{px4, px5}:      black_root(~K, ~V, ~cmp, px4)    case 1n+px3 Tuple{px6, M.DF{px8, px9, False{}}}:      black_root(~K, ~V, ~cmp, px6)    case 1n+px3 Tuple{px6, M.DF{px8, px9, True{}}}:      delete_fix_loop(~K, ~V, ~cmp, px3, delete_fix_step(~K, ~V, ~cmp, px6, px8, px9))def delete_repair(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat, +p: Nat, +was_red: Bool) -> ST.Sh<K, V>:  match m:    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:      delete_fix_loop(~K, ~V, ~cmp, 1n+n, (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, M.DF{x, p, Bool.not(was_red)}))def unlink_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +node: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m2, +pn) = pair_result  delete_repair(~K, ~V, ~cmp, recycle(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, m2, M.node_parent(~K, node), M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, node)), M.node_left(~K, node), M.node_right(~K, node)), Nat.is_eq(id, M.node_left(~K, pn))), id), M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, node)), M.node_left(~K, node), M.node_right(~K, node)), M.node_parent(~K, node), M.node_red(~K, node))def unlink_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:  (m1, +node) = pair_result  unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, M.node_parent(~K, node)))def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V>:  unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:  (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: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & Maybe<&2, V>:  match id:    case 0n:      (m, None{})    case 1n+px2:      remove_present(~K, ~V, ~cmp, m, 1n+px2)def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Maybe<&2, V>:  (m, 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: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:  (m1, +node) = pair_result  entry_value(~K, ~V, ~cmp, M.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: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, pair_result: ST.Sh<K, V> & M.Node<K>) -> MCursor<K, V> & Maybe<&2, V>:  (m1, +node) = pair_result  iterator_reseek(~K, ~V, ~cmp, M.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: ST.Sh<K, V>, +id: Nat, +replacement: V, +equal: Bool) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & 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: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>, +next: Nat, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool) -> MCursor<K, V> & 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: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Bool:  match r:    case Tuple{px2, None{}}:      (px2, False{})    case Tuple{px2, Some{px4}}:      remove_if_apply(~K, ~V, ~cmp, px2, id, replacement, eq(px4, expected))def poll_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>, +k: K, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> MView<K, V> & Maybe<&2, V>:  match valid:    case True{}:      view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k))    case False{}:      (MV{m, lower, upper, descending}, None{})def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Maybe<&2, V>:  MC{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: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Bool:  (m, 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: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.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: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.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: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, V>:  MV{m, +lower, +upper, descending} = view  view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, M.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: ST.Sh<K, V>, +k: K, +expected: V) -> ST.Sh<K, V> & 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: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MView<K, V>:  match fuel st:    case 0n Tuple{px4, None{}}:      iterator_view(~K, ~V, ~cmp, px4)    case 0n Tuple{px4, Some{px6}}:      iterator_view(~K, ~V, ~cmp, px4)    case 1n+px3 Tuple{px7, None{}}:      iterator_view(~K, ~V, ~cmp, px7)    case 1n+px3 Tuple{px7, Some{px9}}:      view_clear_loop(~K, ~V, ~cmp, px3, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, px7)))def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V>:  match view:    case MV{ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}, lower, upper, descending}:      view_clear_loop(~K, ~V, ~cmp, 1n+n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, MV{ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, lower, upper, descending})))