1	# Generated by tools/generators/tree_map.py; edit algorithm definitions there.
2	import Base
3	import ./dynamic_array.bend as D
4	import ./types/dynamic_array.bend as DE
5	
6	# Indexed CLRS red-black map. Keys and payloads are Data for this version.
7	# Comparator is a type index: changing comparator requires rebuilding a map.
8	# Node links are slot indices plus one; zero is the black NIL sentinel.
9	type Node<-K: Data> is Data:
10	  Free{next: Nat}
11	  N{red: Bool, left: Nat, right: Nat, parent: Nat, key: K}
12	
13	# Node storage: one array per node field instead of one array of Node
14	# records. Reading a record out of an array hands back a shared copy that the
15	# runtime reference-counts and takes apart field by field; a field read out of
16	# its own array is a plain word. The store has the shape of a dynamic array
17	# of nodes: slots [0, used) are live, the capacity is 2^depth <= 2^limit, and
18	# it grows by doubling. A slot holds the encoding of its node by ntag (0 free,
19	# 1 black, 2 red), nleft (the free-list link of a free slot), nright, nparent
20	# and nkey (None when free); every other slot holds the encoding of Free{0},
21	# so each array is exactly its field of the node list, padded.
22	type NodeStore<-K: Data> is Type:
23	  NS{limit: Nat, depth: Nat, cap: Nat, used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>}
24	
25	type TreeMap<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
26	  TM{size: Nat, root: Nat, first: Nat, last: Nat, free: Nat,
27	     nodes: NodeStore<K>, payloads: D.DynArray<&2, Maybe<&2, V>>}
28	
29	type Entry<-K: Data, -V: Data> is Data:
30	  Entry{key: K, value: V}
31	
32	type Error is Data:
33	  CapacityExceeded{}
34	  OutOfRange{}
35	  NoCurrent{}
36	  InvalidBounds{}
37	
38	type Rejected<-K: Data, -V: Data> is Data:
39	  Rejected{error: Error, key: K, value: V}
40	
41	type Search is Data:
42	  Search{found: Nat, parent: Nat, left: Bool}
43	
44	type Fix is Data:
45	  Fix{node: Nat, more: Bool}
46	
47	type Ascend is Data:
48	  Ascend{child: Nat, parent: Nat, done: Bool}
49	
50	# A direct branch preserves scalar traversal state in native code. Passing
51	# these records through pick(-T: Type) erases their layout and boxes both arms.
52	type DeleteFix is Data:
53	  DF{node: Nat, parent: Nat, more: Bool}
54	
55	type NavEnd is Data:
56	  NavBest{id: Nat}
57	  NavEqual{id: Nat}
58	
59	type Bound<-K: Data> is Data:
60	  Unbounded{}
61	  Inclusive{key: K}
62	  Exclusive{key: K}
63	
64	type View<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
65	  View{map: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, descending: Bool}
66	
67	type InvalidView<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
68	  InvalidView{map: TreeMap<K, V, cmp>, error: Error}
69	
70	type Cursor<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
71	  Cursor{map: TreeMap<K, V, cmp>, next: Nat, current: Nat,
72	         lower: Bound<K>, upper: Bound<K>, forward: Bool}
73	
74	def ntag(~K: Data, n: Node<K>) -> Nat:
75	  match n:
76	    case Free{x}:
77	      0n
78	    case N{c, l, r, p, k}:
79	      match c:
80	        case True{}:
81	          2n
82	        case False{}:
83	          1n
84	
85	def nleft(~K: Data, n: Node<K>) -> Nat:
86	  match n:
87	    case Free{x}:
88	      x
89	    case N{c, l, r, p, k}:
90	      l
91	
92	def nright(~K: Data, n: Node<K>) -> Nat:
93	  match n:
94	    case Free{x}:
95	      0n
96	    case N{c, l, r, p, k}:
97	      r
98	
99	def nparent(~K: Data, n: Node<K>) -> Nat:
100	  match n:
101	    case Free{x}:
102	      0n
103	    case N{c, l, r, p, k}:
104	      p
105	
106	def nkey(~K: Data, n: Node<K>) -> Maybe<&2, K>:
107	  match n:
108	    case Free{x}:
109	      None{}
110	    case N{c, l, r, p, k}:
111	      Some{k}
112	
113	def mk_node(~K: Data, +t: Nat, +l: Nat, +r: Nat, +p: Nat, k: Maybe<&2, K>) -> Node<K>:
114	  match t k:
115	    case 0n _:
116	      Free{l}
117	    case 1n+ +c Some{key}:
118	      N{Nat.is_eq(c, 1n), l, r, p, key}
119	    case 1n+ +c None{}:
120	      Free{l}
121	
122	def ns_nats(+d: Nat) -> Array<Nat>:
123	  Array.new(Nat, d, 0n)
124	
125	def ns_nokeys(~K: Data, +d: Nat) -> Array<Maybe<&2, K>>:
126	  Array.new(Maybe<&2, K>, d, None{})
127	
128	def ns_length(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Nat:
129	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
130	  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, used)
131	
132	# ---- reading a slot ----
133	
134	def ns_tag_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
135	  (tags, +x) = q
136	  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
137	
138	def ns_left_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
139	  (lefts, +x) = q
140	  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
141	
142	def ns_right_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
143	  (rights, +x) = q
144	  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
145	
146	def ns_parent_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, keys: Array<Maybe<&2, K>>, q: Array<Nat> & Nat) -> NodeStore<K> & Nat:
147	  (parents, +x) = q
148	  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
149	
150	def ns_key_fin(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, q: Array<Maybe<&2, K>> & Maybe<&2, K>) -> NodeStore<K> & Maybe<&2, K>:
151	  (keys, x) = q
152	  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, x)
153	
154	def ns_red_tag(red: Bool) -> Nat:
155	  match red:
156	    case True{}:
157	      2n
158	    case False{}:
159	      1n
160	
161	def ns_set_left_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>:
162	  match q:
163	    case Tuple{tags, 0n}:
164	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
165	    case Tuple{tags, 1n+c}:
166	      NS{limit, depth, cap, used, tags, Array.set(Nat, lefts, U32.from_nat(i), v), rights, parents, keys}
167	
168	def ns_set_right_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>:
169	  match q:
170	    case Tuple{tags, 0n}:
171	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
172	    case Tuple{tags, 1n+c}:
173	      NS{limit, depth, cap, used, tags, lefts, Array.set(Nat, rights, U32.from_nat(i), v), parents, keys}
174	
175	def ns_set_parent_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, q: Array<Nat> & Nat) -> NodeStore<K>:
176	  match q:
177	    case Tuple{tags, 0n}:
178	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
179	    case Tuple{tags, 1n+c}:
180	      NS{limit, depth, cap, used, tags, lefts, rights, Array.set(Nat, parents, U32.from_nat(i), v), keys}
181	
182	def pick(-T: Type, b: Bool, yes: T, no: T) -> T:
183	  match b:
184	    case True{}:
185	      yes
186	    case False{}:
187	      no
188	
189	def node_red(~K: Data, n: Node<K>) -> Bool:
190	  match n:
191	    case Free{x}:
192	      False{}
193	    case N{c, l, r, p, k}:
194	      c
195	
196	def node_left(~K: Data, n: Node<K>) -> Nat:
197	  match n:
198	    case Free{x}:
199	      0n
200	    case N{c, l, r, p, k}:
201	      l
202	
203	def node_right(~K: Data, n: Node<K>) -> Nat:
204	  match n:
205	    case Free{x}:
206	      0n
207	    case N{c, l, r, p, k}:
208	      r
209	
210	def node_parent(~K: Data, n: Node<K>) -> Nat:
211	  match n:
212	    case Free{x}:
213	      0n
214	    case N{c, l, r, p, k}:
215	      p
216	
217	def node_key(~K: Data, n: Node<K>) -> Maybe<&2, K>:
218	  match n:
219	    case Free{x}:
220	      None{}
221	    case N{c, l, r, p, k}:
222	      Some{k}
223	
224	def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
225	  TM{+n, root, lo, hi, free, nodes, payloads} = m
226	  (TM{n, root, lo, hi, free, nodes, payloads}, n)
227	
228	def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
229	  TM{n, +root, lo, hi, free, nodes, payloads} = m
230	  (TM{n, root, lo, hi, free, nodes, payloads}, root)
231	
232	def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
233	  TM{n, root, +lo, hi, free, nodes, payloads} = m
234	  (TM{n, root, lo, hi, free, nodes, payloads}, lo)
235	
236	def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
237	  TM{n, root, lo, +hi, free, nodes, payloads} = m
238	  (TM{n, root, lo, hi, free, nodes, payloads}, hi)
239	
240	def read_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Node<K>:
241	  match r:
242	    case Tuple{nodes, Done{x}}:
243	      (TM{n, root, lo, hi, free, nodes, payloads}, x)
244	    case Tuple{nodes, Fail{e}}:
245	      (TM{n, root, lo, hi, free, nodes, payloads}, Free{0n})
246	
247	def write_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp>:
248	  (nodes, status) = r
249	  TM{n, root, lo, hi, free, nodes, payloads}
250	
251	def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +root: Nat) -> TreeMap<K, V, cmp>:
252	  TM{n, old, lo, hi, free, nodes, payloads} = m
253	  TM{n, root, lo, hi, free, nodes, payloads}
254	
255	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):
256	  match r:
257	    case Tuple{m, Free{next}}:
258	      (m, (Free{next}, EQ{}))
259	    case Tuple{m, N{c, l, r, p, +key}}:
260	      (m, (N{c, l, r, p, key}, cmp(k, key)))
261	
262	def search_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, r: NodeStore<K> & Maybe<&2, K>) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
263	  match r:
264	    case Tuple{nodes, None{}}:
265	      (nodes, (id, None{}))
266	    case Tuple{nodes, Some{key}}:
267	      (nodes, (id, Some{cmp(k, key)}))
268	
269	def search_fin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Search) -> TreeMap<K, V, cmp> & Search:
270	  (nodes, s) = r
271	  (TM{n, root, lo, hi, free, nodes, payloads}, s)
272	
273	def exchange_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
274	  match r:
275	    case Tuple{payloads, Done{old}}:
276	      (TM{n, root, lo, hi, free, nodes, payloads}, old)
277	    case Tuple{payloads, Fail{e}}:
278	      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
279	
280	def append_rollback(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
281	  (nodes, dropped) = r
282	  (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
283	
284	def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +free: Nat) -> TreeMap<K, V, cmp>:
285	  TM{n, root, lo, hi, old, nodes, payloads} = m
286	  TM{n, root, lo, hi, free, nodes, payloads}
287	
288	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>:
289	  (m1, old) = pair_result
290	  (m1, Done{id})
291	
292	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>>:
293	  (m, old) = r
294	  (m, Done{old})
295	
296	def get_id_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
297	  match r:
298	    case Tuple{payloads, Done{x}}:
299	      (TM{n, root, lo, hi, free, nodes, payloads}, x)
300	    case Tuple{payloads, Fail{e}}:
301	      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
302	
303	def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool:
304	  (m, Search{id, p, left}) = r
305	  (m, Nat.is_lt(0n, id))
306	
307	def ascend_choice(x: Nat, p: Nat, q: Nat, found: Bool) -> Ascend:
308	  match found:
309	    case True{}:
310	      Ascend{0n, p, True{}}
311	    case False{}:
312	      Ascend{x, q, False{}}
313	
314	def neighbor_slots_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: NodeStore<K> & Nat) -> TreeMap<K, V, cmp> & Nat:
315	  (nodes, id) = r
316	  (TM{n, root, lo, hi, free, nodes, payloads}, id)
317	
318	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:
319	  (m3, old) = pair_result
320	  (m3, source)
321	
322	def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
323	  TM{n, root, lo, hi, free, nodes, payloads} = m
324	  TM{Nat.sub(n, 1n), root, lo, hi, id, nodes, payloads}
325	
326	def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lo: Nat, +hi: Nat) -> TreeMap<K, V, cmp>:
327	  TM{n, root, oldlo, oldhi, free, nodes, payloads} = m
328	  TM{n, root, lo, hi, free, nodes, payloads}
329	
330	def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool:
331	  (m1, +n) = pair_result
332	  (m1, Nat.is_eq(n, 0n))
333	
334	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>>:
335	  match k r:
336	    case Some{key} Tuple{m, Some{v}}:
337	      (m, Some{Entry{key, v}})
338	    case _ Tuple{m, value}:
339	      (m, None{})
340	
341	def snap_kv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, mk: Maybe<&2, K>, mv: Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
342	  match mk mv:
343	    case Some{key} Some{v}:
344	      (TM{n, root, lo, hi, free, nodes, payloads}, Some{Entry{key, v}})
345	    case _ _:
346	      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
347	
348	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:
349	  match r:
350	    case Tuple{m, None{}}:
351	      (m, fallback)
352	    case Tuple{m, Some{v}}:
353	      (m, v)
354	
355	def ordering_ok(order: Cmp, inclusive: Bool) -> Bool:
356	  match order:
357	    case LT{}:
358	      True{}
359	    case EQ{}:
360	      inclusive
361	    case GT{}:
362	      False{}
363	
364	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>>:
365	  match valid:
366	    case True{}:
367	      Done{View{m, lower, upper, descending}}
368	    case False{}:
369	      Fail{InvalidView{m, InvalidBounds{}}}
370	
371	def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, upper: Bound<K>) -> View<K, V, cmp>:
372	  View{m, Unbounded{}, upper, False{}}
373	
374	def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>) -> View<K, V, cmp>:
375	  View{m, lower, Unbounded{}, False{}}
376	
377	def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> View<K, V, cmp>:
378	  View{m, Unbounded{}, Unbounded{}, True{}}
379	
380	def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
381	  View{m, lower, upper, descending} = view
382	  View{m, lower, upper, Bool.not(descending)}
383	
384	def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> TreeMap<K, V, cmp>:
385	  View{m, lower, upper, descending} = view
386	  m
387	
388	def view_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>, +descending: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> View<K, V, cmp> & Maybe<&2, V>:
389	  (m, v) = r
390	  (View{m, lower, upper, descending}, v)
391	
392	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>>:
393	  (m, status) = r
394	  (View{m, lower, upper, descending}, status)
395	
396	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>:
397	  (m, id) = r
398	  Cursor{m, id, 0n, lower, upper, forward}
399	
400	def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> TreeMap<K, V, cmp>:
401	  Cursor{m, next, current, lower, upper, forward} = cursor
402	  m
403	
404	def iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> View<K, V, cmp>:
405	  Cursor{m, next, current, lower, upper, forward} = cursor
406	  View{m, lower, upper, Bool.not(forward)}
407	
408	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>>:
409	  (m, next) = r
410	  (Cursor{m, next, id, lower, upper, forward}, Some{entry})
411	
412	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>:
413	  match r:
414	    case Tuple{m, Some{old}}:
415	      (Cursor{m, next, current, lower, upper, forward}, Done{old})
416	    case Tuple{m, None{}}:
417	      (Cursor{m, next, current, lower, upper, forward}, Fail{NoCurrent{}})
418	
419	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>:
420	  (m, Search{id, p, on_left}) = r
421	  (Cursor{m, id, 0n, lower, upper, forward}, removed)
422	
423	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>:
424	  match r:
425	    case Tuple{cursor, None{}}:
426	      (cursor, None{})
427	    case Tuple{cursor, Some{Entry{k, v}}}:
428	      (cursor, Some{k})
429	
430	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>:
431	  match r:
432	    case Tuple{cursor, None{}}:
433	      (cursor, None{})
434	    case Tuple{cursor, Some{Entry{k, v}}}:
435	      (cursor, Some{v})
436	
437	def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool:
438	  match r:
439	    case Tuple{m, None{}}:
440	      (m, False{})
441	    case Tuple{m, Some{old}}:
442	      (m, True{})
443	
444	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:
445	  match r:
446	    case Tuple{view, None{}}:
447	      (view, False{})
448	    case Tuple{view, Some{x}}:
449	      (view, True{})
450	
451	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>>:
452	  match valid:
453	    case True{}:
454	      (View{m, lower, upper, descending}, Some{entry})
455	    case False{}:
456	      (View{m, lower, upper, descending}, None{})
457	
458	def ns_empty(~K: Data, +limit: Nat) -> NodeStore<K>:
459	  NS{limit, 0n, 1n, 0n, ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nats(0n), ns_nokeys(~K, 0n)}
460	
461	def ns_rk(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, +t: Nat, +l: Nat, +r: Nat, +p: Nat, q: Array<Maybe<&2, K>> & Maybe<&2, K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
462	  (keys, k) = q
463	  (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Done{mk_node(~K, t, l, r, p, k)})
464	
465	def ns_tag_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
466	  match ok:
467	    case True{}:
468	      ns_tag_fin(~K, limit, depth, cap, used, lefts, rights, parents, keys, Array.get(Nat, tags, U32.from_nat(i)))
469	    case False{}:
470	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
471	
472	def ns_left_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
473	  match ok:
474	    case True{}:
475	      ns_left_fin(~K, limit, depth, cap, used, tags, rights, parents, keys, Array.get(Nat, lefts, U32.from_nat(i)))
476	    case False{}:
477	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
478	
479	def ns_right_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
480	  match ok:
481	    case True{}:
482	      ns_right_fin(~K, limit, depth, cap, used, tags, lefts, parents, keys, Array.get(Nat, rights, U32.from_nat(i)))
483	    case False{}:
484	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
485	
486	def ns_parent_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Nat:
487	  match ok:
488	    case True{}:
489	      ns_parent_fin(~K, limit, depth, cap, used, tags, lefts, rights, keys, Array.get(Nat, parents, U32.from_nat(i)))
490	    case False{}:
491	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, 0n)
492	
493	def ns_key_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Maybe<&2, K>:
494	  match ok:
495	    case True{}:
496	      ns_key_fin(~K, limit, depth, cap, used, tags, lefts, rights, parents, Array.get(Maybe<&2, K>, keys, U32.from_nat(i)))
497	    case False{}:
498	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, None{})
499	
500	def ns_set_left_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>:
501	  match ok:
502	    case True{}:
503	      ns_set_left_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
504	    case False{}:
505	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
506	
507	def ns_set_right_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>:
508	  match ok:
509	    case True{}:
510	      ns_set_right_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
511	    case False{}:
512	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
513	
514	def ns_set_parent_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Nat, ok: Bool) -> NodeStore<K>:
515	  match ok:
516	    case True{}:
517	      ns_set_parent_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
518	    case False{}:
519	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
520	
521	def ns_set_red_tag(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Bool, q: Array<Nat> & Nat) -> NodeStore<K>:
522	  match q:
523	    case Tuple{tags, 0n}:
524	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
525	    case Tuple{tags, 1n+c}:
526	      NS{limit, depth, cap, used, Array.set(Nat, tags, U32.from_nat(i), ns_red_tag(v)), lefts, rights, parents, keys}
527	
528	def ns_put(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +node: Node<K>) -> NodeStore<K>:
529	  NS{limit, depth, cap, used, Array.set(Nat, tags, i, ntag(~K, node)), Array.set(Nat, lefts, i, nleft(~K, node)), Array.set(Nat, rights, i, nright(~K, node)), Array.set(Nat, parents, i, nparent(~K, node)), Array.set(Maybe<&2, K>, keys, i, nkey(~K, node))}
530	
531	def ns_grow_nats(+depth: Nat, a: Array<Nat>) -> Array<Nat>:
532	  ANode{a, ns_nats(depth)}
533	
534	def ns_grow_keys(~K: Data, +depth: Nat, a: Array<Maybe<&2, K>>) -> Array<Maybe<&2, K>>:
535	  ANode{a, ns_nokeys(~K, depth)}
536	
537	def child(~K: Data, +n: Node<K>, forward: Bool) -> Nat:
538	  pick(Nat, forward, node_right(~K, n), node_left(~K, n))
539	
540	# All links reference live slots. Free slots contain no key and no value.
541	
542	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>:
543	  match m id:
544	    case mm 0n:
545	      (mm, None{})
546	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
547	      exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.swap_at(~Maybe<&2, V>, payloads, i, value))
548	
549	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>:
550	  TM{+n, root, +lo, +hi, free, nodes, payloads} = m
551	  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}
552	
553	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>:
554	  match m id:
555	    case mm 0n:
556	      (mm, None{})
557	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
558	      get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.get_at(~Maybe<&2, V>, payloads, i))
559	
560	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:
561	  match r:
562	    case Tuple{m, Free{next}}:
563	      (m, Ascend{0n, 0n, True{}})
564	    case Tuple{m, N{c, l, r, q, key}}:
565	      (m, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))
566	
567	def ascend_par(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +s: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
568	  (nodes, +q) = r
569	  (nodes, ascend_choice(p, p, q, Nat.is_eq(x, s)))
570	
571	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>:
572	  (m3, +hi) = pair_result
573	  set_ends(~K, ~V, ~cmp, m3, lo, hi)
574	
575	def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Bool:
576	  is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))
577	
578	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>:
579	  (m, node) = r
580	  (m, node_key(~K, node))
581	
582	def snap_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, mv: Maybe<&2, V>, r: NodeStore<K> & Maybe<&2, K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
583	  (nodes, mk) = r
584	  snap_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, mk, mv)
585	
586	def above_lower(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
587	  match bound:
588	    case Unbounded{}:
589	      True{}
590	    case Inclusive{lo}:
591	      ordering_ok(cmp(lo, k), True{})
592	    case Exclusive{lo}:
593	      ordering_ok(cmp(lo, k), False{})
594	
595	def below_upper(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
596	  match bound:
597	    case Unbounded{}:
598	      True{}
599	    case Inclusive{hi}:
600	      ordering_ok(cmp(k, hi), True{})
601	    case Exclusive{hi}:
602	      ordering_ok(cmp(k, hi), False{})
603	
604	def bounds_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>) -> Bool:
605	  match lower upper:
606	    case Unbounded{} _:
607	      True{}
608	    case _ Unbounded{}:
609	      True{}
610	    case Inclusive{lo} Inclusive{hi}:
611	      ordering_ok(cmp(lo, hi), True{})
612	    case Inclusive{lo} Exclusive{hi}:
613	      ordering_ok(cmp(lo, hi), True{})
614	    case Exclusive{lo} Inclusive{hi}:
615	      ordering_ok(cmp(lo, hi), True{})
616	    case Exclusive{lo} Exclusive{hi}:
617	      ordering_ok(cmp(lo, hi), True{})
618	
619	def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
620	  match forward:
621	    case True{}:
622	      first_id(~K, ~V, ~cmp, m)
623	    case False{}:
624	      last_id(~K, ~V, ~cmp, m)
625	
626	def iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
627	  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))
628	
629	def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
630	  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))
631	
632	def ns_new(~K: Data) -> NodeStore<K>:
633	  ns_empty(~K, D.max_depth())
634	
635	def ns_with_limit(~K: Data, +k: Nat) -> NodeStore<K>:
636	  ns_empty(~K, D.clamp_limit(k, Nat.is_lt(k, D.max_depth())))
637	
638	def ns_rp(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, +l: Nat, +r: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
639	  (parents, +p) = q
640	  ns_rk(~K, limit, depth, cap, used, tags, lefts, rights, parents, t, l, r, p, Array.get(Maybe<&2, K>, keys, i))
641	
642	def ns_tag_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
643	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
644	  ns_tag_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
645	
646	def ns_left_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
647	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
648	  ns_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
649	
650	def ns_right_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
651	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
652	  ns_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
653	
654	def ns_parent_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
655	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
656	  ns_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
657	
658	def ns_key_at(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Maybe<&2, K>:
659	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
660	  ns_key_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
661	
662	# ---- writing one field of a live slot (free slots and ids past the length unchanged) ----
663	
664	def ns_set_left(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
665	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
666	  ns_set_left_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
667	
668	def ns_set_right(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
669	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
670	  ns_set_right_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
671	
672	def ns_set_parent(~K: Data, s: NodeStore<K>, +i: Nat, +v: Nat) -> NodeStore<K>:
673	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
674	  ns_set_parent_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
675	
676	def ns_set_red_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +v: Bool, ok: Bool) -> NodeStore<K>:
677	  match ok:
678	    case True{}:
679	      ns_set_red_tag(~K, limit, depth, cap, used, lefts, rights, parents, keys, i, v, Array.get(Nat, tags, U32.from_nat(i)))
680	    case False{}:
681	      NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}
682	
683	def ns_set_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, +node: Node<K>, ok: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
684	  match ok:
685	    case True{}:
686	      (ns_put(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, U32.from_nat(i), node), Done{Unit{}})
687	    case False{}:
688	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})
689	
690	def ns_push_room(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +node: Node<K>, room: Bool, grow: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
691	  match room grow:
692	    case True{} _:
693	      (ns_put(~K, limit, depth, cap, 1n+used, tags, lefts, rights, parents, keys, U32.from_nat(used), node), Done{Unit{}})
694	    case False{} True{}:
695	      (ns_put(~K, limit, 1n+depth, Nat.double(cap), 1n+used, ns_grow_nats(depth, tags), ns_grow_nats(depth, lefts), ns_grow_nats(depth, rights), ns_grow_nats(depth, parents), ns_grow_keys(~K, depth, keys), U32.from_nat(used), node), Done{Unit{}})
696	    case False{} False{}:
697	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.CapacityExceeded{}})
698	
699	def ns_drop(~K: Data, s: NodeStore<K>, +m: Nat) -> NodeStore<K>:
700	  NS{limit, depth, cap, used, tags, lefts, rights, parents, keys} = s
701	  ns_put(~K, limit, depth, cap, m, tags, lefts, rights, parents, keys, U32.from_nat(m), Free{0n})
702	
703	def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
704	  (m, Search{id, p, on_left}) = r
705	  get_id(~K, ~V, ~cmp, m, id)
706	
707	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>:
708	  match r:
709	    case Tuple{m, Search{0n, p, on_left}}:
710	      (m, None{})
711	    case Tuple{m, Search{1n+i, p, on_left}}:
712	      exchange(~K, ~V, ~cmp, m, 1n+i, Some{v})
713	
714	def in_range(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, lower: Bound<K>, upper: Bound<K>) -> Bool:
715	  Bool.and(above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper))
716	
717	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>>:
718	  view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, bounds_valid(~K, ~V, ~cmp, lower, upper))
719	
720	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>:
721	  match cursor:
722	    case Cursor{m, next, 0n, lower, upper, forward}:
723	      (Cursor{m, next, 0n, lower, upper, forward}, Fail{NoCurrent{}})
724	    case Cursor{m, next, 1n+ +id, lower, upper, forward}:
725	      iterator_set_done(~K, ~V, ~cmp, next, 1n+id, lower, upper, forward, exchange(~K, ~V, ~cmp, m, 1n+id, Some{v}))
726	
727	def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
728	  iterator(~K, ~V, ~cmp, m)
729	
730	def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
731	  iterator(~K, ~V, ~cmp, m)
732	
733	def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
734	  iterator(~K, ~V, ~cmp, m)
735	
736	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:
737	  match equal:
738	    case False{}:
739	      (m, False{})
740	    case True{}:
741	      changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))
742	
743	def ns_rr(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, +l: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
744	  (rights, +r) = q
745	  ns_rp(~K, limit, depth, cap, used, tags, lefts, rights, keys, i, t, l, r, Array.get(Nat, parents, i))
746	
747	def ns_set_red(~K: Data, s: NodeStore<K>, +i: Nat, +v: Bool) -> NodeStore<K>:
748	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
749	  ns_set_red_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, v, Nat.is_lt(i, used))
750	
751	# ---- writing a slot: the encoding of the node in all five arrays ----
752	
753	def ns_set(~K: Data, s: NodeStore<K>, +i: Nat, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
754	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
755	  ns_set_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, node, Nat.is_lt(i, used))
756	
757	# ---- appending a slot ----
758	
759	def ns_push(~K: Data, s: NodeStore<K>, +node: Node<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Unit>:
760	  NS{+limit, +depth, +cap, +used, tags, lefts, rights, parents, keys} = s
761	  ns_push_room(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, node, Nat.is_lt(used, cap), Nat.is_lt(depth, limit))
762	
763	# ---- dropping slots: the dropped slots get the encoding of Free{0} back ----
764	
765	def ns_pop_fin(~K: Data, +m: Nat, r: NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
766	  (s, x) = r
767	  (ns_drop(~K, s, m), x)
768	
769	def ns_clear_go(~K: Data, k: Nat, s: NodeStore<K>) -> NodeStore<K>:
770	  match k:
771	    case 0n:
772	      s
773	    case 1n+ +m:
774	      ns_clear_go(~K, m, ns_drop(~K, s, m))
775	
776	# O(used): resets the live slots top down and keeps the capacity.
777	def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> TreeMap<K, V, cmp>:
778	  TM{0n, 0n, 0n, 0n, 0n, ns_new(~K), D.new_at(~Maybe<&2, V>)}
779	
780	def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
781	  match m id:
782	    case mm 0n:
783	      mm
784	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
785	      TM{n, root, lo, hi, free, ns_set_left(~K, nodes, i, v), payloads}
786	
787	def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
788	  match m id:
789	    case mm 0n:
790	      mm
791	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
792	      TM{n, root, lo, hi, free, ns_set_right(~K, nodes, i, v), payloads}
793	
794	def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
795	  match m id:
796	    case mm 0n:
797	      mm
798	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
799	      TM{n, root, lo, hi, free, ns_set_parent(~K, nodes, i, v), payloads}
800	
801	def search_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +id: Nat, +k: K) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
802	  match id:
803	    case 0n:
804	      (nodes, (0n, None{}))
805	    case 1n+ +i:
806	      search_key(~K, ~V, ~cmp, 1n+i, k, ns_key_at(~K, nodes, i))
807	
808	def side_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +left: Bool, +i: Nat) -> NodeStore<K> & Nat:
809	  match left:
810	    case True{}:
811	      ns_left_at(~K, nodes, i)
812	    case False{}:
813	      ns_right_at(~K, nodes, i)
814	
815	def ascend_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
816	  (nodes, +s) = r
817	  ascend_par(~K, ~V, ~cmp, x, p, s, ns_parent_at(~K, nodes, i))
818	
819	def snap_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +i: Nat, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
820	  (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r
821	  snap_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, mv, ns_key_at(~K, nodes, i))
822	
823	def with_limit(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +limit: Nat) -> TreeMap<K, V, cmp>:
824	  TM{0n, 0n, 0n, 0n, 0n, ns_with_limit(~K, limit), D.with_limit_at(~Maybe<&2, V>, limit)}
825	
826	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:
827	  match r:
828	    case Tuple{m, None{}}:
829	      (m, False{})
830	    case Tuple{m, Some{old}}:
831	      replace_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
832	
833	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:
834	  match r:
835	    case Tuple{m, Free{free}}:
836	      (Cursor{m, next, current, lower, upper, forward}, False{})
837	    case Tuple{m, N{c, l, rr, p, key}}:
838	      (Cursor{m, next, current, lower, upper, forward}, in_range(~K, ~V, ~cmp, key, lower, upper))
839	
840	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>>:
841	  match r:
842	    case Tuple{m, None{}}:
843	      (View{m, lower, upper, descending}, None{})
844	    case Tuple{m, Some{Entry{+k, v}}}:
845	      view_entry_checked(~K, ~V, ~cmp, m, lower, upper, descending, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))
846	
847	def ns_rl(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, +t: Nat, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
848	  (lefts, +l) = q
849	  ns_rr(~K, limit, depth, cap, used, tags, lefts, parents, keys, i, t, l, Array.get(Nat, rights, i))
850	
851	def ns_clear(~K: Data, s: NodeStore<K>) -> NodeStore<K>:
852	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
853	  ns_clear_go(~K, used, NS{limit, depth, cap, used, tags, lefts, rights, parents, keys})
854	
855	
856	def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
857	  match m id:
858	    case mm 0n:
859	      mm
860	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
861	      write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_set(~K, nodes, i, node))
862	
863	def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool) -> TreeMap<K, V, cmp>:
864	  match m id:
865	    case mm 0n:
866	      mm
867	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
868	      TM{n, root, lo, hi, free, ns_set_red(~K, nodes, i, v), payloads}
869	
870	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>:
871	  match p on_left:
872	    case 0n _:
873	      set_root(~K, ~V, ~cmp, m, x)
874	    case 1n+q True{}:
875	      set_left(~K, ~V, ~cmp, m, 1n+q, x)
876	    case 1n+q False{}:
877	      set_right(~K, ~V, ~cmp, m, 1n+q, x)
878	
879	def search_down2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, r: NodeStore<K> & Nat) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
880	  (nodes, +c) = r
881	  search_probe(~K, ~V, ~cmp, nodes, c, k)
882	
883	def ascend_tag(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +i: Nat, +forward: Bool, r: NodeStore<K> & Nat) -> NodeStore<K> & Ascend:
884	  match r:
885	    case Tuple{nodes, 0n}:
886	      (nodes, Ascend{0n, 0n, True{}})
887	    case Tuple{nodes, 1n+c}:
888	      ascend_side(~K, ~V, ~cmp, x, p, i, side_at(~K, ~V, ~cmp, nodes, forward, i))
889	
890	def extreme_tag(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, +i: Nat, r: NodeStore<K> & Nat) -> NodeStore<K> & Nat:
891	  match r:
892	    case Tuple{nodes, 0n}:
893	      (nodes, 0n)
894	    case Tuple{nodes, 1n+c}:
895	      side_at(~K, ~V, ~cmp, nodes, Bool.not(forward), i)
896	
897	def snap_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
898	  match id:
899	    case 0n:
900	      (m, None{})
901	    case 1n+ +i:
902	      snap_value(~K, ~V, ~cmp, i, get_id(~K, ~V, ~cmp, m, 1n+i))
903	
904	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:
905	  (m, Search{+id, p, on_left}) = r
906	  replace_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
907	
908	def ns_rt(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: U32, q: Array<Nat> & Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
909	  (tags, +t) = q
910	  ns_rl(~K, limit, depth, cap, used, tags, rights, parents, keys, i, t, Array.get(Nat, lefts, i))
911	
912	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>:
913	  set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)
914	
915	def search_down(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +id: Nat, +left: Bool, +k: K) -> NodeStore<K> & (Nat & Maybe<&2, Cmp>):
916	  match id:
917	    case 0n:
918	      (nodes, (0n, None{}))
919	    case 1n+ +i:
920	      search_down2(~K, ~V, ~cmp, k, side_at(~K, ~V, ~cmp, nodes, left, i))
921	
922	def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
923	  (m1, +r) = pair_result
924	  set_red(~K, ~V, ~cmp, m1, r, False{})
925	
926	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>:
927	  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}))
928	
929	def ascend_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, nodes: NodeStore<K>) -> NodeStore<K> & Ascend:
930	  match p:
931	    case 0n:
932	      (nodes, Ascend{0n, 0n, True{}})
933	    case 1n+ +i:
934	      ascend_tag(~K, ~V, ~cmp, x, 1n+i, i, forward, ns_tag_at(~K, nodes, i))
935	
936	def extreme_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, nodes: NodeStore<K>, +i: Nat) -> NodeStore<K> & Nat:
937	  extreme_tag(~K, ~V, ~cmp, forward, i, ns_tag_at(~K, nodes, i))
938	
939	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>:
940	  match node:
941	    case Free{next}:
942	      m
943	    case N{c, l, r, p, old}:
944	      write(~K, ~V, ~cmp, m, id, N{c, l, r, p, k})
945	
946	def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
947	  TM{n, root, lo, hi, +free, nodes, payloads} = m
948	  release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, Free{free}), id)
949	
950	def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
951	  TM{n, root, lo, hi, free, nodes, payloads} = m
952	  TM{0n, 0n, 0n, 0n, 0n, ns_clear(~K, nodes), D.clear_at(~Maybe<&2, V>, payloads)}
953	
954	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>>:
955	  (m, +id) = r
956	  snap_at(~K, ~V, ~cmp, id, m)
957	
958	def ns_get_ok(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>, +i: Nat, ok: Bool) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
959	  match ok:
960	    case True{}:
961	      ns_rt(~K, limit, depth, cap, used, lefts, rights, parents, keys, U32.from_nat(i), Array.get(Nat, tags, U32.from_nat(i)))
962	    case False{}:
963	      (NS{limit, depth, cap, used, tags, lefts, rights, parents, keys}, Fail{DE.IndexOutOfRange{}})
964	
965	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>:
966	  (m3, +pn) = pair_result
967	  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))
968	
969	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>:
970	  (m3, +pn) = pair_result
971	  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))
972	
973	def search_fast(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +p: Nat, +on_left: Bool, st: NodeStore<K> & (Nat & Maybe<&2, Cmp>)) -> NodeStore<K> & Search:
974	  match fuel st:
975	    case 0n Tuple{nodes, x}:
976	      (nodes, Search{0n, p, on_left})
977	    case 1n+f Tuple{nodes, Tuple{id, None{}}}:
978	      (nodes, Search{0n, p, on_left})
979	    case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}:
980	      search_fast(~K, ~V, ~cmp, f, k, id, True{}, search_down(~K, ~V, ~cmp, nodes, id, True{}, k))
981	    case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}:
982	      search_fast(~K, ~V, ~cmp, f, k, id, False{}, search_down(~K, ~V, ~cmp, nodes, id, False{}, k))
983	    case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}:
984	      (nodes, Search{id, p, on_left})
985	
986	def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
987	  black_root_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
988	
989	
990	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>:
991	  match r:
992	    case Tuple{m, Free{next}}:
993	      reuse_slot(~K, ~V, ~cmp, m, id, next, p, k, v)
994	    case Tuple{m, N{c, l, r, q, oldk}}:
995	      (m, Fail{Rejected{CapacityExceeded{}, k, v}})
996	
997	def ascend_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: NodeStore<K> & Ascend) -> NodeStore<K> & Nat:
998	  match fuel st:
999	    case 0n Tuple{nodes, state}:
1000	      (nodes, 0n)
1001	    case 1n+f Tuple{nodes, Ascend{x, p, True{}}}:
1002	      (nodes, p)
1003	    case 1n+f Tuple{nodes, Ascend{+x, +p, False{}}}:
1004	      ascend_slots_loop(~K, ~V, ~cmp, f, forward, ascend_at(~K, ~V, ~cmp, x, p, forward, nodes))
1005	
1006	def extreme_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: NodeStore<K> & Nat) -> NodeStore<K> & Nat:
1007	  match fuel st:
1008	    case 0n Tuple{nodes, next}:
1009	      (nodes, id)
1010	    case 1n+f Tuple{nodes, 0n}:
1011	      (nodes, id)
1012	    case 1n+f Tuple{nodes, 1n+ +j}:
1013	      extreme_slots_loop(~K, ~V, ~cmp, f, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))
1014	
1015	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>:
1016	  (m1, +node) = pair_result
1017	  set_key_node(~K, ~V, ~cmp, m1, id, k, node)
1018	
1019	def nav_fast(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +higher: Bool, +best: Nat, st: NodeStore<K> & (Nat & Maybe<&2, Cmp>)) -> NodeStore<K> & NavEnd:
1020	  match fuel st:
1021	    case 0n Tuple{nodes, x}:
1022	      (nodes, NavBest{best})
1023	    case 1n+f Tuple{nodes, Tuple{id, None{}}}:
1024	      (nodes, NavBest{best})
1025	    case 1n+f Tuple{nodes, Tuple{+id, Some{LT{}}}}:
1026	      nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, id, best), search_down(~K, ~V, ~cmp, nodes, id, True{}, k))
1027	    case 1n+f Tuple{nodes, Tuple{+id, Some{GT{}}}}:
1028	      nav_fast(~K, ~V, ~cmp, f, k, higher, pick(Nat, higher, best, id), search_down(~K, ~V, ~cmp, nodes, id, False{}, k))
1029	    case 1n+f Tuple{nodes, Tuple{+id, Some{EQ{}}}}:
1030	      (nodes, NavEqual{id})
1031	
1032	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>>:
1033	  entry_snapshot(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1034	
1035	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>>:
1036	  entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1037	
1038	def ns_get(~K: Data, s: NodeStore<K>, +i: Nat) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
1039	  NS{limit, depth, cap, +used, tags, lefts, rights, parents, keys} = s
1040	  ns_get_ok(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys, i, Nat.is_lt(i, used))
1041	
1042	# ---- reading one field of a slot (0, the encoding of Free{0}, past the length) ----
1043	
1044	def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Search:
1045	  TM{+n, +root, lo, hi, free, nodes, payloads} = m
1046	  search_fin(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, search_fast(~K, ~V, ~cmp, 1n+n, k, 0n, False{}, search_probe(~K, ~V, ~cmp, nodes, root, k)))
1047	
1048	def neighbor_slots(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +n: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> NodeStore<K> & Nat:
1049	  match c:
1050	    case 0n:
1051	      ascend_slots_loop(~K, ~V, ~cmp, 1n+n, forward, (nodes, Ascend{id, p, False{}}))
1052	    case 1n+ +j:
1053	      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, Bool.not(forward), 1n+j, extreme_at(~K, ~V, ~cmp, Bool.not(forward), nodes, j))
1054	
1055	def extreme_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: NodeStore<K>, +n: Nat, +id: Nat, +forward: Bool) -> NodeStore<K> & Nat:
1056	  match id:
1057	    case 0n:
1058	      (nodes, 0n)
1059	    case 1n+ +j:
1060	      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, forward, 1n+j, extreme_at(~K, ~V, ~cmp, forward, nodes, j))
1061	
1062	def ns_pop_n(~K: Data, +limit: Nat, +depth: Nat, +cap: Nat, used: Nat, tags: Array<Nat>, lefts: Array<Nat>, rights: Array<Nat>, parents: Array<Nat>, keys: Array<Maybe<&2, K>>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
1063	  match used:
1064	    case 0n:
1065	      (NS{limit, depth, cap, 0n, tags, lefts, rights, parents, keys}, Fail{DE.EmptyArray{}})
1066	    case 1n+ +m:
1067	      ns_pop_fin(~K, m, ns_get(~K, NS{limit, depth, cap, 1n+m, tags, lefts, rights, parents, keys}, m))
1068	
1069	def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Node<K>:
1070	  match m id:
1071	    case mm 0n:
1072	      (mm, Free{0n})
1073	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
1074	      read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, ns_get(~K, nodes, i))
1075	
1076	def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1077	  get_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1078	
1079	def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Bool:
1080	  contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1081	
1082	
1083	def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
1084	  TM{+n, root, lo, hi, free, nodes, payloads} = m
1085	  neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, extreme_start(~K, ~V, ~cmp, nodes, n, id, forward))
1086	
1087	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:
1088	  (TM{+n, root, lo, hi, free, nodes, payloads}, +node) = r
1089	  neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, id, node_parent(~K, node), forward, child(~K, node, forward)))
1090	
1091	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>:
1092	  replace_found(~K, ~V, ~cmp, v, search(~K, ~V, ~cmp, m, k))
1093	
1094	def iter_child(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +id: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, +p: Nat, r: NodeStore<K> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1095	  (nodes, +c) = r
1096	  iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, id, p, forward, c)))
1097	
1098	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>:
1099	  match k r:
1100	    case None{} Tuple{m, removed}:
1101	      (Cursor{m, 0n, 0n, lower, upper, forward}, removed)
1102	    case Some{key} Tuple{m, removed}:
1103	      iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, removed, search(~K, ~V, ~cmp, m, key))
1104	
1105	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:
1106	  replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))
1107	
1108	def ns_pop(~K: Data, s: NodeStore<K>) -> NodeStore<K> & Result<&2, &2, DE.Error, Node<K>>:
1109	  NS{+limit, +depth, +cap, used, tags, lefts, rights, parents, keys} = s
1110	  ns_pop_n(~K, limit, depth, cap, used, tags, lefts, rights, parents, keys)
1111	
1112	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>:
1113	  (m2, +yn) = pair_result
1114	  rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
1115	
1116	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>:
1117	  (m2, +yn) = pair_result
1118	  rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
1119	
1120	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):
1121	  probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
1122	
1123	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:
1124	  match fuel st:
1125	    case 0n Tuple{m, state}:
1126	      (m, 0n)
1127	    case 1n+f Tuple{m, Ascend{x, p, True{}}}:
1128	      (m, p)
1129	    case 1n+f Tuple{m, Ascend{+x, +p, False{}}}:
1130	      ascend_loop(~K, ~V, ~cmp, f, forward, ascend_step_node(~K, ~V, ~cmp, x, p, forward, read(~K, ~V, ~cmp, m, p)))
1131	
1132	def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
1133	  neighbor_node(~K, ~V, ~cmp, id, forward, read(~K, ~V, ~cmp, m, id))
1134	
1135	def set_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp>:
1136	  set_key_1(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
1137	
1138	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>:
1139	  (m2, +lo) = pair_result
1140	  refresh_ends_3(~K, ~V, ~cmp, lo, extreme(~K, ~V, ~cmp, m2, r, True{}))
1141	
1142	def key_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1143	  (m, id) = r
1144	  key_finish(~K, ~V, ~cmp, read(~K, ~V, ~cmp, m, id))
1145	
1146	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:
1147	  default_value(~K, ~V, ~cmp, fallback, get(~K, ~V, ~cmp, m, k))
1148	
1149	
1150	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>:
1151	  match valid:
1152	    case True{}:
1153	      view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k))
1154	    case False{}:
1155	      (View{m, lower, upper, descending}, None{})
1156	
1157	def iter_link(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +i: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, r: NodeStore<K> & Nat) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1158	  (nodes, +p) = r
1159	  iter_child(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, 1n+i, lower, upper, forward, entry, p, side_at(~K, ~V, ~cmp, nodes, Bool.not(forward), i))
1160	
1161	def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Bool:
1162	  Cursor{m, +next, current, lower, upper, forward} = cursor
1163	  iterator_has_checked(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
1164	
1165	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>:
1166	  (m1, +xn) = pair_result
1167	  rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_right(~K, xn)))
1168	
1169	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>:
1170	  (m1, +xn) = pair_result
1171	  rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_left(~K, xn)))
1172	
1173	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:
1174	  match fuel st:
1175	    case 0n Tuple{m, node}:
1176	      (m, Search{0n, p, on_left})
1177	    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
1178	      (m, Search{0n, p, on_left})
1179	    case 1n+f Tuple{m, Tuple{N{c, +l, r, p0, key}, LT{}}}:
1180	      search_loop(~K, ~V, ~cmp, f, k, l, id, True{}, probe(~K, ~V, ~cmp, m, l, k))
1181	    case 1n+f Tuple{m, Tuple{N{c, l, +r, p0, key}, GT{}}}:
1182	      search_loop(~K, ~V, ~cmp, f, k, r, id, False{}, probe(~K, ~V, ~cmp, m, r, k))
1183	    case 1n+f Tuple{m, Tuple{N{c, l, r, p0, key}, EQ{}}}:
1184	      (m, Search{id, p, on_left})
1185	
1186	def append_values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: NodeStore<K>, +k: K, +v: V, +id: Nat, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
1187	  match r:
1188	    case Tuple{payloads, Done{u}}:
1189	      (TM{n, root, lo, hi, free, nodes, payloads}, Done{id})
1190	    case Tuple{payloads, Fail{e}}:
1191	      append_rollback(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, ns_pop(~K, nodes))
1192	
1193	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>:
1194	  match node:
1195	    case Free{next}:
1196	      m
1197	    case N{c, l, r, p, k}:
1198	      set_key(~K, ~V, ~cmp, m, target, k)
1199	
1200	def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1201	  (m1, +r) = pair_result
1202	  refresh_ends_2(~K, ~V, ~cmp, r, extreme(~K, ~V, ~cmp, m1, r, False{}))
1203	
1204	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:
1205	  match inclusive:
1206	    case True{}:
1207	      (m, id)
1208	    case False{}:
1209	      neighbor(~K, ~V, ~cmp, m, id, higher)
1210	
1211	
1212	def first_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1213	  key_id(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1214	
1215	def last_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
1216	  key_id(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1217	
1218	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>:
1219	  View{m, +lower, +upper, descending} = view
1220	  view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1221	
1222	def iter_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, +valid: Bool) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1223	  match valid:
1224	    case True{}:
1225	      iter_link(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, lower, upper, forward, entry, ns_parent_at(~K, nodes, i))
1226	    case False{}:
1227	      (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})
1228	
1229	def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
1230	  rotate_left_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
1231	
1232	def rotate_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
1233	  rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
1234	
1235	def append_nodes(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +id: Nat, r: NodeStore<K> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
1236	  match r:
1237	    case Tuple{nodes, Done{u}}:
1238	      append_values(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, k, v, id, D.push_at(~Maybe<&2, V>, payloads, Some{v}))
1239	    case Tuple{nodes, Fail{e}}:
1240	      (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
1241	
1242	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:
1243	  (m2, value) = pair_result
1244	  move_successor_3(~K, ~V, ~cmp, source, exchange(~K, ~V, ~cmp, copy_key(~K, ~V, ~cmp, m2, target, source_node), target, value))
1245	
1246	def refresh_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
1247	  refresh_ends_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
1248	
1249	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:
1250	  match fuel st:
1251	    case 0n Tuple{m, node}:
1252	      (m, best)
1253	    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
1254	      (m, best)
1255	    case 1n+f Tuple{m, Tuple{N{c, +l, r, p, key}, LT{}}}:
1256	      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, l, pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, m, l, k))
1257	    case 1n+f Tuple{m, Tuple{N{c, l, +r, p, key}, GT{}}}:
1258	      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, r, pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, m, r, k))
1259	    case 1n+f Tuple{m, Tuple{node, EQ{}}}:
1260	      nav_equal(~K, ~V, ~cmp, m, id, higher, inclusive)
1261	
1262	def nav_end(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +higher: Bool, +inclusive: Bool, r: NodeStore<K> & NavEnd) -> TreeMap<K, V, cmp> & Nat:
1263	  match r:
1264	    case Tuple{nodes, NavBest{b}}:
1265	      (TM{n, root, lo, hi, free, nodes, payloads}, b)
1266	    case Tuple{nodes, NavEqual{+id}}:
1267	      nav_equal(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, higher, inclusive)
1268	
1269	def iter_kv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, nodes: NodeStore<K>, +i: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, mk: Maybe<&2, K>, mv: Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1270	  match mk mv:
1271	    case Some{+key} Some{v}:
1272	      iter_valid(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, i, current, lower, upper, forward, Entry{key, v}, in_range(~K, ~V, ~cmp, key, lower, upper))
1273	    case _ _:
1274	      (Cursor{TM{n, root, lo, hi, free, nodes, payloads}, 0n, current, lower, upper, forward}, None{})
1275	
1276	def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Bool:
1277	  view_contains_value(~K, ~V, ~cmp, view_get(~K, ~V, ~cmp, view, k))
1278	
1279	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:
1280	  match triangle:
1281	    case True{}:
1282	      (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{}})
1283	    case False{}:
1284	      (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
1285	
1286	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:
1287	  match triangle:
1288	    case True{}:
1289	      (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{}})
1290	    case False{}:
1291	      (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
1292	
1293	def append_count(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +p: Nat, r: NodeStore<K> & Nat) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
1294	  (nodes, +used) = r
1295	  append_nodes(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, 1n+used, ns_push(~K, nodes, N{True{}, 0n, 0n, p, k}))
1296	
1297	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:
1298	  (m1, +source_node) = pair_result
1299	  move_successor_2(~K, ~V, ~cmp, target, source, source_node, exchange(~K, ~V, ~cmp, m1, source, None{}))
1300	
1301	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:
1302	  (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{}})
1303	
1304	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:
1305	  (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{}})
1306	
1307	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:
1308	  TM{+n, +root, lo, hi, free, nodes, payloads} = m
1309	  nav_end(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, higher, inclusive, nav_fast(~K, ~V, ~cmp, 1n+n, k, higher, 0n, search_probe(~K, ~V, ~cmp, nodes, root, k)))
1310	
1311	def iter_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, mv: Maybe<&2, V>, r: NodeStore<K> & Maybe<&2, K>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1312	  (nodes, mk) = r
1313	  iter_kv(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, nodes, i, current, lower, upper, forward, mk, mv)
1314	
1315	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:
1316	  match uncle:
1317	    case N{True{}, l, r, gp, k}:
1318	      (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{}})
1319	    case _:
1320	      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)
1321	
1322	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:
1323	  match uncle:
1324	    case N{True{}, l, r, gp, k}:
1325	      (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{}})
1326	    case _:
1327	      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)
1328	
1329	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>:
1330	  TM{n, root, lo, hi, free, nodes, payloads} = m
1331	  append_count(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, p, ns_length(~K, nodes))
1332	
1333	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:
1334	  move_successor_1(~K, ~V, ~cmp, target, source, read(~K, ~V, ~cmp, m, source))
1335	
1336	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:
1337	  (m2, +wn) = pair_result
1338	  delete_borrow_left(~K, ~V, ~cmp, m2, p, node_right(~K, pn), pn, wn)
1339	
1340	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:
1341	  (m2, +wn) = pair_result
1342	  delete_borrow_right(~K, ~V, ~cmp, m2, p, node_left(~K, pn), pn, wn)
1343	
1344	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>:
1345	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
1346	
1347	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>:
1348	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
1349	
1350	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>:
1351	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
1352	
1353	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>:
1354	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
1355	
1356	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>>:
1357	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
1358	
1359	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>>:
1360	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
1361	
1362	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>>:
1363	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
1364	
1365	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>>:
1366	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
1367	
1368	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:
1369	  match bound:
1370	    case Unbounded{}:
1371	      range_unbounded(~K, ~V, ~cmp, m, forward)
1372	    case Inclusive{k}:
1373	      navigate(~K, ~V, ~cmp, m, k, forward, True{})
1374	    case Exclusive{k}:
1375	      navigate(~K, ~V, ~cmp, m, k, forward, False{})
1376	
1377	def iter_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +i: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1378	  (TM{+n, +root, +lo, +hi, +free, nodes, payloads}, mv) = r
1379	  iter_key(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, i, current, lower, upper, forward, mv, ns_key_at(~K, nodes, i))
1380	
1381	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:
1382	  (m1, +un) = pair_result
1383	  insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, node_right(~K, gn), Nat.is_eq(z, node_right(~K, pn)), un)
1384	
1385	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:
1386	  (m1, +un) = pair_result
1387	  insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, node_left(~K, gn), Nat.is_eq(z, node_left(~K, pn)), un)
1388	
1389	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>:
1390	  TM{n, root, lo, hi, free, nodes, payloads} = m
1391	  match free:
1392	    case 0n:
1393	      append(~K, ~V, ~cmp, TM{n, root, lo, hi, 0n, nodes, payloads}, k, v, p)
1394	    case 1n+ +f:
1395	      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))
1396	
1397	def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:
1398	  (m, source) = r
1399	  move_successor(~K, ~V, ~cmp, m, target, source)
1400	
1401	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:
1402	  (m1, +pn) = pair_result
1403	  delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1404	
1405	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:
1406	  (m1, +pn) = pair_result
1407	  delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1408	
1409	def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> Cursor<K, V, cmp>:
1410	  View{m, +lower, +upper, +descending} = view
1411	  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)))
1412	
1413	def iter_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
1414	  match next:
1415	    case 0n:
1416	      (Cursor{m, 0n, current, lower, upper, forward}, None{})
1417	    case 1n+ +i:
1418	      iter_value(~K, ~V, ~cmp, i, current, lower, upper, forward, get_id(~K, ~V, ~cmp, m, 1n+i))
1419	
1420	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:
1421	  match within:
1422	    case True{}:
1423	      navigate(~K, ~V, ~cmp, m, k, higher, inclusive)
1424	    case False{}:
1425	      range_start(~K, ~V, ~cmp, m, pick(Bound<K>, higher, lower, upper), higher)
1426	
1427	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>>:
1428	  View{m, +lower, +upper, +descending} = view
1429	  +up = pick(Bool, descending, Bool.not(first), first)
1430	  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)))
1431	
1432	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:
1433	  insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_right(~K, gn)))
1434	
1435	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:
1436	  insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_left(~K, gn)))
1437	
1438	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:
1439	  match r:
1440	    case Tuple{m, N{c, 1n+l, 1n+r, p, k}}:
1441	      successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, m, 1n+r, False{}))
1442	    case Tuple{m, node}:
1443	      (m, id)
1444	
1445	
1446	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:
1447	  delete_borrow_read_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1448	
1449	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:
1450	  delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1451	
1452	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>>:
1453	  Cursor{m, +next, current, lower, upper, forward} = cursor
1454	  iter_at(~K, ~V, ~cmp, next, current, lower, upper, forward, m)
1455	
1456	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>>:
1457	  View{m, +lower, +upper, +descending} = view
1458	  +up = pick(Bool, descending, Bool.not(higher), higher)
1459	  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)))))
1460	
1461	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>>:
1462	  view_extreme(~K, ~V, ~cmp, view, True{})
1463	
1464	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>>:
1465	  view_extreme(~K, ~V, ~cmp, view, False{})
1466	
1467	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:
1468	  match on_left:
1469	    case True{}:
1470	      insert_side_left(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1471	    case False{}:
1472	      insert_side_right(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1473	
1474	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:
1475	  match far_red:
1476	    case True{}:
1477	      delete_borrow_left(~K, ~V, ~cmp, m, p, w, pn, wn)
1478	    case False{}:
1479	      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)
1480	
1481	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:
1482	  match far_red:
1483	    case True{}:
1484	      delete_borrow_right(~K, ~V, ~cmp, m, p, w, pn, wn)
1485	    case False{}:
1486	      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)
1487	
1488	def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, K>:
1489	  iterator_key_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
1490	
1491	def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
1492	  iterator_value_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
1493	
1494	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:
1495	  match fuel found st:
1496	    case _ True{} Tuple{cursor, item}:
1497	      (iterator_finish(~K, ~V, ~cmp, cursor), True{})
1498	    case 0n False{} Tuple{cursor, item}:
1499	      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
1500	    case 1n+f False{} Tuple{cursor, None{}}:
1501	      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
1502	    case 1n+f False{} Tuple{cursor, Some{Entry{k, v}}}:
1503	      contains_value_loop(~K, ~V, ~cmp, ~eq, f, wanted, eq(v, wanted), iterator_next(~K, ~V, ~cmp, cursor))
1504	
1505	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>>:
1506	  view_nav(~K, ~V, ~cmp, view, k, False{}, False{})
1507	
1508	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>>:
1509	  view_nav(~K, ~V, ~cmp, view, k, False{}, True{})
1510	
1511	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>>:
1512	  view_nav(~K, ~V, ~cmp, view, k, True{}, True{})
1513	
1514	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>>:
1515	  view_nav(~K, ~V, ~cmp, view, k, True{}, False{})
1516	
1517	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:
1518	  match fuel st:
1519	    case 0n Tuple{cursor, item}:
1520	      (iterator_view(~K, ~V, ~cmp, cursor), count)
1521	    case 1n+f Tuple{cursor, None{}}:
1522	      (iterator_view(~K, ~V, ~cmp, cursor), count)
1523	    case 1n+f Tuple{cursor, Some{item}}:
1524	      view_count_loop(~K, ~V, ~cmp, f, 1n+count, iterator_next(~K, ~V, ~cmp, cursor))
1525	
1526	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>>:
1527	  (cursor, removed) = r
1528	  iterator_next(~K, ~V, ~cmp, cursor)
1529	
1530	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:
1531	  (m1, +gn) = pair_result
1532	  insert_side(~K, ~V, ~cmp, m1, z, p, node_parent(~K, pn), pn, gn, Nat.is_eq(p, node_left(~K, gn)))
1533	
1534	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:
1535	  match near_red far_red:
1536	    case False{} False{}:
1537	      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1538	    case _ _:
1539	      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1540	
1541	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:
1542	  match near_red far_red:
1543	    case False{} False{}:
1544	      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1545	    case _ _:
1546	      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1547	
1548	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:
1549	  (m, n) = r
1550	  contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+n, wanted, False{}, iterator_next(~K, ~V, ~cmp, iterator(~K, ~V, ~cmp, m)))
1551	
1552	def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Nat:
1553	  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1554	  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})))
1555	
1556	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:
1557	  insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, node_parent(~K, pn)))
1558	
1559	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:
1560	  (m4, +far_node) = pair_result
1561	  delete_children_left(~K, ~V, ~cmp, m4, p, node_right(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1562	
1563	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:
1564	  (m4, +far_node) = pair_result
1565	  delete_children_right(~K, ~V, ~cmp, m4, p, node_left(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1566	
1567	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:
1568	  contains_value_start(~K, ~V, ~cmp, ~eq, wanted, size(~K, ~V, ~cmp, m))
1569	
1570	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:
1571	  match is_red:
1572	    case False{}:
1573	      (m, Fix{0n, False{}})
1574	    case True{}:
1575	      insert_grand(~K, ~V, ~cmp, m, z, p, pn)
1576	
1577	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:
1578	  (m3, +near_node) = pair_result
1579	  delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_right(~K, wn)))
1580	
1581	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:
1582	  (m3, +near_node) = pair_result
1583	  delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_left(~K, wn)))
1584	
1585	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:
1586	  (m2, +pn) = pair_result
1587	  insert_parent(~K, ~V, ~cmp, m2, z, node_parent(~K, zn), pn, node_red(~K, pn))
1588	
1589	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:
1590	  (m2, +wn) = pair_result
1591	  delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_left(~K, wn)))
1592	
1593	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:
1594	  (m2, +wn) = pair_result
1595	  delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_right(~K, wn)))
1596	
1597	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:
1598	  (m1, +zn) = pair_result
1599	  insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, node_parent(~K, zn)))
1600	
1601	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:
1602	  (m1, +pn) = pair_result
1603	  delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1604	
1605	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:
1606	  (m1, +pn) = pair_result
1607	  delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1608	
1609	def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat) -> TreeMap<K, V, cmp> & Fix:
1610	  insert_fix_step_1(~K, ~V, ~cmp, z, read(~K, ~V, ~cmp, m, z))
1611	
1612	def delete_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1613	  delete_sibling_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1614	
1615	def delete_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1616	  delete_sibling_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1617	
1618	def insert_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & Fix) -> TreeMap<K, V, cmp>:
1619	  match fuel st:
1620	    case 0n Tuple{m, f}:
1621	      black_root(~K, ~V, ~cmp, m)
1622	    case 1n+p Tuple{m, Fix{z, False{}}}:
1623	      black_root(~K, ~V, ~cmp, m)
1624	    case 1n+p Tuple{m, Fix{z, True{}}}:
1625	      insert_fix_loop(~K, ~V, ~cmp, p, insert_fix_step(~K, ~V, ~cmp, m, z))
1626	
1627	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:
1628	  match red_sibling:
1629	    case True{}:
1630	      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)
1631	    case False{}:
1632	      delete_sibling_left(~K, ~V, ~cmp, m, p)
1633	
1634	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:
1635	  match red_sibling:
1636	    case True{}:
1637	      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)
1638	    case False{}:
1639	      delete_sibling_right(~K, ~V, ~cmp, m, p)
1640	
1641	def insert_fixed(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1642	  (m, n) = r
1643	  insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, Fix{id, True{}}))
1644	
1645	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:
1646	  (m1, +wn) = pair_result
1647	  delete_red_sibling_left(~K, ~V, ~cmp, m1, p, node_right(~K, pn), node_red(~K, wn))
1648	
1649	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:
1650	  (m1, +wn) = pair_result
1651	  delete_red_sibling_right(~K, ~V, ~cmp, m1, p, node_left(~K, pn), node_red(~K, wn))
1652	
1653	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>>:
1654	  match r:
1655	    case Tuple{m, Done{+id}}:
1656	      (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{}})
1657	    case Tuple{m, Fail{e}}:
1658	      (m, Fail{e})
1659	
1660	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:
1661	  delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_right(~K, pn)))
1662	
1663	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:
1664	  delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_left(~K, pn)))
1665	
1666	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>>:
1667	  match r:
1668	    case Tuple{m, Search{0n, +p, +on_left}}:
1669	      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1670	    case Tuple{m, Search{1n+i, p, on_left}}:
1671	      put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, 1n+i, Some{v}))
1672	
1673	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:
1674	  match on_left:
1675	    case True{}:
1676	      delete_side_left(~K, ~V, ~cmp, m, p, pn)
1677	    case False{}:
1678	      delete_side_right(~K, ~V, ~cmp, m, p, pn)
1679	
1680	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>>:
1681	  match r:
1682	    case Tuple{m, Search{0n, +p, +on_left}}:
1683	      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1684	    case Tuple{m, Search{1n+i, p, on_left}}:
1685	      put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, m, 1n+i))
1686	
1687	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>>:
1688	  put_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1689	
1690	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:
1691	  match stop:
1692	    case True{}:
1693	      (set_red(~K, ~V, ~cmp, m, x, False{}), DF{0n, 0n, False{}})
1694	    case False{}:
1695	      delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, node_left(~K, pn)))
1696	
1697	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>>:
1698	  put_absent_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1699	
1700	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:
1701	  (m3, +pn) = pair_result
1702	  delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), node_red(~K, xn)))
1703	
1704	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>>:
1705	  match valid:
1706	    case True{}:
1707	      view_put_finish(~K, ~V, ~cmp, lower, upper, descending, put(~K, ~V, ~cmp, m, k, v))
1708	    case False{}:
1709	      (View{m, lower, upper, descending}, Fail{Rejected{OutOfRange{}, k, v}})
1710	
1711	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:
1712	  (m2, +xn) = pair_result
1713	  delete_fix_step_3(~K, ~V, ~cmp, x, p, root_node, xn, read(~K, ~V, ~cmp, m2, p))
1714	
1715	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>>:
1716	  View{m, +lower, +upper, descending} = view
1717	  view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1718	
1719	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:
1720	  (m1, +root_node) = pair_result
1721	  delete_fix_step_2(~K, ~V, ~cmp, x, p, root_node, read(~K, ~V, ~cmp, m1, x))
1722	
1723	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:
1724	  delete_fix_step_1(~K, ~V, ~cmp, x, p, root_id(~K, ~V, ~cmp, m))
1725	
1726	def delete_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & DeleteFix) -> TreeMap<K, V, cmp>:
1727	  match fuel st:
1728	    case 0n Tuple{m, fix}:
1729	      black_root(~K, ~V, ~cmp, m)
1730	    case 1n+f Tuple{m, DF{x, p, False{}}}:
1731	      black_root(~K, ~V, ~cmp, m)
1732	    case 1n+f Tuple{m, DF{x, p, True{}}}:
1733	      delete_fix_loop(~K, ~V, ~cmp, f, delete_fix_step(~K, ~V, ~cmp, m, x, p))
1734	
1735	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>:
1736	  TM{+n, root, lo, hi, free, nodes, payloads} = m
1737	  delete_fix_loop(~K, ~V, ~cmp, 1n+n, (TM{n, root, lo, hi, free, nodes, payloads}, DF{x, p, Bool.not(was_red)}))
1738	
1739	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>:
1740	  (m2, +pn) = pair_result
1741	  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))
1742	
1743	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>:
1744	  (m1, +node) = pair_result
1745	  unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, node_parent(~K, node)))
1746	
1747	def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
1748	  unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1749	
1750	def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1751	  (m, id) = r
1752	  refresh_ends(~K, ~V, ~cmp, unlink(~K, ~V, ~cmp, m, id))
1753	
1754	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>:
1755	  (m1, value) = pair_result
1756	  (unlink_target(~K, ~V, ~cmp, delete_target(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m1, id))), value)
1757	
1758	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>:
1759	  remove_present_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, m, id, None{}))
1760	
1761	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>:
1762	  match id:
1763	    case 0n:
1764	      (m, None{})
1765	    case 1n+i:
1766	      remove_present(~K, ~V, ~cmp, m, 1n+i)
1767	
1768	def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1769	  (m, Search{id, p, on_left}) = r
1770	  remove_id(~K, ~V, ~cmp, m, id)
1771	
1772	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>>:
1773	  (m1, +node) = pair_result
1774	  entry_value(~K, ~V, ~cmp, node_key(~K, node), remove_id(~K, ~V, ~cmp, m1, id))
1775	
1776	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>:
1777	  (m1, +node) = pair_result
1778	  iterator_reseek(~K, ~V, ~cmp, node_key(~K, node), lower, upper, forward, remove_id(~K, ~V, ~cmp, m1, current))
1779	
1780	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:
1781	  match equal:
1782	    case False{}:
1783	      (m, False{})
1784	    case True{}:
1785	      changed_value(~K, ~V, ~cmp, remove_id(~K, ~V, ~cmp, m, id))
1786	
1787	def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1788	  remove_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1789	
1790	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>>:
1791	  remove_entry_id_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1792	
1793	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>:
1794	  iterator_delete_1(~K, ~V, ~cmp, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
1795	
1796	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:
1797	  match r:
1798	    case Tuple{m, None{}}:
1799	      (m, False{})
1800	    case Tuple{m, Some{old}}:
1801	      remove_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
1802	
1803	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>>:
1804	  (m, id) = r
1805	  remove_entry_id(~K, ~V, ~cmp, m, id)
1806	
1807	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>:
1808	  match valid:
1809	    case True{}:
1810	      view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k))
1811	    case False{}:
1812	      (View{m, lower, upper, descending}, None{})
1813	
1814	def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
1815	  Cursor{m, next, current, lower, upper, forward} = cursor
1816	  iterator_delete(~K, ~V, ~cmp, m, next, current, lower, upper, forward)
1817	
1818	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:
1819	  (m, Search{+id, p, on_left}) = r
1820	  remove_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
1821	
1822	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>>:
1823	  poll_ready(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1824	
1825	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>>:
1826	  poll_ready(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1827	
1828	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>:
1829	  View{m, +lower, +upper, descending} = view
1830	  view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1831	
1832	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:
1833	  remove_if_found(~K, ~V, ~cmp, ~eq, expected, expected, search(~K, ~V, ~cmp, m, k))
1834	
1835	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>:
1836	  match fuel st:
1837	    case 0n Tuple{cursor, item}:
1838	      iterator_view(~K, ~V, ~cmp, cursor)
1839	    case 1n+f Tuple{cursor, None{}}:
1840	      iterator_view(~K, ~V, ~cmp, cursor)
1841	    case 1n+f Tuple{cursor, Some{item}}:
1842	      view_clear_loop(~K, ~V, ~cmp, f, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, cursor)))
1843	
1844	def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
1845	  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1846	  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})))