import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/word.bend as WD
import ../../lib/u32div.bend as UD
import ../../../src/math/hash.bend as HS
import ../../../src/containers/hash_table.bend as H
import ./words.bend as WR
import ./strings.bend as STR
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./modn.bend as M
import ./cyc.bend as CY
import ./arr.bend as AX
import ./inv.bend as IV
import ./state.bend as ST
import ./probe_all.bend as PA
import ./insm.bend as IM
import ./insa.bend as IA
import ./insu.bend as IU
import ./insf.bend as IF
import ../../lib/words32.bend as W32
import ../../lib/links.bend as LK

# Placing a new entry: once its slot s is chosen and its bucket e is the
# empty bucket that ended its probe, and the table does not grow, the
# implementation's arrays are the shadow's with bucket e and slot s written,
# the invariant holds, and the model is the specification's set.


def eq_is_eq(+a: Nat, +b: Nat, +h: {a == b : Nat}) -> {Nat.is_eq(a, b) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_eq(a, z) == True{} : Bool}, a, b, h, N.is_eq_refl(a))

def kwnz_c(+c: U32, +t: String, +sh: Bool) -> {U32.is_eq(K.kw_c(c, t, sh), 0) == False{} : Bool}:
  match sh:
    case True{}:
      WR.short_nonzero(c)
    case False{}:
      WR.long_nonzero(STR.fold(SCon{Chr{c}, t}, 0))

# a key's word is never 0
def kword_nz(+key: String) -> {U32.is_eq(K.kword(key), 0) == False{} : Bool}:
  match key:
    case SNil{}:
      WR.long_nonzero(STR.fold(SNil{}, 0))
    case SCon{Chr{+c}, +t}:
      kwnz_c(c, t, K.short_c(c, t))

# ---- bounds ----

def s_sd(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}:
  N.lt_le_trans(UD.v(s), UD.v(fr), SC.pow2(sd), hs, N.le_trans(UD.v(fr), UD.v(sz), SC.pow2(sd), hfr, N.eq_le(UD.v(sz), SC.pow2(sd), N.eq_from_is_eq(UD.v(sz), SC.pow2(sd), hsz))))

def s32(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(1n+UD.v(s), WD.sc(32n, one)) == True{} : Bool}:
  W32.bound32(one, h1, UD.v(s), sd, N.lt_trans(sd, k, 31n, hsdk, hk31), s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))

# slot(link(s)) = s
def sl_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {UD.v(H.slot(H.link(s))) == UD.v(s) : Nat}:
  LK.slot_link(one, h1, s, s32(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))

def ev(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {UD.v(U32.from_nat(e)) == e : Nat}:
  U.to_nat_from_nat(e, k, N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==})), he)

def ix_h(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(1n+Nat.double(UD.v(U32.from_nat(e))), SC.pow2(1n+k)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+k)) == True{} : Bool}, e, UD.v(U32.from_nat(e)), Equal.sym(Nat, UD.v(U32.from_nat(e)), e, ev(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), N.double_lt_bit(True{}, e, SC.pow2(k), he))

