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/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./strings.bend as STR
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./cyc.bend as CY
import ./arr.bend as AX
import ./state.bend as ST
import ./probe_all.bend as PA
import ./grow.bend as GR
import ./insa.bend as IA
import ./arena.bend as AN
import ../../lib/words32.bend as W32

# keys: the walk from the last bucket down lists every key in bucket order,
# which is the order of the model's entries.


# the key of a bucket, as a list
def kof(b: B.Bk) -> List<&2, String>:
  match b:
    case B.BE{}:
      Nil{}
    case B.BF{w, l, k}:
      Con{k, Nil{}}

# the keys of buckets j .. j + m - 1
def kb(+bs: List<&2, B.Bk>, +m: Nat, +j: Nat) -> List<&2, String>:
  match m:
    case 0n:
      Nil{}
    case 1n+p:
      SC.append(String, kof(B.at(bs, j)), kb(bs, p, 1n+j))

# ---- the model's keys ----

def keys_app(~V: Data, +a: List<&2, S.Entry<V>>, +b: List<&2, S.Entry<V>>) -> {S.keys(~V, SC.append(S.Entry<V>, a, b)) == SC.append(String, S.keys(~V, a), S.keys(~V, b)) : List<&2, String>}:
  match a:
    case Nil{}:
      {==}
    case Con{S.E{+j, +v}, +t}:
      Equal.cong(List<&2, String>, List<&2, String>, z => Con{j, z}, S.keys(~V, SC.append(S.Entry<V>, t, b)), SC.append(String, S.keys(~V, t), S.keys(~V, b)), keys_app(~V, t, b))

def ek_m(~V: Data, +k: String, +m: Maybe<&2, V>, +h: {ST.some_b(~V, m) == True{} : Bool}) -> {S.keys(~V, ST.ent_m(~V, k, m)) == Con{k, Nil{}} : List<&2, String>}:
  match m:
    case None{}:
      Empty.absurd({S.keys(~V, ST.ent_m(~V, k, None{})) == Con{k, Nil{}} : List<&2, String>}, L.false_true(h))
    case Some{v}:
      {==}

def ent_keys(~V: Data, +b: B.Bk, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +h: {B.live_b(ST.lvs(~V, vsl), fr, b) == True{} : Bool}) -> {S.keys(~V, ST.ent(~V, b, vsl)) == kof(b) : List<&2, String>}:
  match b:
    case B.BE{}:
      {==}
    case B.BF{w, +l, +k}:
      +t = UD.v(H.slot(l))
      +hs = Equal.trans(Bool, ST.some_b(~V, ST.nthm(~V, vsl, t)), B.nthb(ST.lvs(~V, vsl), t), True{}, Equal.sym(Bool, B.nthb(ST.lvs(~V, vsl), t), ST.some_b(~V, ST.nthm(~V, vsl, t)), ST.lvs_nth(~V, vsl, t)), L.and_left(B.nthb(ST.lvs(~V, vsl), t), Nat.is_lt(t, fr), h))
      ek_m(~V, k, ST.nthm(~V, vsl, t), hs)

# THEOREM: the model's keys are the buckets' keys in bucket order
def keys_absm(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +n: Nat, +hl: {B.all_lt(B.PLive{bs, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}) -> {S.keys(~V, ST.absm(~V, bs, vsl, m, j)) == kb(bs, m, j) : List<&2, String>}:
  match m:
    case 0n:
      {==}
    case 1n+p:
      +hj = IA.idx_lt(j, p, n, hjm)
      Equal.trans(List<&2, String>, S.keys(~V, ST.absm(~V, bs, vsl, 1n+p, j)), SC.append(String, S.keys(~V, ST.ent(~V, B.at(bs, j), vsl)), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), kb(bs, 1n+p, j), keys_app(~V, ST.ent(~V, B.at(bs, j), vsl), ST.absm(~V, bs, vsl, p, 1n+j)),
        Equal.trans(List<&2, String>, SC.append(String, S.keys(~V, ST.ent(~V, B.at(bs, j), vsl)), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), SC.append(String, kof(B.at(bs, j)), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), kb(bs, 1n+p, j), Equal.cong(List<&2, String>, List<&2, String>, z => SC.append(String, z, S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j))), S.keys(~V, ST.ent(~V, B.at(bs, j), vsl)), kof(B.at(bs, j)), ent_keys(~V, B.at(bs, j), vsl, fr, B.all_inst(B.PLive{bs, ST.lvs(~V, vsl), fr}, n, hl, j, hj))),
          Equal.cong(List<&2, String>, List<&2, String>, z => SC.append(String, kof(B.at(bs, j)), z), S.keys(~V, ST.absm(~V, bs, vsl, p, 1n+j)), kb(bs, p, 1n+j), keys_absm(~V, bs, vsl, fr, n, hl, p, 1n+j, IA.idx_next(j, p, n, hjm)))))

