1	import Base
2	import ./map_bridge.bend as MB
3	
4	# These unfold installed Base algorithms; no map axioms or replacement map.
5	law empty_lookup:
6	  for -V: Data
7	  for d: V
8	  for k: String
9	  {Map.get(V, d, Map.new(&2, V), k) == (MTip{}, d) : Map<&2, V> & V}
10	def empty_lookup(V, d, k):
11	  {==}
12	
13	law empty_set:
14	  for -V: Data
15	  for k: String
16	  for v: V
17	  {Map.set(&2, V, Map.new(&2, V), k, v) == MLeaf{k, v} : Map<&2, V>}
18	def empty_set(V, k, v):
19	  {==}
20	
21	law empty_delete:
22	  for -V: Data
23	  for k: String
24	  {Map.del(&2, V, Map.new(&2, V), k) == MTip{} : Map<&2, V>}
25	def empty_delete(V, k):
26	  {==}
27	
28	law empty_has:
29	  for -V: Data
30	  for k: String
31	  {Map.has(&2, V, Map.new(&2, V), k) == (MTip{}, False{}) : Map<&2, V> & Bool}
32	def empty_has(V, k):
33	  {==}
34	
35	# Presence bits are the key distinction between zero characters and end of string.
36	law zero_character_presence:
37	  for tail: String
38	  {Map.bit.go(SCon{Chr{0}, tail}, 0n, 0n) == (SCon{Chr{0}, tail}, True{}) : String & Bool}
39	def zero_character_presence(tail):
40	  {==}
41	
42	law empty_presence:
43	  {Map.bit.go(SNil{}, 0n, 0n) == (SNil{}, False{}) : String & Bool}
44	def empty_presence():
45	  {==}
46	
47	law boolean_compare_self:
48	  for b: Bool
49	  {Bool.cmp(b, b) == EQ{} : Cmp}
50	def boolean_compare_self(b):
51	  match b:
52	    case False{}:
53	      {==}
54	    case True{}:
55	      {==}
56	
57	law word_compare_self:
58	  for n: Nat
59	  for w: Word(n)
60	  {Word.cmp(n, w, w) == EQ{} : Cmp}
61	def word_compare_self(n, w):
62	  match n:
63	    case 0n:
64	      {==}
65	    case 1n+p:
66	      match w:
67	        case WCon{+b, t}:
68	          Equal.trans(Cmp, Word.cmp.fin(b, b, Word.cmp(p, t, t)), Bool.cmp(b, b), EQ{},
69	            Equal.cong(Cmp, Cmp, x => Word.cmp.fin(b, b, x), Word.cmp(p, t, t), EQ{}, word_compare_self(p, t)),
70	            boolean_compare_self(b))
71	
72	law character_compare_self:
73	  for c: Char
74	  {Char.cmp(c, c) == ((c, c), EQ{}) : (Char & Char) & Cmp}
75	def character_compare_self(c):
76	  match c:
77	    case Chr{U32{w}}:
78	      %word_compare_self(32n, w) : {((Chr{U32{w}}, Chr{U32{w}}), Word.cmp(32n, w, w)) == ((Chr{U32{w}}, Chr{U32{w}}), _) : (Char & Char) & Cmp}
79	      {==}
80	
81	law string_compare_self:
82	  for s: String
83	  {String.cmp(s, s) == ((s, s), EQ{}) : (String & String) & Cmp}
84	def string_compare_self(s):
85	  match s:
86	    case SNil{}:
87	      {==}
88	    case SCon{h, t}:
89	      %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), character_compare_self(h)) : {String.cmp.fin(t, t, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
90	      %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), string_compare_self(t)) : {String.cmp.rec(h, h, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
91	      {==}
92	
93	law singleton_get:
94	  for -V: Data
95	  for d: V
96	  for k: String
97	  for v: V
98	  {Map.get(V, d, MLeaf{k, v}, k) == (MLeaf{k, v}, v) : Map<&2, V> & V}
99	def singleton_get(V, d, k, v):
100	  %Equal.sym((String & String) & Cmp, String.cmp(k, k), ((k, k), EQ{}), string_compare_self(k)) : {Map.get.leaf(V, d, v, _) == (MLeaf{k, v}, v) : Map<&2, V> & V}
101	  {==}
102	
103	law singleton_update:
104	  for -V: Data
105	  for k: String
106	  for old: V
107	  for value: V
108	  {Map.set(&2, V, MLeaf{k, old}, k, value) == MLeaf{k, value} : Map<&2, V>}
109	def singleton_update(V, k, old, value):
110	  %Equal.sym((String & String) & Cmp, String.cmp(k, k), ((k, k), EQ{}), string_compare_self(k)) : {Map.set.fin.go(&2, V, MLeaf{k, old}, k, value, _) == MLeaf{k, value} : Map<&2, V>}
111	  {==}
112	
113	law singleton_delete:
114	  for -V: Data
115	  for k: String
116	  for v: V
117	  {Map.del(&2, V, MLeaf{k, v}, k) == MTip{} : Map<&2, V>}
118	def singleton_delete(V, k, v):
119	  %Equal.sym((String & String) & Cmp, String.cmp(k, k), ((k, k), EQ{}), string_compare_self(k)) : {Map.del.fin(&2, V, Map.pop.leaf(&2, V, v, _)) == MTip{} : Map<&2, V>}
120	  {==}
121	
122	# General routing foundation: actual Base bit traversal preserves the entire
123	# string, irrespective of the requested bit, character codes, or tree validity.
124	def routed_key(r: String & Bool) -> String:
125	  (key, bit) = r
126	  key
127	
128	law recursive_bit_key:
129	  for c: Char
130	  for r: String & Bool
131	  {routed_key(Map.bit.go.rec(c, r)) == SCon{c, routed_key(r)} : String}
132	def recursive_bit_key(c, r):
133	  match r:
134	    case Tuple{key, bit}:
135	      {==}
136	
137	law bit_go_preserves_key:
138	  for key: String
139	  for +character: Nat
140	  for +offset: Nat
141	  {routed_key(Map.bit.go(key, character, offset)) == key : String}
142	def bit_go_preserves_key(key, character, offset):
143	  match key character offset:
144	    case SNil{} ci off:
145	      {==}
146	    case SCon{Chr{x}, tail} 0n 0n:
147	      {==}
148	    case SCon{Chr{x}, tail} 0n 1n+off:
149	      {==}
150	    case SCon{Chr{x}, +tail} 1n+ci off:
151	      +c = {Chr{x} : Char}
152	      Equal.trans(String, routed_key(Map.bit.go.rec(c, Map.bit.go(tail, ci, off))),
153	        SCon{c, routed_key(Map.bit.go(tail, ci, off))}, SCon{c, tail},
154	        recursive_bit_key(c, Map.bit.go(tail, ci, off)),
155	        Equal.cong(String, String, t => SCon{c, t}, routed_key(Map.bit.go(tail, ci, off)), tail, bit_go_preserves_key(tail, ci, off)))
156	
157	law bit_at_preserves_key:
158	  for key: String
159	  for coordinates: Nat & Nat
160	  {routed_key(Map.bit.at(key, coordinates)) == key : String}
161	def bit_at_preserves_key(key, coordinates):
162	  match coordinates:
163	    case Tuple{ci, off}:
164	      bit_go_preserves_key(key, ci, off)
165	
166	law bit_preserves_key:
167	  for key: String
168	  for position: Nat
169	  {routed_key(Map.bit(key, position)) == key : String}
170	def bit_preserves_key(key, position):
171	  bit_at_preserves_key(key, Nat.divmod(position, 33n))
172	
173	# A comparison certificate has content precisely in the EQ branch.
174	def comparison_identity(-A: Type, a: A, b: A, c: Cmp) -> Type:
175	  match c:
176	    case LT{}:
177	      Unit
178	    case EQ{}:
179	      {a == b : A}
180	    case GT{}:
181	      Unit
182	
183	law word_comparison_step:
184	  for n: Nat
185	  for a: Word(n)
186	  for b: Word(n)
187	  for c: Cmp
188	  for x: Bool
189	  for y: Bool
190	  for proof: comparison_identity(Word(n), a, b, c)
191	  comparison_identity(Word(1n+n), WCon{x, a}, WCon{y, b}, Word.cmp.fin(x, y, c))
192	def word_comparison_step(n, a, b, c, x, y, proof):
193	  match c:
194	    case LT{}:
195	      Unit{}
196	    case GT{}:
197	      Unit{}
198	    case EQ{}:
199	      match x y:
200	        case False{} False{}:
201	          Equal.cong(Word(n), Word(1n+n), t => WCon{False{}, t}, a, b, proof)
202	        case True{} True{}:
203	          Equal.cong(Word(n), Word(1n+n), t => WCon{True{}, t}, a, b, proof)
204	        case False{} True{}:
205	          Unit{}
206	        case True{} False{}:
207	          Unit{}
208	
209	law word_comparison_identity:
210	  for n: Nat
211	  for a: Word(n)
212	  for b: Word(n)
213	  comparison_identity(Word(n), a, b, Word.cmp(n, a, b))
214	def word_comparison_identity(n, a, b):
215	  match n:
216	    case 0n:
217	      match a b:
218	        case WNil{} WNil{}:
219	          {==}
220	    case 1n+ +p:
221	      match a b:
222	        case WCon{x, +at} WCon{y, +bt}:
223	          word_comparison_step(p, at, bt, Word.cmp(p, at, bt), x, y, word_comparison_identity(p, at, bt))
224	
225	law comparison_lift:
226	  for -A: Type
227	  for -B: Type
228	  for f: A -> B
229	  for a: A
230	  for b: A
231	  for c: Cmp
232	  for proof: comparison_identity(A, a, b, c)
233	  comparison_identity(B, f(a), f(b), c)
234	def comparison_lift(A, B, f, a, b, c, proof):
235	  match c:
236	    case LT{}:
237	      Unit{}
238	    case GT{}:
239	      Unit{}
240	    case EQ{}:
241	      Equal.cong(A, B, f, a, b, proof)
242	
243	def comparison_result_identity(-A: Type, r: (A & A) & Cmp) -> Type:
244	  ((a, b), c) = r
245	  comparison_identity(A, a, b, c)
246	
247	law character_comparison_identity:
248	  for a: Char
249	  for b: Char
250	  comparison_result_identity(Char, Char.cmp(a, b))
251	def character_comparison_identity(a, b):
252	  match a b:
253	    case Chr{U32{+x}} Chr{U32{+y}}:
254	      comparison_lift(Word(32n), Char, w => Chr{U32{w}}, x, y, Word.cmp(32n, x, y), word_comparison_identity(32n, x, y))
255	
256	law string_comparison_rec_identity:
257	  for h: Char
258	  for r: (String & String) & Cmp
259	  for proof: comparison_result_identity(String, r)
260	  comparison_result_identity(String, String.cmp.rec(h, h, r))
261	def string_comparison_rec_identity(h, r, proof):
262	  match r:
263	    case Tuple{Tuple{a, b}, c}:
264	      comparison_lift(String, String, t => SCon{h, t}, a, b, c, proof)
265	
266	law string_comparison_fin_identity:
267	  for t1: String
268	  for t2: String
269	  for hc: (Char & Char) & Cmp
270	  for hp: comparison_result_identity(Char, hc)
271	  for tp: comparison_result_identity(String, String.cmp(t1, t2))
272	  comparison_result_identity(String, String.cmp.fin(t1, t2, hc))
273	def string_comparison_fin_identity(t1, t2, hc, hp, tp):
274	  match hc:
275	    case Tuple{Tuple{h1, h2}, LT{}}:
276	      Unit{}
277	    case Tuple{Tuple{h1, h2}, GT{}}:
278	      Unit{}
279	    case Tuple{Tuple{h1, h2}, EQ{}}:
280	      %hp : comparison_result_identity(String, String.cmp.rec(h1, _, String.cmp(t1, t2)))
281	      string_comparison_rec_identity(h1, String.cmp(t1, t2), tp)
282	
283	law string_comparison_identity:
284	  for a: String
285	  for b: String
286	  comparison_result_identity(String, String.cmp(a, b))
287	def string_comparison_identity(a, b):
288	  match a b:
289	    case SNil{} SNil{}:
290	      {==}
291	    case SNil{} SCon{h, t}:
292	      Unit{}
293	    case SCon{h, t} SNil{}:
294	      Unit{}
295	    case SCon{+h1, +t1} SCon{+h2, +t2}:
296	      string_comparison_fin_identity(t1, t2, Char.cmp(h1, h2), character_comparison_identity(h1, h2), string_comparison_identity(t1, t2))
297	
298	def comparison_tag(-A: Type, r: (A & A) & Cmp) -> Cmp:
299	  (pair, c) = r
300	  c
301	
302	law string_comparison_shape_step:
303	  for h1: Char
304	  for h2: Char
305	  for t1: String
306	  for t2: String
307	  for c: Cmp
308	  for tp: {String.cmp(t1, t2) == ((t1, t2), comparison_tag(String, String.cmp(t1, t2))) : (String & String) & Cmp}
309	  {String.cmp.fin(t1, t2, ((h1, h2), c)) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.fin(t1, t2, ((h1, h2), c)))) : (String & String) & Cmp}
310	def string_comparison_shape_step(h1, h2, t1, t2, c, tp):
311	  match c:
312	    case LT{}:
313	      {==}
314	    case GT{}:
315	      {==}
316	    case EQ{}:
317	      %Equal.sym((String & String) & Cmp, String.cmp(t1, t2), ((t1, t2), comparison_tag(String, String.cmp(t1, t2))), tp) : {String.cmp.rec(h1, h2, _) == ((SCon{h1, t1}, SCon{h2, t2}), comparison_tag(String, String.cmp.rec(h1, h2, _))) : (String & String) & Cmp}
318	      {==}
319	
320	law string_comparison_shape:
321	  for a: String
322	  for b: String
323	  {String.cmp(a, b) == ((a, b), comparison_tag(String, String.cmp(a, b))) : (String & String) & Cmp}
324	def string_comparison_shape(a, b):
325	  match a b:
326	    case SNil{} SNil{}:
327	      {==}
328	    case SNil{} SCon{h, t}:
329	      {==}
330	    case SCon{h, t} SNil{}:
331	      {==}
332	    case SCon{Chr{U32{+x}}, +t1} SCon{Chr{U32{+y}}, +t2}:
333	      string_comparison_shape_step(Chr{U32{x}}, Chr{U32{y}}, t1, t2, Word.cmp(32n, x, y), string_comparison_shape(t1, t2))
334	
335	law string_comparison_original_identity:
336	  for +a: String
337	  for +b: String
338	  comparison_identity(String, a, b, comparison_tag(String, String.cmp(a, b)))
339	def string_comparison_original_identity(a, b):
340	  %string_comparison_shape(a, b) : comparison_result_identity(String, _)
341	  string_comparison_identity(a, b)
342	
343	law string_equal_from_comparison:
344	  for a: String
345	  for b: String
346	  for e: {comparison_tag(String, String.cmp(a, b)) == EQ{} : Cmp}
347	  {a == b : String}
348	def string_equal_from_comparison(a, b, e):
349	  %e : comparison_identity(String, a, b, _)
350	  string_comparison_original_identity(a, b)
351	
352	law string_equal_comparison:
353	  for a: String
354	  for b: String
355	  for e: {a == b : String}
356	  {String.cmp(a, b) == ((a, b), EQ{}) : (String & String) & Cmp}
357	def string_equal_comparison(a, b, e):
358	  %e : {String.cmp(a, _) == ((a, _), EQ{}) : (String & String) & Cmp}
359	  string_compare_self(a)
360	
361	# First-difference base and common-prefix reduction laws for the existing
362	# algorithm. The unequal-character msb/routing theorem is still outstanding.
363	law difference_empty_left:
364	  for h: Char
365	  for tail: String
366	  {Map.diff(SNil{}, SCon{h, tail}) == 0n : Nat}
367	def difference_empty_left(h, tail):
368	  {==}
369	
370	law difference_empty_right:
371	  for h: Char
372	  for tail: String
373	  {Map.diff(SCon{h, tail}, SNil{}) == 0n : Nat}
374	def difference_empty_right(h, tail):
375	  {==}
376	
377	law difference_common_character:
378	  for h: Char
379	  for a: String
380	  for b: String
381	  {Map.diff(SCon{h, a}, SCon{h, b}) == Nat.add(33n, Map.diff(a, b)) : Nat}
382	def difference_common_character(h, a, b):
383	  match h:
384	    case Chr{U32{w}}:
385	      %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, word_compare_self(32n, w)) : {Map.diff.fin(a, b, (Map.diff.chr(U32.xor(U32{w}, U32{w})), Cmp.is_eq(_))) == Nat.add(33n, Map.diff(a, b)) : Nat}
386	      {==}
387	
388	law difference_empty_presence:
389	  for h: Char
390	  for tail: String
391	  {Map.bit.go(SCon{h, tail}, Map.diff(SNil{}, SCon{h, tail}), 0n) == (SCon{h, tail}, True{}) : String & Bool}
392	def difference_empty_presence(h, tail):
393	  match h:
394	    case Chr{x}:
395	      {==}
396	
397	def lookup_map(-V: Data, r: Map<&2, V> & V) -> Map<&2, V>:
398	  (m, value) = r
399	  m
400	
401	law lookup_leaf_preserves:
402	  for -V: Data
403	  for d: V
404	  for v: V
405	  for key: String
406	  for stored: String
407	  for c: Cmp
408	  {lookup_map(V, Map.get.leaf(V, d, v, ((key, stored), c))) == MLeaf{stored, v} : Map<&2, V>}
409	def lookup_leaf_preserves(V, d, v, key, stored, c):
410	  match c:
411	    case LT{}:
412	      {==}
413	    case EQ{}:
414	      {==}
415	    case GT{}:
416	      {==}
417	
418	law lookup_lo_projection:
419	  for -V: Data
420	  for p: Nat
421	  for hi: Map<&2, V>
422	  for r: Map<&2, V> & V
423	  {lookup_map(V, Map.lo(&2, V, V, p, hi, r)) == MNode{p, lookup_map(V, r), hi} : Map<&2, V>}
424	def lookup_lo_projection(V, p, hi, r):
425	  match r:
426	    case Tuple{lo, value}:
427	      {==}
428	
429	law lookup_hi_projection:
430	  for -V: Data
431	  for p: Nat
432	  for lo: Map<&2, V>
433	  for r: Map<&2, V> & V
434	  {lookup_map(V, Map.hi(&2, V, V, p, lo, r)) == MNode{p, lo, lookup_map(V, r)} : Map<&2, V>}
435	def lookup_hi_projection(V, p, lo, r):
436	  match r:
437	    case Tuple{hi, value}:
438	      {==}
439	
440	law lookup_branch_preserves:
441	  for -V: Data
442	  for +d: V
443	  for +lo: Map<&2, V>
444	  for +hi: Map<&2, V>
445	  for +p: Nat
446	  for kb: String & Bool
447	  for lp: @key: String -> {lookup_map(V, Map.get(V, d, lo, key)) == lo : Map<&2, V>}
448	  for hp: @key: String -> {lookup_map(V, Map.get(V, d, hi, key)) == hi : Map<&2, V>}
449	  {lookup_map(V, MB.get_bit(V, d, lo, hi, p, kb)) == MNode{p, lo, hi} : Map<&2, V>}
450	def lookup_branch_preserves(V, d, lo, hi, p, kb, lp, hp):
451	  match kb:
452	    case Tuple{+key, False{}}:
453	      Equal.trans(Map<&2, V>, lookup_map(V, Map.lo(&2, V, V, p, hi, Map.get(V, d, lo, key))), MNode{p, lookup_map(V, Map.get(V, d, lo, key)), hi}, MNode{p, lo, hi}, lookup_lo_projection(V, p, hi, Map.get(V, d, lo, key)), Equal.cong(Map<&2, V>, Map<&2, V>, m => MNode{p, m, hi}, lookup_map(V, Map.get(V, d, lo, key)), lo, lp(key)))
454	    case Tuple{+key, True{}}:
455	      Equal.trans(Map<&2, V>, lookup_map(V, Map.hi(&2, V, V, p, lo, Map.get(V, d, hi, key))), MNode{p, lo, lookup_map(V, Map.get(V, d, hi, key))}, MNode{p, lo, hi}, lookup_hi_projection(V, p, lo, Map.get(V, d, hi, key)), Equal.cong(Map<&2, V>, Map<&2, V>, m => MNode{p, lo, m}, lookup_map(V, Map.get(V, d, hi, key)), hi, hp(key)))
456	
457	law lookup_preserves_map:
458	  for -V: Data
459	  for +d: V
460	  for m: Map<&2, V>
461	  for +key: String
462	  {lookup_map(V, Map.get(V, d, m, key)) == m : Map<&2, V>}
463	def lookup_preserves_map(V, d, m, key):
464	  match m:
465	    case MTip{}:
466	      {==}
467	    case MLeaf{+stored, v}:
468	      %Equal.sym((String & String) & Cmp, String.cmp(key, stored), ((key, stored), comparison_tag(String, String.cmp(key, stored))), string_comparison_shape(key, stored)) : {lookup_map(V, Map.get.leaf(V, d, v, _)) == MLeaf{stored, v} : Map<&2, V>}
469	      lookup_leaf_preserves(V, d, v, key, stored, comparison_tag(String, String.cmp(key, stored)))
470	    case MNode{+p, +lo, +hi}:
471	      %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)) : {lookup_map(V, _) == MNode{p, lo, hi} : Map<&2, V>}
472	      lookup_branch_preserves(V, d, lo, hi, p, Map.bit(key, p), q => lookup_preserves_map(V, d, lo, q), q => lookup_preserves_map(V, d, hi, q))
473	
474	law natural_add_associative:
475	  for a: Nat
476	  for b: Nat
477	  for c: Nat
478	  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
479	def natural_add_associative(a, b, c):
480	  match a:
481	    case 0n:
482	      {==}
483	    case 1n+p:
484	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, Nat.add(b, c)), Nat.add(Nat.add(p, b), c), natural_add_associative(p, b, c))
485	
486	law natural_add_right_zero:
487	  for a: Nat
488	  {Nat.add(a, 0n) == a : Nat}
489	def natural_add_right_zero(a):
490	  match a:
491	    case 0n:
492	      {==}
493	    case 1n+p:
494	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, natural_add_right_zero(p))
495	
496	law keys_accumulator_size:
497	  for -V: Data
498	  for m: Map<&2, V>
499	  for +acc: List<&2, String>
500	  {List.length(&2, String, Map.keys.go(&2, V, m, acc)) == Nat.add(Map.size(&2, V, m), List.length(&2, String, acc)) : Nat}
501	def keys_accumulator_size(V, m, acc):
502	  match m:
503	    case MTip{}:
504	      {==}
505	    case MLeaf{key, value}:
506	      {==}
507	    case MNode{p, +lo, +hi}:
508	      %Equal.sym(Nat, List.length(&2, String, Map.keys.go(&2, V, lo, Map.keys.go(&2, V, hi, acc))), Nat.add(Map.size(&2, V, lo), List.length(&2, String, Map.keys.go(&2, V, hi, acc))), keys_accumulator_size(V, lo, Map.keys.go(&2, V, hi, acc))) : {_ == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, String, acc)) : Nat}
509	      %Equal.sym(Nat, List.length(&2, String, Map.keys.go(&2, V, hi, acc)), Nat.add(Map.size(&2, V, hi), List.length(&2, String, acc)), keys_accumulator_size(V, hi, acc)) : {Nat.add(Map.size(&2, V, lo), _) == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, String, acc)) : Nat}
510	      natural_add_associative(Map.size(&2, V, lo), Map.size(&2, V, hi), List.length(&2, String, acc))
511	
512	law keys_size:
513	  for -V: Data
514	  for +m: Map<&2, V>
515	  {List.length(&2, String, Map.keys(&2, V, m)) == Map.size(&2, V, m) : Nat}
516	def keys_size(V, m):
517	  Equal.trans(Nat, List.length(&2, String, Map.keys(&2, V, m)), Nat.add(Map.size(&2, V, m), 0n), Map.size(&2, V, m), keys_accumulator_size(V, m, Nil{}), natural_add_right_zero(Map.size(&2, V, m)))
518	
519	law entries_accumulator_size:
520	  for -V: Data
521	  for m: Map<&2, V>
522	  for +acc: List<&2, Sigma<&2, &2, String, _ => V>>
523	  {List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, m, acc)) == Nat.add(Map.size(&2, V, m), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)) : Nat}
524	def entries_accumulator_size(V, m, acc):
525	  match m:
526	    case MTip{}:
527	      {==}
528	    case MLeaf{key, value}:
529	      {==}
530	    case MNode{p, +lo, +hi}:
531	      %Equal.sym(Nat, List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, lo, Map.to_list.go(&2, V, hi, acc))), Nat.add(Map.size(&2, V, lo), List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, hi, acc))), entries_accumulator_size(V, lo, Map.to_list.go(&2, V, hi, acc))) : {_ == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)) : Nat}
532	      %Equal.sym(Nat, List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list.go(&2, V, hi, acc)), Nat.add(Map.size(&2, V, hi), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)), entries_accumulator_size(V, hi, acc)) : {Nat.add(Map.size(&2, V, lo), _) == Nat.add(Nat.add(Map.size(&2, V, lo), Map.size(&2, V, hi)), List.length(&2, Sigma<&2, &2, String, _ => V>, acc)) : Nat}
533	      natural_add_associative(Map.size(&2, V, lo), Map.size(&2, V, hi), List.length(&2, Sigma<&2, &2, String, _ => V>, acc))
534	
535	law entries_size:
536	  for -V: Data
537	  for +m: Map<&2, V>
538	  {List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list(&2, V, m)) == Map.size(&2, V, m) : Nat}
539	def entries_size(V, m):
540	  Equal.trans(Nat, List.length(&2, Sigma<&2, &2, String, _ => V>, Map.to_list(&2, V, m)), Nat.add(Map.size(&2, V, m), 0n), Map.size(&2, V, m), entries_accumulator_size(V, m, Nil{}), natural_add_right_zero(Map.size(&2, V, m)))