def ix1(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {UD.v(U32.shl(U32.from_nat(e))) == Nat.double(e) : Nat}:
  Equal.trans(Nat, UD.v(U32.shl(U32.from_nat(e))), Nat.double(UD.v(U32.from_nat(e))), Nat.double(e), AX.ix_w(U32.from_nat(e), 1n+k, hk31, ix_h(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(U32.from_nat(e)), e, ev(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)))

def ix2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {UD.v(U32.inc(U32.shl(U32.from_nat(e)))) == 1n+Nat.double(e) : Nat}:
  Equal.trans(Nat, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), 1n+Nat.double(UD.v(U32.from_nat(e))), 1n+Nat.double(e), AX.ix_l(U32.from_nat(e), 1n+k, hk31, ix_h(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), UD.v(U32.from_nat(e)), e, ev(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)))

def hi1(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(UD.v(U32.shl(U32.from_nat(e))), SC.pow2(1n+k)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(e), UD.v(U32.shl(U32.from_nat(e))), Equal.sym(Nat, UD.v(U32.shl(U32.from_nat(e))), Nat.double(e), ix1(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), N.lt_trans(Nat.double(e), 1n+Nat.double(e), SC.pow2(1n+k), N.lt_succ(Nat.double(e)), N.double_lt_bit(True{}, e, SC.pow2(k), he)))

def hi2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(UD.v(U32.inc(U32.shl(U32.from_nat(e)))), SC.pow2(1n+k)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(e), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), 1n+Nat.double(e), ix2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), N.double_lt_bit(True{}, e, SC.pow2(k), he))

def len_lt(-T: Data, +d: Nat, +t: AR.Tree<T>, +pf: {AR.perfect(T, d, t) == True{} : Bool}, +i: Nat, +h: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(i, SC.length(T, AR.slots(T, t))) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.pow2(d), SC.length(T, AR.slots(T, t)), Equal.sym(Nat, SC.length(T, AR.slots(T, t)), SC.pow2(d), AR.slots_length(T, d, t, pf)), h)

# ---- the implementation's arrays ----

def tab_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(s)) == 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(s))) : Array<U32>}:
  +p1 = AR.upd_perfect(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key), pt)
  +s1 = AR.set(U32, 1n+k, tabT, U32.shl(U32.from_nat(e)), K.kword(key), W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(U32.from_nat(e)))), hk31, hi1(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), W32.nth_some(AR.slots(U32, tabT), UD.v(U32.shl(U32.from_nat(e))), len_lt(U32, 1n+k, tabT, pt, UD.v(U32.shl(U32.from_nat(e))), hi1(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))), pt)
  +s2 = AR.set(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), U32.inc(U32.shl(U32.from_nat(e))), H.link(s), W32.nth0(AR.slots(U32, 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))))), hk31, hi2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), W32.nth_some(AR.slots(U32, 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)))), len_lt(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), p1, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), hi2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))), p1)
  Equal.trans(Array<U32>, H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(s)), Array.set(U32, AR.thaw(U32, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key))), U32.inc(U32.shl(U32.from_nat(e))), H.link(s)), 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(s))), Equal.cong(Array<U32>, Array<U32>, a => Array.set(U32, a, U32.inc(U32.shl(U32.from_nat(e))), H.link(s)), Array.set(U32, AR.thaw(U32, tabT), U32.shl(U32.from_nat(e)), K.kword(key)), AR.thaw(U32, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key))), s1), s2)

def ks_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Array.set(String, AR.thaw(String, ksT), s, PA.stored(key)) == AR.thaw(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))) : Array<String>}:
  AR.set(String, sd, ksT, s, PA.stored(key), TB.nths(AR.slots(String, ksT), UD.v(s)), hsd, s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), AX.nths_of(sd, ksT, UD.v(s), s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), pk), pk)

def vs_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}) == AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})) : Array<Maybe<&2, V>>}:
  AR.set(Maybe<&2, V>, sd, vsT, s, Some{x}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(s)), hsd, s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), ST.nthm_some(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(s), len_lt(Maybe<&2, V>, sd, vsT, pv, UD.v(s), s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))), pv)

# THEOREM: without growth, placing the entry builds the shadow's real map
def real_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {H.ins_slot(&2, V, n, CY.msk(k), td, fr, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e), K.kword(key), PA.stored(key), x, False{}) == ST.real(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT}) : H.HashMap<&2, V>}:
  Equal.trans(H.HashMap<&2, V>, H.HM{U32.inc(n), CY.msk(k), td, fr, sz, sdU, free, H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(s)), Array.set(String, AR.thaw(String, ksT), s, PA.stored(key)), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}), AR.thaw(U32, nxT)}, H.HM{U32.inc(n), CY.msk(k), td, fr, sz, sdU, free, 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(s))), Array.set(String, AR.thaw(String, ksT), s, PA.stored(key)), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}), AR.thaw(U32, nxT)}, ST.real(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT}),
    Equal.cong(Array<U32>, H.HashMap<&2, V>, a => H.HM{U32.inc(n), CY.msk(k), td, fr, sz, sdU, free, a, Array.set(String, AR.thaw(String, ksT), s, PA.stored(key)), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}), AR.thaw(U32, nxT)}, H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(s)), 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(s))), tab_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)),
    Equal.trans(H.HashMap<&2, V>, H.HM{U32.inc(n), CY.msk(k), td, fr, sz, sdU, free, 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(s))), Array.set(String, AR.thaw(String, ksT), s, PA.stored(key)), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}), AR.thaw(U32, nxT)}, H.HM{U32.inc(n), CY.msk(k), td, fr, sz, sdU, free, 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(s))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}), AR.thaw(U32, nxT)}, ST.real(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT}),
      Equal.cong(Array<String>, H.HashMap<&2, V>, a => H.HM{U32.inc(n), CY.msk(k), td, fr, sz, sdU, free, 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(s))), a, Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}), AR.thaw(U32, nxT)}, Array.set(String, AR.thaw(String, ksT), s, PA.stored(key)), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), ks_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)),
      Equal.cong(Array<Maybe<&2, V>>, H.HashMap<&2, V>, a => H.HM{U32.inc(n), CY.msk(k), td, fr, sz, sdU, free, 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(s))), AR.thaw(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), a, AR.thaw(U32, nxT)}, Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), s, Some{x}), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), vs_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))))

