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	type TreeMap<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
14	  TM{size: Nat, root: Nat, first: Nat, last: Nat, free: Nat,
15	     nodes: D.DynArray<&2, Node<K>>, payloads: D.DynArray<&2, Maybe<&2, V>>}
16	
17	type Entry<-K: Data, -V: Data> is Data:
18	  Entry{key: K, value: V}
19	
20	type Error is Data:
21	  CapacityExceeded{}
22	  OutOfRange{}
23	  NoCurrent{}
24	  InvalidBounds{}
25	
26	type Rejected<-K: Data, -V: Data> is Data:
27	  Rejected{error: Error, key: K, value: V}
28	
29	type Search is Data:
30	  Search{found: Nat, parent: Nat, left: Bool}
31	
32	type Fix is Data:
33	  Fix{node: Nat, more: Bool}
34	
35	type Ascend is Data:
36	  Ascend{child: Nat, parent: Nat, done: Bool}
37	
38	# A direct branch preserves scalar traversal state in native code. Passing
39	# these records through pick(-T: Type) erases their layout and boxes both arms.
40	type DeleteFix is Data:
41	  DF{node: Nat, parent: Nat, more: Bool}
42	
43	type Bound<-K: Data> is Data:
44	  Unbounded{}
45	  Inclusive{key: K}
46	  Exclusive{key: K}
47	
48	type View<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
49	  View{map: TreeMap<K, V, cmp>, lower: Bound<K>, upper: Bound<K>, descending: Bool}
50	
51	type InvalidView<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
52	  InvalidView{map: TreeMap<K, V, cmp>, error: Error}
53	
54	type Cursor<-K: Data, -V: Data, -cmp: K -> K -> Cmp> is Type:
55	  Cursor{map: TreeMap<K, V, cmp>, next: Nat, current: Nat,
56	         lower: Bound<K>, upper: Bound<K>, forward: Bool}
57	
58	def pick(-T: Type, b: Bool, yes: T, no: T) -> T:
59	  match b:
60	    case True{}:
61	      yes
62	    case False{}:
63	      no
64	
65	def node_red(~K: Data, n: Node<K>) -> Bool:
66	  match n:
67	    case Free{x}:
68	      False{}
69	    case N{c, l, r, p, k}:
70	      c
71	
72	def node_left(~K: Data, n: Node<K>) -> Nat:
73	  match n:
74	    case Free{x}:
75	      0n
76	    case N{c, l, r, p, k}:
77	      l
78	
79	def node_right(~K: Data, n: Node<K>) -> Nat:
80	  match n:
81	    case Free{x}:
82	      0n
83	    case N{c, l, r, p, k}:
84	      r
85	
86	def node_parent(~K: Data, n: Node<K>) -> Nat:
87	  match n:
88	    case Free{x}:
89	      0n
90	    case N{c, l, r, p, k}:
91	      p
92	
93	def node_key(~K: Data, n: Node<K>) -> Maybe<&2, K>:
94	  match n:
95	    case Free{x}:
96	      None{}
97	    case N{c, l, r, p, k}:
98	      Some{k}
99	
100	def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> TreeMap<K, V, cmp>:
101	  TM{0n, 0n, 0n, 0n, 0n, D.new_at(~Node<K>), D.new_at(~Maybe<&2, V>)}
102	
103	def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
104	  TM{+n, root, lo, hi, free, nodes, payloads} = m
105	  (TM{n, root, lo, hi, free, nodes, payloads}, n)
106	
107	def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
108	  TM{n, +root, lo, hi, free, nodes, payloads} = m
109	  (TM{n, root, lo, hi, free, nodes, payloads}, root)
110	
111	def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
112	  TM{n, root, +lo, hi, free, nodes, payloads} = m
113	  (TM{n, root, lo, hi, free, nodes, payloads}, lo)
114	
115	def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Nat:
116	  TM{n, root, lo, +hi, free, nodes, payloads} = m
117	  (TM{n, root, lo, hi, free, nodes, payloads}, hi)
118	
119	def read_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Node<K>:
120	  match r:
121	    case Tuple{nodes, Done{x}}:
122	      (TM{n, root, lo, hi, free, nodes, payloads}, x)
123	    case Tuple{nodes, Fail{e}}:
124	      (TM{n, root, lo, hi, free, nodes, payloads}, Free{0n})
125	
126	def write_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp>:
127	  (nodes, status) = r
128	  TM{n, root, lo, hi, free, nodes, payloads}
129	
130	def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +root: Nat) -> TreeMap<K, V, cmp>:
131	  TM{n, old, lo, hi, free, nodes, payloads} = m
132	  TM{n, root, lo, hi, free, nodes, payloads}
133	
134	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):
135	  match r:
136	    case Tuple{m, Free{next}}:
137	      (m, (Free{next}, EQ{}))
138	    case Tuple{m, N{c, l, r, p, +key}}:
139	      (m, (N{c, l, r, p, key}, cmp(k, key)))
140	
141	def exchange_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<K>>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
142	  match r:
143	    case Tuple{payloads, Done{old}}:
144	      (TM{n, root, lo, hi, free, nodes, payloads}, old)
145	    case Tuple{payloads, Fail{e}}:
146	      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
147	
148	def append_rollback(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, r: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Node<K>>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
149	  (nodes, dropped) = r
150	  (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
151	
152	def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +free: Nat) -> TreeMap<K, V, cmp>:
153	  TM{n, root, lo, hi, old, nodes, payloads} = m
154	  TM{n, root, lo, hi, free, nodes, payloads}
155	
156	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>:
157	  (m1, old) = pair_result
158	  (m1, Done{id})
159	
160	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>>:
161	  (m, old) = r
162	  (m, Done{old})
163	
164	def get_id_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<K>>, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
165	  match r:
166	    case Tuple{payloads, Done{x}}:
167	      (TM{n, root, lo, hi, free, nodes, payloads}, x)
168	    case Tuple{payloads, Fail{e}}:
169	      (TM{n, root, lo, hi, free, nodes, payloads}, None{})
170	
171	def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Bool:
172	  (m, Search{id, p, left}) = r
173	  (m, Nat.is_lt(0n, id))
174	
175	def ascend_choice(x: Nat, p: Nat, q: Nat, found: Bool) -> Ascend:
176	  match found:
177	    case True{}:
178	      Ascend{0n, p, True{}}
179	    case False{}:
180	      Ascend{x, q, False{}}
181	
182	def node_slot_done(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Array<Maybe<&2, Node<K>>> & Maybe<&2, Node<K>>) -> Array<Maybe<&2, Node<K>>> & Node<K>:
183	  match r:
184	    case Tuple{nodes, None{}}:
185	      (nodes, Free{0n})
186	    case Tuple{nodes, Some{node}}:
187	      (nodes, node)
188	
189	def neighbor_slots_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +limit: Nat, +depth: Nat, +cap: Nat, +used: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, r: Array<Maybe<&2, Node<K>>> & Nat) -> TreeMap<K, V, cmp> & Nat:
190	  (nodes, id) = r
191	  (TM{n, root, lo, hi, free, D.DA{limit, depth, cap, used, nodes}, payloads}, id)
192	
193	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:
194	  (m3, old) = pair_result
195	  (m3, source)
196	
197	def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
198	  TM{n, root, lo, hi, free, nodes, payloads} = m
199	  TM{Nat.sub(n, 1n), root, lo, hi, id, nodes, payloads}
200	
201	def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +lo: Nat, +hi: Nat) -> TreeMap<K, V, cmp>:
202	  TM{n, root, oldlo, oldhi, free, nodes, payloads} = m
203	  TM{n, root, lo, hi, free, nodes, payloads}
204	
205	def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
206	  TM{n, root, lo, hi, free, nodes, payloads} = m
207	  TM{0n, 0n, 0n, 0n, 0n, D.clear_at(~Node<K>, nodes), D.clear_at(~Maybe<&2, V>, payloads)}
208	
209	def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Bool:
210	  (m1, +n) = pair_result
211	  (m1, Nat.is_eq(n, 0n))
212	
213	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>>:
214	  match k r:
215	    case Some{key} Tuple{m, Some{v}}:
216	      (m, Some{Entry{key, v}})
217	    case _ Tuple{m, value}:
218	      (m, None{})
219	
220	def with_limit(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +limit: Nat) -> TreeMap<K, V, cmp>:
221	  TM{0n, 0n, 0n, 0n, 0n, D.with_limit_at(~Node<K>, limit), D.with_limit_at(~Maybe<&2, V>, limit)}
222	
223	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:
224	  match r:
225	    case Tuple{m, None{}}:
226	      (m, fallback)
227	    case Tuple{m, Some{v}}:
228	      (m, v)
229	
230	def ordering_ok(order: Cmp, inclusive: Bool) -> Bool:
231	  match order:
232	    case LT{}:
233	      True{}
234	    case EQ{}:
235	      inclusive
236	    case GT{}:
237	      False{}
238	
239	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>>:
240	  match valid:
241	    case True{}:
242	      Done{View{m, lower, upper, descending}}
243	    case False{}:
244	      Fail{InvalidView{m, InvalidBounds{}}}
245	
246	def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, upper: Bound<K>) -> View<K, V, cmp>:
247	  View{m, Unbounded{}, upper, False{}}
248	
249	def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, lower: Bound<K>) -> View<K, V, cmp>:
250	  View{m, lower, Unbounded{}, False{}}
251	
252	def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> View<K, V, cmp>:
253	  View{m, Unbounded{}, Unbounded{}, True{}}
254	
255	def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
256	  View{m, lower, upper, descending} = view
257	  View{m, lower, upper, Bool.not(descending)}
258	
259	def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> TreeMap<K, V, cmp>:
260	  View{m, lower, upper, descending} = view
261	  m
262	
263	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>:
264	  (m, v) = r
265	  (View{m, lower, upper, descending}, v)
266	
267	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>>:
268	  (m, status) = r
269	  (View{m, lower, upper, descending}, status)
270	
271	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>:
272	  (m, id) = r
273	  Cursor{m, id, 0n, lower, upper, forward}
274	
275	def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> TreeMap<K, V, cmp>:
276	  Cursor{m, next, current, lower, upper, forward} = cursor
277	  m
278	
279	def iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> View<K, V, cmp>:
280	  Cursor{m, next, current, lower, upper, forward} = cursor
281	  View{m, lower, upper, Bool.not(forward)}
282	
283	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>>:
284	  (m, next) = r
285	  (Cursor{m, next, id, lower, upper, forward}, Some{entry})
286	
287	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>:
288	  match r:
289	    case Tuple{m, Some{old}}:
290	      (Cursor{m, next, current, lower, upper, forward}, Done{old})
291	    case Tuple{m, None{}}:
292	      (Cursor{m, next, current, lower, upper, forward}, Fail{NoCurrent{}})
293	
294	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>:
295	  (m, Search{id, p, on_left}) = r
296	  (Cursor{m, id, 0n, lower, upper, forward}, removed)
297	
298	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>:
299	  match r:
300	    case Tuple{cursor, None{}}:
301	      (cursor, None{})
302	    case Tuple{cursor, Some{Entry{k, v}}}:
303	      (cursor, Some{k})
304	
305	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>:
306	  match r:
307	    case Tuple{cursor, None{}}:
308	      (cursor, None{})
309	    case Tuple{cursor, Some{Entry{k, v}}}:
310	      (cursor, Some{v})
311	
312	def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Maybe<&2, V>) -> TreeMap<K, V, cmp> & Bool:
313	  match r:
314	    case Tuple{m, None{}}:
315	      (m, False{})
316	    case Tuple{m, Some{old}}:
317	      (m, True{})
318	
319	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:
320	  match r:
321	    case Tuple{view, None{}}:
322	      (view, False{})
323	    case Tuple{view, Some{x}}:
324	      (view, True{})
325	
326	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>>:
327	  match valid:
328	    case True{}:
329	      (View{m, lower, upper, descending}, Some{entry})
330	    case False{}:
331	      (View{m, lower, upper, descending}, None{})
332	
333	def child(~K: Data, +n: Node<K>, forward: Bool) -> Nat:
334	  pick(Nat, forward, node_right(~K, n), node_left(~K, n))
335	
336	# All links reference live slots. Free slots contain no key and no value.
337	
338	def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp> & Node<K>:
339	  match m id:
340	    case mm 0n:
341	      (mm, Free{0n})
342	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
343	      read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, D.get_at(~Node<K>, nodes, i))
344	
345	def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
346	  match m id:
347	    case mm 0n:
348	      mm
349	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
350	      write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, D.set_at(~Node<K>, nodes, i, node))
351	
352	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>:
353	  match m id:
354	    case mm 0n:
355	      (mm, None{})
356	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
357	      exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.swap_at(~Maybe<&2, V>, payloads, i, value))
358	
359	def append_values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, nodes: D.DynArray<&2, Node<K>>, +k: K, +v: V, +id: Nat, r: D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
360	  match r:
361	    case Tuple{payloads, Done{u}}:
362	      (TM{n, root, lo, hi, free, nodes, payloads}, Done{id})
363	    case Tuple{payloads, Fail{e}}:
364	      append_rollback(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, D.pop_at(~Node<K>, nodes))
365	
366	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>:
367	  TM{+n, root, +lo, +hi, free, nodes, payloads} = m
368	  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}
369	
370	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>:
371	  match m id:
372	    case mm 0n:
373	      (mm, None{})
374	    case TM{n, root, lo, hi, free, nodes, payloads} 1n+i:
375	      get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, D.get_at(~Maybe<&2, V>, payloads, i))
376	
377	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:
378	  match r:
379	    case Tuple{m, Free{next}}:
380	      (m, Ascend{0n, 0n, True{}})
381	    case Tuple{m, N{c, l, r, q, key}}:
382	      (m, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))
383	
384	def node_slot_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +i: Nat, +valid: Bool) -> Array<Maybe<&2, Node<K>>> & Node<K>:
385	  match valid:
386	    case False{}:
387	      (nodes, Free{0n})
388	    case True{}:
389	      node_slot_done(~K, ~V, ~cmp, Array.get(Maybe<&2, Node<K>>, nodes, U32.from_nat(i)))
390	
391	def ascend_slots_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, r: Array<Maybe<&2, Node<K>>> & Node<K>) -> Array<Maybe<&2, Node<K>>> & Ascend:
392	  match r:
393	    case Tuple{nodes, Free{next}}:
394	      (nodes, Ascend{0n, 0n, True{}})
395	    case Tuple{nodes, N{c, l, r, q, key}}:
396	      (nodes, ascend_choice(p, p, q, Nat.is_eq(x, pick(Nat, forward, l, r))))
397	
398	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>:
399	  (m3, +hi) = pair_result
400	  set_ends(~K, ~V, ~cmp, m3, lo, hi)
401	
402	def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Bool:
403	  is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))
404	
405	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>:
406	  (m, node) = r
407	  (m, node_key(~K, node))
408	
409	def above_lower(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
410	  match bound:
411	    case Unbounded{}:
412	      True{}
413	    case Inclusive{lo}:
414	      ordering_ok(cmp(lo, k), True{})
415	    case Exclusive{lo}:
416	      ordering_ok(cmp(lo, k), False{})
417	
418	def below_upper(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, bound: Bound<K>) -> Bool:
419	  match bound:
420	    case Unbounded{}:
421	      True{}
422	    case Inclusive{hi}:
423	      ordering_ok(cmp(k, hi), True{})
424	    case Exclusive{hi}:
425	      ordering_ok(cmp(k, hi), False{})
426	
427	def bounds_valid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: Bound<K>, upper: Bound<K>) -> Bool:
428	  match lower upper:
429	    case Unbounded{} _:
430	      True{}
431	    case _ Unbounded{}:
432	      True{}
433	    case Inclusive{lo} Inclusive{hi}:
434	      ordering_ok(cmp(lo, hi), True{})
435	    case Inclusive{lo} Exclusive{hi}:
436	      ordering_ok(cmp(lo, hi), True{})
437	    case Exclusive{lo} Inclusive{hi}:
438	      ordering_ok(cmp(lo, hi), True{})
439	    case Exclusive{lo} Exclusive{hi}:
440	      ordering_ok(cmp(lo, hi), True{})
441	
442	def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
443	  match forward:
444	    case True{}:
445	      first_id(~K, ~V, ~cmp, m)
446	    case False{}:
447	      last_id(~K, ~V, ~cmp, m)
448	
449	def iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
450	  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))
451	
452	def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
453	  cursor_started(~K, ~V, ~cmp, Unbounded{}, Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))
454	
455	def set_left_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
456	  match node:
457	    case Free{next}:
458	      m
459	    case N{c, l, r, p, k}:
460	      write(~K, ~V, ~cmp, m, id, N{c, v, r, p, k})
461	
462	def set_right_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
463	  match node:
464	    case Free{next}:
465	      m
466	    case N{c, l, r, p, k}:
467	      write(~K, ~V, ~cmp, m, id, N{c, l, v, p, k})
468	
469	def set_parent_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat, +node: Node<K>) -> TreeMap<K, V, cmp>:
470	  match node:
471	    case Free{next}:
472	      m
473	    case N{c, l, r, p, k}:
474	      write(~K, ~V, ~cmp, m, id, N{c, l, r, v, k})
475	
476	def set_red_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool, +node: Node<K>) -> TreeMap<K, V, cmp>:
477	  match node:
478	    case Free{next}:
479	      m
480	    case N{c, l, r, p, k}:
481	      write(~K, ~V, ~cmp, m, id, N{v, l, r, p, k})
482	
483	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):
484	  probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
485	
486	def append_nodes(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +id: Nat, r: D.DynArray<&2, Node<K>> & Result<&2, &2, DE.Error, Unit>) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
487	  match r:
488	    case Tuple{nodes, Done{u}}:
489	      append_values(~K, ~V, ~cmp, n, root, lo, hi, free, nodes, k, v, id, D.push_at(~Maybe<&2, V>, payloads, Some{v}))
490	    case Tuple{nodes, Fail{e}}:
491	      (TM{n, root, lo, hi, free, nodes, payloads}, Fail{Rejected{CapacityExceeded{}, k, v}})
492	
493	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>:
494	  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}))
495	
496	def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
497	  (m, Search{id, p, on_left}) = r
498	  get_id(~K, ~V, ~cmp, m, id)
499	
500	def extreme_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Nat:
501	  (m, node) = r
502	  (m, child(~K, node, forward))
503	
504	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:
505	  match fuel st:
506	    case 0n Tuple{m, state}:
507	      (m, 0n)
508	    case 1n+f Tuple{m, Ascend{x, p, True{}}}:
509	      (m, p)
510	    case 1n+f Tuple{m, Ascend{+x, +p, False{}}}:
511	      ascend_loop(~K, ~V, ~cmp, f, forward, ascend_step_node(~K, ~V, ~cmp, x, p, forward, read(~K, ~V, ~cmp, m, p)))
512	
513	def node_slot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +used: Nat, +id: Nat) -> Array<Maybe<&2, Node<K>>> & Node<K>:
514	  match id:
515	    case 0n:
516	      (nodes, Free{0n})
517	    case 1n+ +i:
518	      node_slot_checked(~K, ~V, ~cmp, nodes, i, Nat.is_lt(i, used))
519	
520	def extreme_slots_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: Array<Maybe<&2, Node<K>>> & Node<K>) -> Array<Maybe<&2, Node<K>>> & Nat:
521	  (nodes, node) = r
522	  (nodes, child(~K, node, forward))
523	
524	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>:
525	  match node:
526	    case Free{next}:
527	      m
528	    case N{c, l, r, p, old}:
529	      write(~K, ~V, ~cmp, m, id, N{c, l, r, p, k})
530	
531	def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
532	  TM{n, root, lo, hi, +free, nodes, payloads} = m
533	  release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id, Free{free}), id)
534	
535	def key_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
536	  (m, id) = r
537	  key_finish(~K, ~V, ~cmp, read(~K, ~V, ~cmp, m, id))
538	
539	def entry_snapshot_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, id: Nat, r: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>:
540	  (m, node) = r
541	  entry_value(~K, ~V, ~cmp, node_key(~K, node), get_id(~K, ~V, ~cmp, m, id))
542	
543	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>:
544	  match r:
545	    case Tuple{m, Search{0n, p, on_left}}:
546	      (m, None{})
547	    case Tuple{m, Search{1n+i, p, on_left}}:
548	      exchange(~K, ~V, ~cmp, m, 1n+i, Some{v})
549	
550	def in_range(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, lower: Bound<K>, upper: Bound<K>) -> Bool:
551	  Bool.and(above_lower(~K, ~V, ~cmp, k, lower), below_upper(~K, ~V, ~cmp, k, upper))
552	
553	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>>:
554	  view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, bounds_valid(~K, ~V, ~cmp, lower, upper))
555	
556	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>:
557	  match cursor:
558	    case Cursor{m, next, 0n, lower, upper, forward}:
559	      (Cursor{m, next, 0n, lower, upper, forward}, Fail{NoCurrent{}})
560	    case Cursor{m, next, 1n+ +id, lower, upper, forward}:
561	      iterator_set_done(~K, ~V, ~cmp, next, 1n+id, lower, upper, forward, exchange(~K, ~V, ~cmp, m, 1n+id, Some{v}))
562	
563	def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
564	  iterator(~K, ~V, ~cmp, m)
565	
566	def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
567	  iterator(~K, ~V, ~cmp, m)
568	
569	def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> Cursor<K, V, cmp>:
570	  iterator(~K, ~V, ~cmp, m)
571	
572	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:
573	  match equal:
574	    case False{}:
575	      (m, False{})
576	    case True{}:
577	      changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))
578	
579	def set_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
580	  (m1, +node) = pair_result
581	  set_left_node(~K, ~V, ~cmp, m1, id, v, node)
582	
583	def set_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
584	  (m1, +node) = pair_result
585	  set_right_node(~K, ~V, ~cmp, m1, id, v, node)
586	
587	def set_parent_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
588	  (m1, +node) = pair_result
589	  set_parent_node(~K, ~V, ~cmp, m1, id, v, node)
590	
591	def set_red_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Bool, pair_result: TreeMap<K, V, cmp> & Node<K>) -> TreeMap<K, V, cmp>:
592	  (m1, +node) = pair_result
593	  set_red_node(~K, ~V, ~cmp, m1, id, v, node)
594	
595	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:
596	  match fuel st:
597	    case 0n Tuple{m, node}:
598	      (m, Search{0n, p, on_left})
599	    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
600	      (m, Search{0n, p, on_left})
601	    case 1n+f Tuple{m, Tuple{N{c, +l, r, p0, key}, LT{}}}:
602	      search_loop(~K, ~V, ~cmp, f, k, l, id, True{}, probe(~K, ~V, ~cmp, m, l, k))
603	    case 1n+f Tuple{m, Tuple{N{c, l, +r, p0, key}, GT{}}}:
604	      search_loop(~K, ~V, ~cmp, f, k, r, id, False{}, probe(~K, ~V, ~cmp, m, r, k))
605	    case 1n+f Tuple{m, Tuple{N{c, l, r, p0, key}, EQ{}}}:
606	      (m, Search{id, p, on_left})
607	
608	def append_count(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, payloads: D.DynArray<&2, Maybe<&2, V>>, +k: K, +v: V, +p: Nat, r: D.DynArray<&2, Node<K>> & Nat) -> TreeMap<K, V, cmp> & Result<&2, &2, Rejected<K, V>, Nat>:
609	  (nodes, +used) = r
610	  append_nodes(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, 1n+used, D.push_at(~Node<K>, nodes, N{True{}, 0n, 0n, p, k}))
611	
612	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>:
613	  match r:
614	    case Tuple{m, Free{next}}:
615	      reuse_slot(~K, ~V, ~cmp, m, id, next, p, k, v)
616	    case Tuple{m, N{c, l, r, q, oldk}}:
617	      (m, Fail{Rejected{CapacityExceeded{}, k, v}})
618	
619	def extreme_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:
620	  match fuel st:
621	    case 0n Tuple{m, next}:
622	      (m, id)
623	    case 1n+p Tuple{m, 0n}:
624	      (m, id)
625	    case 1n+p Tuple{m, 1n+ +j}:
626	      extreme_loop(~K, ~V, ~cmp, p, forward, 1n+j, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, m, 1n+j)))
627	
628	def ascend_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +used: Nat, +forward: Bool, st: Array<Maybe<&2, Node<K>>> & Ascend) -> Array<Maybe<&2, Node<K>>> & Nat:
629	  match fuel st:
630	    case 0n Tuple{nodes, state}:
631	      (nodes, 0n)
632	    case 1n+f Tuple{nodes, Ascend{x, p, True{}}}:
633	      (nodes, p)
634	    case 1n+f Tuple{nodes, Ascend{+x, +p, False{}}}:
635	      ascend_slots_loop(~K, ~V, ~cmp, f, used, forward, ascend_slots_step(~K, ~V, ~cmp, x, p, forward, node_slot(~K, ~V, ~cmp, nodes, used, p)))
636	
637	def extreme_slots_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +used: Nat, +forward: Bool, +id: Nat, st: Array<Maybe<&2, Node<K>>> & Nat) -> Array<Maybe<&2, Node<K>>> & Nat:
638	  match fuel st:
639	    case 0n Tuple{nodes, next}:
640	      (nodes, id)
641	    case 1n+f Tuple{nodes, 0n}:
642	      (nodes, id)
643	    case 1n+f Tuple{nodes, 1n+ +j}:
644	      extreme_slots_loop(~K, ~V, ~cmp, f, used, forward, 1n+j, extreme_slots_probe(~K, ~V, ~cmp, forward, node_slot(~K, ~V, ~cmp, nodes, used, 1n+j)))
645	
646	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>:
647	  (m1, +node) = pair_result
648	  set_key_node(~K, ~V, ~cmp, m1, id, k, node)
649	
650	def first_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
651	  key_id(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
652	
653	def last_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp> & Maybe<&2, K>:
654	  key_id(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
655	
656	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>>:
657	  (m, +id) = r
658	  entry_snapshot_value(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
659	
660	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:
661	  match r:
662	    case Tuple{m, None{}}:
663	      (m, False{})
664	    case Tuple{m, Some{old}}:
665	      replace_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
666	
667	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:
668	  match r:
669	    case Tuple{m, Free{free}}:
670	      (Cursor{m, next, current, lower, upper, forward}, False{})
671	    case Tuple{m, N{c, l, rr, p, key}}:
672	      (Cursor{m, next, current, lower, upper, forward}, in_range(~K, ~V, ~cmp, key, lower, upper))
673	
674	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>>:
675	  match r:
676	    case Tuple{m, None{}}:
677	      (View{m, lower, upper, descending}, None{})
678	    case Tuple{m, Some{Entry{+k, v}}}:
679	      view_entry_checked(~K, ~V, ~cmp, m, lower, upper, descending, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))
680	
681	def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
682	  set_left_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
683	
684	def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
685	  set_right_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
686	
687	def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Nat) -> TreeMap<K, V, cmp>:
688	  set_parent_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
689	
690	def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +v: Bool) -> TreeMap<K, V, cmp>:
691	  set_red_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))
692	
693	def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Search:
694	  TM{+n, +root, lo, hi, free, nodes, payloads} = m
695	  search_loop(~K, ~V, ~cmp, 1n+n, k, root, 0n, False{}, probe(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, root, k))
696	
697	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>:
698	  TM{n, root, lo, hi, free, nodes, payloads} = m
699	  append_count(~K, ~V, ~cmp, n, root, lo, hi, free, payloads, k, v, p, D.length(Node<K>, nodes))
700	
701	def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
702	  TM{+n, root, lo, hi, free, nodes, payloads} = m
703	  extreme_loop(~K, ~V, ~cmp, 1n+n, forward, id, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, id)))
704	
705	
706	def neighbor_slots(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, nodes: Array<Maybe<&2, Node<K>>>, +n: Nat, +used: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> Array<Maybe<&2, Node<K>>> & Nat:
707	  match c:
708	    case 0n:
709	      ascend_slots_loop(~K, ~V, ~cmp, 1n+n, used, forward, (nodes, Ascend{id, p, False{}}))
710	    case 1n+ +j:
711	      extreme_slots_loop(~K, ~V, ~cmp, 1n+n, used, Bool.not(forward), 1n+j, extreme_slots_probe(~K, ~V, ~cmp, Bool.not(forward), node_slot(~K, ~V, ~cmp, nodes, used, 1n+j)))
712	
713	def set_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +k: K) -> TreeMap<K, V, cmp>:
714	  set_key_1(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))
715	
716	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>>:
717	  entry_snapshot(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
718	
719	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>>:
720	  entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
721	
722	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:
723	  (m, Search{+id, p, on_left}) = r
724	  replace_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
725	
726	def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Bool:
727	  Cursor{m, +next, current, lower, upper, forward} = cursor
728	  iterator_has_checked(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
729	
730	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>:
731	  match p on_left:
732	    case 0n _:
733	      set_root(~K, ~V, ~cmp, m, x)
734	    case 1n+q True{}:
735	      set_left(~K, ~V, ~cmp, m, 1n+q, x)
736	    case 1n+q False{}:
737	      set_right(~K, ~V, ~cmp, m, 1n+q, x)
738	
739	def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
740	  (m1, +r) = pair_result
741	  set_red(~K, ~V, ~cmp, m1, r, False{})
742	
743	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>:
744	  TM{n, root, lo, hi, free, nodes, payloads} = m
745	  match free:
746	    case 0n:
747	      append(~K, ~V, ~cmp, TM{n, root, lo, hi, 0n, nodes, payloads}, k, v, p)
748	    case 1n+ +f:
749	      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))
750	
751	def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
752	  get_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
753	
754	def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Bool:
755	  contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
756	
757	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:
758	  (TM{+n, root, lo, hi, free, D.DA{limit, depth, cap, +used, nodes}, payloads}, +node) = r
759	  neighbor_slots_finish(~K, ~V, ~cmp, n, root, lo, hi, free, limit, depth, cap, used, payloads, neighbor_slots(~K, ~V, ~cmp, nodes, n, used, id, node_parent(~K, node), forward, child(~K, node, forward)))
760	
761	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>:
762	  match node:
763	    case Free{next}:
764	      m
765	    case N{c, l, r, p, k}:
766	      set_key(~K, ~V, ~cmp, m, target, k)
767	
768	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>:
769	  (m2, +lo) = pair_result
770	  refresh_ends_3(~K, ~V, ~cmp, lo, extreme(~K, ~V, ~cmp, m2, r, True{}))
771	
772	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>:
773	  replace_found(~K, ~V, ~cmp, v, search(~K, ~V, ~cmp, m, k))
774	
775	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>:
776	  match k r:
777	    case None{} Tuple{m, removed}:
778	      (Cursor{m, 0n, 0n, lower, upper, forward}, removed)
779	    case Some{key} Tuple{m, removed}:
780	      iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, removed, search(~K, ~V, ~cmp, m, key))
781	
782	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:
783	  replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))
784	
785	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>:
786	  set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)
787	
788	def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
789	  black_root_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
790	
791	
792	def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +forward: Bool) -> TreeMap<K, V, cmp> & Nat:
793	  neighbor_node(~K, ~V, ~cmp, id, forward, read(~K, ~V, ~cmp, m, id))
794	
795	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:
796	  (m2, value) = pair_result
797	  move_successor_3(~K, ~V, ~cmp, source, exchange(~K, ~V, ~cmp, copy_key(~K, ~V, ~cmp, m2, target, source_node), target, value))
798	
799	def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
800	  (m1, +r) = pair_result
801	  refresh_ends_2(~K, ~V, ~cmp, r, extreme(~K, ~V, ~cmp, m1, r, False{}))
802	
803	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:
804	  default_value(~K, ~V, ~cmp, fallback, get(~K, ~V, ~cmp, m, k))
805	
806	
807	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>:
808	  match valid:
809	    case True{}:
810	      view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k))
811	    case False{}:
812	      (View{m, lower, upper, descending}, None{})
813	
814	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>:
815	  (m3, +pn) = pair_result
816	  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))
817	
818	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>:
819	  (m3, +pn) = pair_result
820	  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))
821	
822	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:
823	  (m1, +source_node) = pair_result
824	  move_successor_2(~K, ~V, ~cmp, target, source, source_node, exchange(~K, ~V, ~cmp, m1, source, None{}))
825	
826	def refresh_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>) -> TreeMap<K, V, cmp>:
827	  refresh_ends_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))
828	
829	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:
830	  match inclusive:
831	    case True{}:
832	      (m, id)
833	    case False{}:
834	      neighbor(~K, ~V, ~cmp, m, id, higher)
835	
836	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>:
837	  View{m, +lower, +upper, descending} = view
838	  view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
839	
840	def iterator_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat, +current: Nat, lower: Bound<K>, upper: Bound<K>, +forward: Bool, entry: Entry<K, V>, +valid: Bool) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
841	  match valid:
842	    case True{}:
843	      iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor(~K, ~V, ~cmp, m, id, forward))
844	    case False{}:
845	      (Cursor{m, 0n, current, lower, upper, forward}, None{})
846	
847	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>:
848	  (m2, +yn) = pair_result
849	  rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
850	
851	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>:
852	  (m2, +yn) = pair_result
853	  rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, node_parent(~K, xn)))
854	
855	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:
856	  move_successor_1(~K, ~V, ~cmp, target, source, read(~K, ~V, ~cmp, m, source))
857	
858	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:
859	  match fuel st:
860	    case 0n Tuple{m, node}:
861	      (m, best)
862	    case 1n+f Tuple{m, Tuple{Free{next}, order}}:
863	      (m, best)
864	    case 1n+f Tuple{m, Tuple{N{c, +l, r, p, key}, LT{}}}:
865	      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, l, pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, m, l, k))
866	    case 1n+f Tuple{m, Tuple{N{c, l, +r, p, key}, GT{}}}:
867	      nav_loop(~K, ~V, ~cmp, f, k, higher, inclusive, r, pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, m, r, k))
868	    case 1n+f Tuple{m, Tuple{node, EQ{}}}:
869	      nav_equal(~K, ~V, ~cmp, m, id, higher, inclusive)
870	
871	def iterator_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +current: Nat, +lower: Bound<K>, +upper: Bound<K>, +forward: Bool, r: TreeMap<K, V, cmp> & Maybe<&2, Entry<K, V>>) -> Cursor<K, V, cmp> & Maybe<&2, Entry<K, V>>:
872	  match r:
873	    case Tuple{m, None{}}:
874	      (Cursor{m, 0n, current, lower, upper, forward}, None{})
875	    case Tuple{m, Some{Entry{+k, v}}}:
876	      iterator_checked(~K, ~V, ~cmp, m, id, current, lower, upper, forward, Entry{k, v}, in_range(~K, ~V, ~cmp, k, lower, upper))
877	
878	def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>, +k: K) -> View<K, V, cmp> & Bool:
879	  view_contains_value(~K, ~V, ~cmp, view_get(~K, ~V, ~cmp, view, k))
880	
881	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>:
882	  (m1, +xn) = pair_result
883	  rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_right(~K, xn)))
884	
885	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>:
886	  (m1, +xn) = pair_result
887	  rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, node_left(~K, xn)))
888	
889	def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp> & Nat:
890	  (m, source) = r
891	  move_successor(~K, ~V, ~cmp, m, target, source)
892	
893	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:
894	  TM{+n, +root, lo, hi, free, nodes, payloads} = m
895	  nav_loop(~K, ~V, ~cmp, 1n+n, k, higher, inclusive, root, 0n, probe(~K, ~V, ~cmp, TM{n, root, lo, hi, free, nodes, payloads}, root, k))
896	
897	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>>:
898	  Cursor{m, +next, current, lower, upper, forward} = cursor
899	  iterator_read(~K, ~V, ~cmp, next, current, lower, upper, forward, entry_snapshot(~K, ~V, ~cmp, (m, next)))
900	
901	def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
902	  rotate_left_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
903	
904	def rotate_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +x: Nat) -> TreeMap<K, V, cmp>:
905	  rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))
906	
907	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:
908	  match r:
909	    case Tuple{m, N{c, 1n+l, 1n+r, p, k}}:
910	      successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, m, 1n+r, False{}))
911	    case Tuple{m, node}:
912	      (m, id)
913	
914	
915	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>:
916	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
917	
918	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>:
919	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
920	
921	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>:
922	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
923	
924	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>:
925	  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
926	
927	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>>:
928	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))
929	
930	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>>:
931	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))
932	
933	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>>:
934	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))
935	
936	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>>:
937	  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))
938	
939	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:
940	  match bound:
941	    case Unbounded{}:
942	      range_unbounded(~K, ~V, ~cmp, m, forward)
943	    case Inclusive{k}:
944	      navigate(~K, ~V, ~cmp, m, k, forward, True{})
945	    case Exclusive{k}:
946	      navigate(~K, ~V, ~cmp, m, k, forward, False{})
947	
948	def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, K>:
949	  iterator_key_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
950	
951	def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
952	  iterator_value_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))
953	
954	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:
955	  match fuel found st:
956	    case _ True{} Tuple{cursor, item}:
957	      (iterator_finish(~K, ~V, ~cmp, cursor), True{})
958	    case 0n False{} Tuple{cursor, item}:
959	      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
960	    case 1n+f False{} Tuple{cursor, None{}}:
961	      (iterator_finish(~K, ~V, ~cmp, cursor), False{})
962	    case 1n+f False{} Tuple{cursor, Some{Entry{k, v}}}:
963	      contains_value_loop(~K, ~V, ~cmp, ~eq, f, wanted, eq(v, wanted), iterator_next(~K, ~V, ~cmp, cursor))
964	
965	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:
966	  match fuel st:
967	    case 0n Tuple{cursor, item}:
968	      (iterator_view(~K, ~V, ~cmp, cursor), count)
969	    case 1n+f Tuple{cursor, None{}}:
970	      (iterator_view(~K, ~V, ~cmp, cursor), count)
971	    case 1n+f Tuple{cursor, Some{item}}:
972	      view_count_loop(~K, ~V, ~cmp, f, 1n+count, iterator_next(~K, ~V, ~cmp, cursor))
973	
974	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>>:
975	  (cursor, removed) = r
976	  iterator_next(~K, ~V, ~cmp, cursor)
977	
978	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:
979	  match triangle:
980	    case True{}:
981	      (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{}})
982	    case False{}:
983	      (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
984	
985	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:
986	  match triangle:
987	    case True{}:
988	      (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{}})
989	    case False{}:
990	      (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), Fix{0n, False{}})
991	
992	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:
993	  (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{}})
994	
995	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:
996	  (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{}})
997	
998	def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> Cursor<K, V, cmp>:
999	  View{m, +lower, +upper, +descending} = view
1000	  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)))
1001	
1002	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:
1003	  (m, n) = r
1004	  contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+n, wanted, False{}, iterator_next(~K, ~V, ~cmp, iterator(~K, ~V, ~cmp, m)))
1005	
1006	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:
1007	  match within:
1008	    case True{}:
1009	      navigate(~K, ~V, ~cmp, m, k, higher, inclusive)
1010	    case False{}:
1011	      range_start(~K, ~V, ~cmp, m, pick(Bound<K>, higher, lower, upper), higher)
1012	
1013	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>>:
1014	  View{m, +lower, +upper, +descending} = view
1015	  +up = pick(Bool, descending, Bool.not(first), first)
1016	  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)))
1017	
1018	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:
1019	  match uncle:
1020	    case N{True{}, l, r, gp, k}:
1021	      (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{}})
1022	    case _:
1023	      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)
1024	
1025	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:
1026	  match uncle:
1027	    case N{True{}, l, r, gp, k}:
1028	      (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{}})
1029	    case _:
1030	      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)
1031	
1032	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:
1033	  (m2, +wn) = pair_result
1034	  delete_borrow_left(~K, ~V, ~cmp, m2, p, node_right(~K, pn), pn, wn)
1035	
1036	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:
1037	  (m2, +wn) = pair_result
1038	  delete_borrow_right(~K, ~V, ~cmp, m2, p, node_left(~K, pn), pn, wn)
1039	
1040	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:
1041	  contains_value_start(~K, ~V, ~cmp, ~eq, wanted, size(~K, ~V, ~cmp, m))
1042	
1043	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>>:
1044	  View{m, +lower, +upper, +descending} = view
1045	  +up = pick(Bool, descending, Bool.not(higher), higher)
1046	  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)))))
1047	
1048	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>>:
1049	  view_extreme(~K, ~V, ~cmp, view, True{})
1050	
1051	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>>:
1052	  view_extreme(~K, ~V, ~cmp, view, False{})
1053	
1054	def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp> & Nat:
1055	  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1056	  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})))
1057	
1058	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:
1059	  (m1, +un) = pair_result
1060	  insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, node_right(~K, gn), Nat.is_eq(z, node_right(~K, pn)), un)
1061	
1062	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:
1063	  (m1, +un) = pair_result
1064	  insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, node_left(~K, gn), Nat.is_eq(z, node_left(~K, pn)), un)
1065	
1066	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:
1067	  (m1, +pn) = pair_result
1068	  delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1069	
1070	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:
1071	  (m1, +pn) = pair_result
1072	  delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1073	
1074	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>>:
1075	  view_nav(~K, ~V, ~cmp, view, k, False{}, False{})
1076	
1077	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>>:
1078	  view_nav(~K, ~V, ~cmp, view, k, False{}, True{})
1079	
1080	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>>:
1081	  view_nav(~K, ~V, ~cmp, view, k, True{}, True{})
1082	
1083	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>>:
1084	  view_nav(~K, ~V, ~cmp, view, k, True{}, False{})
1085	
1086	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:
1087	  insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_right(~K, gn)))
1088	
1089	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:
1090	  insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, node_left(~K, gn)))
1091	
1092	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:
1093	  delete_borrow_read_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1094	
1095	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:
1096	  delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1097	
1098	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:
1099	  match on_left:
1100	    case True{}:
1101	      insert_side_left(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1102	    case False{}:
1103	      insert_side_right(~K, ~V, ~cmp, m, z, p, g, pn, gn)
1104	
1105	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:
1106	  match far_red:
1107	    case True{}:
1108	      delete_borrow_left(~K, ~V, ~cmp, m, p, w, pn, wn)
1109	    case False{}:
1110	      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)
1111	
1112	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:
1113	  match far_red:
1114	    case True{}:
1115	      delete_borrow_right(~K, ~V, ~cmp, m, p, w, pn, wn)
1116	    case False{}:
1117	      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)
1118	
1119	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:
1120	  (m1, +gn) = pair_result
1121	  insert_side(~K, ~V, ~cmp, m1, z, p, node_parent(~K, pn), pn, gn, Nat.is_eq(p, node_left(~K, gn)))
1122	
1123	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:
1124	  match near_red far_red:
1125	    case False{} False{}:
1126	      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1127	    case _ _:
1128	      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1129	
1130	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:
1131	  match near_red far_red:
1132	    case False{} False{}:
1133	      (set_red(~K, ~V, ~cmp, m, w, True{}), DF{p, node_parent(~K, pn), True{}})
1134	    case _ _:
1135	      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
1136	
1137	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:
1138	  insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, node_parent(~K, pn)))
1139	
1140	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:
1141	  (m4, +far_node) = pair_result
1142	  delete_children_left(~K, ~V, ~cmp, m4, p, node_right(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1143	
1144	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:
1145	  (m4, +far_node) = pair_result
1146	  delete_children_right(~K, ~V, ~cmp, m4, p, node_left(~K, pn), pn, wn, node_red(~K, near_node), node_red(~K, far_node))
1147	
1148	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:
1149	  match is_red:
1150	    case False{}:
1151	      (m, Fix{0n, False{}})
1152	    case True{}:
1153	      insert_grand(~K, ~V, ~cmp, m, z, p, pn)
1154	
1155	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:
1156	  (m3, +near_node) = pair_result
1157	  delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_right(~K, wn)))
1158	
1159	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:
1160	  (m3, +near_node) = pair_result
1161	  delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, node_left(~K, wn)))
1162	
1163	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:
1164	  (m2, +pn) = pair_result
1165	  insert_parent(~K, ~V, ~cmp, m2, z, node_parent(~K, zn), pn, node_red(~K, pn))
1166	
1167	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:
1168	  (m2, +wn) = pair_result
1169	  delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_left(~K, wn)))
1170	
1171	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:
1172	  (m2, +wn) = pair_result
1173	  delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, node_right(~K, wn)))
1174	
1175	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:
1176	  (m1, +zn) = pair_result
1177	  insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, node_parent(~K, zn)))
1178	
1179	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:
1180	  (m1, +pn) = pair_result
1181	  delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_right(~K, pn)))
1182	
1183	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:
1184	  (m1, +pn) = pair_result
1185	  delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, node_left(~K, pn)))
1186	
1187	def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +z: Nat) -> TreeMap<K, V, cmp> & Fix:
1188	  insert_fix_step_1(~K, ~V, ~cmp, z, read(~K, ~V, ~cmp, m, z))
1189	
1190	def delete_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1191	  delete_sibling_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1192	
1193	def delete_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +p: Nat) -> TreeMap<K, V, cmp> & DeleteFix:
1194	  delete_sibling_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))
1195	
1196	def insert_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & Fix) -> TreeMap<K, V, cmp>:
1197	  match fuel st:
1198	    case 0n Tuple{m, f}:
1199	      black_root(~K, ~V, ~cmp, m)
1200	    case 1n+p Tuple{m, Fix{z, False{}}}:
1201	      black_root(~K, ~V, ~cmp, m)
1202	    case 1n+p Tuple{m, Fix{z, True{}}}:
1203	      insert_fix_loop(~K, ~V, ~cmp, p, insert_fix_step(~K, ~V, ~cmp, m, z))
1204	
1205	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:
1206	  match red_sibling:
1207	    case True{}:
1208	      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)
1209	    case False{}:
1210	      delete_sibling_left(~K, ~V, ~cmp, m, p)
1211	
1212	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:
1213	  match red_sibling:
1214	    case True{}:
1215	      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)
1216	    case False{}:
1217	      delete_sibling_right(~K, ~V, ~cmp, m, p)
1218	
1219	def insert_fixed(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1220	  (m, n) = r
1221	  insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, Fix{id, True{}}))
1222	
1223	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:
1224	  (m1, +wn) = pair_result
1225	  delete_red_sibling_left(~K, ~V, ~cmp, m1, p, node_right(~K, pn), node_red(~K, wn))
1226	
1227	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:
1228	  (m1, +wn) = pair_result
1229	  delete_red_sibling_right(~K, ~V, ~cmp, m1, p, node_left(~K, pn), node_red(~K, wn))
1230	
1231	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>>:
1232	  match r:
1233	    case Tuple{m, Done{+id}}:
1234	      (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{}})
1235	    case Tuple{m, Fail{e}}:
1236	      (m, Fail{e})
1237	
1238	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:
1239	  delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_right(~K, pn)))
1240	
1241	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:
1242	  delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, node_left(~K, pn)))
1243	
1244	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>>:
1245	  match r:
1246	    case Tuple{m, Search{0n, +p, +on_left}}:
1247	      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1248	    case Tuple{m, Search{1n+i, p, on_left}}:
1249	      put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, 1n+i, Some{v}))
1250	
1251	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:
1252	  match on_left:
1253	    case True{}:
1254	      delete_side_left(~K, ~V, ~cmp, m, p, pn)
1255	    case False{}:
1256	      delete_side_right(~K, ~V, ~cmp, m, p, pn)
1257	
1258	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>>:
1259	  match r:
1260	    case Tuple{m, Search{0n, +p, +on_left}}:
1261	      put_allocated(~K, ~V, ~cmp, p, on_left, allocate(~K, ~V, ~cmp, m, p, k, v))
1262	    case Tuple{m, Search{1n+i, p, on_left}}:
1263	      put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, m, 1n+i))
1264	
1265	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>>:
1266	  put_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1267	
1268	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:
1269	  match stop:
1270	    case True{}:
1271	      (set_red(~K, ~V, ~cmp, m, x, False{}), DF{0n, 0n, False{}})
1272	    case False{}:
1273	      delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, node_left(~K, pn)))
1274	
1275	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>>:
1276	  put_absent_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))
1277	
1278	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:
1279	  (m3, +pn) = pair_result
1280	  delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), node_red(~K, xn)))
1281	
1282	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>>:
1283	  match valid:
1284	    case True{}:
1285	      view_put_finish(~K, ~V, ~cmp, lower, upper, descending, put(~K, ~V, ~cmp, m, k, v))
1286	    case False{}:
1287	      (View{m, lower, upper, descending}, Fail{Rejected{OutOfRange{}, k, v}})
1288	
1289	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:
1290	  (m2, +xn) = pair_result
1291	  delete_fix_step_3(~K, ~V, ~cmp, x, p, root_node, xn, read(~K, ~V, ~cmp, m2, p))
1292	
1293	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>>:
1294	  View{m, +lower, +upper, descending} = view
1295	  view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1296	
1297	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:
1298	  (m1, +root_node) = pair_result
1299	  delete_fix_step_2(~K, ~V, ~cmp, x, p, root_node, read(~K, ~V, ~cmp, m1, x))
1300	
1301	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:
1302	  delete_fix_step_1(~K, ~V, ~cmp, x, p, root_id(~K, ~V, ~cmp, m))
1303	
1304	def delete_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: TreeMap<K, V, cmp> & DeleteFix) -> TreeMap<K, V, cmp>:
1305	  match fuel st:
1306	    case 0n Tuple{m, fix}:
1307	      black_root(~K, ~V, ~cmp, m)
1308	    case 1n+f Tuple{m, DF{x, p, False{}}}:
1309	      black_root(~K, ~V, ~cmp, m)
1310	    case 1n+f Tuple{m, DF{x, p, True{}}}:
1311	      delete_fix_loop(~K, ~V, ~cmp, f, delete_fix_step(~K, ~V, ~cmp, m, x, p))
1312	
1313	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>:
1314	  TM{+n, root, lo, hi, free, nodes, payloads} = m
1315	  delete_fix_loop(~K, ~V, ~cmp, 1n+n, (TM{n, root, lo, hi, free, nodes, payloads}, DF{x, p, Bool.not(was_red)}))
1316	
1317	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>:
1318	  (m2, +pn) = pair_result
1319	  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))
1320	
1321	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>:
1322	  (m1, +node) = pair_result
1323	  unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, node_parent(~K, node)))
1324	
1325	def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +id: Nat) -> TreeMap<K, V, cmp>:
1326	  unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1327	
1328	def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Nat) -> TreeMap<K, V, cmp>:
1329	  (m, id) = r
1330	  refresh_ends(~K, ~V, ~cmp, unlink(~K, ~V, ~cmp, m, id))
1331	
1332	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>:
1333	  (m1, value) = pair_result
1334	  (unlink_target(~K, ~V, ~cmp, delete_target(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m1, id))), value)
1335	
1336	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>:
1337	  remove_present_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, m, id, None{}))
1338	
1339	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>:
1340	  match id:
1341	    case 0n:
1342	      (m, None{})
1343	    case 1n+i:
1344	      remove_present(~K, ~V, ~cmp, m, 1n+i)
1345	
1346	def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: TreeMap<K, V, cmp> & Search) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1347	  (m, Search{id, p, on_left}) = r
1348	  remove_id(~K, ~V, ~cmp, m, id)
1349	
1350	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>>:
1351	  (m1, +node) = pair_result
1352	  entry_value(~K, ~V, ~cmp, node_key(~K, node), remove_id(~K, ~V, ~cmp, m1, id))
1353	
1354	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>:
1355	  (m1, +node) = pair_result
1356	  iterator_reseek(~K, ~V, ~cmp, node_key(~K, node), lower, upper, forward, remove_id(~K, ~V, ~cmp, m1, current))
1357	
1358	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:
1359	  match equal:
1360	    case False{}:
1361	      (m, False{})
1362	    case True{}:
1363	      changed_value(~K, ~V, ~cmp, remove_id(~K, ~V, ~cmp, m, id))
1364	
1365	def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: TreeMap<K, V, cmp>, +k: K) -> TreeMap<K, V, cmp> & Maybe<&2, V>:
1366	  remove_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))
1367	
1368	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>>:
1369	  remove_entry_id_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))
1370	
1371	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>:
1372	  iterator_delete_1(~K, ~V, ~cmp, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))
1373	
1374	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:
1375	  match r:
1376	    case Tuple{m, None{}}:
1377	      (m, False{})
1378	    case Tuple{m, Some{old}}:
1379	      remove_if_apply(~K, ~V, ~cmp, m, id, replacement, eq(old, expected))
1380	
1381	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>>:
1382	  (m, id) = r
1383	  remove_entry_id(~K, ~V, ~cmp, m, id)
1384	
1385	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>:
1386	  match valid:
1387	    case True{}:
1388	      view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k))
1389	    case False{}:
1390	      (View{m, lower, upper, descending}, None{})
1391	
1392	def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: Cursor<K, V, cmp>) -> Cursor<K, V, cmp> & Maybe<&2, V>:
1393	  Cursor{m, next, current, lower, upper, forward} = cursor
1394	  iterator_delete(~K, ~V, ~cmp, m, next, current, lower, upper, forward)
1395	
1396	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:
1397	  (m, Search{+id, p, on_left}) = r
1398	  remove_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))
1399	
1400	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>>:
1401	  poll_ready(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))
1402	
1403	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>>:
1404	  poll_ready(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))
1405	
1406	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>:
1407	  View{m, +lower, +upper, descending} = view
1408	  view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, in_range(~K, ~V, ~cmp, k, lower, upper))
1409	
1410	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:
1411	  remove_if_found(~K, ~V, ~cmp, ~eq, expected, expected, search(~K, ~V, ~cmp, m, k))
1412	
1413	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>:
1414	  match fuel st:
1415	    case 0n Tuple{cursor, item}:
1416	      iterator_view(~K, ~V, ~cmp, cursor)
1417	    case 1n+f Tuple{cursor, None{}}:
1418	      iterator_view(~K, ~V, ~cmp, cursor)
1419	    case 1n+f Tuple{cursor, Some{item}}:
1420	      view_clear_loop(~K, ~V, ~cmp, f, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, cursor)))
1421	
1422	def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: View<K, V, cmp>) -> View<K, V, cmp>:
1423	  View{TM{+n, root, lo, hi, free, nodes, payloads}, lower, upper, descending} = view
1424	  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})))