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