# ---- the shadow's slot lists ----


def tab_slots(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {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(s))) == SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(s)) : List<&2, U32>}:
  +p1 = AR.upd_perfect(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key), pt)
  +e1 = AR.upd_slots(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(s), hi2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), p1)
  +e2 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(s)), AR.slots(U32, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key))), SC.update(U32, AR.slots(U32, tabT), UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), AR.upd_slots(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key), hi1(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), pt))
  +e3 = Equal.cong(Nat, List<&2, U32>, z => SC.update(U32, SC.update(U32, AR.slots(U32, tabT), z, K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(s)), UD.v(U32.shl(U32.from_nat(e))), Nat.double(e), ix1(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  +e4 = Equal.cong(Nat, List<&2, U32>, z => SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), z, H.link(s)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), 1n+Nat.double(e), ix2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  Equal.trans(List<&2, U32>, 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(s))), SC.update(U32, AR.slots(U32, 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(s)), SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(s)), e1, Equal.trans(List<&2, U32>, SC.update(U32, AR.slots(U32, 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(s)), SC.update(U32, SC.update(U32, AR.slots(U32, tabT), UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(s)), SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(s)), e2, Equal.trans(List<&2, U32>, SC.update(U32, SC.update(U32, AR.slots(U32, tabT), UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(s)), SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(s)), SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(s)), e3, e4)))

def ks_slots(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))) == SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(s))), PA.stored(key)) : List<&2, String>}:
  Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), SC.update(String, AR.slots(String, ksT), UD.v(s), PA.stored(key)), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(s))), PA.stored(key)), AR.upd_slots(String, sd, ksT, UD.v(s), PA.stored(key), s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), pk), Equal.cong(Nat, List<&2, String>, z => SC.update(String, AR.slots(String, ksT), z, PA.stored(key)), UD.v(s), UD.v(H.slot(H.link(s))), Equal.sym(Nat, UD.v(H.slot(H.link(s))), UD.v(s), sl_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))))

def vs_slots(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})) == SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}) : List<&2, Maybe<&2, V>>}:
  Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(s), Some{x}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}), AR.upd_slots(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}, s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), pv), Equal.cong(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), z, Some{x}), UD.v(s), UD.v(H.slot(H.link(s))), Equal.sym(Nat, UD.v(H.slot(H.link(s))), UD.v(s), sl_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))))

def sl_sd(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(UD.v(H.slot(H.link(s))), SC.pow2(sd)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, UD.v(s), UD.v(H.slot(H.link(s))), Equal.sym(Nat, UD.v(H.slot(H.link(s))), UD.v(s), sl_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), s_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))

def ns2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(H.link(s))), SC.pow2(k)) == True{} : Bool}:
  L.subst(Nat, z => {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), z, SC.pow2(k)) == True{} : Bool}, UD.v(s), UD.v(H.slot(H.link(s))), Equal.sym(Nat, UD.v(H.slot(H.link(s))), UD.v(s), sl_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), hns)

