import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/math/hash.bend as HS
import ../../../src/containers/hash_table.bend as H
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 ./inv.bend as IV
import ./state.bend as ST
import ./size.bend as SZ
import ./speclem.bend as SL
import ./probe_all.bend as PA
import ./insm.bend as IM
import ./insu.bend as IU
import ./insert.bend as IS
import ./words.bend as WR
import ./rawins.bend as RI
import ./rehash.bend as RH
import ./grow.bend as GR
import ../../lib/nat_list.bend as NL
import ../../lib/words32.bend as W32

# Placing a new entry when the table must grow: the grown table holds
# copies of every old bucket, so it looks keys up as the old one did, and
# the new entry goes into the first empty bucket of its path there.


# ---- the specification's set respects equal lookups ----

def sle_c(~V: Data, +m1: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +e: {S.lookup(~V, m1, q) == S.lookup(~V, m2, q) : Maybe<&2, V>}, +c: Bool, +hc: {S.str_eq(key, q) == c : Bool}) -> {S.lookup(~V, S.set(~V, m1, key, x), q) == S.lookup(~V, S.set(~V, m2, key, x), q) : Maybe<&2, V>}:
  match c:
    case True{}:
      Equal.trans(Maybe<&2, V>, S.lookup(~V, S.set(~V, m1, key, x), q), Some{x}, S.lookup(~V, S.set(~V, m2, key, x), q), SL.lookup_set_same(~V, m1, key, x, q, hc), Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, m2, key, x), q), Some{x}, SL.lookup_set_same(~V, m2, key, x, q, hc)))
    case False{}:
      Equal.trans(Maybe<&2, V>, S.lookup(~V, S.set(~V, m1, key, x), q), S.lookup(~V, m1, q), S.lookup(~V, S.set(~V, m2, key, x), q), SL.lookup_set_other(~V, m1, key, x, q, hc), Equal.trans(Maybe<&2, V>, S.lookup(~V, m1, q), S.lookup(~V, m2, q), S.lookup(~V, S.set(~V, m2, key, x), q), e, Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, m2, key, x), q), S.lookup(~V, m2, q), SL.lookup_set_other(~V, m2, key, x, q, hc))))

def ssz_c(~V: Data, +m1: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +hs: {S.size(~V, m1) == S.size(~V, m2) : Nat}, +mv: Maybe<&2, V>, +h1: {S.lookup(~V, m1, key) == mv : Maybe<&2, V>}, +h2: {S.lookup(~V, m2, key) == mv : Maybe<&2, V>}) -> {S.size(~V, S.set(~V, m1, key, x)) == S.size(~V, S.set(~V, m2, key, x)) : Nat}:
  match mv:
    case None{}:
      Equal.trans(Nat, S.size(~V, S.set(~V, m1, key, x)), 1n+S.size(~V, m1), S.size(~V, S.set(~V, m2, key, x)), SL.size_set_new(~V, m1, key, x, h1), Equal.trans(Nat, 1n+S.size(~V, m1), 1n+S.size(~V, m2), S.size(~V, S.set(~V, m2, key, x)), Equal.cong(Nat, Nat, z => 1n+z, S.size(~V, m1), S.size(~V, m2), hs), Equal.sym(Nat, S.size(~V, S.set(~V, m2, key, x)), 1n+S.size(~V, m2), SL.size_set_new(~V, m2, key, x, h2))))
    case Some{+v}:
      Equal.trans(Nat, S.size(~V, S.set(~V, m1, key, x)), S.size(~V, m1), S.size(~V, S.set(~V, m2, key, x)), SL.size_set_old(~V, m1, key, x, v, h1), Equal.trans(Nat, S.size(~V, m1), S.size(~V, m2), S.size(~V, S.set(~V, m2, key, x)), hs, Equal.sym(Nat, S.size(~V, S.set(~V, m2, key, x)), S.size(~V, m2), SL.size_set_old(~V, m2, key, x, v, h2))))