# ---- the walk ----


def WStep(+tabT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +q: Nat, +kk: U32, +KT: AR.Tree<String>) -> Type:
  Sigma<&1, &1, AR.Tree<String>, K2 => {H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}) == H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)} : H.Walk} & ({AR.slots(String, K2) == kl : List<&2, String>} & {AR.perfect(String, sd, K2) == True{} : Bool})>

def acc_eq(+bs: List<&2, B.Bk>, +n: Nat, +q: Nat, +hq: {Nat.is_lt(q, n) == True{} : Bool}) -> {kb(bs, Nat.sub(n, q), q) == SC.append(String, kof(B.at(bs, q)), kb(bs, Nat.sub(n, 1n+q), 1n+q)) : List<&2, String>}:
  +r = Nat.sub(n, 1n+q)
  +e1 = N.sub_add(n, 1n+q, N.lt_succ_le_succ(q, n, hq))
  +e2 = Equal.trans(Nat, Nat.add(q, 1n+r), 1n+Nat.add(q, r), n, N.add_succ(q, r), e1)
  +e3 = L.subst(Nat, z => {Nat.sub(z, q) == 1n+r : Nat}, Nat.add(q, 1n+r), n, e2, N.add_sub_cancel(q, 1n+r))
  Equal.cong(Nat, List<&2, String>, z => kb(bs, z, q), Nat.sub(n, q), 1n+r, e3)

def w_ew(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {UD.v(U32.shl(kk)) == Nat.double(q) : Nat}:
  +hh = L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+k)) == True{} : Bool}, q, UD.v(kk), Equal.sym(Nat, UD.v(kk), q, hkk), N.double_lt_bit(True{}, q, SC.pow2(k), hq))
  Equal.trans(Nat, UD.v(U32.shl(kk)), Nat.double(UD.v(kk)), Nat.double(q), AX.ix_w(kk, 1n+k, hk31, hh), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(kk), q, hkk))

def w_el(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {UD.v(U32.inc(U32.shl(kk))) == 1n+Nat.double(q) : Nat}:
  +hh = L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+k)) == True{} : Bool}, q, UD.v(kk), Equal.sym(Nat, UD.v(kk), q, hkk), N.double_lt_bit(True{}, q, SC.pow2(k), hq))
  Equal.trans(Nat, UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(UD.v(kk)), 1n+Nat.double(q), AX.ix_l(kk, 1n+k, hk31, hh), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), UD.v(kk), q, hkk))

def w_get(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)) == (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))) : Array<U32> & U32}:
  +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(q), UD.v(U32.shl(kk)), Equal.sym(Nat, UD.v(U32.shl(kk)), Nat.double(q), w_ew(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), N.lt_trans(Nat.double(q), 1n+Nat.double(q), SC.pow2(1n+k), N.lt_succ(Nat.double(q)), N.double_lt_bit(True{}, q, SC.pow2(k), hq)))
  Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(kk)))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), AX.getw(1n+k, tabT, U32.shl(kk), hk31, hi, pt), Equal.cong(Nat, Array<U32> & U32, z => (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), z)), UD.v(U32.shl(kk)), Nat.double(q), w_ew(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)))

def w_getl(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> {Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(kk))) == (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))) : Array<U32> & U32}:
  +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(q), UD.v(U32.inc(U32.shl(kk))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(q), w_el(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), N.double_lt_bit(True{}, q, SC.pow2(k), hq))
  Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(kk))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(kk))))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), AX.getw(1n+k, tabT, U32.inc(U32.shl(kk)), hk31, hi, pt), Equal.cong(Nat, Array<U32> & U32, z => (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), z)), UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(q), w_el(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)))

def w_at(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == c : Bool}) -> {B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q) == TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, c) : B.Bk}:
  Equal.trans(B.Bk, B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q), TB.dec(AR.slots(U32, tabT), kl, q), TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, c), TB.at_buckets(AR.slots(U32, tabT), kl, SC.pow2(k), q, hq), Equal.cong(Bool, B.Bk, z => TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, z), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), c, hc))

