1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32alg.bend as A 5 import ../../../spec/lib/common.bend as SC 6 import ../../lib/u32div.bend as UD 7 import ../../../src/containers/hash_table.bend as H 8 import ../hash_table/buckets.bend as B 9 import ../hash_table/insm.bend as IM 10 import ../hash_table/rehash.bend as RH 11 import ../hash_table/tools.bend as TL 12 import ../hash_table/words.bend as WR 13 import ./state.bend as ST 14 import ./tfind.bend as TF 15 import ./unlink.bend as UL 16 import ../../lib/nat_list.bend as NL 17 import ../../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 25 def 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 28 def 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 33 def 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 42 def 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 49 def 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 56 def 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 63 def 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 72 def 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 77 def 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 85 def 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 95 def 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 100 def 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 108 def 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 117 def 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 126 def 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 134 def 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 144 def 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 152 def 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 164 def 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 176 def 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 185 def 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 195 def 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)))