# THEOREM: an update refining set on one model refines it on any model with
# the same lookups and size
def setm_tr(~V: Data, +m1: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, heq: @+q: String -> {S.lookup(~V, m1, q) == S.lookup(~V, m2, q) : Maybe<&2, V>}, +hk: {S.lookup(~V, m1, key) == S.lookup(~V, m2, key) : Maybe<&2, V>}, +hs: {S.size(~V, m1) == S.size(~V, m2) : Nat}, -r: H.HashMap<&2, V>, sm: IS.SetM(~V, m1, key, x, r)) -> IS.SetM(~V, m2, key, x, r):
  match sm:
    case Tuple{+sh2, Tuple{er, Tuple{hg, Tuple{hlk, hsz}}}}:
      (sh2, (er, (hg, (q => Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.model(~V, sh2), q), S.lookup(~V, S.set(~V, m1, key, x), q), S.lookup(~V, S.set(~V, m2, key, x), q), hlk(q), sle_c(~V, m1, m2, key, x, q, heq(q), S.str_eq(key, q), {==})), Equal.trans(Nat, S.size(~V, ST.model(~V, sh2)), S.size(~V, S.set(~V, m1, key, x)), S.size(~V, S.set(~V, m2, key, x)), hsz, ssz_c(~V, m1, m2, key, x, hs, S.lookup(~V, m1, key), {==}, Equal.sym(Maybe<&2, V>, S.lookup(~V, m1, key), S.lookup(~V, m2, key), hk)))))))

def plt_c(+a: Nat, +b: Nat, +h: {Nat.is_lt(SC.pow2(a), SC.pow2(b)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {c == True{} : Bool}:
  match c:
    case True{}:
      {==}
    case False{}:
      Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(SC.pow2(b), SC.pow2(a)), False{}, Equal.sym(Bool, Nat.is_le(SC.pow2(b), SC.pow2(a)), True{}, N.pow2_mono(b, a, N.not_lt_le(a, b, hc))), N.lt_not_le(SC.pow2(a), SC.pow2(b), h))))

def pow2_lt_inv(+a: Nat, +b: Nat, +h: {Nat.is_lt(SC.pow2(a), SC.pow2(b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
  plt_c(a, b, h, Nat.is_lt(a, b), {==})

# ---- facts carried to the grown table ----

def lng_c(+c: Cmp, +h: {Cmp.is_le(c) == True{} : Bool}) -> {Cmp.is_gt(c) == False{} : Bool}:
  match c:
    case LT{}:
      {==}
    case EQ{}:
      {==}
    case GT{}:
      Empty.absurd({Cmp.is_gt(GT{}) == False{} : Bool}, L.false_true(h))

def le_not_gt(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_gt(a, b) == False{} : Bool}:
  lng_c(Nat.cmp(a, b), h)


def fl_from(+nbs: List<&2, B.Bk>, +obs: List<&2, B.Bk>, +j: Nat, +n2: Nat, +hf: {B.all_lt(B.PFrom{nbs, obs, j}, n2) == True{} : Bool}, +nxl: List<&2, U32>, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>, +h: {ST.fl_ok(obs, j, nxl, cnt, f, fr, seen) == True{} : Bool}) -> {ST.fl_ok(nbs, n2, nxl, cnt, f, fr, seen) == True{} : Bool}:
  match cnt:
    case 0n:
      h
    case 1n+p:
      +x1 = Bool.not(U32.is_eq(f, 0))
      +y = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(obs, UD.v(H.slot(f)), j), Bool.not(NL.memn(UD.v(H.slot(f)), seen))))
      +tl = ST.fl_ok(obs, j, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})
      +z = Bool.and(ST.noslot(obs, UD.v(H.slot(f)), j), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))
      +a2 = L.and_left(y, tl, L.and_right(x1, Bool.and(y, tl), h))
      +a5 = L.and_right(y, tl, L.and_right(x1, Bool.and(y, tl), h))
      +ns = L.and_left(ST.noslot(obs, UD.v(H.slot(f)), j), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
      +nm = L.and_right(ST.noslot(obs, UD.v(H.slot(f)), j), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
      +y2 = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(nbs, UD.v(H.slot(f)), n2), Bool.not(NL.memn(UD.v(H.slot(f)), seen))))
      +tl2 = ST.fl_ok(nbs, n2, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})
      L.and_intro(x1, Bool.and(y2, tl2), L.and_left(x1, Bool.and(y, tl), h), L.and_intro(y2, tl2, L.and_intro(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(nbs, UD.v(H.slot(f)), n2), Bool.not(NL.memn(UD.v(H.slot(f)), seen))), L.and_left(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2), L.and_intro(ST.noslot(nbs, UD.v(H.slot(f)), n2), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), RH.ns_from(nbs, obs, j, n2, hf, UD.v(H.slot(f)), ns, n2, N.le_refl(n2)), nm)), fl_from(nbs, obs, j, n2, hf, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}, a5)))