def w_accx(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +b: B.Bk, +hb: {B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q) == b : B.Bk}) -> {kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q) == SC.append(String, kof(b), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)) : List<&2, String>}:
  Equal.trans(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), SC.append(String, kof(B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q)), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), SC.append(String, kof(b), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), acc_eq(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), q, hq), Equal.cong(B.Bk, List<&2, String>, y => SC.append(String, kof(y), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q), b, hb))

def nth_upd_same(+xs: List<&2, String>, +i: Nat, +v: String, +h: {Nat.is_lt(i, SC.length(String, xs)) == True{} : Bool}) -> {SC.nth(String, SC.update(String, xs, i, v), i) == Some{v} : Maybe<&2, String>}:
  match xs i:
    case Nil{} _:
      Empty.absurd({SC.nth(String, SC.update(String, Nil{}, i, v), i) == Some{v} : Maybe<&2, String>}, N.lt_zero_absurd(i, h))
    case Con{x, t} 0n:
      {==}
    case Con{x, t} 1n+p:
      nth_upd_same(t, p, v, h)


def w_long(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool}, +hs: {H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))) == False{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
  +hb = w_at(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, False{}, hc)
  +hw = L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.at(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), q), TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{}), hb, B.all_inst(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k), hwell, q, hq))
  +hsp = L.and_left(Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SC.pow2(sd)), Bool.and(U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), K.kword(TB.keyof(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))))), Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), 0))), hw)
  +hx = L.subst(List<&2, String>, z => {SC.nth(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))) == Some{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))} : Maybe<&2, String>}, kl, AR.slots(String, KT), Equal.sym(List<&2, String>, AR.slots(String, KT), kl, hsl), TB.nths_some(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), AN.len_eq_lt(String, kl, sd, hlen, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), hsp)))
  +esw = AR.swap(String, sd, KT, H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), SNil{}, TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), hsd, hsp, hx, pk)
  +p1 = AR.upd_perfect(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, pk)
  +es1 = AR.upd_slots(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, hsp, pk)
  +hx1 = L.subst(List<&2, String>, z => {SC.nth(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))) == Some{SNil{}} : Maybe<&2, String>}, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), Equal.sym(List<&2, String>, AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), es1), nth_upd_same(AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, AN.len_eq_lt(String, AR.slots(String, KT), sd, AR.slots_length(String, sd, KT, pk), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), hsp)))
  +est = AR.set(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), SNil{}, hsd, hsp, hx1, p1)
  +ek = Equal.cong(Bool, String, b => TB.keyof_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), b), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), False{}, hs)
  +eacc = Equal.trans(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), SC.append(String, kof(TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{})), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, w_accx(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{}), hb), Equal.cong(String, List<&2, String>, z => Con{z, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, TB.keyof(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), ek))
  +xeq = Equal.cong(List<&2, String>, String, z => TB.nths(z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), AR.slots(String, KT), kl, hsl)
  +e1 = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0)), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_w(AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), w_get(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), Equal.cong(Bool, H.Walk, c => H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), False{}, hc))
  +e2 = Equal.trans(H.Walk, H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.wk_kind(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), Equal.cong(Bool, H.Walk, c => H.wk_kind(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), False{}, hs), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(kk))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), w_getl(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)))
  +e3 = Equal.cong(Array<String> & String, H.Walk, r => H.wk_copy(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.swap(String, AR.thaw(String, KT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), SNil{}), (AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), esw)
  +e4 = Equal.cong(String, H.Walk, x => H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(x)), TB.nths(AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), xeq)
  +e5 = Equal.cong(String & String, H.Walk, r => H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), r), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), (TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), STR.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))))
  +e6 = Equal.cong(Array<String>, H.Walk, a => H.WK{AR.thaw(U32, tabT), a, Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, Array.set(String, AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), est)
  +e7 = Equal.cong(List<&2, String>, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), z}, Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Equal.sym(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, eacc))
  +eq = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e1, Equal.trans(H.Walk, H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e2, Equal.trans(H.Walk, H.wk_ll(AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e3, Equal.trans(H.Walk, H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, {==}, Equal.trans(H.Walk, H.wk_long(AR.thaw(U32, tabT), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.str_copy(TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), H.WK{AR.thaw(U32, tabT), Array.set(String, AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e5, Equal.trans(H.Walk, H.WK{AR.thaw(U32, tabT), Array.set(String, AR.thaw(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), Con{TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e6, e7))))))
  +es2 = AR.upd_slots(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), hsp, p1)
  +esl = Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))))), SC.update(String, AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, es2, Equal.trans(List<&2, String>, SC.update(String, AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SC.update(String, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, Equal.cong(List<&2, String>, List<&2, String>, z => SC.update(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), AR.slots(String, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{})), SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), es1), Equal.trans(List<&2, String>, SC.update(String, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, TB.upd_upd(AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}, TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), Equal.trans(List<&2, String>, SC.update(String, AR.slots(String, KT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SC.update(String, kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), kl, Equal.cong(List<&2, String>, List<&2, String>, z => SC.update(String, z, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), AR.slots(String, KT), kl, hsl), TB.upd_self(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))))))
  (AR.upd(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), (eq, (esl, AR.upd_perfect(String, sd, AR.upd(String, sd, KT, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), SNil{}), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), p1))))

