1	import Base
2	import ./map_bridge.bend as MB
3	import ./native_map.bend as N
4	
5	# Projections of actual native results; no alternative lookup algorithm.
6	def value(-V: Data, result: Map<&2, V> & V) -> V:
7	  (tree, found) = result
8	  found
9	
10	def lookup(-V: Data, d: V, m: Map<&2, V>, key: String) -> V:
11	  value(V, Map.get(V, d, m, key))
12	
13	def route_bit(r: String & Bool) -> Bool:
14	  (key, bit) = r
15	  bit
16	
17	law route_pair:
18	  for r: String & Bool
19	  {r == (N.routed_key(r), route_bit(r)) : String & Bool}
20	def route_pair(r):
21	  match r:
22	    case Tuple{key, bit}:
23	      {==}
24	
25	law route_shape:
26	  for +key: String
27	  for +position: Nat
28	  {Map.bit(key, position) == (key, route_bit(Map.bit(key, position))) : String & Bool}
29	def route_shape(key, position):
30	  %N.bit_preserves_key(key, position) : {Map.bit(key, position) == (_, route_bit(Map.bit(key, position))) : String & Bool}
31	  route_pair(Map.bit(key, position))
32	
33	law low_value:
34	  for -V: Data
35	  for p: Nat
36	  for hi: Map<&2, V>
37	  for r: Map<&2, V> & V
38	  {value(V, Map.lo(&2, V, V, p, hi, r)) == value(V, r) : V}
39	def low_value(V, p, hi, r):
40	  match r:
41	    case Tuple{tree, found}:
42	      {==}
43	
44	law high_value:
45	  for -V: Data
46	  for p: Nat
47	  for lo: Map<&2, V>
48	  for r: Map<&2, V> & V
49	  {value(V, Map.hi(&2, V, V, p, lo, r)) == value(V, r) : V}
50	def high_value(V, p, lo, r):
51	  match r:
52	    case Tuple{tree, found}:
53	      {==}
54	
55	law node_left:
56	  for -V: Data
57	  for +d: V
58	  for +lo: Map<&2, V>
59	  for +hi: Map<&2, V>
60	  for +p: Nat
61	  for +key: String
62	  for e: {Map.bit(key, p) == (key, False{}) : String & Bool}
63	  {lookup(V, d, MNode{p, lo, hi}, key) == lookup(V, d, lo, key) : V}
64	def node_left(V, d, lo, hi, p, key, e):
65	  %Equal.sym(Map<&2, V> & V, Map.get(V, d, MNode{p, lo, hi}, key), MB.get_bit(V, d, lo, hi, p, Map.bit(key, p)), MB.get_node(V, d, p, lo, hi, key)) : {value(V, _) == lookup(V, d, lo, key) : V}
66	  %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {value(V, MB.get_bit(V, d, lo, hi, p, _)) == lookup(V, d, lo, key) : V}
67	  low_value(V, p, hi, Map.get(V, d, lo, key))
68	
69	law node_right:
70	  for -V: Data
71	  for +d: V
72	  for +lo: Map<&2, V>
73	  for +hi: Map<&2, V>
74	  for +p: Nat
75	  for +key: String
76	  for e: {Map.bit(key, p) == (key, True{}) : String & Bool}
77	  {lookup(V, d, MNode{p, lo, hi}, key) == lookup(V, d, hi, key) : V}
78	def node_right(V, d, lo, hi, p, key, e):
79	  %Equal.sym(Map<&2, V> & V, Map.get(V, d, MNode{p, lo, hi}, key), MB.get_bit(V, d, lo, hi, p, Map.bit(key, p)), MB.get_node(V, d, p, lo, hi, key)) : {value(V, _) == lookup(V, d, hi, key) : V}
80	  %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {value(V, MB.get_bit(V, d, lo, hi, p, _)) == lookup(V, d, hi, key) : V}
81	  high_value(V, p, lo, Map.get(V, d, hi, key))
82	
83	law leaf_same:
84	  for -V: Data
85	  for d: V
86	  for key: String
87	  for x: V
88	  {lookup(V, d, MLeaf{key, x}, key) == x : V}
89	def leaf_same(V, d, key, x):
90	  Equal.cong(Map<&2, V> & V, V, r => value(V, r), Map.get(V, d, MLeaf{key, x}, key), (MLeaf{key, x}, x), N.singleton_get(V, d, key, x))
91	
92	law splice_same_bit:
93	  for -V: Data
94	  for +d: V
95	  for +x: V
96	  for +rest: Map<&2, V>
97	  for +p: Nat
98	  for +key: String
99	  for bit: Bool
100	  for e: {Map.bit(key, p) == (key, bit) : String & Bool}
101	  {lookup(V, d, Map.ins.splice.bit(&2, V, x, rest, p, (key, bit)), key) == x : V}
102	def splice_same_bit(V, d, x, rest, p, key, bit, e):
103	  match bit:
104	    case False{}:
105	      Equal.trans(V, lookup(V, d, MNode{p, MLeaf{key, x}, rest}, key), lookup(V, d, MLeaf{key, x}, key), x, node_left(V, d, MLeaf{key, x}, rest, p, key, e), leaf_same(V, d, key, x))
106	    case True{}:
107	      Equal.trans(V, lookup(V, d, MNode{p, rest, MLeaf{key, x}}, key), lookup(V, d, MLeaf{key, x}, key), x, node_right(V, d, rest, MLeaf{key, x}, p, key, e), leaf_same(V, d, key, x))
108	
109	law splice_same:
110	  for -V: Data
111	  for d: V
112	  for x: V
113	  for rest: Map<&2, V>
114	  for +p: Nat
115	  for +key: String
116	  {lookup(V, d, Map.ins.splice(&2, V, p, key, x, rest), key) == x : V}
117	def splice_same(V, d, x, rest, p, key):
118	  %Equal.sym(String & Bool, Map.bit(key, p), (key, route_bit(Map.bit(key, p))), route_shape(key, p)) : {lookup(V, d, Map.ins.splice.bit(&2, V, x, rest, p, _), key) == x : V}
119	  splice_same_bit(V, d, x, rest, p, key, route_bit(Map.bit(key, p)), route_shape(key, p))
120	
121	law deep_same_bit:
122	  for -V: Data
123	  for +d: V
124	  for +x: V
125	  for +lo: Map<&2, V>
126	  for +hi: Map<&2, V>
127	  for +p: Nat
128	  for +q: Nat
129	  for +key: String
130	  for bit: Bool
131	  for e: {Map.bit(key, q) == (key, bit) : String & Bool}
132	  for lp: {lookup(V, d, Map.ins(&2, V, lo, key, x, p), key) == x : V}
133	  for hp: {lookup(V, d, Map.ins(&2, V, hi, key, x, p), key) == x : V}
134	  {lookup(V, d, MB.ins_deep(&2, V, x, lo, hi, p, q, (key, bit)), key) == x : V}
135	def deep_same_bit(V, d, x, lo, hi, p, q, key, bit, e, lp, hp):
136	  match bit:
137	    case False{}:
138	      Equal.trans(V, lookup(V, d, MNode{q, Map.ins(&2, V, lo, key, x, p), hi}, key), lookup(V, d, Map.ins(&2, V, lo, key, x, p), key), x, node_left(V, d, Map.ins(&2, V, lo, key, x, p), hi, q, key, e), lp)
139	    case True{}:
140	      Equal.trans(V, lookup(V, d, MNode{q, lo, Map.ins(&2, V, hi, key, x, p)}, key), lookup(V, d, Map.ins(&2, V, hi, key, x, p), key), x, node_right(V, d, lo, Map.ins(&2, V, hi, key, x, p), q, key, e), hp)
141	
142	law insertion_branch_same:
143	  for -V: Data
144	  for d: V
145	  for x: V
146	  for lo: Map<&2, V>
147	  for hi: Map<&2, V>
148	  for p: Nat
149	  for +q: Nat
150	  for +key: String
151	  for descend: Bool
152	  for lp: {lookup(V, d, Map.ins(&2, V, lo, key, x, p), key) == x : V}
153	  for hp: {lookup(V, d, Map.ins(&2, V, hi, key, x, p), key) == x : V}
154	  {lookup(V, d, MB.ins_if(&2, V, key, x, lo, hi, q, p, descend), key) == x : V}
155	def insertion_branch_same(V, d, x, lo, hi, p, q, key, descend, lp, hp):
156	  match descend:
157	    case False{}:
158	      splice_same(V, d, x, MNode{q, lo, hi}, p, key)
159	    case True{}:
160	      %Equal.sym(String & Bool, Map.bit(key, q), (key, route_bit(Map.bit(key, q))), route_shape(key, q)) : {lookup(V, d, MB.ins_deep(&2, V, x, lo, hi, p, q, _), key) == x : V}
161	      deep_same_bit(V, d, x, lo, hi, p, q, key, route_bit(Map.bit(key, q)), route_shape(key, q), lp, hp)
162	
163	# This actual native insertion law needs no well-formedness assumption: querying
164	# the new key follows the same bits used to choose its newly inserted leaf.
165	# Other-key preservation DOES require valid discriminator/difference properties.
166	law insertion_same:
167	  for -V: Data
168	  for +d: V
169	  for m: Map<&2, V>
170	  for +key: String
171	  for +x: V
172	  for +p: Nat
173	  {lookup(V, d, Map.ins(&2, V, m, key, x, p), key) == x : V}
174	def insertion_same(V, d, m, key, x, p):
175	  match m:
176	    case MTip{}:
177	      leaf_same(V, d, key, x)
178	    case MLeaf{k, v}:
179	      splice_same(V, d, x, MLeaf{k, v}, p, key)
180	    case MNode{+q, +lo, +hi}:
181	      %Equal.sym(Map<&2, V>, Map.ins(&2, V, MNode{q, lo, hi}, key, x, p), MB.ins_if(&2, V, key, x, lo, hi, q, p, Nat.is_lt(q, p)), MB.ins_node(&2, V, q, lo, hi, key, x, p)) : {lookup(V, d, _, key) == x : V}
182	      insertion_branch_same(V, d, x, lo, hi, p, q, key, Nat.is_lt(q, p), insertion_same(V, d, lo, key, x, p), insertion_same(V, d, hi, key, x, p))
183	
184	def seek_found(-V: Data, r: Map<&2, V> & String & Maybe<&2, String>) -> Maybe<&2, String>:
185	  (tree, key, found) = r
186	  found
187	
188	law seek_low_found:
189	  for -V: Data
190	  for p: Nat
191	  for hi: Map<&2, V>
192	  for r: Map<&2, V> & String & Maybe<&2, String>
193	  {seek_found(V, Map.lo(&2, V, String & Maybe<&2, String>, p, hi, r)) == seek_found(V, r) : Maybe<&2, String>}
194	def seek_low_found(V, p, hi, r):
195	  match r:
196	    case Tuple{tree, Tuple{key, found}}:
197	      {==}
198	
199	law seek_high_found:
200	  for -V: Data
201	  for p: Nat
202	  for lo: Map<&2, V>
203	  for r: Map<&2, V> & String & Maybe<&2, String>
204	  {seek_found(V, Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r)) == seek_found(V, r) : Maybe<&2, String>}
205	def seek_high_found(V, p, lo, r):
206	  match r:
207	    case Tuple{tree, Tuple{key, found}}:
208	      {==}
209	
210	law seek_left:
211	  for -V: Data
212	  for +lo: Map<&2, V>
213	  for +hi: Map<&2, V>
214	  for +p: Nat
215	  for +key: String
216	  for e: {Map.bit(key, p) == (key, False{}) : String & Bool}
217	  {seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)) == seek_found(V, Map.seek(&2, V, lo, key)) : Maybe<&2, String>}
218	def seek_left(V, lo, hi, p, key, e):
219	  %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {seek_found(V, _) == seek_found(V, Map.seek(&2, V, lo, key)) : Maybe<&2, String>}
220	  %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _)) == seek_found(V, Map.seek(&2, V, lo, key)) : Maybe<&2, String>}
221	  seek_low_found(V, p, hi, Map.seek(&2, V, lo, key))
222	
223	law seek_right:
224	  for -V: Data
225	  for +lo: Map<&2, V>
226	  for +hi: Map<&2, V>
227	  for +p: Nat
228	  for +key: String
229	  for e: {Map.bit(key, p) == (key, True{}) : String & Bool}
230	  {seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)) == seek_found(V, Map.seek(&2, V, hi, key)) : Maybe<&2, String>}
231	def seek_right(V, lo, hi, p, key, e):
232	  %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {seek_found(V, _) == seek_found(V, Map.seek(&2, V, hi, key)) : Maybe<&2, String>}
233	  %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _)) == seek_found(V, Map.seek(&2, V, hi, key)) : Maybe<&2, String>}
234	  seek_high_found(V, p, lo, Map.seek(&2, V, hi, key))
235	
236	law replace_left:
237	  for -V: Data
238	  for d: V
239	  for +lo: Map<&2, V>
240	  for +hi: Map<&2, V>
241	  for +p: Nat
242	  for +key: String
243	  for +x: V
244	  for +e: {Map.bit(key, p) == (key, False{}) : String & Bool}
245	  {lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key) == lookup(V, d, Map.put(&2, V, lo, key, x), key) : V}
246	def replace_left(V, d, lo, hi, p, key, x, e):
247	  %Equal.sym(Map<&2, V>, Map.put(&2, V, MNode{p, lo, hi}, key, x), MB.put_bit(&2, V, x, p, lo, hi, Map.bit(key, p)), MB.put_node(&2, V, x, p, lo, hi, key)) : {lookup(V, d, _, key) == lookup(V, d, Map.put(&2, V, lo, key, x), key) : V}
248	  %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {lookup(V, d, MB.put_bit(&2, V, x, p, lo, hi, _), key) == lookup(V, d, Map.put(&2, V, lo, key, x), key) : V}
249	  node_left(V, d, Map.put(&2, V, lo, key, x), hi, p, key, e)
250	
251	law replace_right:
252	  for -V: Data
253	  for d: V
254	  for +lo: Map<&2, V>
255	  for +hi: Map<&2, V>
256	  for +p: Nat
257	  for +key: String
258	  for +x: V
259	  for +e: {Map.bit(key, p) == (key, True{}) : String & Bool}
260	  {lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key) == lookup(V, d, Map.put(&2, V, hi, key, x), key) : V}
261	def replace_right(V, d, lo, hi, p, key, x, e):
262	  %Equal.sym(Map<&2, V>, Map.put(&2, V, MNode{p, lo, hi}, key, x), MB.put_bit(&2, V, x, p, lo, hi, Map.bit(key, p)), MB.put_node(&2, V, x, p, lo, hi, key)) : {lookup(V, d, _, key) == lookup(V, d, Map.put(&2, V, hi, key, x), key) : V}
263	  %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {lookup(V, d, MB.put_bit(&2, V, x, p, lo, hi, _), key) == lookup(V, d, Map.put(&2, V, hi, key, x), key) : V}
264	  node_right(V, d, lo, Map.put(&2, V, hi, key, x), p, key, e)
265	
266	def replacement_certificate(-V: Data, d: V, m: Map<&2, V>, key: String, x: V, found: Maybe<&2, String>) -> Type:
267	  match found:
268	    case None{}:
269	      Unit
270	    case Some{stored}:
271	      @equal: {key == stored : String} -> {lookup(V, d, Map.put(&2, V, m, key, x), key) == x : V}
272	
273	law certificate_left:
274	  for -V: Data
275	  for +d: V
276	  for +lo: Map<&2, V>
277	  for +hi: Map<&2, V>
278	  for +p: Nat
279	  for +key: String
280	  for +x: V
281	  for found: Maybe<&2, String>
282	  for e: {Map.bit(key, p) == (key, False{}) : String & Bool}
283	  for cp: replacement_certificate(V, d, lo, key, x, found)
284	  replacement_certificate(V, d, MNode{p, lo, hi}, key, x, found)
285	def certificate_left(V, d, lo, hi, p, key, x, found, e, cp):
286	  match found:
287	    case None{}:
288	      Unit{}
289	    case Some{stored}:
290	      equal => Equal.trans(V, lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key), lookup(V, d, Map.put(&2, V, lo, key, x), key), x, replace_left(V, d, lo, hi, p, key, x, e), cp(equal))
291	
292	law certificate_right:
293	  for -V: Data
294	  for +d: V
295	  for +lo: Map<&2, V>
296	  for +hi: Map<&2, V>
297	  for +p: Nat
298	  for +key: String
299	  for +x: V
300	  for found: Maybe<&2, String>
301	  for e: {Map.bit(key, p) == (key, True{}) : String & Bool}
302	  for cp: replacement_certificate(V, d, hi, key, x, found)
303	  replacement_certificate(V, d, MNode{p, lo, hi}, key, x, found)
304	def certificate_right(V, d, lo, hi, p, key, x, found, e, cp):
305	  match found:
306	    case None{}:
307	      Unit{}
308	    case Some{stored}:
309	      equal => Equal.trans(V, lookup(V, d, Map.put(&2, V, MNode{p, lo, hi}, key, x), key), lookup(V, d, Map.put(&2, V, hi, key, x), key), x, replace_right(V, d, lo, hi, p, key, x, e), cp(equal))
310	
311	law certificate_branch:
312	  for -V: Data
313	  for d: V
314	  for +lo: Map<&2, V>
315	  for +hi: Map<&2, V>
316	  for +p: Nat
317	  for +key: String
318	  for x: V
319	  for bit: Bool
320	  for +e: {Map.bit(key, p) == (key, bit) : String & Bool}
321	  for lp: replacement_certificate(V, d, lo, key, x, seek_found(V, Map.seek(&2, V, lo, key)))
322	  for hp: replacement_certificate(V, d, hi, key, x, seek_found(V, Map.seek(&2, V, hi, key)))
323	  replacement_certificate(V, d, MNode{p, lo, hi}, key, x, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)))
324	def certificate_branch(V, d, lo, hi, p, key, x, bit, e, lp, hp):
325	  match bit:
326	    case False{}:
327	      %Equal.sym(Maybe<&2, String>, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), seek_found(V, Map.seek(&2, V, lo, key)), seek_left(V, lo, hi, p, key, e)) : replacement_certificate(V, d, MNode{p, lo, hi}, key, x, _)
328	      certificate_left(V, d, lo, hi, p, key, x, seek_found(V, Map.seek(&2, V, lo, key)), e, lp)
329	    case True{}:
330	      %Equal.sym(Maybe<&2, String>, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), seek_found(V, Map.seek(&2, V, hi, key)), seek_right(V, lo, hi, p, key, e)) : replacement_certificate(V, d, MNode{p, lo, hi}, key, x, _)
331	      certificate_right(V, d, lo, hi, p, key, x, seek_found(V, Map.seek(&2, V, hi, key)), e, hp)
332	
333	law replacement_at_seek:
334	  for -V: Data
335	  for +d: V
336	  for m: Map<&2, V>
337	  for +key: String
338	  for +x: V
339	  replacement_certificate(V, d, m, key, x, seek_found(V, Map.seek(&2, V, m, key)))
340	def replacement_at_seek(V, d, m, key, x):
341	  match m:
342	    case MTip{}:
343	      Unit{}
344	    case MLeaf{stored, old}:
345	      equal =>
346	        %equal : {lookup(V, d, MLeaf{_, x}, key) == x : V}
347	        leaf_same(V, d, key, x)
348	    case MNode{+p, +lo, +hi}:
349	      certificate_branch(V, d, lo, hi, p, key, x, route_bit(Map.bit(key, p)), route_shape(key, p), replacement_at_seek(V, d, lo, key, x), replacement_at_seek(V, d, hi, key, x))
350	
351	law seek_low_shape:
352	  for -V: Data
353	  for p: Nat
354	  for lo: Map<&2, V>
355	  for hi: Map<&2, V>
356	  for key: String
357	  for r: Map<&2, V> & String & Maybe<&2, String>
358	  for e: {r == (lo, key, seek_found(V, r)) : Map<&2, V> & String & Maybe<&2, String>}
359	  {Map.lo(&2, V, String & Maybe<&2, String>, p, hi, r) == (MNode{p, lo, hi}, key, seek_found(V, Map.lo(&2, V, String & Maybe<&2, String>, p, hi, r))) : Map<&2, V> & String & Maybe<&2, String>}
360	def seek_low_shape(V, p, lo, hi, key, r, e):
361	  %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, r, (lo, key, seek_found(V, r)), e) : {Map.lo(&2, V, String & Maybe<&2, String>, p, hi, _) == (MNode{p, lo, hi}, key, seek_found(V, Map.lo(&2, V, String & Maybe<&2, String>, p, hi, _))) : Map<&2, V> & String & Maybe<&2, String>}
362	  {==}
363	
364	law seek_high_shape:
365	  for -V: Data
366	  for p: Nat
367	  for lo: Map<&2, V>
368	  for hi: Map<&2, V>
369	  for key: String
370	  for r: Map<&2, V> & String & Maybe<&2, String>
371	  for e: {r == (hi, key, seek_found(V, r)) : Map<&2, V> & String & Maybe<&2, String>}
372	  {Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r) == (MNode{p, lo, hi}, key, seek_found(V, Map.hi(&2, V, String & Maybe<&2, String>, p, lo, r))) : Map<&2, V> & String & Maybe<&2, String>}
373	def seek_high_shape(V, p, lo, hi, key, r, e):
374	  %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, r, (hi, key, seek_found(V, r)), e) : {Map.hi(&2, V, String & Maybe<&2, String>, p, lo, _) == (MNode{p, lo, hi}, key, seek_found(V, Map.hi(&2, V, String & Maybe<&2, String>, p, lo, _))) : Map<&2, V> & String & Maybe<&2, String>}
375	  {==}
376	
377	law seek_branch_shape:
378	  for -V: Data
379	  for +lo: Map<&2, V>
380	  for +hi: Map<&2, V>
381	  for +p: Nat
382	  for +key: String
383	  for +bit: Bool
384	  for e: {Map.bit(key, p) == (key, bit) : String & Bool}
385	  for lp: {Map.seek(&2, V, lo, key) == (lo, key, seek_found(V, Map.seek(&2, V, lo, key))) : Map<&2, V> & String & Maybe<&2, String>}
386	  for hp: {Map.seek(&2, V, hi, key) == (hi, key, seek_found(V, Map.seek(&2, V, hi, key))) : Map<&2, V> & String & Maybe<&2, String>}
387	  {Map.seek(&2, V, MNode{p, lo, hi}, key) == (MNode{p, lo, hi}, key, seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))) : Map<&2, V> & String & Maybe<&2, String>}
388	def seek_branch_shape(V, lo, hi, p, key, bit, e, lp, hp):
389	  match bit:
390	    case False{}:
391	      %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {_ == (MNode{p, lo, hi}, key, seek_found(V, _)) : Map<&2, V> & String & Maybe<&2, String>}
392	      %Equal.sym(String & Bool, Map.bit(key, p), (key, False{}), e) : {MB.seek_bit(&2, V, lo, hi, p, _) == (MNode{p, lo, hi}, key, seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _))) : Map<&2, V> & String & Maybe<&2, String>}
393	      seek_low_shape(V, p, lo, hi, key, Map.seek(&2, V, lo, key), lp)
394	    case True{}:
395	      %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, MNode{p, lo, hi}, key), MB.seek_bit(&2, V, lo, hi, p, Map.bit(key, p)), MB.seek_node(&2, V, p, lo, hi, key)) : {_ == (MNode{p, lo, hi}, key, seek_found(V, _)) : Map<&2, V> & String & Maybe<&2, String>}
396	      %Equal.sym(String & Bool, Map.bit(key, p), (key, True{}), e) : {MB.seek_bit(&2, V, lo, hi, p, _) == (MNode{p, lo, hi}, key, seek_found(V, MB.seek_bit(&2, V, lo, hi, p, _))) : Map<&2, V> & String & Maybe<&2, String>}
397	      seek_high_shape(V, p, lo, hi, key, Map.seek(&2, V, hi, key), hp)
398	
399	law seek_shape:
400	  for -V: Data
401	  for m: Map<&2, V>
402	  for +key: String
403	  {Map.seek(&2, V, m, key) == (m, key, seek_found(V, Map.seek(&2, V, m, key))) : Map<&2, V> & String & Maybe<&2, String>}
404	def seek_shape(V, m, key):
405	  match m:
406	    case MTip{}:
407	      {==}
408	    case MLeaf{k, v}:
409	      {==}
410	    case MNode{+p, +lo, +hi}:
411	      seek_branch_shape(V, lo, hi, p, key, route_bit(Map.bit(key, p)), route_shape(key, p), seek_shape(V, lo, key), seek_shape(V, hi, key))
412	
413	law set_comparison_case:
414	  for -V: Data
415	  for +d: V
416	  for m: Map<&2, V>
417	  for +key: String
418	  for +stored: String
419	  for x: V
420	  for c: Cmp
421	  for e: {N.comparison_tag(String, String.cmp(key, stored)) == c : Cmp}
422	  for cp: @equal: {key == stored : String} -> {lookup(V, d, Map.put(&2, V, m, key, x), key) == x : V}
423	  {lookup(V, d, Map.set.fin.go(&2, V, m, key, x, ((key, stored), c)), key) == x : V}
424	def set_comparison_case(V, d, m, key, stored, x, c, e, cp):
425	  match c:
426	    case LT{}:
427	      insertion_same(V, d, m, key, x, Map.diff(key, stored))
428	    case GT{}:
429	      insertion_same(V, d, m, key, x, Map.diff(key, stored))
430	    case EQ{}:
431	      cp(N.string_equal_from_comparison(key, stored, e))
432	
433	law set_found_case:
434	  for -V: Data
435	  for d: V
436	  for m: Map<&2, V>
437	  for +key: String
438	  for +stored: String
439	  for x: V
440	  for cp: @equal: {key == stored : String} -> {lookup(V, d, Map.put(&2, V, m, key, x), key) == x : V}
441	  {lookup(V, d, Map.set.fin(&2, V, m, key, x, key, stored), key) == x : V}
442	def set_found_case(V, d, m, key, stored, x, cp):
443	  %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), N.comparison_tag(String, String.cmp(key, stored))), N.string_comparison_shape(key, stored)) : {lookup(V, d, Map.set.fin.go(&2, V, m, key, x, _), key) == x : V}
444	  set_comparison_case(V, d, m, key, stored, x, N.comparison_tag(String, String.cmp(key, stored)), {==}, cp)
445	
446	law set_seek_case:
447	  for -V: Data
448	  for d: V
449	  for m: Map<&2, V>
450	  for key: String
451	  for x: V
452	  for found: Maybe<&2, String>
453	  for cp: replacement_certificate(V, d, m, key, x, found)
454	  {lookup(V, d, Map.set.go(&2, V, x, (m, key, found)), key) == x : V}
455	def set_seek_case(V, d, m, key, x, found, cp):
456	  match found:
457	    case None{}:
458	      leaf_same(V, d, key, x)
459	    case Some{stored}:
460	      set_found_case(V, d, m, key, stored, x, cp)
461	
462	# Public native Map update/lookup same-key law. All seek/routing/comparator
463	# premises are discharged above against Base; no valid-tree premise is needed
464	# for this particular property. Other-key preservation remains a separate law.
465	law set_same:
466	  for -V: Data
467	  for +d: V
468	  for +m: Map<&2, V>
469	  for +key: String
470	  for +x: V
471	  {lookup(V, d, Map.set(&2, V, m, key, x), key) == x : V}
472	def set_same(V, d, m, key, x):
473	  %Equal.sym(Map<&2, V> & String & Maybe<&2, String>, Map.seek(&2, V, m, key), (m, key, seek_found(V, Map.seek(&2, V, m, key))), seek_shape(V, m, key)) : {lookup(V, d, Map.set.go(&2, V, x, _), key) == x : V}
474	  set_seek_case(V, d, m, key, x, seek_found(V, Map.seek(&2, V, m, key)), replacement_at_seek(V, d, m, key, x))