proofs/containers/lru/repl.bend source
proofs/containers/lru/repl.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/math/u64.bend as Wimport ../../../src/containers/lru.bend as LRimport ../hash_table/table.bend as TBimport ../hash_table/state.bend as HTimport ../hash_table/keys.bend as Kimport ./state.bend as STimport ./basic.bend as BAimport ./bump.bend as BUimport ./bumpsh.bend as BSimport ./touch.bend as TOimport ./touchsh.bend as TSHimport ./rmat.bend as RMimport ./gone.bend as GOimport ./unlink.bend as ULimport ./meta.bend as MTimport ./read.bend as RDimport ./hw.bend as HWimport ./elfr.bend as EFimport ./walk.bend as WLimport ./trace.bend as TRimport ./dll.bend as DLimport ./idx.bend as IDimport ../hash_table/tools.bend as TLimport ../../lib/nat_list.bend as NLimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# add, a present key: the entry is rewritten in place (value, lifetime,# deadline), counted as an insertion and touched.# the rewritten slot keeps the invariantdef rp_good(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}) == True{} : Bool}: +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) +hsu = GO.su_lt(su, s, sd, hsv, hs0) +i3 = Equal.trans(Nat, UD.v(LR.tidx(su)), ST.off(UD.v(su), 3n), ST.off(s, 3n), ID.w3(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 3n), UD.v(su), s, hsv)) +i4 = Equal.trans(Nat, UD.v(LR.dlo_idx(su)), ST.off(UD.v(su), 4n), ST.off(s, 4n), ID.w4(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 4n), UD.v(su), s, hsv)) +i5 = Equal.trans(Nat, UD.v(LR.dhi_idx(su)), ST.off(UD.v(su), 5n), ST.off(s, 5n), ID.w5(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 5n), UD.v(su), s, hsv)) +hpl = 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, sl, fl, hg) +hpe = 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, sl, fl, hg) +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) +p2 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), p1, UD.v(LR.dlo_idx(su)), lo) +p3 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), p2, UD.v(LR.dhi_idx(su)), hi) +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) +s2 = UL.wr_s(AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), sd, p1, LR.dlo_idx(su), s, 4n, {==}, hs0, i4, lo) +s3 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), sd, p2, LR.dhi_idx(su), s, 5n, {==}, hs0, i5, hi) +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) +se = Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su), Some{v}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.upd_slots(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hsu, hpe), Equal.cong(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), z, Some{v}), UD.v(su), s, hsv)) +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) +hlv = Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v0}, hm) +hsl = L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se), HW.slok_live(~V, AR.slots(Maybe<&2, V>, eT), s, v, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sl, hle, 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))) +hnf = NL.not_t_f(NL.memn(s, fl), TR.not_vac(~V, s, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), hlv, ST.g_cfl(~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), NL.memn(s, fl), {==})) +hfl = L.subst(List<&2, Maybe<&2, V>>, z => {ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se), Equal.trans(Bool, ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v})), ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), True{}, EF.flok_el(~V, AR.slots(Maybe<&2, V>, eT), s, Some{v}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), fl, hnf), ST.g_cfl(~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))) +km1 = WL.km(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sl, hsl) +km0 = WL.km(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), 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)) +ek = Equal.trans(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl)), WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), sl), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), km1, Equal.trans(List<&2, String>, WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), Equal.trans(List<&2, String>, WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), Equal.trans(List<&2, String>, WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), sl), WL.mapk(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), sl), Equal.cong(List<&2, U32>, List<&2, String>, z => WL.mapk(z, AR.slots(String, ksT), sl), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.mapk_hw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, {==}, AR.slots(String, ksT), sl)), Equal.trans(List<&2, String>, WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), Equal.trans(List<&2, String>, WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), sl), WL.mapk(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), sl), Equal.cong(List<&2, U32>, List<&2, String>, z => WL.mapk(z, AR.slots(String, ksT), sl), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.mapk_hw(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, {==}, AR.slots(String, ksT), sl)), Equal.trans(List<&2, String>, WL.mapk(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), sl), WL.mapk(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), AR.slots(String, ksT), sl), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), Equal.cong(List<&2, U32>, List<&2, String>, z => WL.mapk(z, AR.slots(String, ksT), sl), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.mapk_hw(AR.slots(U32, lkT), s, 3n, t, {==}, {==}, AR.slots(String, ksT), sl)))), Equal.sym(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), km0))) +hkeys = L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), SP.keys_of(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl)), Equal.sym(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl)), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), ek), 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)) ST.good_intro(~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), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl, 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), 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, sl, fl, hg), 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), 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), pe, p3, 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), 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), ST.g_cbits(~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_csize(~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_cdepth(~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_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), 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), 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), 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, sl, fl, hg), 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), ST.g_cload(~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_ccap(~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(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k)), True{}, Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k)), Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.pow2(k)), Equal.cong(List<&2, U32>, Bool, z => ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, z, SC.pow2(k)), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.bsl_hw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, {==}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, SC.pow2(k))), Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k)), Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.pow2(k)), Equal.cong(List<&2, U32>, Bool, z => ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, z, SC.pow2(k)), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.bsl_hw(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, {==}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, SC.pow2(k))), Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k)), Equal.cong(List<&2, U32>, Bool, z => ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, z, SC.pow2(k)), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.bsl_hw(AR.slots(U32, lkT), s, 3n, t, {==}, {==}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, 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)), Equal.trans(Bool, ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), sl), True{}, Equal.trans(Bool, ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), sl), Equal.trans(Bool, ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl), Equal.cong(List<&2, U32>, Bool, z => ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), z, sl), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.has_hw(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, {==}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), sl)), Equal.trans(Bool, ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), sl), Equal.trans(Bool, ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), sl), Equal.cong(List<&2, U32>, Bool, z => ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), z, sl), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.has_hw(~V, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, {==}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), sl)), Equal.trans(Bool, ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), sl), Equal.cong(List<&2, U32>, Bool, z => ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), z, sl), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.has_hw(~V, AR.slots(U32, lkT), s, 3n, t, {==}, {==}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), sl)))), 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)), hsl, 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, sl, fl, hg), ST.g_clen(~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_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, sl, 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, sl, fl, hg), Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), sl, 0, 0), ST.seg(AR.slots(U32, lkT), sl, 0, 0), True{}, Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), sl, 0, 0), ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl, 0, 0), ST.seg(AR.slots(U32, lkT), sl, 0, 0), Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), sl, 0, 0), ST.seg(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), sl, 0, 0), ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl, 0, 0), Equal.cong(List<&2, U32>, Bool, z => ST.seg(z, sl, 0, 0), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.seg_hw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, {==}, sl, 0, 0)), Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl, 0, 0), ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), sl, 0, 0), ST.seg(AR.slots(U32, lkT), sl, 0, 0), Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), sl, 0, 0), ST.seg(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), sl, 0, 0), ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), sl, 0, 0), Equal.cong(List<&2, U32>, Bool, z => ST.seg(z, sl, 0, 0), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.seg_hw(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, {==}, sl, 0, 0)), Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), sl, 0, 0), ST.seg(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), sl, 0, 0), ST.seg(AR.slots(U32, lkT), sl, 0, 0), Equal.cong(List<&2, U32>, Bool, z => ST.seg(z, sl, 0, 0), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.seg_hw(AR.slots(U32, lkT), s, 3n, t, {==}, {==}, sl, 0, 0)))), 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, sl, fl, hg)), hkeys, ST.g_cfree(~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(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), fl), ST.fll(AR.slots(U32, lkT), fl), True{}, Equal.trans(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), fl), ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), fl), ST.fll(AR.slots(U32, lkT), fl), Equal.trans(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), fl), ST.fll(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), fl), ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), fl), Equal.cong(List<&2, U32>, Bool, z => ST.fll(z, fl), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.fll_hw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, {==}, fl)), Equal.trans(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), fl), ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), fl), ST.fll(AR.slots(U32, lkT), fl), Equal.trans(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), fl), ST.fll(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), fl), ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), fl), Equal.cong(List<&2, U32>, Bool, z => ST.fll(z, fl), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.fll_hw(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, {==}, fl)), Equal.trans(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), fl), ST.fll(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), fl), ST.fll(AR.slots(U32, lkT), fl), Equal.cong(List<&2, U32>, Bool, z => ST.fll(z, fl), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.fll_hw(AR.slots(U32, lkT), s, 3n, t, {==}, {==}, fl)))), ST.g_cfll(~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)), hfl, ST.g_cfnd(~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_cfcnt(~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))# the rewritten slot still holds key and now holds vdef rp_hk(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> {S.str_eq(ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), key) == True{} : Bool}: +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) +hsu = GO.su_lt(su, s, sd, hsv, hs0) +i3 = Equal.trans(Nat, UD.v(LR.tidx(su)), ST.off(UD.v(su), 3n), ST.off(s, 3n), ID.w3(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 3n), UD.v(su), s, hsv)) +i4 = Equal.trans(Nat, UD.v(LR.dlo_idx(su)), ST.off(UD.v(su), 4n), ST.off(s, 4n), ID.w4(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 4n), UD.v(su), s, hsv)) +i5 = Equal.trans(Nat, UD.v(LR.dhi_idx(su)), ST.off(UD.v(su), 5n), ST.off(s, 5n), ID.w5(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 5n), UD.v(su), s, hsv)) +hpl = 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, sl, fl, hg) +hpe = 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, sl, fl, hg) +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) +p2 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), p1, UD.v(LR.dlo_idx(su)), lo) +p3 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), p2, UD.v(LR.dhi_idx(su)), hi) +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) +s2 = UL.wr_s(AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), sd, p1, LR.dlo_idx(su), s, 4n, {==}, hs0, i4, lo) +s3 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), sd, p2, LR.dhi_idx(su), s, 5n, {==}, hs0, i5, hi) +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) +se = Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su), Some{v}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.upd_slots(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hsu, hpe), Equal.cong(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), z, Some{v}), UD.v(su), s, hsv)) +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) +hlv = Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v0}, hm) +hsl = L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se), HW.slok_live(~V, AR.slots(Maybe<&2, V>, eT), s, v, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sl, hle, 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))) L.subst(String, z => {S.str_eq(z, key) == True{} : Bool}, ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), Equal.sym(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), ST.skey(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), Equal.cong(List<&2, U32>, String, z => ST.skey(z, AR.slots(String, ksT), s), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.skey_hw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, {==}, AR.slots(String, ksT), s)), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), ST.skey(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), s), Equal.cong(List<&2, U32>, String, z => ST.skey(z, AR.slots(String, ksT), s), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.skey_hw(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, {==}, AR.slots(String, ksT), s)), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), s), ST.skey(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), Equal.cong(List<&2, U32>, String, z => ST.skey(z, AR.slots(String, ksT), s), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.skey_hw(AR.slots(U32, lkT), s, 3n, t, {==}, {==}, AR.slots(String, ksT), s))))), hk)def rp_hm(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> {HT.nthm(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), s) == Some{v} : Maybe<&2, V>}: +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) +hsu = GO.su_lt(su, s, sd, hsv, hs0) +i3 = Equal.trans(Nat, UD.v(LR.tidx(su)), ST.off(UD.v(su), 3n), ST.off(s, 3n), ID.w3(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 3n), UD.v(su), s, hsv)) +i4 = Equal.trans(Nat, UD.v(LR.dlo_idx(su)), ST.off(UD.v(su), 4n), ST.off(s, 4n), ID.w4(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 4n), UD.v(su), s, hsv)) +i5 = Equal.trans(Nat, UD.v(LR.dhi_idx(su)), ST.off(UD.v(su), 5n), ST.off(s, 5n), ID.w5(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 5n), UD.v(su), s, hsv)) +hpl = 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, sl, fl, hg) +hpe = 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, sl, fl, hg) +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) +p2 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), p1, UD.v(LR.dlo_idx(su)), lo) +p3 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), p2, UD.v(LR.dhi_idx(su)), hi) +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) +s2 = UL.wr_s(AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), sd, p1, LR.dlo_idx(su), s, 4n, {==}, hs0, i4, lo) +s3 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), sd, p2, LR.dhi_idx(su), s, 5n, {==}, hs0, i5, hi) +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) +se = Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su), Some{v}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.upd_slots(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hsu, hpe), Equal.cong(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), z, Some{v}), UD.v(su), s, hsv)) +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) +hlv = Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v0}, hm) +hsl = L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se), HW.slok_live(~V, AR.slots(Maybe<&2, V>, eT), s, v, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sl, hle, 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))) Equal.trans(Maybe<&2, V>, HT.nthm(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), s), HT.nthm(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), s), Some{v}, Equal.cong(List<&2, Maybe<&2, V>>, Maybe<&2, V>, z => HT.nthm(~V, z, s), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se), TL.nthm_upd_same(~V, AR.slots(Maybe<&2, V>, eT), s, Some{v}, hle))def le4(~V: Data, +k1: String, +k2: String, +v: V, +t1: U32, +t2: U32, +a1: U32, +a2: U32, +b1: U32, +b2: U32, +ek: {k1 == k2 : String}, +et: {t1 == t2 : U32}, +ea: {a1 == a2 : U32}, +eb: {b1 == b2 : U32}) -> {SP.LE{k1, v, t1, W.U64{a1, b1}} == SP.LE{k2, v, t2, W.U64{a2, b2}} : SP.Ent<V>}: +r1 = L.subst(String, z => {SP.LE{k1, v, t1, W.U64{a1, b1}} == SP.LE{z, v, t1, W.U64{a1, b1}} : SP.Ent<V>}, k1, k2, ek, {==}) +r2 = L.subst(U32, z => {SP.LE{k1, v, t1, W.U64{a1, b1}} == SP.LE{k2, v, z, W.U64{a1, b1}} : SP.Ent<V>}, t1, t2, et, r1) +r3 = L.subst(U32, z => {SP.LE{k1, v, t1, W.U64{a1, b1}} == SP.LE{k2, v, t2, W.U64{z, b1}} : SP.Ent<V>}, a1, a2, ea, r2) L.subst(U32, z => {SP.LE{k1, v, t1, W.U64{a1, b1}} == SP.LE{k2, v, t2, W.U64{a2, z}} : SP.Ent<V>}, b1, b2, eb, r3)def rp_sp(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +e: {sl == SC.append(Nat, a, Con{s, b}) : List<&2, Nat>}) -> {SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), key), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)) == SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}) : List<&2, SP.Ent<V>>}: +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) +hsu = GO.su_lt(su, s, sd, hsv, hs0) +i3 = Equal.trans(Nat, UD.v(LR.tidx(su)), ST.off(UD.v(su), 3n), ST.off(s, 3n), ID.w3(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 3n), UD.v(su), s, hsv)) +i4 = Equal.trans(Nat, UD.v(LR.dlo_idx(su)), ST.off(UD.v(su), 4n), ST.off(s, 4n), ID.w4(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 4n), UD.v(su), s, hsv)) +i5 = Equal.trans(Nat, UD.v(LR.dhi_idx(su)), ST.off(UD.v(su), 5n), ST.off(s, 5n), ID.w5(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 5n), UD.v(su), s, hsv)) +hpl = 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, sl, fl, hg) +hpe = 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, sl, fl, hg) +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) +p2 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), p1, UD.v(LR.dlo_idx(su)), lo) +p3 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), p2, UD.v(LR.dhi_idx(su)), hi) +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) +s2 = UL.wr_s(AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), sd, p1, LR.dlo_idx(su), s, 4n, {==}, hs0, i4, lo) +s3 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), sd, p2, LR.dhi_idx(su), s, 5n, {==}, hs0, i5, hi) +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) +se = Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su), Some{v}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.upd_slots(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hsu, hpe), Equal.cong(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), z, Some{v}), UD.v(su), s, hsv)) +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) +hlv = Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v0}, hm) +hsl = L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se), HW.slok_live(~V, AR.slots(Maybe<&2, V>, eT), s, v, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sl, hle, 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))) +gp = rp_good(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi) +hkeysp = 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), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl, gp) +nd = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, sl, SC.append(Nat, a, Con{s, b}), e, 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, sl, fl, hg)) +nm = L.subst(Bool, z => {z == True{} : Bool}, NL.nodupn(SC.append(Nat, a, Con{s, b})), Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b)))), NL.nd_mid(a, s, b), nd) +hy = NL.not_t_f(NL.memn(s, SC.append(Nat, a, b)), L.and_right(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), nm)) +hn0 = L.subst(List<&2, Nat>, z => {S.nodup(SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), z))) == True{} : Bool}, sl, SC.append(Nat, a, Con{s, b}), e, 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)) +hnp = L.subst(List<&2, Nat>, z => {S.nodup(SP.keys_of(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), z))) == True{} : Bool}, sl, SC.append(Nat, a, Con{s, b}), e, hkeysp) +d0 = EF.spec_drop(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, s, b, v0, hm, key, hk, hn0) +dp = EF.spec_drop(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), a, s, b, v, rp_hm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi), key, rp_hk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi), hnp) +f1 = Equal.cong(List<&2, Maybe<&2, V>>, List<&2, SP.Ent<V>>, z => ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), z, SC.append(Nat, a, b)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se) +f2 = EF.es_el(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s, Some{v}, SC.append(Nat, a, b), hy) +f3 = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), Equal.cong(List<&2, U32>, List<&2, SP.Ent<V>>, z => ST.es(~V, z, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.es_fs(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b), hy)), Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), Equal.cong(List<&2, U32>, List<&2, SP.Ent<V>>, z => ST.es(~V, z, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.es_fs(~V, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b), hy)), Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), Equal.cong(List<&2, U32>, List<&2, SP.Ent<V>>, z => ST.es(~V, z, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.es_fs(~V, AR.slots(U32, lkT), s, 3n, t, {==}, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b), hy)))) +fr = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), f1, Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), f2, f3)) +esk = Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key, Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), ST.skey(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), Equal.cong(List<&2, U32>, String, z => ST.skey(z, AR.slots(String, ksT), s), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 5n), hi), s3), HW.skey_hw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), s, 5n, hi, {==}, {==}, AR.slots(String, ksT), s)), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), AR.slots(String, ksT), s), ST.skey(SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), s), Equal.cong(List<&2, U32>, String, z => ST.skey(z, AR.slots(String, ksT), s), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 4n), lo), s2), HW.skey_hw(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), s, 4n, lo, {==}, {==}, AR.slots(String, ksT), s)), Equal.trans(String, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), AR.slots(String, ksT), s), ST.skey(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), AR.slots(String, ksT), s), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), Equal.cong(List<&2, U32>, String, z => ST.skey(z, AR.slots(String, ksT), s), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 3n), t), s1), HW.skey_hw(AR.slots(U32, lkT), s, 3n, t, {==}, {==}, AR.slots(String, ksT), s)))), K.str_eq_of(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key, hk)) +w3 = Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), ST.off(s, 3n)), W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 3n)), t, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), ST.off(s, 5n), hi, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), s3, ST.off(s, 3n), ID.off_ne(s, s, 5n, 3n, {==}, {==}, DL.ne_word(s, s, 5n, 3n, {==}))), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 3n)), W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), ST.off(s, 3n)), t, MT.nth_other(AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), ST.off(s, 4n), lo, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), s2, ST.off(s, 3n), ID.off_ne(s, s, 4n, 3n, {==}, {==}, DL.ne_word(s, s, 4n, 3n, {==}))), MT.nth_same(3n+sd, lkT, hpl, ST.off(s, 3n), ID.off_lt(s, sd, hs0, 3n, {==}), t, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), s1))) +w4 = Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), ST.off(s, 4n)), W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), ST.off(s, 4n)), lo, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), ST.off(s, 5n), hi, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), s3, ST.off(s, 4n), ID.off_ne(s, s, 5n, 4n, {==}, {==}, DL.ne_word(s, s, 5n, 4n, {==}))), MT.nth_same(3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), p1, ST.off(s, 4n), ID.off_lt(s, sd, hs0, 4n, {==}), lo, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), s2)) +w5 = MT.nth_same(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), p2, ST.off(s, 5n), ID.off_lt(s, sd, hs0, 5n, {==}), hi, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), s3) +ev = le4(~V, ST.skey(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s), key, v, ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), s, 3n), t, ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), s, 4n), lo, ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), s, 5n), hi, esk, w3, w4, w5) +c1 = Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SP.snoc(~V, z, TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, a, Con{s, b})), key), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, a, b)), dp) +c2 = Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SP.snoc(~V, z, TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), fr) +c3 = Equal.cong(SP.Ent<V>, List<&2, SP.Ent<V>>, z => SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), z), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v), SP.LE{key, v, t, W.U64{lo, hi}}, ev) +c4 = Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SP.snoc(~V, z, SP.LE{key, v, t, W.U64{lo, hi}}), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), 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), Equal.sym(List<&2, SP.Ent<V>>, 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.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), d0)) +cx = Equal.trans(List<&2, SP.Ent<V>>, SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), SP.snoc(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, a, b)), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), SP.snoc(~V, 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.LE{key, v, t, W.U64{lo, hi}}), c1, Equal.trans(List<&2, SP.Ent<V>>, SP.snoc(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, a, b)), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), SP.snoc(~V, 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.LE{key, v, t, W.U64{lo, hi}}), c2, Equal.trans(List<&2, SP.Ent<V>>, SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), SP.LE{key, v, t, W.U64{lo, hi}}), SP.snoc(~V, 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.LE{key, v, t, W.U64{lo, hi}}), c3, c4))) L.subst(List<&2, Nat>, z => {SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), z), key), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)) == SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), z), key), SP.LE{key, v, t, W.U64{lo, hi}}) : List<&2, SP.Ent<V>>}, SC.append(Nat, a, Con{s, b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{s, b}), e), cx)# the implementation: put_ent, then the count, then the touchdef rp_impl(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> {LR.replace(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, LR.E{v, t, lo, hi}) == LR.touch(&2, V, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})), su) : LR.LRU<&2, V>}: +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) +hsu = GO.su_lt(su, s, sd, hsv, hs0) +i3 = Equal.trans(Nat, UD.v(LR.tidx(su)), ST.off(UD.v(su), 3n), ST.off(s, 3n), ID.w3(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 3n), UD.v(su), s, hsv)) +i4 = Equal.trans(Nat, UD.v(LR.dlo_idx(su)), ST.off(UD.v(su), 4n), ST.off(s, 4n), ID.w4(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 4n), UD.v(su), s, hsv)) +i5 = Equal.trans(Nat, UD.v(LR.dhi_idx(su)), ST.off(UD.v(su), 5n), ST.off(s, 5n), ID.w5(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 5n), UD.v(su), s, hsv)) +hpl = 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, sl, fl, hg) +hpe = 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, sl, fl, hg) +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) +p2 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), p1, UD.v(LR.dlo_idx(su)), lo) +p3 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), p2, UD.v(LR.dhi_idx(su)), hi) +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) +s2 = UL.wr_s(AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), sd, p1, LR.dlo_idx(su), s, 4n, {==}, hs0, i4, lo) +s3 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), sd, p2, LR.dhi_idx(su), s, 5n, {==}, hs0, i5, hi) +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) +se = Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su), Some{v}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.upd_slots(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hsu, hpe), Equal.cong(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), z, Some{v}), UD.v(su), s, hsv)) +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) +hlv = Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v0}, hm) +hsl = L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), se), HW.slok_live(~V, AR.slots(Maybe<&2, V>, eT), s, v, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sl, hle, 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))) +hd32 = 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))), hsd) +hx = HT.nthm_some(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su), UT.len_of(Maybe<&2, V>, sd, eT, hpe, UD.v(su), hsu)) +eE = AR.set(Maybe<&2, V>, sd, eT, su, Some{v}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su)), hd32, hsu, hx, hpe) +a1 = UL.wr(one, h1, lkT, sd, hsd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) +a2 = UL.wr(one, h1, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), sd, hsd, p1, LR.dlo_idx(su), s, 4n, {==}, hs0, i4, lo) +a3 = UL.wr(one, h1, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), sd, hsd, p2, LR.dhi_idx(su), s, 5n, {==}, hs0, i5, hi) +eL = Equal.trans(Array<U32>, Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.tidx(su), t), LR.dlo_idx(su), lo), LR.dhi_idx(su), hi), Array.set(U32, Array.set(U32, AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), LR.dlo_idx(su), lo), LR.dhi_idx(su), hi), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), Equal.cong(Array<U32>, Array<U32>, z => Array.set(U32, Array.set(U32, z, LR.dlo_idx(su), lo), LR.dhi_idx(su), hi), Array.set(U32, AR.thaw(U32, lkT), LR.tidx(su), t), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), a1), Equal.trans(Array<U32>, Array.set(U32, Array.set(U32, AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), LR.dlo_idx(su), lo), LR.dhi_idx(su), hi), Array.set(U32, AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), LR.dhi_idx(su), hi), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), Equal.cong(Array<U32>, Array<U32>, z => Array.set(U32, z, LR.dhi_idx(su), hi), Array.set(U32, AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), LR.dlo_idx(su), lo), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo)), a2), a3)) +e1 = Equal.cong(Array<Maybe<&2, V>>, LR.LRU<&2, V>, x => LR.repl_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), su, (x, Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.tidx(su), t), LR.dlo_idx(su), lo), LR.dhi_idx(su), hi))), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, Some{v}), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), eE) +e2 = Equal.cong(Array<U32>, LR.LRU<&2, V>, y => LR.repl_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), su, (AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), y)), Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.tidx(su), t), LR.dlo_idx(su), lo), LR.dhi_idx(su), hi), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), eL) Equal.trans(LR.LRU<&2, V>, LR.repl_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), su, (Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, Some{v}), Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.tidx(su), t), LR.dlo_idx(su), lo), LR.dhi_idx(su), hi))), LR.repl_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), su, (AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.tidx(su), t), LR.dlo_idx(su), lo), LR.dhi_idx(su), hi))), LR.repl_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), su, (AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)))), e1, e2)def rp_spl(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, sp: NL.Split(s, sl)) -> {SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), key), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)) == SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}) : List<&2, SP.Ent<V>>}: match sp: case Tuple{+a, Tuple{+b, +e}}: rp_sp(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi, a, b, e)def rp_t(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +m2: AR.Tree<U32>, +em: {ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}) == 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, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), SP.c_ins(ST.ctr(AR.slots(U32, mT)))} : SP.Lru<V>}, -r: LR.LRU<&2, V>, to: TSH.TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, m2), 3n), ST.w64(AR.slots(U32, m2), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), key), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, m2))}, r)) -> RM.POK(~V, Bool, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, False{}), (r, False{})): match to: case Tuple{+sh3, Tuple{+e3, Tuple{+em3, g3}}}: +eo = Equal.cong(SP.Lru<V>, U32, w => RD.l_on(~V, w), ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}), 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, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, em) +el = Equal.cong(SP.Lru<V>, W.U64, w => RD.l_life(~V, w), ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}), 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, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, em) +ec = Equal.cong(SP.Lru<V>, SP.Ctr, w => RD.l_c(~V, w), ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}), 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, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, em) +es1 = BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), key), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), ST.ctr(AR.slots(U32, m2)), SP.c_ins(ST.ctr(AR.slots(U32, mT))), eo, el, rp_spl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi, NL.split_mem(s, sl, hmem)), ec) +esp = Equal.trans(SP.Lru<V>, ST.model(~V, sh3), SP.L{cap, W32.nth0(AR.slots(U32, m2), 3n), ST.w64(AR.slots(U32, m2), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), key), TO.ev(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, m2))}, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, em3, es1) (sh3, (False{}, (Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V> & Bool, z => (z, False{}), r, ST.real(~V, sh3), e3), (Equal.cong(SP.Lru<V>, SP.Lru<V> & Bool, z => (z, False{}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(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.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, esp)), g3))))def rp_c(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, cm: BS.CntM(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl, 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, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})))) -> RM.POK(~V, Bool, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, False{}), (LR.touch(&2, V, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})), su), False{})): match cm: case Tuple{+m2, Tuple{+e1, Tuple{+em, g1}}}: +E = Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V>, z => LR.touch(&2, V, z, su), LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})), ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}), e1) ok = rp_t(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi, m2, em, LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}), su), TSH.touch_sh(~V, one, h1, cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl, g1, s, hmem, su, hsv, key, rp_hk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi), v, rp_hm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi))) L.subst(LR.LRU<&2, V>, z => RM.POK(~V, Bool, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, False{}), (z, False{})), LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}), su), LR.touch(&2, V, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})), su), Equal.sym(LR.LRU<&2, V>, LR.touch(&2, V, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})), su), LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl}), su), E), ok)# THEOREM (add, a present key): the entry is replaced and becomes the newest,# counted as an insertion; nothing is evicteddef repl_ok(~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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v0: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v0} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> RM.POK(~V, Bool, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, False{}), (LR.replace(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, LR.E{v, t, lo, hi}), False{})): +gp = rp_good(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi) ok = rp_c(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi, BS.cntm_ins(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl, gp, 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, sl, fl, hg), 0, 16n, {==}, {==}, {==}))) +E = rp_impl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, s, hmem, su, hsv, v0, hm, key, hk, v, t, lo, hi) L.subst(LR.LRU<&2, V>, z => RM.POK(~V, Bool, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, False{}), (z, False{})), LR.touch(&2, V, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})), su), LR.replace(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, LR.E{v, t, lo, hi}), Equal.sym(LR.LRU<&2, V>, LR.replace(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, LR.E{v, t, lo, hi}), LR.touch(&2, V, LR.fbump(&2, V, 0, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sl, fl})), su), E), ok)