def w_short(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool}, +hs: {H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))) == True{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
  +hb = w_at(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, False{}, hc)
  +ek = Equal.cong(Bool, String, b => TB.keyof_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q))))), b), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), True{}, hs)
  +eacc = Equal.trans(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), SC.append(String, kof(TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{})), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)), Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, w_accx(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, TB.dec_c(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)), kl, False{}), hb), Equal.cong(String, List<&2, String>, z => Con{z, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, TB.keyof(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), 1n+Nat.double(q)))))), SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, ek))
  +e1 = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0)), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_w(AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), w_get(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), Equal.cong(Bool, H.Walk, c => H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), False{}, hc))
  +e2 = Equal.cong(Bool, H.Walk, c => H.wk_kind(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), True{}, hs)
  +e3 = Equal.cong(List<&2, String>, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), z}, Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Equal.sym(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}, eacc))
  (KT, (Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e1, Equal.trans(H.Walk, H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), False{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), Con{SCon{Chr{U32.and(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 2147483647)}, SNil{}}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e2, e3)), (hsl, pk)))

def w_empty(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == True{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
  +hb = w_at(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, True{}, hc)
  +e1 = Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0)), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), True{}), Equal.cong(Array<U32> & U32, H.Walk, r => H.wk_w(AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(kk)), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), Nat.double(q))), w_get(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk)), Equal.cong(Bool, H.Walk, c => H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), c), U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), True{}, hc))
  +e2 = Equal.cong(List<&2, String>, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), z}, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), Equal.sym(List<&2, String>, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), w_accx(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, B.BE{}, hb)))
  (KT, (Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}), H.wk_if(AR.thaw(U32, tabT), AR.thaw(String, KT), kk, kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q), W32.nth0(AR.slots(U32, tabT), Nat.double(q)), True{}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), q), q)}, e1, e2), (hsl, pk)))

def w_full(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == False{} : Bool}, +d: Bool, +hd: {H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))) == d : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
  match d:
    case True{}:
      w_short(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc, hd)
    case False{}:
      w_long(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc, hd)

def w_c(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0) == c : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
  match c:
    case True{}:
      w_empty(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc)
    case False{}:
      w_full(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, hc, H.is_short(W32.nth0(AR.slots(U32, tabT), Nat.double(q))), {==})

# THEOREM: one step of the walk prepends bucket q's key
def wstep(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> WStep(tabT, kl, k, sd, q, kk, KT):
  w_c(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, q, hq, kk, hkk, KT, hsl, pk, U32.is_eq(W32.nth0(AR.slots(U32, tabT), Nat.double(q)), 0), {==})


def WalkOK(+tabT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +q: Nat, +kk: U32, +KT: AR.Tree<String>) -> Type:
  Sigma<&1, &1, AR.Tree<String>, K2 => {H.wk_go(1n+q, kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+q), 1n+q)}) == H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), 0n)} : H.Walk} & ({AR.slots(String, K2) == kl : List<&2, String>} & {AR.perfect(String, sd, K2) == True{} : Bool})>

def walk_0(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +kk: U32, +KT: AR.Tree<String>, st: WStep(tabT, kl, k, sd, 0n, kk, KT)) -> WalkOK(tabT, kl, k, sd, 0n, kk, KT):
  match st:
    case Tuple{+K2, Tuple{+e1, rest}}:
      (+hs2, pk2) = rest
      (K2, (Equal.trans(H.Walk, H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n), 1n)}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 0n), 0n)}, H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), 0n)}, e1, Equal.cong(Nat, H.Walk, z => H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), z, 0n)}, Nat.sub(SC.pow2(k), 0n), SC.pow2(k), N.sub_zero(SC.pow2(k)))), (hs2, pk2)))

