proofs/containers/lru/repl.bend

bend-collections-laws-containers@1.0.0.0 · 232 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
7import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
10import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/basic.bend as BA
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bump.bend as BU
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bumpsh.bend as BS
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touch.bend as TO
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touchsh.bend as TSH
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rmat.bend as RM
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/gone.bend as GO
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/meta.bend as MT
24
25import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/read.bend as RD
26import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/hw.bend as HW
27import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/elfr.bend as EF
28import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/walk.bend as WL
29import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/trace.bend as TR
30import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dll.bend as DL
31import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
32import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as TL
33import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
34import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
35import bend-collections-laws-containers@1.0.0.0/proofs/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
43def 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}:
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>, 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)))
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, 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))
70
71# the rewritten slot still holds key and now holds v
72def 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}:
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)), 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)
93
94def 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>}:
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
117def 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>}:
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<V>}, 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<V>}, 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<V>}, 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<V>}, b1, b2, eb, r3)
122
123
124def 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>>}:
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<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)
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<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))))
156  +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))
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.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))
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<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)
163  +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)
164  +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)
165  +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))
166  +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)))
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<V>>}, 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
171def 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>}:
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<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))
198  +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)
199  +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)
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
202def 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>>}:
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
208def 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{})):
209  match to:
210    case Tuple{+sh3, Tuple{+e3, Tuple{+em3, g3}}}:
211      +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)
212      +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)
213      +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)
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<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)
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<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))))
217
218
219def 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{})):
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
228def 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{})):
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)