# with 2(n + 1) <= 2^cap and cap <= 30, growth stays below 2^31 buckets
def k30(~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}, +hsdk1: {Nat.is_le(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}, +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}, +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}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +hovi: {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))) == True{} : Bool}) -> {Nat.is_lt(1n+k, 31n) == True{} : Bool}:
  +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))), True{}, 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)
  +lt = N.not_le_lt(Nat.double(1n+UD.v(n)), SC.pow2(k), IU.gt_true_nle(Nat.double(1n+UD.v(n)), SC.pow2(k), hov))
  N.lt_le_trans(k, cap, 30n, pow2_lt_inv(k, cap, N.lt_le_trans(SC.pow2(k), Nat.double(1n+UD.v(n)), SC.pow2(cap), lt, hcap)), hc30)


def ig_2(~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}, +hsdk1: {Nat.is_le(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}, +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}, +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))) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +NT: AR.Tree<U32>, +eg: {H.grow_tab(CY.msk(k), td, AR.thaw(U32, tabT)) == AR.thaw(U32, NT) : Array<U32>}, +hr: {GR.rinv(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k)) == True{} : Bool}, fe: RI.FirstE(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k), UD.v(HS.bucket(K.kword(key), CY.msk(1n+k))))) -> IS.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))))):
  match fe:
    case Tuple{+e2, Tuple{+he2, Tuple{+hz2, hp0}}}:
      +hp2 = {hp0 : {B.occpath(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k), UD.v(HS.bucket(K.kword(key), CY.msk(1n+k))), M.dist(SC.pow2(1n+k), UD.v(HS.bucket(K.kword(key), CY.msk(1n+k))), e2)) == True{} : Bool}}
      +r1 = GR.r_1(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr)
      +r5 = N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), GR.r_5(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr))
      +r6 = GR.r_6(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr)
      +hlv = RH.live_from(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), r6, ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fr), hl, SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k)))
      +hns2 = RH.ns_from(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), r6, UD.v(s), hns, SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k)))
      +hno2 = RH.pno_from(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), r6, key, IM.nohb_pno(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key, SC.pow2(k), hno, SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k)))
      +hfl2 = fl_from(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), r6, AR.slots(U32, nxT), Nat.sub(UD.v(fr), 1n+UD.v(n)), free, UD.v(fr), Con{UD.v(s), Nil{}}, hfl)
      +ecn = Equal.trans(Nat, UD.v(n), 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, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+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), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), r5))
      +hld2 = N.le_trans(Nat.double(UD.v(n)), SC.pow2(k), SC.pow2(1n+k), hld, N.lt_le(SC.pow2(k), SC.pow2(1n+k), N.pow2_lt_succ(k)))
      +vtd = N.eq_from_is_eq(UD.v(td), 1n+k, htd)
      +htd5 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(5n)) == True{} : Bool}, 1n+k, UD.v(td), Equal.sym(Nat, UD.v(td), 1n+k, vtd), N.lt_trans(1n+k, 31n, 32n, hk30, {==}))
      +etd = Equal.trans(Nat, UD.v(U32.inc(td)), 1n+UD.v(td), 2n+k, W32.inc_val(one, h1, td, W32.bound32(one, h1, UD.v(td), 5n, {==}, htd5)), Equal.cong(Nat, Nat, z => 1n+z, UD.v(td), 1n+k, vtd))
      +ov2 = IU.over_val(one, h1, 1n+k, hk30, {==}, n, hld2)
      +le2 = N.double_le(1n+UD.v(n), SC.pow2(k), IU.over_c(one, h1, k, hk31, hk0, UD.v(n), hld))
      +hovi2 = Equal.trans(Bool, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k))), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(1n+k)), False{}, ov2, le_not_gt(Nat.double(1n+UD.v(n)), SC.pow2(1n+k), le2))
      res = IS.ins_nogrow(~V, one, h1, n, 1n+k, U32.inc(td), fr, sz, sd, sdU, free, NT, ksT, vsT, nxT, s, e2, key, x, hk30, {==}, hsd, N.le_lt_succ(sd, k, hsdk1), r1, pk, pv, pn, IS.eq_is_eq(UD.v(U32.inc(td)), 2n+k, etd), hsz, hsdu, GR.r_3(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), GR.r_2(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), GR.r_4(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), IS.eq_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), ecn), hld2, hlv, hfr, hnf, hfl2, hs, hns2, he2, hz2, hp2, hno2, hovi2)
      +ea = 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))), True{}, hovi)
      +eb = Equal.cong(U32, H.HashMap<&2, V>, mm => H.ins_fin(&2, V, n, mm, U32.inc(td), fr, sz, sdU, free, H.ins_raw(H.grow_tab(CY.msk(k), td, AR.thaw(U32, tabT)), mm, K.kword(key), H.link(s)), AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), U32.inc(U32.shl(CY.msk(k))), CY.msk(1n+k), GR.msk_up(one, h1, k, hk31))
      +ec = Equal.cong(Array<U32>, H.HashMap<&2, V>, t => H.ins_fin(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, H.ins_raw(t, CY.msk(1n+k), K.kword(key), H.link(s)), AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), H.grow_tab(CY.msk(k), td, AR.thaw(U32, tabT)), AR.thaw(U32, NT), eg)
      +ed = Equal.cong(Array<U32>, H.HashMap<&2, V>, tt => H.ins_fin(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, tt, AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), K.kword(key), H.link(s)), H.put_bucket(AR.thaw(U32, NT), U32.from_nat(e2), K.kword(key), H.link(s)), RI.raw_ok(one, h1, 1n+k, hk30, NT, r1, AR.slots(String, ksT), K.kword(key), H.link(s), e2, he2, hz2, hp2))
      +ef = Equal.sym(H.HashMap<&2, V>, H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k)))), H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, False{}), Equal.cong(Bool, H.HashMap<&2, V>, b => H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, b), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k))), False{}, hovi2))
      +eq = 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, True{}), H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k)))), ea, Equal.trans(H.HashMap<&2, V>, H.ins_fin(&2, V, n, U32.inc(U32.shl(CY.msk(k))), U32.inc(td), fr, sz, sdU, free, H.ins_raw(H.grow_tab(CY.msk(k), td, AR.thaw(U32, tabT)), U32.inc(U32.shl(CY.msk(k))), K.kword(key), H.link(s)), AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), H.ins_fin(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, H.ins_raw(H.grow_tab(CY.msk(k), td, AR.thaw(U32, tabT)), CY.msk(1n+k), K.kword(key), H.link(s)), AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k)))), eb, Equal.trans(H.HashMap<&2, V>, H.ins_fin(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, H.ins_raw(H.grow_tab(CY.msk(k), td, AR.thaw(U32, tabT)), CY.msk(1n+k), K.kword(key), H.link(s)), AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), H.ins_fin(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), K.kword(key), H.link(s)), AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k)))), ec, Equal.trans(H.HashMap<&2, V>, H.ins_fin(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), K.kword(key), H.link(s)), AR.thaw(U32, nxT), H.store(&2, V, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), s, PA.stored(key), x)), H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, False{}), H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k)))), ed, ef))))
      r2 = L.subst(H.HashMap<&2, V>, r => IS.SetM(~V, ST.absm(~V, TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(1n+k), 0n), key, x, r), H.ins_slot(&2, V, n, CY.msk(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+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, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), Equal.sym(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(1n+k), U32.inc(td), fr, sz, sdU, free, AR.thaw(U32, NT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), s, U32.from_nat(e2), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(1n+k)))), eq), res)
      +hsz = Equal.trans(Nat, S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(1n+k), 0n)), IV.occn(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), S.size(~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)), SZ.size_absm(~V, TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fr), SC.pow2(1n+k), hlv, SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))), Equal.trans(Nat, IV.occn(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), S.size(~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)), r5, Equal.sym(Nat, S.size(~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)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), SZ.size_absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fr), SC.pow2(k), hl, SC.pow2(k), N.le_refl(SC.pow2(k))))))
      setm_tr(~V, ST.absm(~V, TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(1n+k), 0n), 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 => RH.lookup_copy(~V, TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), r6, GR.r_7(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), GR.r_4(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), huq, AR.slots(Maybe<&2, V>, vsT), q), RH.lookup_copy(~V, TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), r6, GR.r_7(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), GR.r_4(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), huq, AR.slots(Maybe<&2, V>, vsT), key), hsz, 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)))), r2)