def walk_s2(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +p: Nat, +kk: U32, +KT: AR.Tree<String>, +K2: AR.Tree<String>, +e1: {H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 2n+p), 2n+p)}) == H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+p), 1n+p)} : H.Walk}, wo: WalkOK(tabT, kl, k, sd, p, U32.sub(kk, 1), K2)) -> WalkOK(tabT, kl, k, sd, 1n+p, kk, KT):
  match wo:
    case Tuple{+K3, Tuple{+e2, rest}}:
      (+hs3, pk3) = rest
      (K3, (Equal.trans(H.Walk, H.wk_go(2n+p, kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 2n+p), 2n+p)}), H.wk_go(1n+p, U32.sub(kk, 1), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+p), 1n+p)}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K3), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), 0n)}, Equal.cong(H.Walk, H.Walk, w => H.wk_go(1n+p, U32.sub(kk, 1), w), H.wk_step(kk, H.WK{AR.thaw(U32, tabT), AR.thaw(String, KT), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 2n+p), 2n+p)}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+p), 1n+p)}, e1), e2), (hs3, pk3)))

def walk_s(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +p: Nat, +kk: U32, +KT: AR.Tree<String>, st: WStep(tabT, kl, k, sd, 1n+p, kk, KT), rec: @+K2: AR.Tree<String> -> @+hs2: {AR.slots(String, K2) == kl : List<&2, String>} -> @+pk2: {AR.perfect(String, sd, K2) == True{} : Bool} -> WalkOK(tabT, kl, k, sd, p, U32.sub(kk, 1), K2)) -> WalkOK(tabT, kl, k, sd, 1n+p, kk, KT):
  match st:
    case Tuple{+K2, Tuple{+e1, rest}}:
      (+hs2, pk2) = rest
      walk_s2(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, p, kk, KT, K2, e1, rec(K2, hs2, pk2))

# THEOREM: the walk over buckets q, q - 1, .., 0 lists every key in bucket order
def walk(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +q: Nat, +hq: {Nat.is_lt(q, SC.pow2(k)) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == q : Nat}, +KT: AR.Tree<String>, +hsl: {AR.slots(String, KT) == kl : List<&2, String>}, +pk: {AR.perfect(String, sd, KT) == True{} : Bool}) -> WalkOK(tabT, kl, k, sd, q, kk, KT):
  match q:
    case 0n:
      walk_0(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, kk, KT, wstep(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, 0n, hq, kk, hkk, KT, hsl, pk))
    case 1n+p:
      +hle = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+p, UD.v(kk), Equal.sym(Nat, UD.v(kk), 1n+p, hkk), N.zero_le(p))
      +hk2 = Equal.trans(Nat, UD.v(U32.sub(kk, 1)), Nat.sub(UD.v(kk), 1n), p, U.sub_nat(kk, 1, hle), Equal.trans(Nat, Nat.sub(UD.v(kk), 1n), Nat.sub(1n+p, 1n), p, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), UD.v(kk), 1n+p, hkk), N.sub_zero(p)))
      walk_s(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, p, kk, KT, wstep(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, 1n+p, hq, kk, hkk, KT, hsl, pk), K2 => hs2 => pk2 => walk(one, h1, k, hk31, tabT, pt, kl, sd, hsd, hlen, hwell, p, N.lt_trans(p, 1n+p, SC.pow2(k), N.lt_succ(p), hq), U32.sub(kk, 1), hk2, K2, hs2, pk2))

# ---- the operation ----

def KeysOK(~V: Data, +sh: ST.Sh<V>, r: H.HashMap<&2, V> & List<&2, String>) -> Type:
  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.keys(~V, ST.model(~V, sh))) : H.HashMap<&2, V> & List<&2, String>} & ({ST.good(~V, sh2) == True{} : Bool} & {ST.model(~V, sh2) == ST.model(~V, sh) : List<&2, S.Entry<V>>})>