# THEOREM: the new shadow's buckets are the old ones with bucket e filled
def bs2_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}) : List<&2, B.Bk>}:
  +htb = len_lt(U32, 1n+k, tabT, pt, 1n+Nat.double(e), N.double_lt_bit(True{}, e, SC.pow2(k), he))
  +hkl = len_lt(String, sd, ksT, pk, UD.v(H.slot(H.link(s))), sl_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  +bp = IA.buckets_put(AR.slots(U32, tabT), AR.slots(String, ksT), e, K.kword(key), H.link(s), PA.stored(key), SC.pow2(k), ns2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), kword_nz(key), htb, hkl)
  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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s)), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(s))), 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(s), key}),
    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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s)), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(s))), PA.stored(key)), SC.pow2(k)), Equal.cong(List<&2, U32>, List<&2, B.Bk>, z => TB.buckets(z, AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), SC.update(U32, SC.update(U32, AR.slots(U32, tabT), Nat.double(e), K.kword(key)), 1n+Nat.double(e), H.link(s)), tab_slots(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), 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(s)), z, SC.pow2(k)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(s))), PA.stored(key)), ks_slots(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))),
    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(s)), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(H.link(s))), 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(s), 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(s), key}), bp, 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(s), z}), TB.keyof(K.kword(key), PA.stored(key)), key, IA.keyof_stored(key))))

def he_len(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(e, SC.length(B.Bk, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)))) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(e, z) == True{} : Bool}, SC.pow2(k), SC.length(B.Bk, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))), Equal.sym(Nat, SC.length(B.Bk, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))), SC.pow2(k), IA.len_dlist(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), 0n)), he)

def hs_len(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(UD.v(H.slot(H.link(s))), SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT))) == True{} : Bool}:
  len_lt(Maybe<&2, V>, sd, vsT, pv, UD.v(H.slot(H.link(s))), sl_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))

def sl_fr(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {Nat.is_lt(UD.v(H.slot(H.link(s))), UD.v(fr)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(z, UD.v(fr)) == True{} : Bool}, UD.v(s), UD.v(H.slot(H.link(s))), Equal.sym(Nat, UD.v(H.slot(H.link(s))), UD.v(s), sl_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), hs)


# ---- the invariant after placing ----


def g_well(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {ST.cwell(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  +hwb = L.and_intro(Nat.is_lt(UD.v(H.slot(H.link(s))), SC.pow2(sd)), Bool.and(U32.is_eq(K.kword(key), K.kword(key)), Bool.not(U32.is_eq(H.link(s), 0))), sl_sd(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), L.and_intro(U32.is_eq(K.kword(key), K.kword(key)), Bool.not(U32.is_eq(H.link(s), 0)), U.u32_eq_refl(K.kword(key)), IM.not_f(U32.is_eq(H.link(s), 0), W32.link_nz(one, h1, s, s32(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)))))
  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(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), IM.well_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), sd, hwb, SC.pow2(k), hwell, SC.pow2(k), N.le_refl(SC.pow2(k))))

def g_clus(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {ST.cclus(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  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(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), IM.clus_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}, {==}, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), SC.pow2(k), CY.msk(k), hp, hcl))

def g_uniq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {ST.cuniq(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  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(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), IM.uq_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), K.kword(key), H.link(s), key, SC.pow2(k), he, huq, hno, ns2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)))

def g_n(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {ST.cn(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  +ea = IU.inc_n(one, h1, k, hk31, hk0, n, hld)
  +eb = 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)), hcn))
  +ec = 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(s), key}), SC.pow2(k)), 1n+IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IM.occn_up(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}, {==}, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), hz, SC.pow2(k), he))
  +ed = Equal.cong(List<&2, B.Bk>, Nat, z => IV.occn(z, 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(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)))
  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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), SC.pow2(k)), SC.pow2(k)), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), SC.pow2(k)), SC.pow2(k)), eb, 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(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), SC.pow2(k)), SC.pow2(k)), ec, ed))))

def g_load(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}, +hov: {Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)) == False{} : Bool}) -> {ST.cload(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  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), IU.inc_n(one, h1, k, hk31, hk0, n, hld)), IU.gt_false_le(Nat.double(1n+UD.v(n)), SC.pow2(k), hov))