def ig_1(~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}, +hsdk1: {Nat.is_le(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}, +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}, +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))) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, gg: GR.GrowOK(tabT, AR.slots(String, ksT), k, sd, td)) -> IS.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))))):
  match gg:
    case Tuple{+NT, Tuple{+eg, +hr}}:
      +r5 = N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), GR.r_5(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr))
      +ob = L.subst(Nat, z => {Nat.is_le(Nat.double(z), SC.pow2(k)) == True{} : Bool}, 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), hld)
      +hem = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 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, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), r5), N.le_lt_trans(IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), N.le_trans(IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), Nat.double(IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))), SC.pow2(k), N.double_self_le(IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))), ob), N.pow2_lt_succ(k)))
      +pno = RH.pno_from(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), GR.r_6(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), key, IM.nohb_pno(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key, SC.pow2(k), hno, SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k)))
      ig_2(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk1, pt, pk, pv, pn, htd, hsz, hsdu, hwell, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, hno, hovi, hk30, NT, eg, hr, RI.find_e(TB.buckets(AR.slots(U32, NT), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k), N.succ_le_lt(0n, SC.pow2(1n+k), N.pow2_pos(1n+k)), CY.msk(1n+k), key, UD.v(HS.bucket(K.kword(key), CY.msk(1n+k))), PA.home_lt(K.kword(key), 1n+k), GR.r_2(tabT, AR.slots(String, ksT), k, sd, NT, SC.pow2(k), hr), pno, hem))