def keys_w(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: 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>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, wo: WalkOK(tabT, AR.slots(String, ksT), k, sd, UD.v(CY.msk(k)), CY.msk(k), ksT), +ew: {H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}) == H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k)))}) : H.Walk}) -> KeysOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, H.keys(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}))):
  match wo:
    case Tuple{+K2, Tuple{+e2, rest}}:
      (+hs2, pk2) = rest
      +kl = AR.slots(String, ksT)
      +pkT = ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)
      +hgT = L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, b, vsT, nxT) == True{} : Bool}, AR.perfect(String, sd, ksT), True{}, pkT, hg)
      +g2 = L.subst(List<&2, String>, z => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, z, AR.perfect(String, sd, K2), vsT, nxT) == True{} : Bool}, kl, AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), kl, hs2), L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, b, vsT, nxT) == True{} : Bool}, True{}, AR.perfect(String, sd, K2), Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2), hgT))
      +m2 = Equal.cong(List<&2, String>, List<&2, S.Entry<V>>, z => ST.absm(~V, TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), AR.slots(String, K2), kl, hs2)
      +ek = Equal.sym(List<&2, String>, S.keys(~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)), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n), keys_absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), SC.pow2(k), 0n, N.le_refl(SC.pow2(k))))
      +ea = Equal.trans(H.Walk, H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k)))}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n)}, ew, e2)
      +eb = Equal.cong(H.Walk, H.HashMap<&2, V> & List<&2, String>, w => H.keys_fin(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), w), H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.WK{AR.thaw(U32, tabT), AR.thaw(String, K2), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n)}, ea)
      +ec = Equal.cong(List<&2, String>, H.HashMap<&2, V> & List<&2, String>, z => (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), z), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n), S.keys(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})), ek)
      (ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}, (Equal.trans(H.HashMap<&2, V> & List<&2, String>, H.keys(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT})), (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), 0n)), (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), S.keys(~V, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}))), eb, ec), (g2, m2)))

# THEOREM: keys lists the model's keys in order and keeps the map and its model
def keys_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> KeysOK(~V, sh, H.keys(&2, V, ST.real(~V, sh))):
  match sh:
    case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:
      +ck = ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)
      +hk31 = L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ck)
      +a0 = GR.mskv(k, N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==})))
      +eq0 = Equal.trans(Nat, 1n+UD.v(CY.msk(k)), Nat.add(UD.v(CY.msk(k)), 1n), SC.pow2(k), Equal.sym(Nat, Nat.add(UD.v(CY.msk(k)), 1n), 1n+UD.v(CY.msk(k)), N.add_comm(UD.v(CY.msk(k)), 1n)), a0)
      +hq0 = L.subst(Nat, z => {Nat.is_lt(UD.v(CY.msk(k)), z) == True{} : Bool}, 1n+UD.v(CY.msk(k)), SC.pow2(k), eq0, N.lt_succ(UD.v(CY.msk(k))))
      +ef = Equal.trans(Nat, U32.to_nat(U32.inc(CY.msk(k))), SC.pow2(k), 1n+UD.v(CY.msk(k)), PA.fuel_eq(1n, {==}, k, hk31), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), eq0))
      +esub = Equal.trans(Nat, Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), Nat.sub(1n+UD.v(CY.msk(k)), 1n+UD.v(CY.msk(k))), 0n, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n+UD.v(CY.msk(k))), SC.pow2(k), 1n+UD.v(CY.msk(k)), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), eq0)), N.sub_self(UD.v(CY.msk(k))))
      +eacc = Equal.cong(Nat, List<&2, String>, z => kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), z, 1n+UD.v(CY.msk(k))), 0n, Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), Equal.sym(Nat, Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 0n, esub))
      +ew = Equal.trans(H.Walk, H.wk_go(U32.to_nat(U32.inc(CY.msk(k))), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k)))}), Equal.cong(Nat, H.Walk, f => H.wk_go(f, CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), Nil{}}), U32.to_nat(U32.inc(CY.msk(k))), 1n+UD.v(CY.msk(k)), ef), Equal.cong(List<&2, String>, H.Walk, z => H.wk_go(1n+UD.v(CY.msk(k)), CY.msk(k), H.WK{AR.thaw(U32, tabT), AR.thaw(String, ksT), z}), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), 0n, 1n+UD.v(CY.msk(k))), kb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), Nat.sub(SC.pow2(k), 1n+UD.v(CY.msk(k))), 1n+UD.v(CY.msk(k))), eacc))
      keys_w(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, walk(1n, {==}, k, hk31, tabT, ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), AR.slots(String, ksT), sd, ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), AR.slots_length(String, sd, ksT, ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), UD.v(CY.msk(k)), hq0, CY.msk(k), {==}, ksT, {==}, ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ew)