proofs/containers/lru/tabsl.bend
bend-collections-laws-containers@1.0.0.0 · 201 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as A
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/rehash.bend as RH
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as TL
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/words.bend as WR
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/tfind.bend as TF
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
18
19# The table and the recency list across table changes: copies of buckets
20# (a rehash, a backward shift) and an emptied bucket.
21
22
23# ---- a bucket with word w and link l ----
24
25def AnybAt(+bs: List<&2, B.Bk>, +m: Nat, +l: U32, +w: U32) -> Type:
26 Sigma<&1, &1, Nat, j => {Nat.is_lt(j, m) == True{} : Bool} & {ST.isbf(B.at(bs, j), w, l) == True{} : Bool}>
27
28def ab_up(+bs: List<&2, B.Bk>, +q: Nat, +l: U32, +w: U32, e: AnybAt(bs, q, l, w)) -> AnybAt(bs, 1n+q, l, w):
29 match e:
30 case Tuple{+j, Tuple{+hj, hb}}:
31 (j, (N.lt_trans(j, q, 1n+q, hj, N.lt_succ(q)), hb))
32
33def ab_c(+bs: List<&2, B.Bk>, +q: Nat, +l: U32, +w: U32, +c: Bool, +hc: {ST.isbf(B.at(bs, q), w, l) == c : Bool}, +h: {Bool.or(c, ST.anyb(bs, q, l, w)) == True{} : Bool}, rec: @h2: {ST.anyb(bs, q, l, w) == True{} : Bool} -> AnybAt(bs, q, l, w)) -> AnybAt(bs, 1n+q, l, w):
34 match c:
35 case True{}:
36 (q, (N.lt_succ(q), hc))
37 case False{}:
38 ab_up(bs, q, l, w, rec(h))
39
40
41# some bucket below m has word w and link l: one is found
42def find_anyb(+bs: List<&2, B.Bk>, +m: Nat, +l: U32, +w: U32, +h: {ST.anyb(bs, m, l, w) == True{} : Bool}) -> AnybAt(bs, m, l, w):
43 match m:
44 case 0n:
45 Empty.absurd(AnybAt(bs, 0n, l, w), L.false_true(h))
46 case 1n+q:
47 ab_c(bs, q, l, w, ST.isbf(B.at(bs, q), w, l), {==}, h, h2 => find_anyb(bs, q, l, w, h2))
48
49def ai_c(+bs: List<&2, B.Bk>, +q: Nat, +l: U32, +w: U32, +j: Nat, +hj: {Nat.is_lt(j, 1n+q) == True{} : Bool}, +h: {ST.isbf(B.at(bs, j), w, l) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(j, q) == c : Bool}, rec: @hq: {Nat.is_lt(j, q) == True{} : Bool} -> {ST.anyb(bs, q, l, w) == True{} : Bool}) -> {ST.anyb(bs, 1n+q, l, w) == True{} : Bool}:
50 match c:
51 case True{}:
52 NL.or_tl(ST.isbf(B.at(bs, q), w, l), ST.anyb(bs, q, l, w), L.subst(Nat, z => {ST.isbf(B.at(bs, z), w, l) == True{} : Bool}, j, q, N.eq_from_is_eq(j, q, hc), h))
53 case False{}:
54 NL.or_tr(ST.isbf(B.at(bs, q), w, l), ST.anyb(bs, q, l, w), rec(N.lt_or_eq(j, q, N.lt_succ_le(j, q, hj), hc)))
55
56def anyb_intro(+bs: List<&2, B.Bk>, +m: Nat, +l: U32, +w: U32, +j: Nat, +hj: {Nat.is_lt(j, m) == True{} : Bool}, +h: {ST.isbf(B.at(bs, j), w, l) == True{} : Bool}) -> {ST.anyb(bs, m, l, w) == True{} : Bool}:
57 match m:
58 case 0n:
59 Empty.absurd({ST.anyb(bs, 0n, l, w) == True{} : Bool}, N.lt_zero_absurd(j, hj))
60 case 1n+q:
61 ai_c(bs, q, l, w, j, hj, h, Nat.is_eq(j, q), {==}, hq => anyb_intro(bs, q, l, w, j, hq, h))
62
63def isbf_occ(+b: B.Bk, +w: U32, +l: U32, +h: {ST.isbf(b, w, l) == True{} : Bool}) -> {B.occ(b) == True{} : Bool}:
64 match b:
65 case B.BE{}:
66 Empty.absurd({B.occ(B.BE{}) == True{} : Bool}, L.false_true(h))
67 case B.BF{+x, +y, +k}:
68 {==}
69
70# ---- copies: every old bucket has a copy ----
71
72def ht1(+nw: List<&2, B.Bk>, +n2: Nat, +l: U32, +w: U32, +b: B.Bk, +hb: {ST.isbf(b, w, l) == True{} : Bool}, e: RH.EqAt(nw, n2, b)) -> {ST.anyb(nw, n2, l, w) == True{} : Bool}:
73 match e:
74 case Tuple{+j2, Tuple{+hj2, e2}}:
75 anyb_intro(nw, n2, l, w, j2, hj2, L.subst(B.Bk, z => {ST.isbf(z, w, l) == True{} : Bool}, b, B.at(nw, j2), Equal.sym(B.Bk, B.at(nw, j2), b, e2), hb))
76
77def ht0(+od: List<&2, B.Bk>, +nw: List<&2, B.Bk>, +no: Nat, +n2: Nat, +hto: {B.all_lt(B.PTo{od, nw, n2}, no) == True{} : Bool}, +l: U32, +w: U32, e: AnybAt(od, no, l, w)) -> {ST.anyb(nw, n2, l, w) == True{} : Bool}:
78 match e:
79 case Tuple{+j, Tuple{+hj, hb}}:
80 +hbb = {hb : {ST.isbf(B.at(od, j), w, l) == True{} : Bool}}
81 +hae = B.imp_elim(B.occ(B.at(od, j)), B.anyeq(nw, n2, B.at(od, j)), B.all_inst(B.PTo{od, nw, n2}, no, hto, j, hj), isbf_occ(B.at(od, j), w, l, hbb))
82 ht1(nw, n2, l, w, B.at(od, j), hbb, RH.find_eq(nw, n2, B.at(od, j), hae))
83
84# THEOREM: a table holding copies of all old buckets has a bucket for every slot
85def has_to(~V: Data, +od: List<&2, B.Bk>, +nw: List<&2, B.Bk>, +no: Nat, +n2: Nat, +hto: {B.all_lt(B.PTo{od, nw, n2}, no) == True{} : Bool}, +ll: List<&2, U32>, +sl: List<&2, Nat>, +h: {ST.hasall(~V, od, no, ll, sl) == True{} : Bool}) -> {ST.hasall(~V, nw, n2, ll, sl) == True{} : Bool}:
86 match sl:
87 case Nil{}:
88 {==}
89 case Con{+s, +t}:
90 +h0 = L.and_left(ST.anyb(od, no, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, od, no, ll, t), h)
91 L.and_intro(ST.anyb(nw, n2, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, nw, n2, ll, t), ht0(od, nw, no, n2, hto, LK.lnk(s), ST.lw(ll, s, 2n), find_anyb(od, no, LK.lnk(s), ST.lw(ll, s, 2n), h0)), has_to(~V, od, nw, no, n2, hto, ll, t, L.and_right(ST.anyb(od, no, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, od, no, ll, t), h)))
92
93# ---- copies: every new bucket is a copy ----
94
95def bf1(+od: List<&2, B.Bk>, +no: Nat, +sl: List<&2, Nat>, +ll: List<&2, U32>, +h: {ST.bsl(od, sl, ll, no) == True{} : Bool}, +b: B.Bk, e: RH.EqAt(od, no, b)) -> {ST.bslb(sl, ll, b) == True{} : Bool}:
96 match e:
97 case Tuple{+j, Tuple{+hj, e2}}:
98 L.subst(B.Bk, z => {ST.bslb(sl, ll, z) == True{} : Bool}, B.at(od, j), b, e2, TF.bsl_inst(od, sl, ll, no, h, j, hj))
99
100def bf0(+od: List<&2, B.Bk>, +no: Nat, +sl: List<&2, Nat>, +ll: List<&2, U32>, +h: {ST.bsl(od, sl, ll, no) == True{} : Bool}, +b: B.Bk, +hq: {B.implies(B.occ(b), B.anyeq(od, no, b)) == True{} : Bool}) -> {ST.bslb(sl, ll, b) == True{} : Bool}:
101 match b:
102 case B.BE{}:
103 {==}
104 case B.BF{+w, +l, +k}:
105 bf1(od, no, sl, ll, h, B.BF{w, l, k}, RH.find_eq(od, no, B.BF{w, l, k}, hq))
106
107# THEOREM: a table of copies of old buckets keeps the slot correspondence
108def bsl_from(+nw: List<&2, B.Bk>, +od: List<&2, B.Bk>, +no: Nat, +n2: Nat, +hf: {B.all_lt(B.PFrom{nw, od, no}, n2) == True{} : Bool}, +sl: List<&2, Nat>, +ll: List<&2, U32>, +h: {ST.bsl(od, sl, ll, no) == True{} : Bool}) -> {ST.bsl(nw, sl, ll, n2) == True{} : Bool}:
109 match n2:
110 case 0n:
111 {==}
112 case 1n+q:
113 L.and_intro(ST.bslb(sl, ll, B.at(nw, q)), ST.bsl(nw, sl, ll, q), bf0(od, no, sl, ll, h, B.at(nw, q), L.and_left(B.eval(B.PFrom{nw, od, no}, q), B.all_lt(B.PFrom{nw, od, no}, q), hf)), bsl_from(nw, od, no, q, L.and_right(B.eval(B.PFrom{nw, od, no}, q), B.all_lt(B.PFrom{nw, od, no}, q), hf), sl, ll, h))
114
115# ---- an emptied bucket ----
116
117def ib_c(+bs: List<&2, B.Bk>, +i: Nat, +hlen: {Nat.is_lt(i, SC.length(B.Bk, bs)) == True{} : Bool}, +q: Nat, +l: U32, +w: U32, +hne: {ST.isbf(B.at(bs, i), w, l) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, q) == c : Bool}) -> {ST.isbf(B.at(IM.bupd(bs, i, B.BE{}), q), w, l) == ST.isbf(B.at(bs, q), w, l) : Bool}:
118 match c:
119 case True{}:
120 +e = N.eq_from_is_eq(i, q, hc)
121 Equal.trans(Bool, ST.isbf(B.at(IM.bupd(bs, i, B.BE{}), q), w, l), False{}, ST.isbf(B.at(bs, q), w, l), Equal.cong(B.Bk, Bool, z => ST.isbf(z, w, l), B.at(IM.bupd(bs, i, B.BE{}), q), B.BE{}, IM.at_bu_eq(bs, i, B.BE{}, hlen, q, hc)), Equal.sym(Bool, ST.isbf(B.at(bs, q), w, l), False{}, L.subst(Nat, z => {ST.isbf(B.at(bs, z), w, l) == False{} : Bool}, i, q, e, hne)))
122 case False{}:
123 Equal.cong(B.Bk, Bool, z => ST.isbf(z, w, l), B.at(IM.bupd(bs, i, B.BE{}), q), B.at(bs, q), IM.at_bupd_other(bs, i, B.BE{}, q, hc))
124
125# emptying a bucket that does not have word w and link l keeps any other
126def anyb_rm(+bs: List<&2, B.Bk>, +i: Nat, +hlen: {Nat.is_lt(i, SC.length(B.Bk, bs)) == True{} : Bool}, +l: U32, +w: U32, +hne: {ST.isbf(B.at(bs, i), w, l) == False{} : Bool}, +m: Nat) -> {ST.anyb(IM.bupd(bs, i, B.BE{}), m, l, w) == ST.anyb(bs, m, l, w) : Bool}:
127 match m:
128 case 0n:
129 {==}
130 case 1n+q:
131 +e1 = Equal.cong(Bool, Bool, z => Bool.or(z, ST.anyb(IM.bupd(bs, i, B.BE{}), q, l, w)), ST.isbf(B.at(IM.bupd(bs, i, B.BE{}), q), w, l), ST.isbf(B.at(bs, q), w, l), ib_c(bs, i, hlen, q, l, w, hne, Nat.is_eq(i, q), {==}))
132 Equal.trans(Bool, ST.anyb(IM.bupd(bs, i, B.BE{}), 1n+q, l, w), Bool.or(ST.isbf(B.at(bs, q), w, l), ST.anyb(IM.bupd(bs, i, B.BE{}), q, l, w)), ST.anyb(bs, 1n+q, l, w), e1, Equal.cong(Bool, Bool, z => Bool.or(ST.isbf(B.at(bs, q), w, l), z), ST.anyb(IM.bupd(bs, i, B.BE{}), q, l, w), ST.anyb(bs, q, l, w), anyb_rm(bs, i, hlen, l, w, hne, q)))
133
134def isbf_ne_c(+w0: U32, +l0: U32, +w: U32, +lx: U32, +s: Nat, +x: Nat, +hsi: {UD.v(H.slot(l0)) == s : Nat}, +hx: {UD.v(H.slot(lx)) == x : Nat}, +hne: {Nat.is_eq(x, s) == False{} : Bool}, +c: Bool, +hc: {U32.is_eq(l0, lx) == c : Bool}) -> {Bool.and(U32.is_eq(w0, w), c) == False{} : Bool}:
135 match c:
136 case False{}:
137 WR.and_false(U32.is_eq(w0, w))
138 case True{}:
139 +el = A.eq_of(l0, lx, hc)
140 +exq = Equal.trans(Nat, x, UD.v(H.slot(lx)), s, Equal.sym(Nat, UD.v(H.slot(lx)), x, hx), Equal.trans(Nat, UD.v(H.slot(lx)), UD.v(H.slot(l0)), s, Equal.cong(U32, Nat, z => UD.v(H.slot(z)), lx, l0, Equal.sym(U32, l0, lx, el)), hsi))
141 Empty.absurd({Bool.and(U32.is_eq(w0, w), True{}) == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_eq(x, s), False{}, Equal.sym(Bool, Nat.is_eq(x, s), True{}, L.subst(Nat, z => {Nat.is_eq(x, z) == True{} : Bool}, x, s, exq, N.is_eq_refl(x))), hne)))
142
143# the emptied bucket (slot s) is not the bucket of another slot x
144def isbf_ne(+b: B.Bk, +w: U32, +lx: U32, +s: Nat, +x: Nat, +hsi: {UD.v(H.slot(B.lnk(b))) == s : Nat}, +hx: {UD.v(H.slot(lx)) == x : Nat}, +hne: {Nat.is_eq(x, s) == False{} : Bool}) -> {ST.isbf(b, w, lx) == False{} : Bool}:
145 match b:
146 case B.BE{}:
147 {==}
148 case B.BF{+w0, +l0, +k0}:
149 isbf_ne_c(w0, l0, w, lx, s, x, hsi, hx, hne, U32.is_eq(l0, lx), {==})
150
151# THEOREM: emptying slot s's bucket leaves a bucket for every other slot
152def has_rm(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +bs: List<&2, B.Bk>, +no: Nat, +i: Nat, +hlen: {Nat.is_lt(i, SC.length(B.Bk, bs)) == True{} : Bool}, +s: Nat, +hsi: {UD.v(H.slot(B.lnk(B.at(bs, i)))) == s : Nat}, +ll: List<&2, U32>, +xs: List<&2, Nat>, +hs: {NL.memn(s, xs) == False{} : Bool}, +hb: {ST.sall(~V, ST.PLive{fr, el}, xs) == True{} : Bool}, +h: {ST.hasall(~V, bs, no, ll, xs) == True{} : Bool}) -> {ST.hasall(~V, IM.bupd(bs, i, B.BE{}), no, ll, xs) == True{} : Bool}:
153 match xs:
154 case Nil{}:
155 {==}
156 case Con{+x, +t}:
157 +hx0 = UL.bnd_of(~V, x, Con{x, t}, fr, el, sd, hfr, hb, UL.self_in(x, t))
158 +hxs = NL.or_ff_l(Nat.is_eq(x, s), NL.memn(s, t), hs)
159 +hn = isbf_ne(B.at(bs, i), ST.lw(ll, x, 2n), LK.lnk(x), s, x, hsi, UL.ix_o(one, h1, x, sd, hsd, hx0), hxs)
160 +e = anyb_rm(bs, i, hlen, LK.lnk(x), ST.lw(ll, x, 2n), hn, no)
161 +h0 = L.and_left(ST.anyb(bs, no, LK.lnk(x), ST.lw(ll, x, 2n)), ST.hasall(~V, bs, no, ll, t), h)
162 L.and_intro(ST.anyb(IM.bupd(bs, i, B.BE{}), no, LK.lnk(x), ST.lw(ll, x, 2n)), ST.hasall(~V, IM.bupd(bs, i, B.BE{}), no, ll, t), Equal.trans(Bool, ST.anyb(IM.bupd(bs, i, B.BE{}), no, LK.lnk(x), ST.lw(ll, x, 2n)), ST.anyb(bs, no, LK.lnk(x), ST.lw(ll, x, 2n)), True{}, e, h0), has_rm(~V, one, h1, sd, hsd, fr, el, hfr, bs, no, i, hlen, s, hsi, ll, t, NL.or_ff_r(Nat.is_eq(x, s), NL.memn(s, t), hs), L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.sall(~V, ST.PLive{fr, el}, t), hb), L.and_right(ST.anyb(bs, no, LK.lnk(x), ST.lw(ll, x, 2n)), ST.hasall(~V, bs, no, ll, t), h)))
163
164def brm_b(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +ll: List<&2, U32>, +b0: B.Bk, +hb: {ST.bslb(SC.append(Nat, a, Con{s, b}), ll, b0) == True{} : Bool}, +hne: {B.implies(B.occ(b0), Bool.not(Nat.is_eq(s, UD.v(H.slot(B.lnk(b0)))))) == True{} : Bool}) -> {ST.bslb(SC.append(Nat, a, b), ll, b0) == True{} : Bool}:
165 match b0:
166 case B.BE{}:
167 {==}
168 case B.BF{+w, +l, +k}:
169 +x = UD.v(H.slot(l))
170 +hm = L.and_left(NL.memn(x, SC.append(Nat, a, Con{s, b})), U32.is_eq(ST.lw(ll, x, 2n), w), hb)
171 +hm2 = L.subst(Bool, z => {z == True{} : Bool}, NL.memn(x, SC.append(Nat, a, Con{s, b})), Bool.or(NL.memn(x, SC.append(Nat, a, b)), Nat.is_eq(s, x)), NL.memn_mid(x, a, s, b), hm)
172 +hm3 = L.subst(Bool, z => {Bool.or(NL.memn(x, SC.append(Nat, a, b)), z) == True{} : Bool}, Nat.is_eq(s, x), False{}, L.not_true(Nat.is_eq(s, x), hne), hm2)
173 L.and_intro(NL.memn(x, SC.append(Nat, a, b)), U32.is_eq(ST.lw(ll, x, 2n), w), Equal.trans(Bool, NL.memn(x, SC.append(Nat, a, b)), Bool.or(NL.memn(x, SC.append(Nat, a, b)), False{}), True{}, Equal.sym(Bool, Bool.or(NL.memn(x, SC.append(Nat, a, b)), False{}), NL.memn(x, SC.append(Nat, a, b)), WR.or_false(NL.memn(x, SC.append(Nat, a, b)))), hm3), L.and_right(NL.memn(x, SC.append(Nat, a, Con{s, b})), U32.is_eq(ST.lw(ll, x, 2n), w), hb))
174
175
176def imp_ne(+bs: List<&2, B.Bk>, +no: Nat, +huq: {B.all_lt(B.PUniq{bs}, no) == True{} : Bool}, +i: Nat, +q: Nat, +hi: {Nat.is_lt(i, no) == True{} : Bool}, +hq: {Nat.is_lt(q, no) == True{} : Bool}, +hqi: {Nat.is_eq(q, i) == False{} : Bool}, +hoi: {B.occ(B.at(bs, i)) == True{} : Bool}, +s: Nat, +hsi: {UD.v(H.slot(B.lnk(B.at(bs, i)))) == s : Nat}, +c: Bool, +hc: {B.occ(B.at(bs, q)) == c : Bool}) -> {B.implies(c, Bool.not(Nat.is_eq(s, UD.v(H.slot(B.lnk(B.at(bs, q))))))) == True{} : Bool}:
177 match c:
178 case False{}:
179 {==}
180 case True{}:
181 +e0 = TL.slot_ne(bs, no, huq, i, q, hi, hq, hqi, hoi, hc)
182 +e1 = L.subst(Nat, z => {Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, q)))), z) == False{} : Bool}, UD.v(H.slot(B.lnk(B.at(bs, i)))), s, hsi, e0)
183 NL.not_f(Nat.is_eq(s, UD.v(H.slot(B.lnk(B.at(bs, q))))), NL.ne_sym(UD.v(H.slot(B.lnk(B.at(bs, q)))), s, e1))
184
185def br_c(+bs: List<&2, B.Bk>, +no: Nat, +huq: {B.all_lt(B.PUniq{bs}, no) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, no) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, bs)) == True{} : Bool}, +hoi: {B.occ(B.at(bs, i)) == True{} : Bool}, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hsi: {UD.v(H.slot(B.lnk(B.at(bs, i)))) == s : Nat}, +ll: List<&2, U32>, +h: {ST.bsl(bs, SC.append(Nat, a, Con{s, b}), ll, no) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, no) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, q) == c : Bool}) -> {ST.bslb(SC.append(Nat, a, b), ll, B.at(IM.bupd(bs, i, B.BE{}), q)) == True{} : Bool}:
186 match c:
187 case True{}:
188 L.subst(B.Bk, z => {ST.bslb(SC.append(Nat, a, b), ll, z) == True{} : Bool}, B.BE{}, B.at(IM.bupd(bs, i, B.BE{}), q), Equal.sym(B.Bk, B.at(IM.bupd(bs, i, B.BE{}), q), B.BE{}, IM.at_bu_eq(bs, i, B.BE{}, hlen, q, hc)), {==})
189 case False{}:
190 +hb = brm_b(a, s, b, ll, B.at(bs, q), TF.bsl_inst(bs, SC.append(Nat, a, Con{s, b}), ll, no, h, q, hq), imp_ne(bs, no, huq, i, q, hi, hq, NL.ne_sym(i, q, hc), hoi, s, hsi, B.occ(B.at(bs, q)), {==}))
191 L.subst(B.Bk, z => {ST.bslb(SC.append(Nat, a, b), ll, z) == True{} : Bool}, B.at(bs, q), B.at(IM.bupd(bs, i, B.BE{}), q), Equal.sym(B.Bk, B.at(IM.bupd(bs, i, B.BE{}), q), B.at(bs, q), IM.at_bupd_other(bs, i, B.BE{}, q, hc)), hb)
192
193# THEOREM: emptying slot s's bucket: every full bucket's slot is listed
194# once s is taken off the list
195def bsl_rm(+bs: List<&2, B.Bk>, +no: Nat, +huq: {B.all_lt(B.PUniq{bs}, no) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, no) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, bs)) == True{} : Bool}, +hoi: {B.occ(B.at(bs, i)) == True{} : Bool}, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hsi: {UD.v(H.slot(B.lnk(B.at(bs, i)))) == s : Nat}, +ll: List<&2, U32>, +h: {ST.bsl(bs, SC.append(Nat, a, Con{s, b}), ll, no) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, no) == True{} : Bool}) -> {ST.bsl(IM.bupd(bs, i, B.BE{}), SC.append(Nat, a, b), ll, m) == True{} : Bool}:
196 match m:
197 case 0n:
198 {==}
199 case 1n+q:
200 +hq = N.succ_le_lt(q, no, hm)
201 L.and_intro(ST.bslb(SC.append(Nat, a, b), ll, B.at(IM.bupd(bs, i, B.BE{}), q)), ST.bsl(IM.bupd(bs, i, B.BE{}), SC.append(Nat, a, b), ll, q), br_c(bs, no, huq, i, hi, hlen, hoi, a, s, b, hsi, ll, h, q, hq, Nat.is_eq(i, q), {==}), bsl_rm(bs, no, huq, i, hi, hlen, hoi, a, s, b, hsi, ll, h, q, N.lt_le(q, no, hq)))