# THEOREM: placing a new entry into a table that must grow refines set
def ins_grow(~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}, +hsdk1: {Nat.is_le(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}, +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}, +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}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +hovi: {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))) == True{} : Bool}) -> IS.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))))):
  +hk30 = k30(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk1, pt, pk, pv, pn, htd, hsz, hsdu, hwell, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, hno, cap, hc30, hcap, hovi)
  +ob = L.subst(Nat, z => {Nat.is_le(Nat.double(z), SC.pow2(k)) == True{} : Bool}, 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), hld)
  ig_1(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk1, pt, pk, pv, pn, htd, hsz, hsdu, hwell, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, hno, hovi, hk30, GR.grow_ok(one, h1, k, hk31, hk30, hk0, tabT, pt, AR.slots(String, ksT), sd, AR.slots_length(String, sd, ksT, pk), hwell, huq, ob, td, N.eq_from_is_eq(UD.v(td), 1n+k, htd)))

# ---- either way ----


def ia_c(~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}, +hsdk1: {Nat.is_le(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}, +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}, +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}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +hsdk2: {Bool.or(Nat.is_lt(sd, k), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(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}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}, +c: Bool, +hc: {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))) == c : Bool}) -> IS.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))))):
  match c:
    case False{}:
      +h2 = L.subst(Bool, b => {Bool.or(Nat.is_lt(sd, k), b) == True{} : Bool}, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), False{}, hc, hsdk2)
      +hsdk = Equal.trans(Bool, Nat.is_lt(sd, k), Bool.or(Nat.is_lt(sd, k), False{}), True{}, Equal.sym(Bool, Bool.or(Nat.is_lt(sd, k), False{}), Nat.is_lt(sd, k), WR.or_false(Nat.is_lt(sd, k))), h2)
      IS.ins_nogrow(~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, hc)
    case True{}:
      ins_grow(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk1, pt, pk, pv, pn, htd, hsz, hsdu, hwell, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, hno, cap, hc30, hcap, hc)

# THEOREM: placing a new entry, whether or not the table grows, refines set
def ins_any(~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}, +hsdk1: {Nat.is_le(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}, +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}, +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}, +hcl: {B.cluster(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +hsdk2: {Bool.or(Nat.is_lt(sd, k), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(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}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}) -> IS.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))))):
  ia_c(~V, one, h1, n, k, td, fr, sz, sd, sdU, free, tabT, ksT, vsT, nxT, s, e, key, x, hk31, hk0, hsd, hsdk1, pt, pk, pv, pn, htd, hsz, hsdu, hwell, huq, hcn, hld, hl, hfr, hnf, hfl, hs, hns, hno, hcl, hsdk2, he, hz, hp, cap, hc30, hcap, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), {==})