1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/array.bend as AR 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/hash_table.bend as S 7 import ../../../spec/containers/lru.bend as SP 8 import ../../lib/u32div.bend as UD 9 import ../../../src/math/u64.bend as W 10 import ../../../src/containers/hash_table.bend as H 11 import ../../../src/containers/lru.bend as LR 12 import ../hash_table/table.bend as TB 13 import ../hash_table/buckets.bend as B 14 import ../hash_table/cyc.bend as CY 15 import ../hash_table/inv.bend as IV 16 import ../hash_table/state.bend as HT 17 import ../hash_table/keys.bend as K 18 import ./state.bend as ST 19 import ./basic.bend as BA 20 import ./bump.bend as BU 21 import ./bumpsh.bend as BS 22 import ./tfind.bend as TF 23 import ./unlink.bend as UL 24 import ./lists.bend as LS 25 import ./meta.bend as MT 26 import ../../../src/math/hash.bend as HS 27 import ../hash_table/probe_all.bend as PA 28 29 import ./read.bend as RD 30 import ./hw.bend as HW 31 import ./elfr.bend as EF 32 import ./walk.bend as WL 33 import ./trace.bend as TR 34 import ./dll.bend as DL 35 import ./idx.bend as ID 36 import ./tabsl.bend as TS 37 import ./rebuild.bend as RB 38 import ./linktail.bend as LT 39 import ./room.bend as RO 40 import ./repl.bend as RP 41 import ./ins1.bend as I1 42 import ../hash_table/tools.bend as TL 43 import ../hash_table/insa.bend as IA 44 import ../hash_table/insm.bend as IM 45 import ../hash_table/insu.bend as IU 46 import ../hash_table/insert.bend as IS 47 import ../hash_table/modn.bend as M 48 import ../../lib/u32.bend as UW 49 import ../../lib/nat_list.bend as NL 50 import ../../lib/links.bend as LK 51 import ../../lib/words32.bend as W32 52 import ../../lib/u32_tree.bend as UT 53 54 # add, a new key, the core: slot s (free, off the list) takes the key, its 55 # bucket fills the empty bucket e that ends the key's probe, the slot is 56 # linked as the newest; the model gains the entry, counted as an insertion. 57 58 59 60 # the model of the placed entry 61 def ic_model(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +s: Nat, +su: U32, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hsn: {NL.memn(s, sl) == False{} : Bool}, +fl2: List<&2, Nat>, +free2: U32, +fr2u: U32, +hfree: {U32.is_eq(free2, LK.fst_or(fl2, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, lkT), fl2) == True{} : Bool}, +hfl: {ST.flok(~V, fl2, UD.v(fr2u), AR.slots(Maybe<&2, V>, eT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl2) == True{} : Bool}, +hcnt: {Nat.is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{s, Nil{}})), SC.length(Nat, fl2)), UD.v(fr2u)) == True{} : Bool}, +hsfl: {NL.memn(s, fl2) == False{} : Bool}, +hsfr: {Nat.is_lt(s, UD.v(fr2u)) == True{} : Bool}, +hfrle: {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(fr2u)) == True{} : Bool}, +hfr2: {Nat.is_le(UD.v(fr2u), SC.pow2(sd)) == True{} : Bool}, +Mf: AR.Tree, +pf5: {AR.perfect(U32, 5n, Mf) == True{} : Bool}, +hsm: {AR.slots(U32, Mf) == SC.update(U32, AR.slots(U32, mT), 0n, fr2u) : List<&2, U32>}, +v: V, +t: U32, +lo: U32, +hi: U32, +m 62 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 63 +hsd1 = UL.sd1(sd, hsd) 64 +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1) 65 +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) 66 +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==}) 67 +hk0 = L.and_right(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) 68 +hsu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(su), Equal.sym(Nat, UD.v(su), s, hsv), hs0) 69 +i2 = Equal.trans(Nat, UD.v(LR.hidx(su)), ST.off(UD.v(su), 2n), ST.off(s, 2n), ID.w2(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 2n), UD.v(su), s, hsv)) 70 +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)) 71 +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)) 72 +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)) 73 +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) 74 +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) 75 +hpk = 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) 76 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 77 +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) 78 +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) 79 +p4 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), p3, UD.v(LR.hidx(su)), K.kword(key)) 80 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 81 +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) 82 +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) 83 +s4 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sd, p3, LR.hidx(su), s, 2n, {==}, hs0, i2, K.kword(key)) 84 +sk = Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), UD.v(su), PA.stored(key)), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), AR.upd_slots(String, sd, ksT, UD.v(su), PA.stored(key), hsu, hpk), Equal.cong(Nat, List<&2, String>, z => SC.update(String, AR.slots(String, ksT), z, PA.stored(key)), UD.v(su), s, hsv)) 85 +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)) 86 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 87 +hlk = UT.len_of(String, sd, ksT, hpk, s, hs0) 88 +hb32 = W32.bound32(one, h1, UD.v(su), sd, hsd1, hsu) 89 +hsls = Equal.trans(Nat, UD.v(H.slot(H.link(su))), UD.v(su), s, LK.slot_link(one, h1, su, hb32), hsv) 90 +elk = LT.lnk_su(su, s, sd, hsd, hsv, hs0) 91 +hns = I1.noslot_bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), s, hsn, 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)) 92 +hns2 = L.subst(Nat, z => {HT.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), z, SC.pow2(k)) == True{} : Bool}, s, UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), s, hsls), hns) 93 +hel = I1.tp_len(AR.slots(U32, tabT), AR.slots(String, ksT), k, e, he) 94 +tsl = I1.tp_sl(k, hk30, tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), e, he, K.kword(key), H.link(su)) 95 +w2 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 2n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 2n), K.kword(key), Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 2n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 2n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 2n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 2n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 2n, {==}, {==})), MT.nth_same(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), p3, ST.off(s, 2n), ID.off_lt(s, sd, hs0, 2n, {==}), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key)), s4)) 96 +w3 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 3n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 3n), t, Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 3n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 3n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 3n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 3n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 3n, {==}, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), ST.off(s, 3n)), 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)), t, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(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, 2n), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, 97 +w4 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 4n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 4n), lo, Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 4n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 4n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 4n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 4n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 4n, {==}, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), ST.off(s, 4n)), 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)), lo, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(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, 2n), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+s 98 +w5 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 5n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 5n), hi, Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 5n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 5n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 5n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 5n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 5n, {==}, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), ST.off(s, 5n)), 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, 5n)), hi, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(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, 2n), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+s 99 +f1 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), Equal.cong(List<&2, U32>, List<&2, SP.Ent>, z => ST.es(~V, z, AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR. 100 +f3 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), sl), Equal.cong(List<&2, Maybe<&2, V>>, List<&2, SP.Ent>, z => ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), z, sl), 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), EF.es_el(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), s, Some{v}, sl, hsn)) 101 +f4 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, AR.slots(U32, lkT), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), Equal.cong(List<&2, String>, List<&2, SP.Ent>, z => ST.es(~V, AR.slots(U32, lkT), z, AR.slots(Maybe<&2, V>, eT), sl), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), sk), I1.es_ks(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, PA.stored(key), AR.slots(Maybe<&2, V>, eT), sl, hsn)) 102 +esl = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), f1, Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), f3, f4)) 103 +hmf = 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)) 104 +enk = Equal.trans(String, TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), TB.nths(SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), s), PA.stored(key), Equal.cong(List<&2, String>, String, z => TB.nths(z, s), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), sk), IA.nths_upd_same(AR.slots(String, ksT), s, PA.stored(key), hlk)) 105 +esk = Equal.trans(String, ST.skey(AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), TB.keyof(K.kword(key), TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s)), key, Equal.cong(U32, String, z => TB.keyof(z, TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s)), ST.lw(AR.slots(U32, t3), s, 2n), K.kword(key), w2), Equal.trans(String, TB.keyof(K.kword(key), TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s)), TB.keyof(K.kword(key), PA.stored(key)), key, Equal.cong(String, String, z => TB.keyof(K.kword(key), z), TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), PA.stored(key), enk), IA.keyof_stored(key))) 106 +le = RP.le4(~V, ST.skey(AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), key, v, ST.lw(AR.slots(U32, t3), s, 3n), t, ST.lw(AR.slots(U32, t3), s, 4n), lo, ST.lw(AR.slots(U32, t3), s, 5n), hi, esk, w3, w4, w5) 107 +es1 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}}), SC.append(SP.Ent, ST.sent_m(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s, Some{v}), Nil{}), Con{SP.LE{key, v, t, W.U64{lo, hi}}, Nil{}}, Equal.cong(Maybe<&2, V>, List<&2, SP.Ent>, z => SC.append(SP.Ent, ST.sent_m(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s, z), Nil{}), HT.nthm(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), s), Some{v}, hmf), Equal.cong(SP.Ent, List<&2, SP.Ent>, z => Con{z, Nil{}}, SP.LE{ST.skey(AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), v, ST.lw(AR.slots(U32, t3), s, 3n), W.U64{ST.lw(AR.slots(U32, t3), s, 4n), ST.lw(AR.slots(U32, t3), s, 5n)}}, SP.LE{key, v, t, W.U64{lo, hi}}, le)) 108 +eap = LS.es_app(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl, Con{s, Nil{}}) 109 +esq = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, sl, Con{s, Nil{}})), SC.append(SP.Ent, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}})), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), eap, Equal.trans(List<&2, SP.Ent>, SC.append(SP.Ent, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}})), SC.append(SP.Ent, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), Con{SP.LE{key, v, t, W.U64{lo, hi}}, Nil{}}), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), Equal.trans(List<&2, SP.Ent>, SC.append(SP.Ent, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}})), SC.append(SP.Ent, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), S 110 +e16 = Equal.trans(W.U64, ST.w64(AR.slots(U32, mB), 16n), SP.inc64(ST.w64(AR.slots(U32, Mf), 16n)), SP.inc64(ST.w64(AR.slots(U32, mT), 16n)), ew, Equal.cong(W.U64, W.U64, z => SP.inc64(z), ST.w64(AR.slots(U32, Mf), 16n), ST.w64(AR.slots(U32, mT), 16n), BA.w64_eq(AR.slots(U32, Mf), AR.slots(U32, mT), 16n, Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 16n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 16n), W32.nth0(AR.slots(U32, mT), 16n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 16n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 16n, fr2u, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 17n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 17n), W32.nth0(AR.slots(U32, mT), 17n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 17n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 17n, fr2u, {==}))))) 111 +ec = BA.ct5(ST.w64(AR.slots(U32, mB), 16n), ST.w64(AR.slots(U32, mB), 18n), ST.w64(AR.slots(U32, mB), 20n), ST.w64(AR.slots(U32, mB), 22n), ST.w64(AR.slots(U32, mB), 24n), SP.inc64(ST.w64(AR.slots(U32, mT), 16n)), ST.w64(AR.slots(U32, mT), 18n), ST.w64(AR.slots(U32, mT), 20n), ST.w64(AR.slots(U32, mT), 22n), ST.w64(AR.slots(U32, mT), 24n), e16, BA.w64_eq(AR.slots(U32, mB), AR.slots(U32, mT), 18n, Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 18n), W32.nth0(AR.slots(U32, Mf), 18n), W32.nth0(AR.slots(U32, mT), 18n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 18n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 18n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 18n), W32.nth0(AR.slots(U32, mT), 18n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 18n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 18n, fr2u, {==}))), Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 19n), W32.nth0(AR.slots(U32, Mf), 19n), W32.nth0(AR.slots(U32, mT), 19n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 19n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 19n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 19n), W32.nth0(AR.slots(U32, mT), 19n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 19n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 19n, fr2u, {==})))), BA.w64_eq(AR.slots(U32, mB), AR.slots(U32, mT), 20n, Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 20n), W32.nth0(AR.slots(U32, Mf), 20n), W32.nth0(AR.slots(U32, mT), 20n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 20n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 20n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 20n), W32.nth0(AR.slots(U32, mT), 20n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 20n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 20n, fr2u, {==}))), E 112 BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, mB), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mB), 4n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, sl, Con{s, Nil{}})), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), ST.ctr(AR.slots(U32, mB)), SP.c_ins(ST.ctr(AR.slots(U32, mT))), Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 3n), W32.nth0(AR.slots(U32, Mf), 3n), W32.nth0(AR.slots(U32, mT), 3n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 3n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 3n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 3n), W32.nth0(AR.slots(U32, mT), 3n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 3n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 3n, fr2u, {==}))), BA.w64_eq(AR.slots(U32, mB), AR.slots(U32, mT), 4n, Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 4n), W32.nth0(AR.slots(U32, Mf), 4n), W32.nth0(AR.slots(U32, mT), 4n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 4n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 4n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 4n), W32.nth0(AR.slots(U32, mT), 4n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 4n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 4n, fr2u, {==}))), Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 5n), W32.nth0(AR.slots(U32, Mf), 5n), W32.nth0(AR.slots(U32, mT), 5n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 5n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 5n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 5n), W32.nth0(AR.slots(U32, mT), 5n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 5n), AR.slots(U32 113 114 # the invariant of the placed entry 115 def ic_good(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +s: Nat, +su: U32, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hsn: {NL.memn(s, sl) == False{} : Bool}, +fl2: List<&2, Nat>, +free2: U32, +fr2u: U32, +hfree: {U32.is_eq(free2, LK.fst_or(fl2, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, lkT), fl2) == True{} : Bool}, +hfl: {ST.flok(~V, fl2, UD.v(fr2u), AR.slots(Maybe<&2, V>, eT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl2) == True{} : Bool}, +hcnt: {Nat.is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{s, Nil{}})), SC.length(Nat, fl2)), UD.v(fr2u)) == True{} : Bool}, +hsfl: {NL.memn(s, fl2) == False{} : Bool}, +hsfr: {Nat.is_lt(s, UD.v(fr2u)) == True{} : Bool}, +hfrle: {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(fr2u)) == True{} : Bool}, +hfr2: {Nat.is_le(UD.v(fr2u), SC.pow2(sd)) == True{} : Bool}, +Mf: AR.Tree, +pf5: {AR.perfect(U32, 5n, Mf) == True{} : Bool}, +hsm: {AR.slots(U32, Mf) == SC.update(U32, AR.slots(U32, mT), 0n, fr2u) : List<&2, U32>}, +v: V, +t: U32, +lo: U32, +hi: U32, +mB 116 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 117 +hsd1 = UL.sd1(sd, hsd) 118 +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1) 119 +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) 120 +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==}) 121 +hk0 = L.and_right(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) 122 +hsu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(su), Equal.sym(Nat, UD.v(su), s, hsv), hs0) 123 +i2 = Equal.trans(Nat, UD.v(LR.hidx(su)), ST.off(UD.v(su), 2n), ST.off(s, 2n), ID.w2(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 2n), UD.v(su), s, hsv)) 124 +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)) 125 +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)) 126 +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)) 127 +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) 128 +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) 129 +hpk = 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) 130 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 131 +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) 132 +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) 133 +p4 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), p3, UD.v(LR.hidx(su)), K.kword(key)) 134 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 135 +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) 136 +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) 137 +s4 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sd, p3, LR.hidx(su), s, 2n, {==}, hs0, i2, K.kword(key)) 138 +sk = Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), UD.v(su), PA.stored(key)), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), AR.upd_slots(String, sd, ksT, UD.v(su), PA.stored(key), hsu, hpk), Equal.cong(Nat, List<&2, String>, z => SC.update(String, AR.slots(String, ksT), z, PA.stored(key)), UD.v(su), s, hsv)) 139 +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)) 140 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 141 +hlk = UT.len_of(String, sd, ksT, hpk, s, hs0) 142 +hb32 = W32.bound32(one, h1, UD.v(su), sd, hsd1, hsu) 143 +hsls = Equal.trans(Nat, UD.v(H.slot(H.link(su))), UD.v(su), s, LK.slot_link(one, h1, su, hb32), hsv) 144 +elk = LT.lnk_su(su, s, sd, hsd, hsv, hs0) 145 +hns = I1.noslot_bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), s, hsn, 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)) 146 +hns2 = L.subst(Nat, z => {HT.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), z, SC.pow2(k)) == True{} : Bool}, s, UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), s, hsls), hns) 147 +hel = I1.tp_len(AR.slots(U32, tabT), AR.slots(String, ksT), k, e, he) 148 +tsl = I1.tp_sl(k, hk30, tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), e, he, K.kword(key), H.link(su)) 149 +bs1 = Equal.cong(List<&2, U32>, List<&2, B.Bk>, z => TB.buckets(z, AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(su)), tsl) 150 +ekl = Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(su))), PA.stored(key)), sk, Equal.cong(Nat, List<&2, String>, z => SC.update(String, AR.slots(String, ksT), z, PA.stored(key)), s, UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), s, hsls))) 151 +bs2 = Equal.cong(List<&2, String>, List<&2, B.Bk>, z => TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(su)), z, SC.pow2(k)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(su))), PA.stored(key)), ekl) 152 +htb = UT.len_of(U32, 1n+k, tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), 1n+Nat.double(e), N.double_lt_bit(True{}, e, SC.pow2(k), he)) 153 +hkl2 = L.subst(Nat, z => {Nat.is_lt(z, SC.length(String, AR.slots(String, ksT))) == True{} : Bool}, s, UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), s, hsls), hlk) 154 +bs3 = IA.buckets_put(AR.slots(U32, tabT), AR.slots(String, ksT), e, K.kword(key), H.link(su), PA.stored(key), SC.pow2(k), hns2, IS.kword_nz(key), htb, hkl2) 155 +bs4 = Equal.cong(String, List<&2, B.Bk>, z => IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), z}), TB.keyof(K.kword(key), PA.stored(key)), key, IA.keyof_stored(key)) 156 +bp = Equal.trans(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(su)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bs1, Equal.trans(List<&2, B.Bk>, TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(su)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(su)), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(su))), PA.stored(key)), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bs2, Equal.trans(List<&2, B.Bk>, TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(su)), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(su))), PA.stored(key)), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), TB.keyof(K.kword(key), PA.stored(key))}), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bs3, bs4))) 157 +w2 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 2n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 2n), K.kword(key), Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 2n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 2n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 2n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 2n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 2n, {==}, {==})), MT.nth_same(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), p3, ST.off(s, 2n), ID.off_lt(s, sd, hs0, 2n, {==}), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key)), s4)) 158 +w3 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 3n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 3n), t, Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 3n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 3n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 3n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 3n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 3n, {==}, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), ST.off(s, 3n)), 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)), t, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(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, 2n), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, 159 +w4 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 4n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 4n), lo, Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 4n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 4n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 4n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 4n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 4n, {==}, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), ST.off(s, 4n)), 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)), lo, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(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, 2n), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+s 160 +w5 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 5n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 5n), hi, Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 5n), ST.lw(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), s, 5n), ST.lw(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), s, 5n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 5n), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.lw_tr_hi(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, s, 5n, {==}, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), ST.off(s, 5n)), 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, 5n)), hi, MT.nth_other(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(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, 2n), K.kword(key), AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+s 161 +f1 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), Equal.cong(List<&2, U32>, List<&2, SP.Ent>, z => ST.es(~V, z, AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR. 162 +f3 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v}), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), sl), Equal.cong(List<&2, Maybe<&2, V>>, List<&2, SP.Ent>, z => ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), z, sl), 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), EF.es_el(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), s, Some{v}, sl, hsn)) 163 +f4 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, AR.slots(U32, lkT), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), Equal.cong(List<&2, String>, List<&2, SP.Ent>, z => ST.es(~V, AR.slots(U32, lkT), z, AR.slots(Maybe<&2, V>, eT), sl), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), sk), I1.es_ks(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, PA.stored(key), AR.slots(Maybe<&2, V>, eT), sl, hsn)) 164 +esl = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), f1, Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), f3, f4)) 165 +hmf = 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)) 166 +enk = Equal.trans(String, TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), TB.nths(SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), s), PA.stored(key), Equal.cong(List<&2, String>, String, z => TB.nths(z, s), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), sk), IA.nths_upd_same(AR.slots(String, ksT), s, PA.stored(key), hlk)) 167 +esk = Equal.trans(String, ST.skey(AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), TB.keyof(K.kword(key), TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s)), key, Equal.cong(U32, String, z => TB.keyof(z, TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s)), ST.lw(AR.slots(U32, t3), s, 2n), K.kword(key), w2), Equal.trans(String, TB.keyof(K.kword(key), TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s)), TB.keyof(K.kword(key), PA.stored(key)), key, Equal.cong(String, String, z => TB.keyof(K.kword(key), z), TB.nths(AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), PA.stored(key), enk), IA.keyof_stored(key))) 168 +le = RP.le4(~V, ST.skey(AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), key, v, ST.lw(AR.slots(U32, t3), s, 3n), t, ST.lw(AR.slots(U32, t3), s, 4n), lo, ST.lw(AR.slots(U32, t3), s, 5n), hi, esk, w3, w4, w5) 169 +es1 = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}}), SC.append(SP.Ent, ST.sent_m(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s, Some{v}), Nil{}), Con{SP.LE{key, v, t, W.U64{lo, hi}}, Nil{}}, Equal.cong(Maybe<&2, V>, List<&2, SP.Ent>, z => SC.append(SP.Ent, ST.sent_m(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s, z), Nil{}), HT.nthm(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), s), Some{v}, hmf), Equal.cong(SP.Ent, List<&2, SP.Ent>, z => Con{z, Nil{}}, SP.LE{ST.skey(AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), s), v, ST.lw(AR.slots(U32, t3), s, 3n), W.U64{ST.lw(AR.slots(U32, t3), s, 4n), ST.lw(AR.slots(U32, t3), s, 5n)}}, SP.LE{key, v, t, W.U64{lo, hi}}, le)) 170 +eap = LS.es_app(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl, Con{s, Nil{}}) 171 +esq = Equal.trans(List<&2, SP.Ent>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, sl, Con{s, Nil{}})), SC.append(SP.Ent, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}})), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), eap, Equal.trans(List<&2, SP.Ent>, SC.append(SP.Ent, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}})), SC.append(SP.Ent, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), Con{SP.LE{key, v, t, W.U64{lo, hi}}, Nil{}}), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), Equal.trans(List<&2, SP.Ent>, SC.append(SP.Ent, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), sl), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), Con{s, Nil{}})), SC.append(SP.Ent, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), S 172 +hslt = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, UD.v(su), UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), UD.v(su), LK.slot_link(one, h1, su, hb32)), hsu) 173 +hwb = L.and_intro(Nat.is_lt(UD.v(H.slot(H.link(su))), SC.pow2(sd)), Bool.and(U32.is_eq(K.kword(key), K.kword(key)), Bool.not(U32.is_eq(H.link(su), 0))), hslt, L.and_intro(U32.is_eq(K.kword(key), K.kword(key)), Bool.not(U32.is_eq(H.link(su), 0)), UW.u32_eq_refl(K.kword(key)), IM.not_f(U32.is_eq(H.link(su), 0), W32.link_nz(one, h1, su, hb32)))) 174 +hwell = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PWell{z, sd}, SC.pow2(k)) == True{} : Bool}, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bp), IM.well_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}, hel, sd, hwb, SC.pow2(k), ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), SC.pow2(k), N.le_refl(SC.pow2(k)))) 175 +hclus = L.subst(List<&2, B.Bk>, z => {B.cluster(z, SC.pow2(k), CY.msk(k)) == True{} : Bool}, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bp), IM.clus_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}, {==}, hel, SC.pow2(k), CY.msk(k), hp, 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))) 176 +huniq = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PUniq{z}, SC.pow2(k)) == True{} : Bool}, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bp), IM.uq_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, hel, K.kword(key), H.link(su), key, SC.pow2(k), he, 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), hno, hns2)) 177 +ea = IU.inc_n(one, h1, k, hk31, hk0, n, 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)) 178 +eo = Equal.trans(Nat, UD.v(U32.inc(n)), 1n+UD.v(n), IV.occn(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), SC.pow2(k)), ea, Equal.trans(Nat, 1n+UD.v(n), 1n+IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), SC.pow2(k)), Equal.cong(Nat, Nat, z => 1n+z, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), ST.g_cn(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg))), Equal.trans(Nat, 1n+IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k)), IV.occn(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), SC.pow2(k)), Equal.sym(Nat, IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k)), 1n+IV.occn(TB.buckets(AR.slots(U32, tabT), 179 +hcn2 = IS.eq_is_eq(UD.v(U32.inc(n)), IV.occn(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), SC.pow2(k)), eo) 180 +hld2 = L.subst(Nat, z => {Nat.is_le(Nat.double(z), SC.pow2(k)) == True{} : Bool}, 1n+UD.v(n), UD.v(U32.inc(n)), Equal.sym(Nat, UD.v(U32.inc(n)), 1n+UD.v(n), ea), hroom) 181 +b0 = RB.bsl_sub(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, lkT), SC.pow2(k), ST.g_cbsl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), RB.subl_ml(sl, sl, Con{s, Nil{}}, RB.subl_refl(sl))) 182 +b1 = Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, t3), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, sl, Con{s, Nil{}}), 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)), SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, t3), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, sl, Con{s, Nil{}}), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), 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)), SC.append(Nat, sl, Con{s, Nil{}}), z, SC.pow2(k)), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.bsl_tr(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su 183 +m1 = L.subst(Nat, z => {NL.memn(z, SC.append(Nat, sl, Con{s, Nil{}})) == True{} : Bool}, s, UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), s, hsls), NL.mem_app_r(s, sl, Con{s, Nil{}}, UL.self_in(s, Nil{}))) 184 +wq = L.subst(U32, z => {U32.is_eq(z, K.kword(key)) == True{} : Bool}, K.kword(key), ST.lw(AR.slots(U32, t3), s, 2n), Equal.sym(U32, ST.lw(AR.slots(U32, t3), s, 2n), K.kword(key), w2), UW.u32_eq_refl(K.kword(key))) 185 +wq2 = L.subst(Nat, z => {U32.is_eq(ST.lw(AR.slots(U32, t3), z, 2n), K.kword(key)) == True{} : Bool}, s, UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), s, hsls), wq) 186 +hbn = L.and_intro(NL.memn(UD.v(H.slot(H.link(su))), SC.append(Nat, sl, Con{s, Nil{}})), U32.is_eq(ST.lw(AR.slots(U32, t3), UD.v(H.slot(H.link(su))), 2n), K.kword(key)), m1, wq2) 187 +hbsl = L.subst(List<&2, B.Bk>, z => {ST.bsl(z, SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, t3), SC.pow2(k)) == True{} : Bool}, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bp), I1.bsl_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}, hel, SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, t3), hbn, SC.pow2(k), Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, t3), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, sl, Con{s, Nil{}}), AR.slots(U32, lkT), SC.pow2(k)), True{}, b1, b0))) 188 +ha0 = 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, t3), 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, t3), 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, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), 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, t3), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), 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, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), 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, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.has_tr(~V, AR.slots(U 189 +ha1 = I1.has_up(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}, hz, SC.pow2(k), AR.slots(U32, t3), sl, ha0) 190 +hib0 = L.and_intro(U32.is_eq(K.kword(key), ST.lw(AR.slots(U32, t3), s, 2n)), U32.is_eq(H.link(su), LK.lnk(s)), L.subst(U32, z => {U32.is_eq(K.kword(key), z) == True{} : Bool}, K.kword(key), ST.lw(AR.slots(U32, t3), s, 2n), Equal.sym(U32, ST.lw(AR.slots(U32, t3), s, 2n), K.kword(key), w2), UW.u32_eq_refl(K.kword(key))), L.subst(U32, z => {U32.is_eq(H.link(su), z) == True{} : Bool}, H.link(su), LK.lnk(s), elk, UW.u32_eq_refl(H.link(su)))) 191 +hib = L.subst(B.Bk, z => {ST.isbf(z, ST.lw(AR.slots(U32, t3), s, 2n), LK.lnk(s)) == True{} : Bool}, B.BF{K.kword(key), H.link(su), key}, B.at(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), e), Equal.sym(B.Bk, B.at(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), e), B.BF{K.kword(key), H.link(su), key}, IM.at_bupd_same(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}, hel)), hib0) 192 +ha2 = L.and_intro(ST.anyb(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), LK.lnk(s), ST.lw(AR.slots(U32, t3), s, 2n)), True{}, TS.anyb_intro(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), LK.lnk(s), ST.lw(AR.slots(U32, t3), s, 2n), e, he, hib), {==}) 193 +ha3 = L.subst(Bool, z => {z == True{} : Bool}, Bool.and(ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), sl), ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), Con{s, Nil{}})), ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), SC.append(Nat, sl, Con{s, Nil{}})), Equal.sym(Bool, ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), SC.append(Nat, sl, Con{s, Nil{}})), Bool.and(ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), sl), ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), Con{s, Nil{}})), LS.sall_app(~V, ST.PHas{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3)}, sl, Con{s, Nil{}})), L.and_intro(ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), sl), ST.hasall(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), SC.pow2(k), AR.slots(U32, t3), Con{s, Nil{}}), ha1, ha2)) 194 +hhas = L.subst(List<&2, B.Bk>, z => {ST.hasall(~V, z, SC.pow2(k), AR.slots(U32, t3), SC.append(Nat, sl, Con{s, Nil{}})) == True{} : Bool}, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(su), key}), bp), ha3) 195 +sa1 = L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, sl, UD.v(fr2u), 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.slok(~V, sl, UD.v(fr2u), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v})), ST.slok(~V, sl, UD.v(fr2u), AR.slots(Maybe<&2, V>, eT)), True{}, EF.slok_el(~V, AR.slots(Maybe<&2, V>, eT), s, Some{v}, UD.v(fr2u), sl, hsn), I1.slok_mono(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(fr2u), AR.slots(Maybe<&2, V>, eT), hfrle, 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)))) 196 +lvs = L.subst(List<&2, Maybe<&2, V>>, z => {ST.live(~V, z, s) == 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.live_same(~V, AR.slots(Maybe<&2, V>, eT), s, v, hle)) 197 +sa2 = L.and_intro(Bool.and(Nat.is_lt(s, UD.v(fr2u)), ST.live(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), s)), True{}, L.and_intro(Nat.is_lt(s, UD.v(fr2u)), ST.live(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), s), hsfr, lvs), {==}) 198 +hsl2 = L.subst(Bool, z => {z == True{} : Bool}, Bool.and(ST.slok(~V, sl, UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}))), ST.slok(~V, Con{s, Nil{}}, UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})))), ST.slok(~V, SC.append(Nat, sl, Con{s, Nil{}}), UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}))), Equal.sym(Bool, ST.slok(~V, SC.append(Nat, sl, Con{s, Nil{}}), UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}))), Bool.and(ST.slok(~V, sl, UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}))), ST.slok(~V, Con{s, Nil{}}, UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})))), LS.sall_app(~V, ST.PLive{UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}))}, sl, Con{s, Nil{}})), L.and_intro(ST.slok(~V, sl, UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}))), ST.slok(~V, Con{s, Nil{}}, UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}))), sa1, sa2)) 199 +hlen2 = IS.eq_is_eq(SC.length(Nat, SC.append(Nat, sl, Con{s, Nil{}})), UD.v(U32.inc(n)), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, sl, Con{s, Nil{}})), 1n+SC.length(Nat, sl), UD.v(U32.inc(n)), I1.len_snoc(sl, s), Equal.trans(Nat, 1n+SC.length(Nat, sl), 1n+UD.v(n), UD.v(U32.inc(n)), Equal.cong(Nat, Nat, z => 1n+z, SC.length(Nat, sl), UD.v(n), N.eq_from_is_eq(SC.length(Nat, sl), UD.v(n), 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))), Equal.sym(Nat, UD.v(U32.inc(n)), 1n+UD.v(n), ea)))) 200 +htl = L.subst(U32, z => {U32.is_eq(LK.lnk(s), z) == True{} : Bool}, LK.lnk(s), LK.last_or(SC.append(Nat, sl, Con{s, Nil{}}), 0), Equal.sym(U32, LK.last_or(SC.append(Nat, sl, Con{s, Nil{}}), 0), LK.lnk(s), LK.last_app(sl, Con{s, Nil{}}, 0)), LK.u_refl(LK.lnk(s))) 201 +hnk = TF.nokey_of(~V, one, h1, AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), key, hno, AR.slots(U32, lkT), AR.slots(Maybe<&2, V>, eT), sd, hsd1, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), sl, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), ST.g_chas(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) 202 +hnm = L.subst(List<&2, String>, z => {S.mem(key, z) == False{} : Bool}, 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.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), 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))), I1.nokey_nm(~V, AR.slots(U32, lkT), AR.slots(String, ksT), sl, key, hnk)) 203 +hk1 = I1.nds_snoc(SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), key, 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), hnm) 204 +ekk = Equal.trans(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, sl, Con{s, Nil{}}))), SP.keys_of(~V, SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}})), SC.append(String, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), Con{key, Nil{}}), Equal.cong(List<&2, SP.Ent>, List<&2, String>, z => SP.keys_of(~V, z), ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, sl, Con{s, Nil{}})), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), esq), Equal.trans(List<&2, String>, SP.keys_of(~V, SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}})), SP.keys_of(~V, SC.append(SP.Ent, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), Con{SP.LE{key, v, t, W.U64{lo, hi}}, Nil{}})), SC.append(String, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), Con{key, Nil{}}), Equal.cong(List<&2, SP.Ent>, List<&2, String>, z => SP.keys_of(~V, z), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SC.append(SP.Ent, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), Con{SP.LE{key, v, t, W.U64{lo, hi}}, Nil{}}), LS.snoc_app(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}})), LS.keys_app(~V, ST.es(~V, AR.slots(U32, lkT), AR.slo 205 +hkeys = L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, SC.append(String, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), Con{key, Nil{}}), SP.keys_of(~V, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, sl, Con{s, Nil{}}))), Equal.sym(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, t3), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), SC.append(Nat, sl, Con{s, Nil{}}))), SC.append(String, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), Con{key, Nil{}}), ekk), hk1) 206 +hfl2 = L.subst(List<&2, Maybe<&2, V>>, z => {ST.flok(~V, fl2, UD.v(fr2u), 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, fl2, UD.v(fr2u), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, Some{v})), ST.flok(~V, fl2, UD.v(fr2u), AR.slots(Maybe<&2, V>, eT)), True{}, EF.flok_el(~V, AR.slots(Maybe<&2, V>, eT), s, Some{v}, UD.v(fr2u), fl2, hsfl), hfl)) 207 +hout = TR.out_of_in(~V, tr, SC.append(Nat, sl, Con{s, Nil{}}), fl2, UD.v(fr2u), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), hin, hsl2, hfl2) 208 +hfll2 = Equal.trans(Bool, ST.fll(AR.slots(U32, t3), fl2), ST.fll(AR.slots(U32, lkT), fl2), True{}, Equal.trans(Bool, ST.fll(AR.slots(U32, t3), fl2), ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), fl2), ST.fll(AR.slots(U32, lkT), fl2), Equal.trans(Bool, ST.fll(AR.slots(U32, t3), fl2), ST.fll(TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), fl2), ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), fl2), Equal.cong(List<&2, U32>, Bool, z => ST.fll(z, fl2), AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr), hs3), TR.fll_tr(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), tr, hlo, fl2, hout)), Equal.trans(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), fl2), 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)), fl2), ST.fll(AR.slots(U32, lkT), fl2), Equal.trans(Bool, ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, 209 +e0 = Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 0n), W32.nth0(AR.slots(U32, Mf), 0n), fr2u, BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 0n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 0n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 0n), fr2u, Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 0n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_same(AR.slots(U32, mT), 0n, fr2u, UT.len_of(U32, 5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), 0n, {==})))) 210 +gx = ST.good_intro(~V, cap, U32.inc(n), LK.fst_or(SC.append(Nat, sl, Con{s, Nil{}}), 0), LK.lnk(s), free2, fr2u, 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), True{}, k, sd, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), t3, SC.append(Nat, sl, Con{s, Nil{}}), fl2, 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), I1.tp_p(k, hk30, tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), e, he, K.kword(key), H.link(su)), AR.upd_perfect(String, sd, ksT, UD.v(su), PA.stored(key), hpk), AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}, hpe), hp3, {==}, 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.perfec 211 RO.good_mk(~V, cap, U32.inc(n), LK.fst_or(SC.append(Nat, sl, Con{s, Nil{}}), 0), LK.lnk(s), free2, mB, fr2u, 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), k, sd, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su)), AR.upd(String, sd, ksT, UD.v(su), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), t3, SC.append(Nat, sl, Con{s, Nil{}}), fl2, gx, e0, Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 1n), W32.nth0(AR.slots(U32, Mf), 1n), W32.nth0(AR.slots(U32, mT), 1n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 1n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 1n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 1n), W32.nth0(AR.slots(U32, mT), 1n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 1n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 1n, fr2u, {==}))), Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 2n), W32.nth0(AR.slots(U32, Mf), 2n), W32.nth0(AR.slots(U32, mT), 2n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 2n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 2n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 2n), W32.nth0(AR.slots(U32, mT), 2n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 2n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W32.nth0_upd_other(AR.slots(U32, mT), 0n, 2n, fr2u, {==}))), Equal.trans(U32, W32.nth0(AR.slots(U32, mB), 6n), W32.nth0(AR.slots(U32, Mf), 6n), W32.nth0(AR.slots(U32, mT), 6n), BS.keep(AR.slots(U32, Mf), mB, 16n, x, y, eb, 6n, {==}, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, Mf), 6n), W32.nth0(SC.update(U32, AR.slots(U32, mT), 0n, fr2u), 6n), W32.nth0(AR.slots(U32, mT), 6n), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, 6n), AR.slots(U32, Mf), SC.update(U32, AR.slots(U32, mT), 0n, fr2u), hsm), W 212 213 214 def ic_l(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +s: Nat, +su: U32, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hsn: {NL.memn(s, sl) == False{} : Bool}, +fl2: List<&2, Nat>, +free2: U32, +fr2u: U32, +hfree: {U32.is_eq(free2, LK.fst_or(fl2, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, lkT), fl2) == True{} : Bool}, +hfl: {ST.flok(~V, fl2, UD.v(fr2u), AR.slots(Maybe<&2, V>, eT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl2) == True{} : Bool}, +hcnt: {Nat.is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{s, Nil{}})), SC.length(Nat, fl2)), UD.v(fr2u)) == True{} : Bool}, +hsfl: {NL.memn(s, fl2) == False{} : Bool}, +hsfr: {Nat.is_lt(s, UD.v(fr2u)) == True{} : Bool}, +hfrle: {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(fr2u)) == True{} : Bool}, +hfr2: {Nat.is_le(UD.v(fr2u), SC.pow2(sd)) == True{} : Bool}, +Mf: AR.Tree, +pf5: {AR.perfect(U32, 5n, Mf) == True{} : Bool}, +hsm: {AR.slots(U32, Mf) == SC.update(U32, AR.slots(U32, mT), 0n, fr2u) : List<&2, U32>}, +v: V, +t: U32, +lo: U32, +hi: U32, +mB: A 215 match lt: 216 case Tuple{+t3, Tuple{+tr, Tuple{+ef, Tuple{+hp3, Tuple{+hs3, Tuple{+hlo, Tuple{+hin, g3}}}}}}}: 217 +hg3 = {g3 : {ST.seg(AR.slots(U32, t3), SC.append(Nat, sl, Con{s, Nil{}}), 0, 0) == True{} : Bool}} 218 (ST.LS{cap, U32.inc(n), LK.fst_or(SC.append(Nat, sl, Con{s, Nil{}}), 0), LK.lnk(s), free2, mB, k, sd, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su)), AR.upd(String, sd, ksT, UD.v(su), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), t3, SC.append(Nat, sl, Con{s, Nil{}}), fl2}, (ef, (ic_model(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, s, su, hsv, hs0, hsn, fl2, free2, fr2u, hfree, hfll, hfl, hfnd, hcnt, hsfl, hsfr, hfrle, hfr2, Mf, pf5, hsm, v, t, lo, hi, mB, pm2, ew, x, y, eb, t3, tr, hp3, hs3, hlo, hin, hg3), ic_good(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, s, su, hsv, hs0, hsn, fl2, free2, fr2u, hfree, hfll, hfl, hfnd, hcnt, hsfl, hsfr, hfrle, hfr2, Mf, pf5, hsm, v, t, lo, hi, mB, pm2, ew, x, y, eb, t3, tr, hp3, hs3, hlo, hin, hg3)))) 219 220 221 def ic_b(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +s: Nat, +su: U32, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hsn: {NL.memn(s, sl) == False{} : Bool}, +fl2: List<&2, Nat>, +free2: U32, +fr2u: U32, +hfree: {U32.is_eq(free2, LK.fst_or(fl2, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, lkT), fl2) == True{} : Bool}, +hfl: {ST.flok(~V, fl2, UD.v(fr2u), AR.slots(Maybe<&2, V>, eT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl2) == True{} : Bool}, +hcnt: {Nat.is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{s, Nil{}})), SC.length(Nat, fl2)), UD.v(fr2u)) == True{} : Bool}, +hsfl: {NL.memn(s, fl2) == False{} : Bool}, +hsfr: {Nat.is_lt(s, UD.v(fr2u)) == True{} : Bool}, +hfrle: {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(fr2u)) == True{} : Bool}, +hfr2: {Nat.is_le(UD.v(fr2u), SC.pow2(sd)) == True{} : Bool}, +Mf: AR.Tree, +pf5: {AR.perfect(U32, 5n, Mf) == True{} : Bool}, +hsm: {AR.slots(U32, Mf) == SC.update(U32, AR.slots(U32, mT), 0n, fr2u) : List<&2, U32>}, +v: V, +t: U32, +lo: U32, +hi: U32, bo: BU 222 match bo: 223 case Tuple{+mB, Tuple{+ea, Tuple{+pm2, Tuple{+ew, Tuple{+x, Tuple{+y, eb}}}}}}: 224 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) 225 +hsd1 = UL.sd1(sd, hsd) 226 +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1) 227 +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) 228 +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==}) 229 +hk0 = L.and_right(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg)) 230 +hsu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(su), Equal.sym(Nat, UD.v(su), s, hsv), hs0) 231 +i2 = Equal.trans(Nat, UD.v(LR.hidx(su)), ST.off(UD.v(su), 2n), ST.off(s, 2n), ID.w2(one, h1, su, sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 2n), UD.v(su), s, hsv)) 232 +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)) 233 +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)) 234 +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)) 235 +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) 236 +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) 237 +hpk = 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) 238 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.tidx(su)), t) 239 +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) 240 +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) 241 +p4 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), p3, UD.v(LR.hidx(su)), K.kword(key)) 242 +s1 = UL.wr_s(lkT, sd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 243 +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) 244 +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) 245 +s4 = UL.wr_s(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sd, p3, LR.hidx(su), s, 2n, {==}, hs0, i2, K.kword(key)) 246 +sk = Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), SC.update(String, AR.slots(String, ksT), UD.v(su), PA.stored(key)), SC.update(String, AR.slots(String, ksT), s, PA.stored(key)), AR.upd_slots(String, sd, ksT, UD.v(su), PA.stored(key), hsu, hpk), Equal.cong(Nat, List<&2, String>, z => SC.update(String, AR.slots(String, ksT), z, PA.stored(key)), UD.v(su), s, hsv)) 247 +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)) 248 +hle = UT.len_of(Maybe<&2, V>, sd, eT, hpe, s, hs0) 249 +hlk = UT.len_of(String, sd, ksT, hpk, s, hs0) 250 +hb32 = W32.bound32(one, h1, UD.v(su), sd, hsd1, hsu) 251 +hsls = Equal.trans(Nat, UD.v(H.slot(H.link(su))), UD.v(su), s, LK.slot_link(one, h1, su, hb32), hsv) 252 +elk = LT.lnk_su(su, s, sd, hsd, hsv, hs0) 253 +hns = I1.noslot_bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), s, hsn, 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)) 254 +hns2 = L.subst(Nat, z => {HT.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), z, SC.pow2(k)) == True{} : Bool}, s, UD.v(H.slot(H.link(su))), Equal.sym(Nat, UD.v(H.slot(H.link(su))), s, hsls), hns) 255 +hel = I1.tp_len(AR.slots(U32, tabT), AR.slots(String, ksT), k, e, he) 256 +tsl = I1.tp_sl(k, hk30, tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), e, he, K.kword(key), H.link(su)) 257 +hxk = TB.nths_some(AR.slots(String, ksT), UD.v(su), UT.len_of(String, sd, ksT, hpk, UD.v(su), hsu)) 258 +eK = AR.set(String, sd, ksT, su, PA.stored(key), TB.nths(AR.slots(String, ksT), UD.v(su)), hsd32, hsu, hxk, hpk) 259 +hxe = 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)) 260 +eE = AR.set(Maybe<&2, V>, sd, eT, su, Some{v}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su)), hsd32, hsu, hxe, hpe) 261 +a1 = UL.wr(one, h1, lkT, sd, hsd, hpl, LR.tidx(su), s, 3n, {==}, hs0, i3, t) 262 +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) 263 +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) 264 +a4 = UL.wr(one, h1, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), sd, hsd, p3, LR.hidx(su), s, 2n, {==}, hs0, i2, K.kword(key)) 265 +eL = Equal.trans(Array, Array.set(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), LR.hidx(su), K.kword(key)), Array.set(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), LR.hidx(su), K.kword(key)), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), Equal.cong(Array, Array, z => Array.set(U32, Array.set(U32, Array.set(U32, z, LR.dlo_idx(su), lo), LR.dhi_idx(su), hi), LR.hidx(su), K.kword(key)), Array.set(U32, AR.thaw(U32, lkT), LR.tidx(su), t), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t)), a1), Equal.trans(Array, Array.set(U32, Array.set(U32, 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), LR.hidx(su), K.kword(key)), Array.set(U32, 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), LR.hidx(su), K.kword(key)), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), Equal.cong(Array, Array, z => Array.set(U32, Array.set(U32, z, LR.dhi_idx(su), hi), LR.hidx(su), K.kword(key)), 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), Equal.trans(Array, Array.set(U32, 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), LR.hidx(su), K.kword(key)), Array.se 266 +r1 = Equal.cong(Array, LR.LRU<&2, V>, z => LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, z, AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), Array.set(String, AR.thaw(String, ksT), su, PA.stored(key)), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, Some{v}), Array.set(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), LR.hidx(su), K.kword(key))}, su), LR.bump(0, AR.thaw(U32, Mf)), AR.thaw(U32, mB), ea) 267 +r2 = Equal.cong(Array, LR.LRU<&2, V>, z => LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), z, Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, Some{v}), Array.set(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), LR.hidx(su), K.kword(key))}, su), Array.set(String, AR.thaw(String, ksT), su, PA.stored(key)), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), eK) 268 +r3 = Equal.cong(Array>, LR.LRU<&2, V>, z => LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), z, Array.set(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), LR.hidx(su), K.kword(key))}, su), 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) 269 +r4 = Equal.cong(Array, LR.LRU<&2, V>, z => LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), z}, su), Array.set(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), LR.hidx(su), K.kword(key)), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), eL) 270 +ER = Equal.trans(LR.LRU<&2, V>, LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, LR.bump(0, AR.thaw(U32, Mf)), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), Array.set(String, AR.thaw(String, ksT), su, PA.stored(key)), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, Some{v}), Array.set(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), LR.hidx(su), K.kword(key))}, su), LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), Array.set(String, AR.thaw(String, ksT), su, PA.stored(key)), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su, Some{v}), Array.set(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), LR.hidx(su), K.kword(key))}, su), LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), 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, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key)))}, su), r1, Equal.trans(LR.LRU<&2, V>, LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), Array.set(String, AR.thaw( 271 +hseg4 = Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), 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, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), sl, 0, 0), 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), Equal.trans(Bool, ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), sl, 0, 0), ST.seg(SC.update(U32, 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, 2n), K.kword(key)), sl, 0, 0), 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), 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, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key))), SC.update(U32, 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, 2n), K.kword(key)), s4), DL.seg_fs(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(L 272 273 ok = ic_l(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, s, su, hsv, hs0, hsn, fl2, free2, fr2u, hfree, hfll, hfl, hfnd, hcnt, hsfl, hsfr, hfrle, hfr2, Mf, pf5, hsm, v, t, lo, hi, mB, pm2, ew, x, y, eb, LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), 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, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key)))}, su), LT.link_tail_ok(~V, one, h1, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key)), sd, hsd, p4, cap, U32.inc(n), free2, mB, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su)), AR.upd(String, sd, ksT, UD.v(su), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v}), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), head, tail, su, s, sl, hsv, hs0, hsn, hseg4, 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), 7 274 L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, z), LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), 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, AR.upd(U32, 3n+sd, lkT, UD.v(LR.tidx(su)), t), UD.v(LR.dlo_idx(su)), lo), UD.v(LR.dhi_idx(su)), hi), UD.v(LR.hidx(su)), K.kword(key)))}, su), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, Mf), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), su, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), Equal.sym(LR.LRU<&2, V>, LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, Mf), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), su, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.link_tail(&2, V, LR.F{cap, U32.inc(n), head, tail, free2, AR.thaw(U32, mB), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(su))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(su), PA.stored(key))), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), Some{v})), AR.thaw(U32, AR.upd(U32, 3 275 276 # THEOREM (add, the core of a new entry) 277 def ins_core(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +s: Nat, +su: U32, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hsn: {NL.memn(s, sl) == False{} : Bool}, +fl2: List<&2, Nat>, +free2: U32, +fr2u: U32, +hfree: {U32.is_eq(free2, LK.fst_or(fl2, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, lkT), fl2) == True{} : Bool}, +hfl: {ST.flok(~V, fl2, UD.v(fr2u), AR.slots(Maybe<&2, V>, eT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl2) == True{} : Bool}, +hcnt: {Nat.is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{s, Nil{}})), SC.length(Nat, fl2)), UD.v(fr2u)) == True{} : Bool}, +hsfl: {NL.memn(s, fl2) == False{} : Bool}, +hsfr: {Nat.is_lt(s, UD.v(fr2u)) == True{} : Bool}, +hfrle: {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(fr2u)) == True{} : Bool}, +hfr2: {Nat.is_le(UD.v(fr2u), SC.pow2(sd)) == True{} : Bool}, +Mf: AR.Tree, +pf5: {AR.perfect(U32, 5n, Mf) == True{} : Bool}, +hsm: {AR.slots(U32, Mf) == SC.update(U32, AR.slots(U32, mT), 0n, fr2u) : List<&2, U32>}, +v: V, +t: U32, +lo: U32, +hi: U32) -> 278 ic_b(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, s, su, hsv, hs0, hsn, fl2, free2, fr2u, hfree, hfll, hfl, hfnd, hcnt, hsfl, hsfr, hfrle, hfr2, Mf, pf5, hsm, v, t, lo, hi, BU.bump_ok(Mf, pf5, 0, 16n, {==}, {==}, {==}))