proofs/containers/lru/rmat.bend source
proofs/containers/lru/rmat.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/table.bend as TBimport ../hash_table/buckets.bend as Bimport ../hash_table/cyc.bend as CYimport ../hash_table/inv.bend as IVimport ../hash_table/state.bend as HTimport ../hash_table/insm.bend as IMimport ../hash_table/delw.bend as DWimport ./state.bend as STimport ./basic.bend as BAimport ./bump.bend as BUimport ./bumpsh.bend as BSimport ./unlink.bend as ULimport ./drop.bend as DRimport ./touchsh.bend as TSHimport ./rmrb.bend as RRimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32# Removing the entry of slot s whose bucket is i: the bucket is deleted,# the slot unlinked and freed, and a removal (or eviction) counted.# the operation r agrees with spec: the same result, and the modeldef POK(~V: Data, -X: Data, spec: SP.Lru<V> & X, r: LR.LRU<&2, V> & X) -> Type: Sigma<&1, &1, ST.Sh<V>, sh2 => Sigma<&1, &1, X, x => {r == (ST.real(~V, sh2), x) : LR.LRU<&2, V> & X} & ({spec == (ST.model(~V, sh2), x) : SP.Lru<V> & X} & {ST.good(~V, sh2) == True{} : Bool})>>def fin_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +tabT2: AR.Tree<U32>, +t2: AR.Tree<U32>, +hm2: {ST.model(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}) == SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ST.ctr(AR.slots(U32, mT))} : SP.Lru<V>}, -r: LR.LRU<&2, V> & Maybe<&2, V>, +er: {r == (LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}) : LR.LRU<&2, V> & Maybe<&2, V>}, co: BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})))) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), r): match co: case Tuple{+sh3, Tuple{+e3, Tuple{+em3, g3}}}: +ees = Equal.cong(SP.Lru<V>, List<&2, SP.Ent<V>>, z => ST.lru_es(~V, z), ST.model(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ST.ctr(AR.slots(U32, mT))}, hm2) +em = Equal.trans(SP.Lru<V>, ST.model(~V, sh3), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, em3, Equal.cong(List<&2, SP.Ent<V>>, SP.Lru<V>, z => SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ees)) +r1 = Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, r, (LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}), (ST.real(~V, sh3), Some{v}), er, Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => (z, Some{v}), LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), ST.real(~V, sh3), e3)) (sh3, (Some{v}, (r1, (Equal.cong(SP.Lru<V>, SP.Lru<V> & Maybe<&2, V>, z => (z, Some{v}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, ST.model(~V, sh3), Equal.sym(SP.Lru<V>, ST.model(~V, sh3), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, em)), g3))))def fin_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +tabT2: AR.Tree<U32>, +t2: AR.Tree<U32>, +hm2: {ST.model(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}) == SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ST.ctr(AR.slots(U32, mT))} : SP.Lru<V>}, -r: LR.LRU<&2, V> & Maybe<&2, V>, +er: {r == (LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}) : LR.LRU<&2, V> & Maybe<&2, V>}, co: BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})))) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), r): match co: case Tuple{+sh3, Tuple{+e3, Tuple{+em3, g3}}}: +ees = Equal.cong(SP.Lru<V>, List<&2, SP.Ent<V>>, z => ST.lru_es(~V, z), ST.model(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ST.ctr(AR.slots(U32, mT))}, hm2) +em = Equal.trans(SP.Lru<V>, ST.model(~V, sh3), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, em3, Equal.cong(List<&2, SP.Ent<V>>, SP.Lru<V>, z => SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ees)) +r1 = Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, r, (LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}), (ST.real(~V, sh3), Some{v}), er, Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => (z, Some{v}), LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), ST.real(~V, sh3), e3)) (sh3, (Some{v}, (r1, (Equal.cong(SP.Lru<V>, SP.Lru<V> & Maybe<&2, V>, z => (z, Some{v}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, ST.model(~V, sh3), Equal.sym(SP.Lru<V>, ST.model(~V, sh3), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, em)), g3))))def rmu_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, -r1: LR.LRU<&2, V>, u: UL.UnlOK(~V, cap, n, free, mT, tabT2, ksT, eT, lkT, sd, a, s, b, r1)) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_core(&2, V, r1, su, 2)): match u: case Tuple{+t2, Tuple{+tr, Tuple{+e1, Tuple{+p2, Tuple{+s2, Tuple{+l1, Tuple{+i1, g0}}}}}}}: +g2 = {g0 : {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}} +hsd = RR.f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm) +hs0 = RR.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm) +E1 = Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => LR.drop_core(&2, V, z, su, 2), r1, LR.F{cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t2)}, e1) +E2 = DR.drop_ok(~V, one, h1, cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, mT, tabT2, ksT, eT, t2, sd, hsd, p2, ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), su, s, hsv, hs0, 2) +E3 = Equal.cong(Maybe<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => (LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v}, hm) +er = Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.drop_core(&2, V, r1, su, 2), LR.drop_core(&2, V, LR.F{cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t2)}, su, 2), (LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}), E1, Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.drop_core(&2, V, LR.F{cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t2)}, su, 2), (LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s)), (LR.fbump(&2, V, 2, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}), E2, E3)) +hg2 = RR.good_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm) +hm2 = RR.model_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm, key, hk) co = BS.count_rm(~V, cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}, hg2, BU.bump_ok(mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), 2, 20n, {==}, {==}, {==})) fin_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, tabT2, t2, hm2, LR.drop_core(&2, V, r1, su, 2), er, co)def rmd_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, d: DW.DelAt2(AR.slots(String, ksT), k, tabT, i)) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2)): match d: case Tuple{+tabT2, Tuple{+e, hd}}: +hsd = TSH.sd29(k, sd, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +E0 = Equal.cong(Array<U32>, LR.LRU<&2, V> & Maybe<&2, V>, z => LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), z, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(U32, tabT2), e) ok = rmu_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, tabT2, hd, LR.unlink(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su), UL.unlink_ok(~V, one, h1, lkT, sd, hsd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), cap, n, free, mT, tabT2, ksT, eT, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), head, tail, su, a, s, b, hsv, ST.g_cdll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_ctail(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), z), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2), E0), ok)def rmx_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2)): +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==}) +cn = N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), ST.g_cn(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +hem = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(k)) == True{} : Bool}, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), cn, BA.n_lt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) rmd_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, DW.del_ok2(k, hk31, AR.slots(String, ksT), tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), i, hi, ST.g_cclus(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cuniq(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), hoi, hem))def rms_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +s: Nat, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, sp: NL.Split(s, sl)) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2)): match sp: case Tuple{+a, Tuple{+b, +e}}: +hg2 = L.subst(List<&2, Nat>, z => {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, z, fl}) == True{} : Bool}, sl, SC.append(Nat, a, Con{s, b}), e, hg) L.subst(List<&2, Nat>, z => POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), z), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2)), SC.append(Nat, a, Con{s, b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{s, b}), e), rmx_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg2, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk))# THEOREM: removing the entry of the listed slot s (bucket i), counted by c_rmdef rm_at_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2)): rms_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, NL.split_mem(s, sl, hmem))def rmu_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, -r1: LR.LRU<&2, V>, u: UL.UnlOK(~V, cap, n, free, mT, tabT2, ksT, eT, lkT, sd, a, s, b, r1)) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_core(&2, V, r1, su, 1)): match u: case Tuple{+t2, Tuple{+tr, Tuple{+e1, Tuple{+p2, Tuple{+s2, Tuple{+l1, Tuple{+i1, g0}}}}}}}: +g2 = {g0 : {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}} +hsd = RR.f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm) +hs0 = RR.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm) +E1 = Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => LR.drop_core(&2, V, z, su, 1), r1, LR.F{cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t2)}, e1) +E2 = DR.drop_ok(~V, one, h1, cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, mT, tabT2, ksT, eT, t2, sd, hsd, p2, ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), su, s, hsv, hs0, 1) +E3 = Equal.cong(Maybe<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => (LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v}, hm) +er = Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.drop_core(&2, V, r1, su, 1), LR.drop_core(&2, V, LR.F{cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t2)}, su, 1), (LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}), E1, Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.drop_core(&2, V, LR.F{cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t2)}, su, 1), (LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s)), (LR.fbump(&2, V, 1, ST.real(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}})), Some{v}), E2, E3)) +hg2 = RR.good_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm) +hm2 = RR.model_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, p2, s2, l1, i1, g2, su, hsv, v, hm, key, hk) co = BS.count_ev(~V, cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}, hg2, BU.bump_ok(mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), 1, 18n, {==}, {==}, {==})) fin_ev(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, tabT2, t2, hm2, LR.drop_core(&2, V, r1, su, 1), er, co)def rmd_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, d: DW.DelAt2(AR.slots(String, ksT), k, tabT, i)) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1)): match d: case Tuple{+tabT2, Tuple{+e, hd}}: +hsd = TSH.sd29(k, sd, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +E0 = Equal.cong(Array<U32>, LR.LRU<&2, V> & Maybe<&2, V>, z => LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), z, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(U32, tabT2), e) ok = rmu_ev(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, tabT2, hd, LR.unlink(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su), UL.unlink_ok(~V, one, h1, lkT, sd, hsd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), cap, n, free, mT, tabT2, ksT, eT, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), head, tail, su, a, s, b, hsv, ST.g_cdll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_ctail(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), z), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT2), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1), E0), ok)def rmx_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1)): +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==}) +cn = N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), ST.g_cn(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +hem = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(k)) == True{} : Bool}, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), cn, BA.n_lt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) rmd_ev(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, DW.del_ok2(k, hk31, AR.slots(String, ksT), tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), i, hi, ST.g_cclus(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cuniq(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), hoi, hem))def rms_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +s: Nat, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, sp: NL.Split(s, sl)) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1)): match sp: case Tuple{+a, Tuple{+b, +e}}: +hg2 = L.subst(List<&2, Nat>, z => {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, z, fl}) == True{} : Bool}, sl, SC.append(Nat, a, Con{s, b}), e, hg) L.subst(List<&2, Nat>, z => POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), z), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1)), SC.append(Nat, a, Con{s, b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{s, b}), e), rmx_ev(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg2, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk))# THEOREM: removing the entry of the listed slot s (bucket i), counted by c_evdef rm_at_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> POK(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 1)): rms_ev(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk, NL.split_mem(s, sl, hmem))