1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/array.bend as AR 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/hash_table.bend as S 7 import ../../../spec/containers/lru.bend as SP 8 import ../../lib/u32div.bend as UD 9 import ../../../src/math/u64.bend as W 10 import ../../../src/containers/lru.bend as LR 11 import ../hash_table/table.bend as TB 12 import ../hash_table/state.bend as HT 13 import ../hash_table/keys.bend as K 14 import ./state.bend as ST 15 import ./basic.bend as BA 16 import ./bump.bend as BU 17 import ./bumpsh.bend as BS 18 import ./touch.bend as TO 19 import ./touchsh.bend as TSH 20 import ./rmat.bend as RM 21 import ./gone.bend as GO 22 import ./unlink.bend as UL 23 import ./meta.bend as MT 24 25 import ./read.bend as RD 26 import ./hw.bend as HW 27 import ./elfr.bend as EF 28 import ./walk.bend as WL 29 import ./trace.bend as TR 30 import ./dll.bend as DL 31 import ./idx.bend as ID 32 import ../hash_table/tools.bend as TL 33 import ../../lib/nat_list.bend as NL 34 import ../../lib/words32.bend as W32 35 import ../../lib/u32_tree.bend as UT 36 37 # add, a present key: the entry is rewritten in place (value, lifetime, 38 # deadline), counted as an insertion and touched. 39 40 41 42 # the rewritten slot keeps the invariant 43 def rp_good(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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}: 44 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 45 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) 46 +hsu = GO.su_lt(su, s, sd, hsv, hs0) 47 +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)) 48 +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)) 49 +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)) 50 +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) 51 +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) 52 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 53 +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) 54 +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) 55 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 56 +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) 57 +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) 58 +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) 59 +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)) 60 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 61 +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) 62 +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))) 63 +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), {==})) 64 +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))) 65 +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) 66 +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)) 67 +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>, 68 +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)) 69 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, 70 71 # the rewritten slot still holds key and now holds v 72 def rp_hk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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}: 73 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 74 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) 75 +hsu = GO.su_lt(su, s, sd, hsv, hs0) 76 +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)) 77 +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)) 78 +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)) 79 +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) 80 +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) 81 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 82 +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) 83 +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) 84 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 85 +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) 86 +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) 87 +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) 88 +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)) 89 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 90 +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) 91 +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))) 92 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)), 93 94 def rp_hm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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>}: 95 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 96 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) 97 +hsu = GO.su_lt(su, s, sd, hsv, hs0) 98 +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)) 99 +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)) 100 +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)) 101 +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) 102 +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) 103 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 104 +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) 105 +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) 106 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 107 +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) 108 +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) 109 +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) 110 +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)) 111 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 112 +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) 113 +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))) 114 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)) 115 116 117 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}: 118 +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}, k1, k2, ek, {==}) 119 +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}, t1, t2, et, r1) 120 +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}, a1, a2, ea, r2) 121 L.subst(U32, z => {SP.LE{k1, v, t1, W.U64{a1, b1}} == SP.LE{k2, v, t2, W.U64{a2, z}} : SP.Ent}, b1, b2, eb, r3) 122 123 124 def rp_sp(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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>}: 125 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 126 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) 127 +hsu = GO.su_lt(su, s, sd, hsv, hs0) 128 +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)) 129 +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)) 130 +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)) 131 +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) 132 +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) 133 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 134 +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) 135 +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) 136 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 137 +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) 138 +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) 139 +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) 140 +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)) 141 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 142 +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) 143 +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))) 144 +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) 145 +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) 146 +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)) 147 +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) 148 +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)) 149 +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)) 150 +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) 151 +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) 152 +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) 153 +f1 = Equal.cong(List<&2, Maybe<&2, V>>, List<&2, SP.Ent>, 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) 154 +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) 155 +f3 = Equal.trans(List<&2, SP.Ent>, 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>, 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>, 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>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, A 156 +fr = Equal.trans(List<&2, SP.Ent>, 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>, 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)) 157 +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. 158 +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))) 159 +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)) 160 +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) 161 +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) 162 +c1 = Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, 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) 163 +c2 = Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, 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) 164 +c3 = Equal.cong(SP.Ent, List<&2, SP.Ent>, 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) 165 +c4 = Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, 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>, 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)) 166 +cx = Equal.trans(List<&2, SP.Ent>, 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>, 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) 167 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>}, SC.append(Nat, a, Con{s, b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{s, b}), e), cx) 168 169 170 # the implementation: put_ent, then the count, then the touch 171 def rp_impl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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>}: 172 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 173 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) 174 +hsu = GO.su_lt(su, s, sd, hsv, hs0) 175 +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)) 176 +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)) 177 +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)) 178 +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) 179 +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) 180 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 181 +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) 182 +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) 183 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 184 +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) 185 +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) 186 +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe) 187 +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)) 188 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 189 +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) 190 +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))) 191 +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) 192 +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)) 193 +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) 194 +a1 = UL.wr(one, h1, lkT, sd, hsd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 195 +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) 196 +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) 197 +eL = Equal.trans(Array, 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, Array, 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, 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, Array, 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)) 198 +e1 = Equal.cong(Array>, 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) 199 +e2 = Equal.cong(Array, 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) 200 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) 201 202 def rp_spl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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>}: 203 match sp: 204 case Tuple{+a, Tuple{+b, +e}}: 205 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) 206 207 208 def rp_t(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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, +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}, -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 209 match to: 210 case Tuple{+sh3, Tuple{+e3, Tuple{+em3, g3}}}: 211 +eo = Equal.cong(SP.Lru, 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) 212 +el = Equal.cong(SP.Lru, 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) 213 +ec = Equal.cong(SP.Lru, 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) 214 +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) 215 +esp = Equal.trans(SP.Lru, 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) 216 (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, SP.Lru & 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, 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)))) 217 218 219 def rp_c(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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, fr 220 match cm: 221 case Tuple{+m2, Tuple{+e1, Tuple{+em, g1}}}: 222 +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) 223 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))) 224 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) 225 226 # THEOREM (add, a present key): the entry is replaced and becomes the newest, 227 # counted as an insertion; nothing is evicted 228 def repl_ok(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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{})): 229 +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) 230 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, {==}, {==}, {==}))) 231 +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) 232 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)