def g_live(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {ST.clive(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  +l1 = IM.live_up(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), K.kword(key), H.link(s), key, AR.slots(Maybe<&2, V>, vsT), x, hs_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), UD.v(fr), UD.v(fr), N.le_refl(UD.v(fr)), sl_fr(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), SC.pow2(k), hl, SC.pow2(k), N.le_refl(SC.pow2(k)))
  +l2 = L.subst(List<&2, Maybe<&2, V>>, z => {B.all_lt(B.PLive{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), ST.lvs(~V, z), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}), vs_slots(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), l1)
  L.subst(List<&2, B.Bk>, z =>  {B.all_lt(B.PLive{z, ST.lvs(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}))), UD.v(fr)}, 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(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), l2)

def g_free(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {ST.cfree(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  +ea = IU.inc_n(one, h1, k, hk31, hk0, n, hld)
  +f1 = L.subst(Nat, z => {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{z, Nil{}}) == True{} : Bool}, UD.v(s), UD.v(H.slot(H.link(s))), Equal.sym(Nat, UD.v(H.slot(H.link(s))), UD.v(s), sl_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), hfl)
  +hm = L.subst(Bool, b => {Bool.or(b, False{}) == True{} : Bool}, True{}, Nat.is_eq(UD.v(H.slot(H.link(s))), UD.v(H.slot(H.link(s)))), Equal.sym(Bool, Nat.is_eq(UD.v(H.slot(H.link(s))), UD.v(H.slot(H.link(s)))), True{}, N.is_eq_refl(UD.v(H.slot(H.link(s))))), {==})
  +f2 = IF.fl_weak(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(H.slot(H.link(s))), Nil{}}, Nil{}, {==}, IF.fl_tr(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), K.kword(key), H.link(s), key, SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(H.slot(H.link(s))), Nil{}}, hm, f1))
  +f3 = L.subst(List<&2, B.Bk>, z =>  {ST.fl_ok(z, SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), 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(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)), f2)
  +f4 = L.subst(Nat, z => {ST.fl_ok(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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), z), free, UD.v(fr), Nil{}) == True{} : Bool}, 1n+UD.v(n), UD.v(U32.inc(n)), Equal.sym(Nat, UD.v(U32.inc(n)), 1n+UD.v(n), ea), f3)
  +le = L.subst(Nat, z => {Nat.is_le(z, UD.v(fr)) == True{} : Bool}, 1n+UD.v(n), UD.v(U32.inc(n)), Equal.sym(Nat, UD.v(U32.inc(n)), 1n+UD.v(n), ea), hnf)
  L.and_intro(Nat.is_le(UD.v(U32.inc(n)), UD.v(fr)), ST.fl_ok(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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), UD.v(U32.inc(n))), free, UD.v(fr), Nil{}), le, f4)

# THEOREM: the placed entry keeps the invariant
def good2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}, +hov: {Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)) == False{} : Bool}) -> {ST.goodF(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT) == True{} : Bool}:
  ST.good_intro(~V, U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.perfect(String, sd, AR.upd(String, sd, ksT, UD.v(s), PA.stored(key))), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT, L.and_intro(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), hk31, hk0), hsd, AR.upd_perfect(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(s), AR.upd_perfect(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key), pt)), AR.upd_perfect(String, sd, ksT, UD.v(s), PA.stored(key), pk), AR.upd_perfect(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}, pv), pn, htd, hsz, hsdu, g_well(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), g_clus(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), g_uniq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), g_n(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), g_load(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno, hov), g_live(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), hfr, g_free(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), hsdk)

# ---- the model after placing ----


def lk2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}, +q: String) -> {S.lookup(~V, ST.model(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT}), q) == S.lookup(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x), q) : Maybe<&2, V>}:
  +e1 = Equal.cong(List<&2, B.Bk>, Maybe<&2, V>, z => S.lookup(~V, ST.absm(~V, z, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.pow2(k), 0n), q), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  +e2 = Equal.cong(List<&2, Maybe<&2, V>>, Maybe<&2, V>, z => S.lookup(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), z, SC.pow2(k), 0n), q), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}), vs_slots(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.model(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT}), q), S.lookup(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.pow2(k), 0n), q), S.lookup(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x), q), e1, Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}), SC.pow2(k), 0n), q), S.lookup(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x), q), e2, IM.lookup_ins(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), K.kword(key), H.link(s), key, AR.slots(Maybe<&2, V>, vsT), x, SC.pow2(k), he, hs_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), hz, huq, hno, ns2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), q)))

