1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../spec/containers/hash_table.bend as S
6	import ../../lib/u32div.bend as UD
7	import ../../../src/containers/hash_table.bend as H
8	import ./buckets.bend as B
9	import ./modn.bend as M
10	import ./inv.bend as IV
11	import ../../lib/u32alg.bend as A
12	import ./keys.bend as K2
13	import ./state.bend as ST
14	import ./tools.bend as T
15	import ./setv.bend as SV
16	import ./lookup.bend as LK
17	import ./speclem.bend as SL
18	import ./size.bend as SZ
19	
20	# Inserting a full bucket into an empty one, at the bucket level.
21	
22	def bupd(bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk) -> List<&2, B.Bk>:
23	  match bs e:
24	    case Nil{} _:
25	      Nil{}
26	    case Con{c, t} 0n:
27	      Con{b, t}
28	    case Con{c, t} 1n+p:
29	      Con{c, bupd(t, p, b)}
30	
31	def at_bupd_same(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +h: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}) -> {B.at(bupd(bs, e, b), e) == b : B.Bk}:
32	  match bs e:
33	    case Nil{} _:
34	      Empty.absurd({B.at(bupd(Nil{}, e, b), e) == b : B.Bk}, N.lt_zero_absurd(e, h))
35	    case Con{c, t} 0n:
36	      {==}
37	    case Con{c, t} 1n+p:
38	      at_bupd_same(t, p, b, h)
39	
40	def at_bupd_other(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +j: Nat, +h: {Nat.is_eq(e, j) == False{} : Bool}) -> {B.at(bupd(bs, e, b), j) == B.at(bs, j) : B.Bk}:
41	  match bs e j:
42	    case Nil{} _ _:
43	      {==}
44	    case Con{c, t} 0n 0n:
45	      Empty.absurd({B.at(bupd(Con{c, t}, 0n, b), 0n) == B.at(Con{c, t}, 0n) : B.Bk}, L.true_false(h))
46	    case Con{c, t} 0n 1n+q:
47	      {==}
48	    case Con{c, t} 1n+p 0n:
49	      {==}
50	    case Con{c, t} 1n+p 1n+q:
51	      at_bupd_other(t, p, b, q, h)
52	
53	# ---- occupancy only grows ----
54	
55	def occ_up_c(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +x: Nat, +h: {B.occ(B.at(bs, x)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, x) == c : Bool}) -> {B.occ(B.at(bupd(bs, e, b), x)) == True{} : Bool}:
56	  match c:
57	    case True{}:
58	      L.subst(Nat, z => {B.occ(B.at(bupd(bs, e, b), z)) == True{} : Bool}, e, x, N.eq_from_is_eq(e, x, hc), L.subst(B.Bk, bb => {B.occ(bb) == True{} : Bool}, b, B.at(bupd(bs, e, b), e), Equal.sym(B.Bk, B.at(bupd(bs, e, b), e), b, at_bupd_same(bs, e, b, he)), hb))
59	    case False{}:
60	      L.subst(B.Bk, bb => {B.occ(bb) == True{} : Bool}, B.at(bs, x), B.at(bupd(bs, e, b), x), Equal.sym(B.Bk, B.at(bupd(bs, e, b), x), B.at(bs, x), at_bupd_other(bs, e, b, x, hc)), h)
61	
62	def occ_up(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +x: Nat, +h: {B.occ(B.at(bs, x)) == True{} : Bool}) -> {B.occ(B.at(bupd(bs, e, b), x)) == True{} : Bool}:
63	  occ_up_c(bs, e, b, hb, he, x, h, Nat.is_eq(e, x), {==})
64	
65	def occpath_up(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +n: Nat, +h: Nat, +m: Nat, +hp: {B.occpath(bs, n, h, m) == True{} : Bool}) -> {B.occpath(bupd(bs, e, b), n, h, m) == True{} : Bool}:
66	  match m:
67	    case 0n:
68	      {==}
69	    case 1n+s:
70	      L.and_intro(B.occ(B.at(bupd(bs, e, b), M.pos(n, h, s))), B.occpath(bupd(bs, e, b), n, h, s), occ_up(bs, e, b, hb, he, M.pos(n, h, s), L.and_left(B.occ(B.at(bs, M.pos(n, h, s))), B.occpath(bs, n, h, s), hp)), occpath_up(bs, e, b, hb, he, n, h, s, L.and_right(B.occ(B.at(bs, M.pos(n, h, s))), B.occpath(bs, n, h, s), hp)))
71	
72	def at_bu_eq(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +j: Nat, +hc: {Nat.is_eq(e, j) == True{} : Bool}) -> {B.at(bupd(bs, e, b), j) == b : B.Bk}:
73	  L.subst(Nat, z => {B.at(bupd(bs, e, b), z) == b : B.Bk}, e, j, N.eq_from_is_eq(e, j, hc), at_bupd_same(bs, e, b, he))
74	
75	# ---- the cluster property ----
76	
77	def imp_occ(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +n: Nat, +h: Nat, +m: Nat, +a: Bool, +hi: {B.implies(a, B.occpath(bs, n, h, m)) == True{} : Bool}) -> {B.implies(a, B.occpath(bupd(bs, e, b), n, h, m)) == True{} : Bool}:
78	  match a:
79	    case True{}:
80	      occpath_up(bs, e, b, hb, he, n, h, m, hi)
81	    case False{}:
82	      {==}
83	
84	def clus_i(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +n: Nat, +mask: U32, +hp: {B.occpath(bs, n, B.hb(mask, b), M.dist(n, B.hb(mask, b), e)) == True{} : Bool}, +cl: {B.cluster(bs, n, mask) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {B.eval(B.PClus{bupd(bs, e, b), n, mask}, j) == True{} : Bool}:
85	  match c:
86	    case True{}:
87	      +hp1 = L.subst(Bool, a => {B.implies(a, B.occpath(bs, n, B.hb(mask, b), M.dist(n, B.hb(mask, b), e))) == True{} : Bool}, True{}, B.occ(b), Equal.sym(Bool, B.occ(b), True{}, hb), hp)
88	      +p0 = L.subst(B.Bk, x => {B.implies(B.occ(x), B.occpath(bupd(bs, e, b), n, B.hb(mask, x), M.dist(n, B.hb(mask, x), e))) == True{} : Bool}, b, B.at(bupd(bs, e, b), e), Equal.sym(B.Bk, B.at(bupd(bs, e, b), e), b, at_bupd_same(bs, e, b, he)), imp_occ(bs, e, b, hb, he, n, B.hb(mask, b), M.dist(n, B.hb(mask, b), e), B.occ(b), hp1))
89	      L.subst(Nat, z => {B.eval(B.PClus{bupd(bs, e, b), n, mask}, z) == True{} : Bool}, e, j, N.eq_from_is_eq(e, j, hc), p0)
90	    case False{}:
91	      +old = B.all_inst(B.PClus{bs, n, mask}, n, cl, j, hj)
92	      L.subst(B.Bk, x => {B.implies(B.occ(x), B.occpath(bupd(bs, e, b), n, B.hb(mask, x), M.dist(n, B.hb(mask, x), j))) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), B.at(bs, j), at_bupd_other(bs, e, b, j, hc)), imp_occ(bs, e, b, hb, he, n, B.hb(mask, B.at(bs, j)), M.dist(n, B.hb(mask, B.at(bs, j)), j), B.occ(B.at(bs, j)), old))
93	
94	def clus_m(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +n: Nat, +mask: U32, +hp: {B.occpath(bs, n, B.hb(mask, b), M.dist(n, B.hb(mask, b), e)) == True{} : Bool}, +cl: {B.cluster(bs, n, mask) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PClus{bupd(bs, e, b), n, mask}, m) == True{} : Bool}:
95	  match m:
96	    case 0n:
97	      {==}
98	    case 1n+q:
99	      +hq = N.succ_le_lt(q, n, hm)
100	      L.and_intro(B.eval(B.PClus{bupd(bs, e, b), n, mask}, q), B.all_lt(B.PClus{bupd(bs, e, b), n, mask}, q), clus_i(bs, e, b, hb, he, n, mask, hp, cl, q, hq, Nat.is_eq(e, q), {==}), clus_m(bs, e, b, hb, he, n, mask, hp, cl, q, N.lt_le(q, n, hq)))
101	
102	# THEOREM: filling the empty bucket e that ends b's probe keeps the clusters
103	def clus_up(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +n: Nat, +mask: U32, +hp: {B.occpath(bs, n, B.hb(mask, b), M.dist(n, B.hb(mask, b), e)) == True{} : Bool}, +cl: {B.cluster(bs, n, mask) == True{} : Bool}) -> {B.cluster(bupd(bs, e, b), n, mask) == True{} : Bool}:
104	  clus_m(bs, e, b, hb, he, n, mask, hp, cl, n, N.le_refl(n))
105	
106	# ---- well-formed buckets ----
107	
108	def well_i(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +sd: Nat, +hwb: {B.wb(sd, b) == True{} : Bool}, +n: Nat, +hw: {B.all_lt(B.PWell{bs, sd}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {B.eval(B.PWell{bupd(bs, e, b), sd}, j) == True{} : Bool}:
109	  match c:
110	    case True{}:
111	      L.subst(B.Bk, x => {B.wb(sd, x) == True{} : Bool}, b, B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), b, at_bu_eq(bs, e, b, he, j, hc)), hwb)
112	    case False{}:
113	      L.subst(B.Bk, x => {B.wb(sd, x) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), B.at(bs, j), at_bupd_other(bs, e, b, j, hc)), B.all_inst(B.PWell{bs, sd}, n, hw, j, hj))
114	
115	def well_up(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +sd: Nat, +hwb: {B.wb(sd, b) == True{} : Bool}, +n: Nat, +hw: {B.all_lt(B.PWell{bs, sd}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PWell{bupd(bs, e, b), sd}, m) == True{} : Bool}:
116	  match m:
117	    case 0n:
118	      {==}
119	    case 1n+q:
120	      +hq = N.succ_le_lt(q, n, hm)
121	      L.and_intro(B.eval(B.PWell{bupd(bs, e, b), sd}, q), B.all_lt(B.PWell{bupd(bs, e, b), sd}, q), well_i(bs, e, b, he, sd, hwb, n, hw, q, hq, Nat.is_eq(e, q), {==}), well_up(bs, e, b, he, sd, hwb, n, hw, q, N.lt_le(q, n, hq)))
122	
123	# ---- occupancy count ----
124	
125	def occn_lo(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +m: Nat, +hm: {Nat.is_le(m, e) == True{} : Bool}) -> {IV.occn(bupd(bs, e, b), m) == IV.occn(bs, m) : Nat}:
126	  match m:
127	    case 0n:
128	      {==}
129	    case 1n+q:
130	      +hq = N.succ_le_lt(q, e, hm)
131	      +ne = N.is_eq_sym_false(q, e, N.is_eq_lt(q, e, hq))
132	      Equal.trans(Nat, Nat.add(IV.bitv(B.occ(B.at(bupd(bs, e, b), q))), IV.occn(bupd(bs, e, b), q)), Nat.add(IV.bitv(B.occ(B.at(bs, q))), IV.occn(bupd(bs, e, b), q)), Nat.add(IV.bitv(B.occ(B.at(bs, q))), IV.occn(bs, q)),
133	        Equal.cong(B.Bk, Nat, x => Nat.add(IV.bitv(B.occ(x)), IV.occn(bupd(bs, e, b), q)), B.at(bupd(bs, e, b), q), B.at(bs, q), at_bupd_other(bs, e, b, q, ne)),
134	        Equal.cong(Nat, Nat, z => Nat.add(IV.bitv(B.occ(B.at(bs, q))), z), IV.occn(bupd(bs, e, b), q), IV.occn(bs, q), occn_lo(bs, e, b, q, N.lt_le(q, e, hq))))
135	
136	def occn_at(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}) -> {IV.occn(bupd(bs, e, b), 1n+e) == 1n+IV.occn(bs, 1n+e) : Nat}:
137	  +lo = occn_lo(bs, e, b, e, N.le_refl(e))
138	  +a1 = Equal.cong(B.Bk, Nat, x => Nat.add(IV.bitv(B.occ(x)), IV.occn(bupd(bs, e, b), e)), B.at(bupd(bs, e, b), e), b, at_bupd_same(bs, e, b, he))
139	  +a2 = Equal.cong(Bool, Nat, o => Nat.add(IV.bitv(o), IV.occn(bupd(bs, e, b), e)), B.occ(b), True{}, hb)
140	  +a3 = Equal.cong(B.Bk, Nat, x => 1n+Nat.add(IV.bitv(B.occ(x)), IV.occn(bs, e)), B.BE{}, B.at(bs, e), Equal.sym(B.Bk, B.at(bs, e), B.BE{}, hz))
141	  Equal.trans(Nat, IV.occn(bupd(bs, e, b), 1n+e), Nat.add(IV.bitv(B.occ(b)), IV.occn(bupd(bs, e, b), e)), 1n+IV.occn(bs, 1n+e), a1,
142	    Equal.trans(Nat, Nat.add(IV.bitv(B.occ(b)), IV.occn(bupd(bs, e, b), e)), 1n+IV.occn(bupd(bs, e, b), e), 1n+IV.occn(bs, 1n+e), a2,
143	      Equal.trans(Nat, 1n+IV.occn(bupd(bs, e, b), e), 1n+IV.occn(bs, e), 1n+IV.occn(bs, 1n+e), Equal.cong(Nat, Nat, z => 1n+z, IV.occn(bupd(bs, e, b), e), IV.occn(bs, e), lo), a3)))
144	
145	def occn_hi_s(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +q: Nat, +ne: {Nat.is_eq(e, 1n+q) == False{} : Bool}, +ih: {IV.occn(bupd(bs, e, b), 1n+q) == 1n+IV.occn(bs, 1n+q) : Nat}) -> {IV.occn(bupd(bs, e, b), 2n+q) == 1n+IV.occn(bs, 2n+q) : Nat}:
146	  +x = IV.bitv(B.occ(B.at(bs, 1n+q)))
147	  Equal.trans(Nat, Nat.add(IV.bitv(B.occ(B.at(bupd(bs, e, b), 1n+q))), IV.occn(bupd(bs, e, b), 1n+q)), Nat.add(x, IV.occn(bupd(bs, e, b), 1n+q)), 1n+IV.occn(bs, 2n+q),
148	    Equal.cong(B.Bk, Nat, y => Nat.add(IV.bitv(B.occ(y)), IV.occn(bupd(bs, e, b), 1n+q)), B.at(bupd(bs, e, b), 1n+q), B.at(bs, 1n+q), at_bupd_other(bs, e, b, 1n+q, ne)),
149	    Equal.trans(Nat, Nat.add(x, IV.occn(bupd(bs, e, b), 1n+q)), Nat.add(x, 1n+IV.occn(bs, 1n+q)), 1n+IV.occn(bs, 2n+q), Equal.cong(Nat, Nat, z => Nat.add(x, z), IV.occn(bupd(bs, e, b), 1n+q), 1n+IV.occn(bs, 1n+q), ih), N.add_succ(x, IV.occn(bs, 1n+q))))
150	
151	def occn_hi_c(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +p: Nat, +hq: {Nat.is_le(e, 1n+p) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, 1n+p) == c : Bool}, rec: @hep: {Nat.is_le(e, p) == True{} : Bool} -> {IV.occn(bupd(bs, e, b), 1n+p) == 1n+IV.occn(bs, 1n+p) : Nat}) -> {IV.occn(bupd(bs, e, b), 2n+p) == 1n+IV.occn(bs, 2n+p) : Nat}:
152	  match c:
153	    case True{}:
154	      L.subst(Nat, z => {IV.occn(bupd(bs, e, b), 1n+z) == 1n+IV.occn(bs, 1n+z) : Nat}, e, 1n+p, N.eq_from_is_eq(e, 1n+p, hc), occn_at(bs, e, b, hb, he, hz))
155	    case False{}:
156	      occn_hi_s(bs, e, b, p, hc, rec(N.lt_succ_le(e, p, N.lt_or_eq(e, 1n+p, hq, hc))))
157	
158	def occn_hi(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +q: Nat, +hq: {Nat.is_le(e, q) == True{} : Bool}) -> {IV.occn(bupd(bs, e, b), 1n+q) == 1n+IV.occn(bs, 1n+q) : Nat}:
159	  match q:
160	    case 0n:
161	      L.subst(Nat, z => {IV.occn(bupd(bs, e, b), 1n+z) == 1n+IV.occn(bs, 1n+z) : Nat}, e, 0n, N.le_antisym(e, 0n, hq, N.zero_le(e)), occn_at(bs, e, b, hb, he, hz))
162	    case 1n+p:
163	      occn_hi_c(bs, e, b, hb, he, hz, p, hq, Nat.is_eq(e, 1n+p), {==}, hep => occn_hi(bs, e, b, hb, he, hz, p, hep))
164	
165	# THEOREM: filling an empty bucket e < n adds one full bucket among the first n
166	def occn_up(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +hb: {B.occ(b) == True{} : Bool}, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}) -> {IV.occn(bupd(bs, e, b), n) == 1n+IV.occn(bs, n) : Nat}:
167	  match n:
168	    case 0n:
169	      Empty.absurd({IV.occn(bupd(bs, e, b), 0n) == 1n+IV.occn(bs, 0n) : Nat}, N.lt_zero_absurd(e, hen))
170	    case 1n+q:
171	      occn_hi(bs, e, b, hb, he, hz, q, N.lt_succ_le(e, q, hen))
172	
173	# ---- no earlier bucket holds a key / has a link ----
174	
175	def nohb_below(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +k: String, +i: Nat, +hi: {Nat.is_le(i, e) == True{} : Bool}, +h: {B.nohb(bs, k, i) == True{} : Bool}) -> {B.nohb(bupd(bs, e, b), k, i) == True{} : Bool}:
176	  match i:
177	    case 0n:
178	      {==}
179	    case 1n+j:
180	      +hje = N.succ_le_lt(j, e, hi)
181	      +ne = N.is_eq_sym_false(j, e, N.is_eq_lt(j, e, hje))
182	      L.and_intro(Bool.not(B.hold(k, B.at(bupd(bs, e, b), j))), B.nohb(bupd(bs, e, b), k, j), L.subst(B.Bk, x => {Bool.not(B.hold(k, x)) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), B.at(bs, j), at_bupd_other(bs, e, b, j, ne)), L.and_left(Bool.not(B.hold(k, B.at(bs, j))), B.nohb(bs, k, j), h)), nohb_below(bs, e, b, k, j, N.lt_le(j, e, hje), L.and_right(Bool.not(B.hold(k, B.at(bs, j))), B.nohb(bs, k, j), h)))
183	
184	def nh_pt(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +k: String, +hnb: {Bool.not(B.hold(k, b)) == True{} : Bool}, +j: Nat, +h0: {Bool.not(B.hold(k, B.at(bs, j))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {Bool.not(B.hold(k, B.at(bupd(bs, e, b), j))) == True{} : Bool}:
185	  match c:
186	    case True{}:
187	      L.subst(B.Bk, x => {Bool.not(B.hold(k, x)) == True{} : Bool}, b, B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), b, at_bu_eq(bs, e, b, he, j, hc)), hnb)
188	    case False{}:
189	      L.subst(B.Bk, x => {Bool.not(B.hold(k, x)) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), B.at(bs, j), at_bupd_other(bs, e, b, j, hc)), h0)
190	
191	def nohb_up(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +k: String, +hnb: {Bool.not(B.hold(k, b)) == True{} : Bool}, +i: Nat, +h: {B.nohb(bs, k, i) == True{} : Bool}) -> {B.nohb(bupd(bs, e, b), k, i) == True{} : Bool}:
192	  match i:
193	    case 0n:
194	      {==}
195	    case 1n+j:
196	      L.and_intro(Bool.not(B.hold(k, B.at(bupd(bs, e, b), j))), B.nohb(bupd(bs, e, b), k, j), nh_pt(bs, e, b, he, k, hnb, j, L.and_left(Bool.not(B.hold(k, B.at(bs, j))), B.nohb(bs, k, j), h), Nat.is_eq(e, j), {==}), nohb_up(bs, e, b, he, k, hnb, j, L.and_right(Bool.not(B.hold(k, B.at(bs, j))), B.nohb(bs, k, j), h)))
197	
198	def nolb_below(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +l: U32, +i: Nat, +hi: {Nat.is_le(i, e) == True{} : Bool}, +h: {B.nolb(bs, l, i) == True{} : Bool}) -> {B.nolb(bupd(bs, e, b), l, i) == True{} : Bool}:
199	  match i:
200	    case 0n:
201	      {==}
202	    case 1n+j:
203	      +hje = N.succ_le_lt(j, e, hi)
204	      +ne = N.is_eq_sym_false(j, e, N.is_eq_lt(j, e, hje))
205	      L.and_intro(Bool.not(Bool.and(B.occ(B.at(bupd(bs, e, b), j)), U32.is_eq(B.lnk(B.at(bupd(bs, e, b), j)), l))), B.nolb(bupd(bs, e, b), l, j), L.subst(B.Bk, x => {Bool.not(Bool.and(B.occ(x), U32.is_eq(B.lnk(x), l))) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), B.at(bs, j), at_bupd_other(bs, e, b, j, ne)), L.and_left(Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))), B.nolb(bs, l, j), h)), nolb_below(bs, e, b, l, j, N.lt_le(j, e, hje), L.and_right(Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))), B.nolb(bs, l, j), h)))
206	
207	def nl_pt(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +l: U32, +hnb: {Bool.not(Bool.and(B.occ(b), U32.is_eq(B.lnk(b), l))) == True{} : Bool}, +j: Nat, +h0: {Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(bupd(bs, e, b), j)), U32.is_eq(B.lnk(B.at(bupd(bs, e, b), j)), l))) == True{} : Bool}:
208	  match c:
209	    case True{}:
210	      L.subst(B.Bk, x => {Bool.not(Bool.and(B.occ(x), U32.is_eq(B.lnk(x), l))) == True{} : Bool}, b, B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), b, at_bu_eq(bs, e, b, he, j, hc)), hnb)
211	    case False{}:
212	      L.subst(B.Bk, x => {Bool.not(Bool.and(B.occ(x), U32.is_eq(B.lnk(x), l))) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, b), j), Equal.sym(B.Bk, B.at(bupd(bs, e, b), j), B.at(bs, j), at_bupd_other(bs, e, b, j, hc)), h0)
213	
214	def nolb_up(+bs: List<&2, B.Bk>, +e: Nat, +b: B.Bk, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +l: U32, +hnb: {Bool.not(Bool.and(B.occ(b), U32.is_eq(B.lnk(b), l))) == True{} : Bool}, +i: Nat, +h: {B.nolb(bs, l, i) == True{} : Bool}) -> {B.nolb(bupd(bs, e, b), l, i) == True{} : Bool}:
215	  match i:
216	    case 0n:
217	      {==}
218	    case 1n+j:
219	      L.and_intro(Bool.not(Bool.and(B.occ(B.at(bupd(bs, e, b), j)), U32.is_eq(B.lnk(B.at(bupd(bs, e, b), j)), l))), B.nolb(bupd(bs, e, b), l, j), nl_pt(bs, e, b, he, l, hnb, j, L.and_left(Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))), B.nolb(bs, l, j), h), Nat.is_eq(e, j), {==}), nolb_up(bs, e, b, he, l, hnb, j, L.and_right(Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))), B.nolb(bs, l, j), h)))
220	
221	# no bucket holds key: none below i does
222	def nohb_pno(+bs: List<&2, B.Bk>, +key: String, +n: Nat, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_le(i, n) == True{} : Bool}) -> {B.nohb(bs, key, i) == True{} : Bool}:
223	  match i:
224	    case 0n:
225	      {==}
226	    case 1n+j:
227	      +hj = N.succ_le_lt(j, n, hi)
228	      L.and_intro(Bool.not(B.hold(key, B.at(bs, j))), B.nohb(bs, key, j), B.all_inst(B.PNo{bs, key}, n, hno, j, hj), nohb_pno(bs, key, n, hno, j, N.lt_le(j, n, hj)))
229	
230	# ---- slot links ----
231	
232	def u32_ne_c(+a: U32, +l: U32, +h: {Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(l))) == False{} : Bool}, +c: Bool, +hc: {U32.is_eq(a, l) == c : Bool}) -> {c == False{} : Bool}:
233	  match c:
234	    case False{}:
235	      {==}
236	    case True{}:
237	      +r = L.subst(U32, z => {Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(z))) == False{} : Bool}, l, a, Equal.sym(U32, a, l, A.eq_of(a, l, hc)), h)
238	      Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(a))), False{}, Equal.sym(Bool, Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(a))), True{}, N.is_eq_refl(UD.v(H.slot(a)))), r)))
239	
240	# links with different slots differ
241	def u32_ne(+a: U32, +l: U32, +h: {Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(l))) == False{} : Bool}) -> {U32.is_eq(a, l) == False{} : Bool}:
242	  u32_ne_c(a, l, h, U32.is_eq(a, l), {==})
243	
244	def not_f(+b: Bool, +h: {b == False{} : Bool}) -> {Bool.not(b) == True{} : Bool}:
245	  L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, False{}, b, Equal.sym(Bool, b, False{}, h), {==})
246	
247	def nl_bit(+o: Bool, +a: U32, +l: U32, +h: {Bool.not(Bool.and(o, Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(l))))) == True{} : Bool}) -> {Bool.not(Bool.and(o, U32.is_eq(a, l))) == True{} : Bool}:
248	  match o:
249	    case False{}:
250	      {==}
251	    case True{}:
252	      not_f(U32.is_eq(a, l), u32_ne(a, l, K2.not_true_eq(Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(l))), h)))
253	
254	# no full bucket uses the slot of l: none has link l
255	def nolb_noslot(+bs: List<&2, B.Bk>, +l: U32, +m: Nat, +h: {ST.noslot(bs, UD.v(H.slot(l)), m) == True{} : Bool}) -> {B.nolb(bs, l, m) == True{} : Bool}:
256	  match m:
257	    case 0n:
258	      {==}
259	    case 1n+j:
260	      +x = Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), UD.v(H.slot(l)))))
261	      L.and_intro(Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))), B.nolb(bs, l, j), nl_bit(B.occ(B.at(bs, j)), B.lnk(B.at(bs, j)), l, L.and_left(x, ST.noslot(bs, UD.v(H.slot(l)), j), h)), nolb_noslot(bs, l, j, L.and_right(x, ST.noslot(bs, UD.v(H.slot(l)), j), h)))
262	
263	def nolb_pre(+bs: List<&2, B.Bk>, +l: U32, +n: Nat, +h: {B.nolb(bs, l, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.nolb(bs, l, m) == True{} : Bool}:
264	  match m:
265	    case 0n:
266	      {==}
267	    case 1n+j:
268	      +hj = N.succ_le_lt(j, n, hm)
269	      L.and_intro(Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))), B.nolb(bs, l, j), T.nolb_inst(bs, l, n, h, j, hj), nolb_pre(bs, l, n, h, j, N.lt_le(j, n, hj)))
270	
271	def noslot_c(+bs: List<&2, B.Bk>, +s: Nat, +q: Nat, +h: {Bool.and(Bool.not(Bool.and(B.occ(B.at(bs, q)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, q)))), s))), ST.noslot(bs, s, q)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(j, q) == c : Bool}, rec: @hlt: {Nat.is_lt(j, q) == True{} : Bool} -> {Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), s))) == True{} : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), s))) == True{} : Bool}:
272	  match c:
273	    case True{}:
274	      L.subst(Nat, z => {Bool.not(Bool.and(B.occ(B.at(bs, z)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, z)))), s))) == True{} : Bool}, q, j, Equal.sym(Nat, j, q, N.eq_from_is_eq(j, q, hc)), L.and_left(Bool.not(Bool.and(B.occ(B.at(bs, q)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, q)))), s))), ST.noslot(bs, s, q), h))
275	    case False{}:
276	      rec(N.lt_or_eq(j, q, N.lt_succ_le(j, q, hj), hc))
277	
278	def noslot_inst(+bs: List<&2, B.Bk>, +s: Nat, +m: Nat, +h: {ST.noslot(bs, s, m) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, m) == True{} : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), s))) == True{} : Bool}:
279	  match m:
280	    case 0n:
281	      Empty.absurd({Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), s))) == True{} : Bool}, N.lt_zero_absurd(j, hj))
282	    case 1n+q:
283	      noslot_c(bs, s, q, h, j, hj, Nat.is_eq(j, q), {==}, hlt => noslot_inst(bs, s, q, L.and_right(Bool.not(Bool.and(B.occ(B.at(bs, q)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, q)))), s))), ST.noslot(bs, s, q), h), j, hlt))
284	
285	# a full bucket that does not use slot s has a slot other than s
286	def slot_other(+b: B.Bk, +s: Nat, +ho: {B.occ(b) == True{} : Bool}, +h: {Bool.not(Bool.and(B.occ(b), Nat.is_eq(UD.v(H.slot(B.lnk(b))), s))) == True{} : Bool}) -> {Nat.is_eq(UD.v(H.slot(B.lnk(b))), s) == False{} : Bool}:
287	  K2.not_true_eq(Nat.is_eq(UD.v(H.slot(B.lnk(b))), s), L.subst(Bool, o => {Bool.not(Bool.and(o, Nat.is_eq(UD.v(H.slot(B.lnk(b))), s))) == True{} : Bool}, B.occ(b), True{}, ho, h))
288	
289	# ---- uniqueness ----
290	
291	def uq_oth(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +l: U32, +key: String, +i: Nat, +b: B.Bk, +hu: {B.uq_b(bs, i, b) == True{} : Bool}, +hpn: {Bool.not(B.hold(key, b)) == True{} : Bool}, +hns: {Bool.not(Bool.and(B.occ(b), Nat.is_eq(UD.v(H.slot(B.lnk(b))), UD.v(H.slot(l))))) == True{} : Bool}) -> {B.uq_b(bupd(bs, e, B.BF{w, l, key}), i, b) == True{} : Bool}:
292	  match b:
293	    case B.BE{}:
294	      {==}
295	    case B.BF{w2, +l2, +k2}:
296	      +e1 = K2.not_true_eq(S.str_eq(k2, key), hpn)
297	      +e2 = Equal.trans(Bool, S.str_eq(key, k2), S.str_eq(k2, key), False{}, K2.str_sym(key, k2), e1)
298	      +hk = not_f(S.str_eq(key, k2), e2)
299	      +f1 = K2.not_true_eq(Nat.is_eq(UD.v(H.slot(l2)), UD.v(H.slot(l))), hns)
300	      +hl = not_f(U32.is_eq(l, l2), u32_ne(l, l2, N.is_eq_sym_false(UD.v(H.slot(l2)), UD.v(H.slot(l)), f1)))
301	      L.and_intro(B.nohb(bupd(bs, e, B.BF{w, l, key}), k2, i), B.nolb(bupd(bs, e, B.BF{w, l, key}), l2, i), nohb_up(bs, e, B.BF{w, l, key}, he, k2, hk, i, L.and_left(B.nohb(bs, k2, i), B.nolb(bs, l2, i), hu)), nolb_up(bs, e, B.BF{w, l, key}, he, l2, hl, i, L.and_right(B.nohb(bs, k2, i), B.nolb(bs, l2, i), hu)))
302	
303	def uq_i(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {B.eval(B.PUniq{bupd(bs, e, B.BF{w, L, key})}, j) == True{} : Bool}:
304	  match c:
305	    case True{}:
306	      +u0 = L.and_intro(B.nohb(bupd(bs, e, B.BF{w, L, key}), key, e), B.nolb(bupd(bs, e, B.BF{w, L, key}), L, e), nohb_below(bs, e, B.BF{w, L, key}, key, e, N.le_refl(e), nohb_pno(bs, key, n, hno, e, N.lt_le(e, n, hen))), nolb_below(bs, e, B.BF{w, L, key}, L, e, N.le_refl(e), nolb_pre(bs, L, n, nolb_noslot(bs, L, n, hns), e, N.lt_le(e, n, hen))))
307	      +u1 = L.subst(B.Bk, x => {B.uq_b(bupd(bs, e, B.BF{w, L, key}), e, x) == True{} : Bool}, B.BF{w, L, key}, B.at(bupd(bs, e, B.BF{w, L, key}), e), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), e), B.BF{w, L, key}, at_bupd_same(bs, e, B.BF{w, L, key}, he)), u0)
308	      L.subst(Nat, z => {B.eval(B.PUniq{bupd(bs, e, B.BF{w, L, key})}, z) == True{} : Bool}, e, j, N.eq_from_is_eq(e, j, hc), u1)
309	    case False{}:
310	      +u0 = uq_oth(bs, e, he, w, L, key, j, B.at(bs, j), B.all_inst(B.PUniq{bs}, n, huq, j, hj), B.all_inst(B.PNo{bs, key}, n, hno, j, hj), noslot_inst(bs, UD.v(H.slot(L)), n, hns, j, hj))
311	      L.subst(B.Bk, x => {B.uq_b(bupd(bs, e, B.BF{w, L, key}), j, x) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, B.BF{w, L, key}), j), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), j), B.at(bs, j), at_bupd_other(bs, e, B.BF{w, L, key}, j, hc)), u0)
312	
313	def uq_m(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PUniq{bupd(bs, e, B.BF{w, L, key})}, m) == True{} : Bool}:
314	  match m:
315	    case 0n:
316	      {==}
317	    case 1n+q:
318	      +hq = N.succ_le_lt(q, n, hm)
319	      L.and_intro(B.eval(B.PUniq{bupd(bs, e, B.BF{w, L, key})}, q), B.all_lt(B.PUniq{bupd(bs, e, B.BF{w, L, key})}, q), uq_i(bs, e, he, w, L, key, n, hen, huq, hno, hns, q, hq, Nat.is_eq(e, q), {==}), uq_m(bs, e, he, w, L, key, n, hen, huq, hno, hns, q, N.lt_le(q, n, hq)))
320	
321	# THEOREM: a key held nowhere, in a slot used nowhere, keeps keys and links unique
322	def uq_up(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}) -> {B.all_lt(B.PUniq{bupd(bs, e, B.BF{w, L, key})}, n) == True{} : Bool}:
323	  uq_m(bs, e, he, w, L, key, n, hen, huq, hno, hns, n, N.le_refl(n))
324	
325	# ---- liveness ----
326	
327	def live_mono(+lv: List<&2, Bool>, +f: Nat, +f2: Nat, +hle: {Nat.is_le(f, f2) == True{} : Bool}, +b: B.Bk, +h: {B.live_b(lv, f, b) == True{} : Bool}) -> {B.live_b(lv, f2, b) == True{} : Bool}:
328	  match b:
329	    case B.BE{}:
330	      {==}
331	    case B.BF{w, +l, k}:
332	      L.and_intro(B.nthb(lv, UD.v(H.slot(l))), Nat.is_lt(UD.v(H.slot(l)), f2), L.and_left(B.nthb(lv, UD.v(H.slot(l))), Nat.is_lt(UD.v(H.slot(l)), f), h), N.lt_le_trans(UD.v(H.slot(l)), f, f2, L.and_right(B.nthb(lv, UD.v(H.slot(l))), Nat.is_lt(UD.v(H.slot(l)), f), h), hle))
333	
334	def live_new(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +w: U32, +L: U32, +key: String, +x: V, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +fr2: Nat, +hs2: {Nat.is_lt(UD.v(H.slot(L)), fr2) == True{} : Bool}) -> {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr2, B.BF{w, L, key}) == True{} : Bool}:
335	  +a = Equal.trans(Bool, B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), UD.v(H.slot(L))), ST.some_b(~V, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(L)))), True{}, ST.lvs_nth(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(L))), Equal.cong(Maybe<&2, V>, Bool, m => ST.some_b(~V, m), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(L))), Some{x}, T.nthm_upd_same(~V, vsl, UD.v(H.slot(L)), Some{x}, hs)))
336	  L.and_intro(B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), UD.v(H.slot(L))), Nat.is_lt(UD.v(H.slot(L)), fr2), a, hs2)
337	
338	def live_i(~V: Data, +bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +vsl: List<&2, Maybe<&2, V>>, +x: V, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +fr: Nat, +fr2: Nat, +hle: {Nat.is_le(fr, fr2) == True{} : Bool}, +hs2: {Nat.is_lt(UD.v(H.slot(L)), fr2) == True{} : Bool}, +n: Nat, +hl: {B.all_lt(B.PLive{bs, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {B.eval(B.PLive{bupd(bs, e, B.BF{w, L, key}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr2}, j) == True{} : Bool}:
339	  match c:
340	    case True{}:
341	      L.subst(B.Bk, y => {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr2, y) == True{} : Bool}, B.BF{w, L, key}, B.at(bupd(bs, e, B.BF{w, L, key}), j), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), j), B.BF{w, L, key}, at_bu_eq(bs, e, B.BF{w, L, key}, he, j, hc)), live_new(~V, vsl, w, L, key, x, hs, fr2, hs2))
342	    case False{}:
343	      L.subst(B.Bk, y => {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr2, y) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, B.BF{w, L, key}), j), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), j), B.at(bs, j), at_bupd_other(bs, e, B.BF{w, L, key}, j, hc)), live_mono(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr, fr2, hle, B.at(bs, j), SV.lv_b(~V, vsl, UD.v(H.slot(L)), x, fr, hs, B.at(bs, j), B.all_inst(B.PLive{bs, ST.lvs(~V, vsl), fr}, n, hl, j, hj))))
344	
345	# THEOREM: the new bucket's slot holds a value and is below the new fresh mark
346	def live_up(~V: Data, +bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +vsl: List<&2, Maybe<&2, V>>, +x: V, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +fr: Nat, +fr2: Nat, +hle: {Nat.is_le(fr, fr2) == True{} : Bool}, +hs2: {Nat.is_lt(UD.v(H.slot(L)), fr2) == True{} : Bool}, +n: Nat, +hl: {B.all_lt(B.PLive{bs, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PLive{bupd(bs, e, B.BF{w, L, key}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr2}, m) == True{} : Bool}:
347	  match m:
348	    case 0n:
349	      {==}
350	    case 1n+q:
351	      +hq = N.succ_le_lt(q, n, hm)
352	      L.and_intro(B.eval(B.PLive{bupd(bs, e, B.BF{w, L, key}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr2}, q), B.all_lt(B.PLive{bupd(bs, e, B.BF{w, L, key}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x})), fr2}, q), live_i(~V, bs, e, he, w, L, key, vsl, x, hs, fr, fr2, hle, hs2, n, hl, q, hq, Nat.is_eq(e, q), {==}), live_up(~V, bs, e, he, w, L, key, vsl, x, hs, fr, fr2, hle, hs2, n, hl, q, N.lt_le(q, n, hq)))
353	
354	# ---- other keys and slots ----
355	
356	def pno_i(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +n: Nat, +hno: {B.all_lt(B.PNo{bs, q}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}) -> {B.eval(B.PNo{bupd(bs, e, B.BF{w, L, key}), q}, j) == True{} : Bool}:
357	  nh_pt(bs, e, B.BF{w, L, key}, he, q, not_f(S.str_eq(key, q), hq), j, B.all_inst(B.PNo{bs, q}, n, hno, j, hj), Nat.is_eq(e, j), {==})
358	
359	def pno_up(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +n: Nat, +hno: {B.all_lt(B.PNo{bs, q}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PNo{bupd(bs, e, B.BF{w, L, key}), q}, m) == True{} : Bool}:
360	  match m:
361	    case 0n:
362	      {==}
363	    case 1n+p:
364	      +hp = N.succ_le_lt(p, n, hm)
365	      L.and_intro(B.eval(B.PNo{bupd(bs, e, B.BF{w, L, key}), q}, p), B.all_lt(B.PNo{bupd(bs, e, B.BF{w, L, key}), q}, p), pno_i(bs, e, he, w, L, key, q, hq, n, hno, p, hp), pno_up(bs, e, he, w, L, key, q, hq, n, hno, p, N.lt_le(p, n, hp)))
366	
367	def ns_pt(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +t: Nat, +hst: {Nat.is_eq(UD.v(H.slot(L)), t) == False{} : Bool}, +j: Nat, +h0: {Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), t))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(bupd(bs, e, B.BF{w, L, key}), j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bupd(bs, e, B.BF{w, L, key}), j)))), t))) == True{} : Bool}:
368	  match c:
369	    case True{}:
370	      L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), t))) == True{} : Bool}, B.BF{w, L, key}, B.at(bupd(bs, e, B.BF{w, L, key}), j), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), j), B.BF{w, L, key}, at_bu_eq(bs, e, B.BF{w, L, key}, he, j, hc)), not_f(Nat.is_eq(UD.v(H.slot(L)), t), hst))
371	    case False{}:
372	      L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), t))) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, B.BF{w, L, key}), j), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), j), B.at(bs, j), at_bupd_other(bs, e, B.BF{w, L, key}, j, hc)), h0)
373	
374	# THEOREM: a slot other than the new one is still used by no bucket
375	def noslot_up(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +t: Nat, +hst: {Nat.is_eq(UD.v(H.slot(L)), t) == False{} : Bool}, +m: Nat, +h: {ST.noslot(bs, t, m) == True{} : Bool}) -> {ST.noslot(bupd(bs, e, B.BF{w, L, key}), t, m) == True{} : Bool}:
376	  match m:
377	    case 0n:
378	      {==}
379	    case 1n+j:
380	      +x = Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), t)))
381	      L.and_intro(Bool.not(Bool.and(B.occ(B.at(bupd(bs, e, B.BF{w, L, key}), j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bupd(bs, e, B.BF{w, L, key}), j)))), t))), ST.noslot(bupd(bs, e, B.BF{w, L, key}), t, j), ns_pt(bs, e, he, w, L, key, t, hst, j, L.and_left(x, ST.noslot(bs, t, j), h), Nat.is_eq(e, j), {==}), noslot_up(bs, e, he, w, L, key, t, hst, j, L.and_right(x, ST.noslot(bs, t, j), h)))
382	
383	# ---- the model after the insertion ----
384	
385	
386	def ne_empty(+bs: List<&2, B.Bk>, +e: Nat, +q: String, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +j: Nat, +hk: {B.hold(q, B.at(bs, j)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(e, j) == c : Bool}) -> {c == False{} : Bool}:
387	  match c:
388	    case False{}:
389	      {==}
390	    case True{}:
391	      +h1 = L.subst(Nat, z => {B.hold(q, B.at(bs, z)) == True{} : Bool}, j, e, Equal.sym(Nat, e, j, N.eq_from_is_eq(e, j, hc)), hk)
392	      Empty.absurd({True{} == False{} : Bool}, L.false_true(L.subst(B.Bk, y => {B.hold(q, y) == True{} : Bool}, B.at(bs, e), B.BE{}, hz, h1)))
393	
394	def lk_held(~V: Data, +bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +vsl: List<&2, Maybe<&2, V>>, +x: V, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}, +q: String, e0: T.Holder(bs, q, n)) -> {S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q) == S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q) : Maybe<&2, V>}:
395	  match e0:
396	    case Tuple{+j, Tuple{+hj, +hkj}}:
397	      +ne = ne_empty(bs, e, q, hz, j, hkj, Nat.is_eq(e, j), {==})
398	      +eat = at_bupd_other(bs, e, B.BF{w, L, key}, j, ne)
399	      +hkj2 = L.subst(B.Bk, y => {B.hold(q, y) == True{} : Bool}, B.at(bs, j), B.at(bupd(bs, e, B.BF{w, L, key}), j), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), j), B.at(bs, j), eat), hkj)
400	      +sj = UD.v(H.slot(B.lnk(B.at(bs, j))))
401	      +hne = N.is_eq_sym_false(sj, UD.v(H.slot(L)), slot_other(B.at(bs, j), UD.v(H.slot(L)), B.hold_occ(q, B.at(bs, j), hkj), noslot_inst(bs, UD.v(H.slot(L)), n, hns, j, hj)))
402	      +huq2 = uq_up(bs, e, he, w, L, key, n, hen, huq, hno, hns)
403	      Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(B.lnk(B.at(bupd(bs, e, B.BF{w, L, key}), j))))), S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), LK.lookup_hit(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), q, n, huq2, j, hj, hkj2),
404	        Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(B.lnk(B.at(bupd(bs, e, B.BF{w, L, key}), j))))), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), sj), S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), Equal.cong(B.Bk, Maybe<&2, V>, y => ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(B.lnk(y)))), B.at(bupd(bs, e, B.BF{w, L, key}), j), B.at(bs, j), eat),
405	          Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), sj), ST.nthm(~V, vsl, sj), S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), T.nthm_upd_other(~V, vsl, UD.v(H.slot(L)), sj, Some{x}, hne), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), ST.nthm(~V, vsl, sj), LK.lookup_hit(~V, bs, vsl, q, n, huq, j, hj, hkj)))))
406	
407	def lk_other(~V: Data, +bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +vsl: List<&2, Maybe<&2, V>>, +x: V, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +d: Bool, +hd: {B.all_lt(B.PNo{bs, q}, n) == d : Bool}) -> {S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q) == S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q) : Maybe<&2, V>}:
408	  match d:
409	    case True{}:
410	      Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q), None{}, S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), LK.lookup_none(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), q, n, pno_up(bs, e, he, w, L, key, q, hq, n, hd, n, N.le_refl(n))), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), None{}, LK.lookup_none(~V, bs, vsl, q, n, hd)))
411	    case False{}:
412	      lk_held(~V, bs, e, he, w, L, key, vsl, x, n, hen, hs, hz, huq, hno, hns, q, T.find_hold(bs, q, n, hd))
413	
414	def lk_c(~V: Data, +bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +vsl: List<&2, Maybe<&2, V>>, +x: V, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}, +q: String, +c: Bool, +hc: {S.str_eq(key, q) == c : Bool}) -> {S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q) == S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q) : Maybe<&2, V>}:
415	  match c:
416	    case True{}:
417	      +huq2 = uq_up(bs, e, he, w, L, key, n, hen, huq, hno, hns)
418	      +eat = at_bupd_same(bs, e, B.BF{w, L, key}, he)
419	      +hk2 = L.subst(B.Bk, y => {B.hold(q, y) == True{} : Bool}, B.BF{w, L, key}, B.at(bupd(bs, e, B.BF{w, L, key}), e), Equal.sym(B.Bk, B.at(bupd(bs, e, B.BF{w, L, key}), e), B.BF{w, L, key}, eat), hc)
420	      Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(B.lnk(B.at(bupd(bs, e, B.BF{w, L, key}), e))))), S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q), LK.lookup_hit(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), q, n, huq2, e, hen, hk2),
421	        Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(B.lnk(B.at(bupd(bs, e, B.BF{w, L, key}), e))))), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(L))), S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q), Equal.cong(B.Bk, Maybe<&2, V>, y => ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(B.lnk(y)))), B.at(bupd(bs, e, B.BF{w, L, key}), e), B.BF{w, L, key}, eat),
422	          Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), UD.v(H.slot(L))), Some{x}, S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q), T.nthm_upd_same(~V, vsl, UD.v(H.slot(L)), Some{x}, hs), Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q), Some{x}, SL.lookup_set_same(~V, ST.absm(~V, bs, vsl, n, 0n), key, x, q, hc)))))
423	    case False{}:
424	      Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q), S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q), lk_other(~V, bs, e, he, w, L, key, vsl, x, n, hen, hs, hz, huq, hno, hns, q, hc, B.all_lt(B.PNo{bs, q}, n), {==}), Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q), S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), q), SL.lookup_set_other(~V, ST.absm(~V, bs, vsl, n, 0n), key, x, q, hc)))
425	
426	# THEOREM: putting an absent key into an empty bucket, with its value in an
427	# unused slot, looks every key up as the specification's set does
428	def lookup_ins(~V: Data, +bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +vsl: List<&2, Maybe<&2, V>>, +x: V, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}, +q: String) -> {S.lookup(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n), q) == S.lookup(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x), q) : Maybe<&2, V>}:
429	  lk_c(~V, bs, e, he, w, L, key, vsl, x, n, hen, hs, hz, huq, hno, hns, q, S.str_eq(key, q), {==})
430	
431	# THEOREM: ... and adds one entry
432	def size_ins(~V: Data, +bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +vsl: List<&2, Maybe<&2, V>>, +x: V, +n: Nat, +hen: {Nat.is_lt(e, n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(L)), SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}, +hz: {B.at(bs, e) == B.BE{} : B.Bk}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +hns: {ST.noslot(bs, UD.v(H.slot(L)), n) == True{} : Bool}, +fr: Nat, +fr2: Nat, +hle: {Nat.is_le(fr, fr2) == True{} : Bool}, +hs2: {Nat.is_lt(UD.v(H.slot(L)), fr2) == True{} : Bool}, +hl: {B.all_lt(B.PLive{bs, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}) -> {S.size(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n)) == S.size(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x)) : Nat}:
433	  Equal.trans(Nat, S.size(~V, ST.absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), n, 0n)), IV.occn(bupd(bs, e, B.BF{w, L, key}), n), S.size(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x)), SZ.size_absm(~V, bupd(bs, e, B.BF{w, L, key}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(L)), Some{x}), fr2, n, live_up(~V, bs, e, he, w, L, key, vsl, x, hs, fr, fr2, hle, hs2, n, hl, n, N.le_refl(n)), n, N.le_refl(n)),
434	    Equal.trans(Nat, IV.occn(bupd(bs, e, B.BF{w, L, key}), n), 1n+IV.occn(bs, n), S.size(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x)), occn_up(bs, e, B.BF{w, L, key}, {==}, he, hz, n, hen),
435	      Equal.trans(Nat, 1n+IV.occn(bs, n), 1n+S.size(~V, ST.absm(~V, bs, vsl, n, 0n)), S.size(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x)), Equal.cong(Nat, Nat, z => 1n+z, IV.occn(bs, n), S.size(~V, ST.absm(~V, bs, vsl, n, 0n)), Equal.sym(Nat, S.size(~V, ST.absm(~V, bs, vsl, n, 0n)), IV.occn(bs, n), SZ.size_absm(~V, bs, vsl, fr, n, hl, n, N.le_refl(n)))), Equal.sym(Nat, S.size(~V, S.set(~V, ST.absm(~V, bs, vsl, n, 0n), key, x)), 1n+S.size(~V, ST.absm(~V, bs, vsl, n, 0n)), SL.size_set_new(~V, ST.absm(~V, bs, vsl, n, 0n), key, x, LK.lookup_none(~V, bs, vsl, key, n, hno))))))