proofs/containers/lru/remove.bend source
proofs/containers/lru/remove.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32alg.bend as Aimport ../../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/keys.bend as Kimport ./state.bend as STimport ./basic.bend as BAimport ./find.bend as FDimport ./tfind.bend as TFimport ./touch.bend as TOimport ./rmat.bend as RMimport ./unlink.bend as ULimport ../hash_table/get.bend as Gimport ../../../src/math/hash.bend as HSimport ../hash_table/probe_impl.bend as PIimport ../hash_table/probe_all.bend as PAimport ./read.bend as RDimport ./qrm.bend as QRimport ../../lib/nat_list.bend as NLimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# remove: the implementation's remove is the specification's.def rm_v0(~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}, +key: String, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +l: U32, +hsv: {UD.v(H.slot(l)) == s : Nat}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +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}, +m: Maybe<&2, V>, +hmm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == m : Maybe<&2, V>}, +hsm: {HT.some_b(~V, m) == True{} : Bool}) -> RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), 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)}, H.slot(l), 2)): match m: case None{}: Empty.absurd(RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), 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)}, H.slot(l), 2)), L.false_true(hsm)) case Some{+v}: +hm = {hmm : {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}} +hlv = L.subst(Maybe<&2, V>, z => {HT.some_b(~V, z) == True{} : Bool}, Some{v}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Equal.sym(Maybe<&2, V>, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v}, hm), {==}) +hf = Equal.trans(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), FD.fnd(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s)), Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}, FD.find_hit(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s, hlv, key, hk, sl, hmem, ST.g_ckeys(~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, sl, fl, hg)), Equal.cong(Maybe<&2, V>, Maybe<&2, SP.Ent<V>>, z => FD.fnd(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v}, hm)) L.subst(Maybe<&2, SP.Ent<V>>, z => RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, z), 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)}, H.slot(l), 2)), Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}, hf), RM.rm_at_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem, one, h1, i, hi, hoi, hsi, H.slot(l), hsv, v, hm, key, hk))# the probe's result, then the removal it asks fordef rm_res(~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}, +key: String, +one: Nat, +h1: {one == 1n : Nat}, +h: Nat, +r0: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), h, key, r0)) -> RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), QR.qrm_of(~V, r0, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT))): match r0: case B.RHit{+i, +l}: (+hi, rest) = hres (+hk0, hl) = rest +hsi = Equal.cong(U32, Nat, z => UD.v(H.slot(z)), B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl) +hbl = TF.bsl_inst(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k), ST.g_cbsl(~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, sl, fl, hg), i, hi) +hmem = L.subst(Nat, z => {NL.memn(z, sl) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), hsi, TF.hit_mem(sl, AR.slots(U32, lkT), key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hk0, hbl)) +hk = L.subst(Nat, z => {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), z), key) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), hsi, TF.hit_key(sl, AR.slots(U32, lkT), AR.slots(String, ksT), key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hk0, hbl, TF.bkok_at(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), i, hi))) +hls = TF.slok_mem(~V, AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(H.slot(l)), sl, 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, sl, fl, hg), hmem) rm_v0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, one, h1, UD.v(H.slot(l)), hmem, l, {==}, hk, i, hi, B.hold_occ(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hk0), hsi, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(H.slot(l))), {==}, L.and_right(Nat.is_lt(UD.v(H.slot(l)), UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), UD.v(H.slot(l))), hls)) case B.REnd{+e0}: (+he, rest) = hres (+hz, rest2) = rest (+hp, hno) = rest2 +hsd1 = UL.sd1(sd, RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)) +hnk = TF.nokey_of(~V, one, h1, AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), key, hno, AR.slots(U32, lkT), AR.slots(Maybe<&2, V>, eT), sd, hsd1, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), 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, sl, fl, hg), sl, 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, sl, fl, hg), ST.g_chas(~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, sl, fl, hg)) +hf = FD.find_miss(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), key, sl, hnk) L.subst(Maybe<&2, SP.Ent<V>>, z => RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, z), QR.qrm_of(~V, B.REnd{e0}, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT))), None{}, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), None{}, hf), (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (None{}, ({==}, ({==}, hg)))))# the long path's result read back as the removal the probe asks fordef lp_fd(~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}, +key: String, +h: Nat, +r0: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), h, key, r0)) -> {LR.rm_fd(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, ksT), PA.stored(key))) == QR.qrm_of(~V, r0, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)) : LR.LRU<&2, V> & Maybe<&2, V>}: match r0: case B.RHit{+i, +l}: (+hi, rest) = hres (+hk0, hl) = rest +hwb = B.all_inst(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k), ST.g_cwell(~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, sl, fl, hg), i, hi) +hz = L.subst(U32, z => {U32.is_eq(z, 0) == False{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl, RD.lnz(sd, key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hwb, hk0)) +E1 = Equal.cong(Bool, LR.LRU<&2, V> & Maybe<&2, V>, z => LR.rm_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), U32.from_nat(i), l, z), U32.is_eq(l, 0), False{}, hz) +E2 = Equal.cong(Array<U32> & U32, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.rm_hit(&2, V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), U32.from_nat(i), l, r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 6n)), (AR.thaw(U32, mT), CY.msk(k)), UT.uget(5n, {==}, 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, sl, fl, hg), 6, {==}), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, mT), z), W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), A.eq_of(W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), ST.g_cmask(~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, sl, fl, hg))))) Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.rm_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), U32.from_nat(i), l, U32.is_eq(l, 0)), LR.rm_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), U32.from_nat(i), l, False{}), QR.qrm_of(~V, B.RHit{i, l}, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), E1, E2) case B.REnd{+e0}: {==}def rm_po(~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}, +key: String, +one: Nat, +h1: {one == 1n : Nat}, +r0: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r0), hresb: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r0), po: PA.ProbeOK(tabT, sd, AR.slots(String, ksT), PA.stored(key), K.kword(key), r0, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key))) -> RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key))): match po: case Tuple{+K2, Tuple{+e, Tuple{+hsl, pk2}}}: +pk = ST.g_cpk(~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, sl, fl, hg) +g1 = L.subst(List<&2, String>, z => {ST.goodF(~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, z, AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl), hg) +hg2 = L.subst(Bool, z => {ST.goodF(~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, K2), z, eT, lkT, sl, fl) == True{} : Bool}, AR.perfect(String, sd, ksT), AR.perfect(String, sd, K2), Equal.trans(Bool, AR.perfect(String, sd, ksT), True{}, AR.perfect(String, sd, K2), pk, Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2)), g1) hres2 = L.subst(List<&2, String>, z => B.ResOK(TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r0), AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl), hres) hres3 = L.subst(List<&2, String>, z => B.ResOK(TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r0), AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl), hresb) ok = rm_res(~V, cap, n, head, tail, free, mT, k, sd, tabT, K2, eT, lkT, sl, fl, hg2, key, one, h1, UD.v(HS.bucket(K.kword(key), CY.msk(k))), r0, hres2) +el = lp_fd(~V, cap, n, head, tail, free, mT, k, sd, tabT, K2, eT, lkT, sl, fl, hg2, key, UD.v(HS.bucket(K.kword(key), CY.msk(k))), r0, hres3) +E = Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), (PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), QR.qrm_of(~V, r0, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), Equal.cong(H.Found & U32, LR.LRU<&2, V> & Maybe<&2, V>, x => LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), x), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key), (PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)), e), el) ok2 = L.subst(List<&2, String>, z => RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), z, AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), z, AR.slots(Maybe<&2, V>, eT), sl), key)), QR.qrm_of(~V, r0, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT))), AR.slots(String, K2), AR.slots(String, ksT), hsl, ok) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.remove_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), z), QR.qrm_of(~V, r0, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), QR.qrm_of(~V, r0, AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), E), ok2)# the long path: probe, then remove at the found bucketdef rm_long(~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}, +key: String, +one: Nat, +h1: {one == 1n : Nat}) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key), LR.remove_long(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key)): ok = rm_po(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, one, h1, B.pf(key, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(K.kword(key), CY.msk(k))))), UD.v(HS.bucket(K.kword(key), CY.msk(k)))), G.res_e0(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), N.succ_le_lt(0n, SC.pow2(k), N.pow2_pos(k)), CY.msk(k), key, UD.v(HS.bucket(K.kword(key), CY.msk(k))), PA.home_lt(K.kword(key), k), 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, sl, fl, hg), IV.home_all(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd, CY.msk(k), key, SC.pow2(k), ST.g_cwell(~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, sl, fl, hg), SC.pow2(k), N.le_refl(SC.pow2(k))), IV.find_empty(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 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)), 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, sl, fl, hg)), BA.n_lt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)))), G.res_e0(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), N.succ_le_lt(0n, SC.pow2(k), N.pow2_pos(k)), CY.msk(k), key, UD.v(HS.bucket(K.kword(key), CY.msk(k))), PA.home_lt(K.kword(key), k), 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, sl, fl, hg), IV.home_all(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd, CY.msk(k), key, SC.pow2(k), ST.g_cwell(~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, sl, fl, hg), SC.pow2(k), N.le_refl(SC.pow2(k))), IV.find_empty(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 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)), 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, sl, fl, hg)), BA.n_lt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)))), PA.probe_ok(one, h1, k, N.lt_trans(k, 30n, 31n, 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, sl, fl, hg)), {==}), 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, sl, fl, hg), sd, N.lt_trans(sd, 3n+sd, 32n, N.lt_le_trans(sd, 1n+sd, 3n+sd, N.lt_succ(sd), N.le_trans(1n+sd, 2n+sd, 3n+sd, N.le_succ(1n+sd), N.le_succ(2n+sd))), RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)), AR.slots(String, ksT), ksT, {==}, ST.g_cpk(~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, sl, fl, hg), ST.g_cwell(~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, sl, fl, hg), key)) +E = Equal.cong(Array<U32> & U32, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.rm_m(&2, V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), key, r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 6n)), (AR.thaw(U32, mT), CY.msk(k)), UT.uget(5n, {==}, 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, sl, fl, hg), 6, {==}), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, mT), z), W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), A.eq_of(W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), ST.g_cmask(~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, sl, fl, hg))))) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key), z), LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), LR.remove_long(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.remove_long(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key), LR.rm_found(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), E), ok)# the fused one-character pathdef rm_short(~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}, +one: Nat, +h1: {one == 1n : Nat}, +c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), {SCon{Chr{c}, SNil{}} : String}), LR.rm_q(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), H.short_word(c))): +ew = K.kword_short(c, hc) hres = L.subst(U32, z => B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(z, CY.msk(k))), {SCon{Chr{c}, SNil{}} : String}, B.pf({SCon{Chr{c}, SNil{}} : String}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep({SCon{Chr{c}, SNil{}} : String}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(z, CY.msk(k))))), UD.v(HS.bucket(z, CY.msk(k))))), K.kword({SCon{Chr{c}, SNil{}} : String}), H.short_word(c), ew, G.res_e0(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), N.succ_le_lt(0n, SC.pow2(k), N.pow2_pos(k)), CY.msk(k), {SCon{Chr{c}, SNil{}} : String}, UD.v(HS.bucket(K.kword({SCon{Chr{c}, SNil{}} : String}), CY.msk(k))), PA.home_lt(K.kword({SCon{Chr{c}, SNil{}} : String}), k), 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, sl, fl, hg), IV.home_all(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd, CY.msk(k), {SCon{Chr{c}, SNil{}} : String}, SC.pow2(k), ST.g_cwell(~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, sl, fl, hg), SC.pow2(k), N.le_refl(SC.pow2(k))), IV.find_empty(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 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)), 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, sl, fl, hg)), BA.n_lt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg))))) ok = rm_res(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, {SCon{Chr{c}, SNil{}} : String}, one, h1, UD.v(HS.bucket(H.short_word(c), CY.msk(k))), B.pf({SCon{Chr{c}, SNil{}} : String}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep({SCon{Chr{c}, SNil{}} : String}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(H.short_word(c), CY.msk(k))))), UD.v(HS.bucket(H.short_word(c), CY.msk(k)))), hres) +eq = QR.qrm_ok(~V, cap, n, head, tail, free, mT, ksT, eT, lkT, one, h1, k, N.lt_trans(k, 30n, 31n, 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, sl, fl, hg)), {==}), 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, sl, fl, hg), sd, AR.slots(String, ksT), c, hc, ST.g_cwell(~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, sl, fl, hg), SC.pow2(k), HS.bucket(H.short_word(c), CY.msk(k)), PA.home_lt(H.short_word(c), k)) +ef = Equal.cong(Nat, LR.LRU<&2, V> & Maybe<&2, V>, f => LR.qrm(&2, V, f, H.qstep(AR.thaw(U32, tabT), HS.bucket(H.short_word(c), CY.msk(k)), H.short_word(c)), CY.msk(k), H.short_word(c), HS.bucket(H.short_word(c), CY.msk(k)), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), U32.to_nat(U32.inc(CY.msk(k))), SC.pow2(k), PA.fuel_eq(one, h1, k, N.lt_trans(k, 30n, 31n, 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, sl, fl, hg)), {==}))) +E1 = Equal.cong(Array<U32> & U32, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.rm_q2(&2, V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.short_word(c), r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 6n)), (AR.thaw(U32, mT), CY.msk(k)), UT.uget(5n, {==}, 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, sl, fl, hg), 6, {==}), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, mT), z), W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), A.eq_of(W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), ST.g_cmask(~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, sl, fl, hg))))) +E = Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.rm_q(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), H.short_word(c)), LR.qrm(&2, V, U32.to_nat(U32.inc(CY.msk(k))), H.qstep(AR.thaw(U32, tabT), HS.bucket(H.short_word(c), CY.msk(k)), H.short_word(c)), CY.msk(k), H.short_word(c), HS.bucket(H.short_word(c), CY.msk(k)), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), QR.qrm_of(~V, B.pf({SCon{Chr{c}, SNil{}} : String}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep({SCon{Chr{c}, SNil{}} : String}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(H.short_word(c), CY.msk(k))))), UD.v(HS.bucket(H.short_word(c), CY.msk(k)))), AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), E1, Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.qrm(&2, V, U32.to_nat(U32.inc(CY.msk(k))), H.qstep(AR.thaw(U32, tabT), HS.bucket(H.short_word(c), CY.msk(k)), H.short_word(c)), CY.msk(k), H.short_word(c), HS.bucket(H.short_word(c), CY.msk(k)), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), LR.qrm(&2, V, SC.pow2(k), H.qstep(AR.thaw(U32, tabT), HS.bucket(H.short_word(c), CY.msk(k)), H.short_word(c)), CY.msk(k), H.short_word(c), HS.bucket(H.short_word(c), CY.msk(k)), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), QR.qrm_of(~V, B.pf({SCon{Chr{c}, SNil{}} : String}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep({SCon{Chr{c}, SNil{}} : String}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(H.short_word(c), CY.msk(k))))), UD.v(HS.bucket(H.short_word(c), CY.msk(k)))), AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), ef, eq)) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), {SCon{Chr{c}, SNil{}} : String}), z), QR.qrm_of(~V, B.pf({SCon{Chr{c}, SNil{}} : String}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep({SCon{Chr{c}, SNil{}} : String}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(H.short_word(c), CY.msk(k))))), UD.v(HS.bucket(H.short_word(c), CY.msk(k)))), AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), LR.rm_q(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), H.short_word(c)), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.rm_q(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), H.short_word(c)), QR.qrm_of(~V, B.pf({SCon{Chr{c}, SNil{}} : String}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep({SCon{Chr{c}, SNil{}} : String}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(H.short_word(c), CY.msk(k))))), UD.v(HS.bucket(H.short_word(c), CY.msk(k)))), AR.thaw(U32, tabT), CY.msk(k), cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)), E), ok)def rm_sh(~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}, +one: Nat, +h1: {one == 1n : Nat}, +c: U32, +b: Bool, +hb: {U32.is_lt(c, H.tag()) == b : Bool}) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), {SCon{Chr{c}, SNil{}} : String}), LR.rm_short(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), c, b)): match b: case True{}: rm_short(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, c, hb) case False{}: rm_long(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, {SCon{Chr{c}, SNil{}} : String}, one, h1)def rm_ch(~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}, +one: Nat, +h1: {one == 1n : Nat}, +c: U32, +t: String) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), SCon{Chr{c}, t}), LR.rm_c(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), c, t)): match t: case SNil{}: rm_sh(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, c, U32.is_lt(c, H.tag()), {==}) case SCon{+d, +t2}: rm_long(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, SCon{Chr{c}, SCon{d, t2}}, one, h1)def remove_sh(~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}, +key: String, +one: Nat, +h1: {one == 1n : Nat}) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key), LR.remove(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key)): match key: case SNil{}: rm_long(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, SNil{}, one, h1) case SCon{Chr{+c}, +t}: rm_ch(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, c, t)# THEOREM (remove): the specification's removedef remove_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, sh), key), LR.remove(&2, V, ST.real(~V, sh), key)): match sh: case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: remove_sh(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, one, h1)