def sz2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}) -> {S.size(~V, ST.model(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT})) == S.size(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x)) : Nat}:
  +e1 = Equal.cong(List<&2, B.Bk>, Nat, z => S.size(~V, ST.absm(~V, z, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.pow2(k), 0n)), 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(s))), AR.slots(String, AR.upd(String, sd, ksT, UD.v(s), 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(s), key}), bs2_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  +e2 = Equal.cong(List<&2, Maybe<&2, V>>, Nat, z => S.size(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), z, SC.pow2(k), 0n)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}), vs_slots(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  Equal.trans(Nat, S.size(~V, ST.model(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT})), S.size(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.pow2(k), 0n)), S.size(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x)), e1, Equal.trans(Nat, S.size(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x})), SC.pow2(k), 0n)), S.size(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, B.BF{K.kword(key), H.link(s), key}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(H.link(s))), Some{x}), SC.pow2(k), 0n)), S.size(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x)), e2, IM.size_ins(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e, he_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), K.kword(key), H.link(s), key, AR.slots(Maybe<&2, V>, vsT), x, SC.pow2(k), he, hs_len(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), hz, huq, hno, ns2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), UD.v(fr), UD.v(fr), N.le_refl(UD.v(fr)), sl_fr(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno), hl)))

# the result of an update: a good shadow whose model agrees with the
# specification's set on every lookup and on the size
def SetM(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, r: H.HashMap<&2, V>) -> Type:
  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : H.HashMap<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & ((@+q: String -> {S.lookup(~V, ST.model(~V, sh2), q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) & {S.size(~V, ST.model(~V, sh2)) == S.size(~V, S.set(~V, m, key, x)) : Nat}))>


# THEOREM: placing a new entry without growing the table refines set
def ins_nogrow(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fr: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +s: U32, +e: Nat, +key: String, +x: V, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hsdk: {Nat.is_lt(sd, k) == True{} : Bool}, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, V>, sd, vsT) == True{} : Bool}, +pn: {AR.perfect(U32, sd, nxT) == True{} : Bool}, +htd: {Nat.is_eq(UD.v(td), 1n+k) == True{} : Bool}, +hsz: {Nat.is_eq(UD.v(sz), SC.pow2(sd)) == True{} : Bool}, +hsdu: {Nat.is_eq(UD.v(sdU), sd) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hcn: {Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hl: {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr)}, SC.pow2(k)) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(sz)) == True{} : Bool}, +hnf: {Nat.is_le(1n+UD.v(n), UD.v(fr)) == True{} : Bool}, +hfl: {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), UD.v(fr)) == True{} : Bool}, +hns: {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(s), SC.pow2(k)) == True{} : Bool}, +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}, +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}, +hovi: {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))) == False{} : Bool}) -> SetM(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x, H.ins_slot(&2, V, n, CY.msk(k), td, fr, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))))):
  +hov = Equal.trans(Bool, Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), False{}, Equal.sym(Bool, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), IU.over_val(one, h1, k, hk31, hk0, n, hld)), hovi)
  +er = Equal.trans(H.HashMap<&2, V>, H.ins_slot(&2, V, n, CY.msk(k), td, fr, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_slot(&2, V, n, CY.msk(k), td, fr, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e), K.kword(key), PA.stored(key), x, False{}), ST.real(~V, ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT}), Equal.cong(Bool, H.HashMap<&2, V>, b => H.ins_slot(&2, V, n, CY.msk(k), td, fr, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e), K.kword(key), PA.stored(key), x, b), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), False{}, hovi), real_eq(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno))
  (ST.HS{U32.inc(n), k, td, fr, sz, sd, sdU, free, 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(s)), AR.upd(String, sd, ksT, UD.v(s), PA.stored(key)), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(s), Some{x}), nxT}, (er, (good2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno, hov), (q => lk2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno, q), sz2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk, pt, pk, pv, pn, htd, hsz, hsdu, hwell, hcl, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, he, hz, hp, hno)))))