proofs/containers/lru/grow.bend source

proofs/containers/lru/grow.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32alg.bend as Aimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/math/u64.bend as Wimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/table.bend as TBimport ../hash_table/buckets.bend as Bimport ../hash_table/cyc.bend as CYimport ../hash_table/inv.bend as IVimport ../hash_table/keys.bend as Kimport ./state.bend as STimport ./basic.bend as BAimport ./bumpsh.bend as BSimport ./unlink.bend as ULimport ./meta.bend as MTimport ../../../src/math/hash.bend as HSimport ../hash_table/probe_all.bend as PAimport ./read.bend as RDimport ./ins.bend as ICimport ./insp.bend as IPimport ./pre.bend as PRimport ./room.bend as ROimport ../hash_table/arena.bend as ANimport ../hash_table/insgrow.bend as IGimport ./ins1.bend as I1import ../../lib/u32.bend as Uimport ../hash_table/insert.bend as ISimport ../hash_table/modn.bend as Mimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# add, a new key, a full arena: the arena doubles (a blank second half) and# the new entry takes the next fresh slot.# THEOREM: the doubled arena keeps the invariantdef gw_good(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hr: {U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)) == False{} : Bool}) -> {ST.good(~V, ST.LS{cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), k, 1n+sd, tabT, AR.TNode{ksT, AR.trep(String, sd, "")}, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}, sl, Nil{}}) == True{} : Bool}:  +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg)  +hsd1 = UL.sd1(sd, hsd)  +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1)  +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +ehs = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ST.g_csize(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle1 = L.subst(Nat, z => {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.pow2(sd), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ehs), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle2 = N.not_lt_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), Equal.trans(Bool, Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), False{}, Equal.sym(Bool, U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U.is_lt_nat(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), hr))  +efp = Equal.trans(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), N.le_antisym(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), hle1, hle2), ehs)  +eln = Equal.trans(Nat, SC.length(Nat, sl), Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.sym(Nat, Nat.add(SC.length(Nat, sl), 0n), SC.length(Nat, sl), N.add_zero(SC.length(Nat, sl))), N.eq_from_is_eq(Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)))  +env = Equal.trans(Nat, UD.v(n), SC.length(Nat, sl), SC.pow2(sd), Equal.sym(Nat, SC.length(Nat, sl), UD.v(n), N.eq_from_is_eq(SC.length(Nat, sl), UD.v(n), ST.g_clen(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))), Equal.trans(Nat, SC.length(Nat, sl), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), eln, efp))  +hrm = L.subst(Nat, z => {Nat.is_le(Nat.double(1n+z), SC.pow2(k)) == True{} : Bool}, UD.v(n), SC.pow2(sd), env, hroom)  +hsdk2 = IG.pow2_lt_inv(1n+sd, k, N.lt_le_trans(SC.pow2(1n+sd), Nat.double(1n+SC.pow2(sd)), SC.pow2(k), N.double_lt(SC.pow2(sd), 1n+SC.pow2(sd), N.lt_succ(SC.pow2(sd))), hrm))  +hlk = AR.slots_length(String, sd, ksT, ST.g_cpk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle = AR.slots_length(Maybe<&2, V>, sd, eT, ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hll = AR.slots_length(U32, 3n+sd, lkT, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +ebs = AN.bs_app(AR.slots(U32, tabT), AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, "")), sd, hlk, SC.pow2(k), ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +esg = PR.es_pre(~V, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0)), sd, hll, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, "")), hlk, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), hle, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), sl, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +esz = Equal.trans(Nat, UD.v(U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), Nat.double(UD.v(W32.nth0(AR.slots(U32, mT), 1n))), SC.pow2(1n+sd), U.shl_value(W32.nth0(AR.slots(U32, mT), 1n), k, N.lt_le(k, 32n, N.lt_trans(k, 30n, 32n, hk30, {==})), L.subst(Nat, z => {Nat.is_lt(Nat.double(z), SC.pow2(k)) == True{} : Bool}, SC.pow2(sd), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ehs), N.pow2_strict(1n+sd, k, hsdk2))), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ehs))  +edp0 = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, ST.g_cdepth(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hm5 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(5n)) == True{} : Bool}, sd, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, edp0), hsd32)  +edp = Equal.trans(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 1n+sd, W32.inc_val(one, h1, W32.nth0(AR.slots(U32, mT), 2n), W32.bound32(one, h1, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 5n, {==}, hm5)), Equal.cong(Nat, Nat, z => 1n+z, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, edp0))  +gx = ST.good_intro(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), True{}, k, 1n+sd, tabT, SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), AR.perfect(String, 1n+sd, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}, sl, Nil{}, ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), hsdk2, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), L.and_intro(AR.perfect(String, sd, ksT), AR.perfect(String, sd, AR.trep(String, sd, "")), ST.g_cpk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), AR.trep_perfect(String, sd, "")), L.and_intro(AR.perfect(Maybe<&2, V>, sd, eT), AR.perfect(Maybe<&2, V>, sd, AR.trep(Maybe<&2, V>, sd, None{})), ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), AR.trep_perfect(Maybe<&2, V>, sd, None{})), L.and_intro(AR.perfect(U32, 3n+sd, lkT), AR.perfect(U32, 3n+sd, AR.trep(U32, 3n+sd, 0)), ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), AR.trep_perfect(U32, 3n+sd, 0)), {==}, ST.g_cmask(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), ST.g_cbits(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), IS.eq_is_eq(UD.v(U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), SC.pow2(1n+sd), esz), IS.eq_is_eq(UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 1n+sd, edp), N.le_trans(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), SC.pow2(1n+sd), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), N.lt_le(SC.pow2(sd), SC.pow2(1n+sd), N.pow2_lt_succ(sd))), L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PWell{z, 1n+sd}, SC.pow2(k)) == True{} : Bool}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs), AN.well_mono(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd, 1n+sd, N.lt_le(SC.pow2(sd), SC.pow2(1n+sd), N.pow2_lt_succ(sd)), SC.pow2(k), ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), SC.pow2(k), N.le_refl(SC.pow2(k)))), L.subst(List<&2, B.Bk>, z => {B.cluster(z, SC.pow2(k), CY.msk(k)) == True{} : Bool}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs), ST.g_cclus(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PUniq{z}, SC.pow2(k)) == True{} : Bool}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs), ST.g_cuniq(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), L.subst(List<&2, B.Bk>, z => {Nat.is_eq(UD.v(n), IV.occn(z, SC.pow2(k))) == True{} : Bool}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs), ST.g_cn(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), ST.g_cload(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), ST.g_ccap(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), L.subst(List<&2, B.Bk>, z => {ST.bsl(z, sl, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.pow2(k)) == True{} : Bool}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs), Equal.trans(Bool, ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k)), True{}, PR.bsl_pre(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0)), sd, hll, SC.pow2(k), ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), ST.g_cbsl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))), L.subst(List<&2, B.Bk>, z => {ST.hasall(~V, z, SC.pow2(k), SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), sl) == True{} : Bool}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs), Equal.trans(Bool, ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), sl), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), sl), True{}, PR.has_pre(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0)), sd, hll, AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), sl, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), ST.g_chas(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))), PR.slok_pre(~V, sd, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), hle, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), sl, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), ST.g_clen(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), ST.g_ctail(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), Equal.trans(Bool, ST.seg(SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), sl, 0, 0), ST.seg(AR.slots(U32, lkT), sl, 0, 0), True{}, PR.seg_pre(~V, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0)), sd, hll, AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), sl, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 0, 0), ST.g_cdll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), L.subst(List<&2, SP.Ent<V>>, z => {S.nodup(SP.keys_of(~V, z)) == True{} : Bool}, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), sl), Equal.sym(List<&2, SP.Ent<V>>, ST.es(~V, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), esg), ST.g_ckeys(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)), ST.g_cfree(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), {==}, {==}, {==}, ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +p1 = UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))  +e1 = Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 1n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 1n), U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 1n, {==}), MT.nth_same(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))))  +e2 = MT.nth_same(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), p1, 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))))  RO.good_mk(~V, cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), W32.nth0(AR.slots(U32, mT), 0n), U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), k, 1n+sd, tabT, AR.TNode{ksT, AR.trep(String, sd, "")}, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}, sl, Nil{}, gx, Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 0n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 0n), W32.nth0(AR.slots(U32, mT), 0n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 0n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 0n, {==})), e1, e2, Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 6n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 6n), W32.nth0(AR.slots(U32, mT), 6n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 6n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 6n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 7n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 7n), W32.nth0(AR.slots(U32, mT), 7n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 7n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 7n, {==})), UT.uset_p(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), p1, 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))))# ... and the model's entriesdef gw_es(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hr: {U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)) == False{} : Bool}) -> {ST.es(~V, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), sl) == ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl) : List<&2, SP.Ent<V>>}:  +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg)  +hsd1 = UL.sd1(sd, hsd)  +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1)  +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +ehs = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ST.g_csize(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle1 = L.subst(Nat, z => {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.pow2(sd), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ehs), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle2 = N.not_lt_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), Equal.trans(Bool, Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), False{}, Equal.sym(Bool, U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U.is_lt_nat(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), hr))  +efp = Equal.trans(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), N.le_antisym(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), hle1, hle2), ehs)  +eln = Equal.trans(Nat, SC.length(Nat, sl), Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.sym(Nat, Nat.add(SC.length(Nat, sl), 0n), SC.length(Nat, sl), N.add_zero(SC.length(Nat, sl))), N.eq_from_is_eq(Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)))  +env = Equal.trans(Nat, UD.v(n), SC.length(Nat, sl), SC.pow2(sd), Equal.sym(Nat, SC.length(Nat, sl), UD.v(n), N.eq_from_is_eq(SC.length(Nat, sl), UD.v(n), ST.g_clen(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))), Equal.trans(Nat, SC.length(Nat, sl), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), eln, efp))  +hrm = L.subst(Nat, z => {Nat.is_le(Nat.double(1n+z), SC.pow2(k)) == True{} : Bool}, UD.v(n), SC.pow2(sd), env, hroom)  +hsdk2 = IG.pow2_lt_inv(1n+sd, k, N.lt_le_trans(SC.pow2(1n+sd), Nat.double(1n+SC.pow2(sd)), SC.pow2(k), N.double_lt(SC.pow2(sd), 1n+SC.pow2(sd), N.lt_succ(SC.pow2(sd))), hrm))  +hlk = AR.slots_length(String, sd, ksT, ST.g_cpk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle = AR.slots_length(Maybe<&2, V>, sd, eT, ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hll = AR.slots_length(U32, 3n+sd, lkT, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +ebs = AN.bs_app(AR.slots(U32, tabT), AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, "")), sd, hlk, SC.pow2(k), ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +esg = PR.es_pre(~V, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0)), sd, hll, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, "")), hlk, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), hle, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), sl, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  esgdef igr_n(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +free2: U32, +hf2: {U32.is_eq(free2, 0) == True{} : Bool}, +hr: {U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)) == False{} : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), False{})):  +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg)  +hsd1 = UL.sd1(sd, hsd)  +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1)  +hk30 = L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +ehs = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ST.g_csize(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle1 = L.subst(Nat, z => {Nat.is_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.pow2(sd), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), ehs), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle2 = N.not_lt_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), Equal.trans(Bool, Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), False{}, Equal.sym(Bool, U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n))), U.is_lt_nat(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), hr))  +efp = Equal.trans(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), SC.pow2(sd), N.le_antisym(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(W32.nth0(AR.slots(U32, mT), 1n)), hle1, hle2), ehs)  +eln = Equal.trans(Nat, SC.length(Nat, sl), Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.sym(Nat, Nat.add(SC.length(Nat, sl), 0n), SC.length(Nat, sl), N.add_zero(SC.length(Nat, sl))), N.eq_from_is_eq(Nat.add(SC.length(Nat, sl), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)))  +env = Equal.trans(Nat, UD.v(n), SC.length(Nat, sl), SC.pow2(sd), Equal.sym(Nat, SC.length(Nat, sl), UD.v(n), N.eq_from_is_eq(SC.length(Nat, sl), UD.v(n), ST.g_clen(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))), Equal.trans(Nat, SC.length(Nat, sl), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), eln, efp))  +hrm = L.subst(Nat, z => {Nat.is_le(Nat.double(1n+z), SC.pow2(k)) == True{} : Bool}, UD.v(n), SC.pow2(sd), env, hroom)  +hsdk2 = IG.pow2_lt_inv(1n+sd, k, N.lt_le_trans(SC.pow2(1n+sd), Nat.double(1n+SC.pow2(sd)), SC.pow2(k), N.double_lt(SC.pow2(sd), 1n+SC.pow2(sd), N.lt_succ(SC.pow2(sd))), hrm))  +hlk = AR.slots_length(String, sd, ksT, ST.g_cpk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hle = AR.slots_length(Maybe<&2, V>, sd, eT, ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hll = AR.slots_length(U32, 3n+sd, lkT, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +ebs = AN.bs_app(AR.slots(U32, tabT), AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, "")), sd, hlk, SC.pow2(k), ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +esg = PR.es_pre(~V, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0)), sd, hll, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, "")), hlk, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), hle, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), sl, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +pm = ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg)  +gg = gw_good(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, hg, one, h1, hroom, hr)  +sbs = Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs)  +hnog = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PNo{z, key}, SC.pow2(k)) == True{} : Bool}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), sbs, hno)  +hzg = L.subst(List<&2, B.Bk>, z => {B.at(z, e) == B.BE{} : B.Bk}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), sbs, hz)  +hpg = L.subst(List<&2, B.Bk>, z => {B.occpath(z, 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}, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), sbs, hp)  +hs0g = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+sd)) == True{} : Bool}, SC.pow2(sd), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), efp), N.pow2_lt_succ(sd))  +hsn = IP.nm_lt(~V, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +hd2 = N.lt_trans(1n+(1n+sd), 31n, 32n, N.lt_trans(1n+sd, k, 30n, hsdk2, hk30), {==})  +ei = W32.inc_val(one, h1, W32.nth0(AR.slots(U32, mT), 0n), W32.bound32(one, h1, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), 1n+sd, hd2, hs0g))  +ecnt = Equal.trans(Nat, Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), 0n), SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), N.add_zero(SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}}))), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), 1n+SC.length(Nat, sl), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), I1.len_snoc(sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Equal.trans(Nat, 1n+SC.length(Nat, sl), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), Equal.cong(Nat, Nat, z => 1n+z, SC.length(Nat, sl), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), eln), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ei))))  +hsfr = L.subst(Nat, z => {Nat.is_lt(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), ei), N.lt_succ(UD.v(W32.nth0(AR.slots(U32, mT), 0n))))  +hfrle = L.subst(U32, z => {Nat.is_le(UD.v(z), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))) == True{} : Bool}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 0n), Equal.sym(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 0n), W32.nth0(AR.slots(U32, mT), 0n), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 0n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 0n), W32.nth0(AR.slots(U32, mT), 0n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 0n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 0n, {==}))), N.lt_le(UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), hsfr))  +hfr2 = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(1n+sd)) == True{} : Bool}, 1n+SC.pow2(sd), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n+SC.pow2(sd), Equal.trans(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 0n)), 1n+SC.pow2(sd), ei, Equal.cong(Nat, Nat, z => 1n+z, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), efp))), N.double_succ_le(SC.pow2(sd), N.pow2_pos(sd)))  +q1 = UT.uset_p(5n, mT, pm, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))  +q2 = UT.uset_p(5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), q1, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))  +q3 = UT.uset_p(5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), q2, 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))  +t1 = UT.uset_s(5n, mT, pm, 0n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))  +t2 = UT.uset_s(5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), q1, 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))  +t3 = UT.uset_s(5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), q2, 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))  +a1 = Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), SC.update(U32, SC.update(U32, SC.update(U32, AR.slots(U32, mT), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), t3, Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), t2, Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), AR.slots(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), SC.update(U32, AR.slots(U32, mT), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), t1))))  +c1 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), PR.upd_comm(AR.slots(U32, mT), 0n, 1n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)), U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), {==}))  +c2 = PR.upd_comm(SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 0n, 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)), U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), {==})  +g1 = Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))))  +hsm = Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), SC.update(U32, SC.update(U32, SC.update(U32, AR.slots(U32, mT), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), a1, Equal.trans(List<&2, U32>, SC.update(U32, SC.update(U32, SC.update(U32, AR.slots(U32, mT), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), SC.update(U32, SC.update(U32, SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), c1, Equal.trans(List<&2, U32>, SC.update(U32, SC.update(U32, SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), SC.update(U32, SC.update(U32, SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), c2, Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), SC.update(U32, SC.update(U32, AR.slots(U32, mT), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), g1)))))  ok = IC.ins_core(~V, cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), k, 1n+sd, tabT, AR.TNode{ksT, AR.trep(String, sd, "")}, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}, sl, Nil{}, gg, one, h1, key, hnog, e, he, hzg, hpg, hroom, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), W32.nth0(AR.slots(U32, mT), 0n), {==}, hs0g, hsn, Nil{}, free2, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)), hf2, {==}, {==}, {==}, IS.eq_is_eq(Nat.add(SC.length(Nat, SC.append(Nat, sl, Con{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Nil{}})), 0n), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), ecnt), {==}, hsfr, hfrle, hfr2, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), q3, hsm, v, t, lo, hi)  +ec = BA.ctr_eq(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.slots(U32, mT), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 16n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 16n), W32.nth0(AR.slots(U32, mT), 16n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 16n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 16n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 17n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 17n), W32.nth0(AR.slots(U32, mT), 17n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 17n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 17n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 18n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 18n), W32.nth0(AR.slots(U32, mT), 18n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 18n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 18n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 19n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 19n), W32.nth0(AR.slots(U32, mT), 19n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 19n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 19n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 20n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 20n), W32.nth0(AR.slots(U32, mT), 20n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 20n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 20n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 21n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 21n), W32.nth0(AR.slots(U32, mT), 21n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 21n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 21n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 22n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 22n), W32.nth0(AR.slots(U32, mT), 22n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 22n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 22n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 23n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 23n), W32.nth0(AR.slots(U32, mT), 23n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 23n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 23n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 24n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 24n), W32.nth0(AR.slots(U32, mT), 24n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 24n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 24n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 25n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 25n), W32.nth0(AR.slots(U32, mT), 25n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 25n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 25n, {==})))  +esp = BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 4n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))))), SP.c_ins(ST.ctr(AR.slots(U32, mT))), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 3n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 3n), W32.nth0(AR.slots(U32, mT), 3n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 3n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 3n, {==})), BA.w64_eq(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.slots(U32, mT), 4n, Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 4n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 4n), W32.nth0(AR.slots(U32, mT), 4n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 4n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 4n, {==})), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 5n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 5n), W32.nth0(AR.slots(U32, mT), 5n), MT.nth_other(AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), UT.uset_s(5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_p(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), 5n, {==}), MT.nth_other(mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)), AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), UT.uset_s(5n, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg), 1n, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 5n, {==}))), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SP.snoc(~V, z, SP.LE{key, v, t, W.U64{lo, hi}}), ST.es(~V, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), esg), Equal.cong(SP.Ctr, SP.Ctr, z => SP.c_ins(z), ST.ctr(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))))), ST.ctr(AR.slots(U32, mT)), ec))  ok2 = L.subst(SP.Lru<V>, z => BS.CountOK(~V, z, LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})), SP.L{cap, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 3n), ST.w64(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), 4n), SP.snoc(~V, ST.es(~V, SC.append(U32, AR.slots(U32, lkT), AR.slots(U32, AR.trep(U32, 3n+sd, 0))), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))))))}, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, esp, ok)  +G2 = UT.uget(5n, {==}, mT, pm, 2, {==})  +x1 = Equal.cong(Array<U32> & U32, LR.LRU<&2, V>, r => LR.grow_sz(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), r), Array.get(U32, AR.thaw(U32, mT), 2), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 2n)), G2)  +m1 = UT.uset_a(5n, {==}, mT, pm, 0, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))  +m2 = UT.uset_a(5n, {==}, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), q1, 1, {==}, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))  +m3 = UT.uset_a(5n, {==}, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), q2, 2, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))  +eM = Equal.trans(Array<U32>, Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, mT), 0, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), Array.set(U32, Array.set(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), Equal.cong(Array<U32>, Array<U32>, z => Array.set(U32, Array.set(U32, z, 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), Array.set(U32, AR.thaw(U32, mT), 0, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), AR.thaw(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), m1), Equal.trans(Array<U32>, Array.set(U32, Array.set(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), Array.set(U32, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), Equal.cong(Array<U32>, Array<U32>, z => Array.set(U32, z, 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), Array.set(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n)))), 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n)))), m2), m3))  +edp0 = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, ST.g_cdepth(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Nil{}, hg))  +eK = Equal.cong(Array<String>, Array<String>, a => ANode{AR.thaw(String, ksT), a}, Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), ""), AR.thaw(String, AR.trep(String, sd, "")), Equal.trans(Array<String>, Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), ""), Array.new(String, sd, ""), AR.thaw(String, AR.trep(String, sd, "")), Equal.cong(Nat, Array<String>, d => Array.new(String, d, ""), UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, edp0), AR.new(String, sd, "")))  +eE = Equal.cong(Array<Maybe<&2, V>>, Array<Maybe<&2, V>>, a => ANode{AR.thaw(Maybe<&2, V>, eT), a}, LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n))), AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), Equal.trans(Array<Maybe<&2, V>>, LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n))), LR.vac(&2, V, sd), AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), Equal.cong(Nat, Array<Maybe<&2, V>>, d => LR.vac(&2, V, d), UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, edp0), PR.vac_eq(~V, sd)))  +e3 = Equal.trans(Nat, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), Nat.add(sd, 3n), 3n+sd, Equal.cong(Nat, Nat, z => Nat.add(z, 3n), UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, edp0), N.add_comm(sd, 3n))  +eL = Equal.cong(Array<U32>, Array<U32>, a => ANode{AR.thaw(U32, lkT), a}, Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0), AR.thaw(U32, AR.trep(U32, 3n+sd, 0)), Equal.trans(Array<U32>, Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0), Array.new(U32, 3n+sd, 0), AR.thaw(U32, AR.trep(U32, 3n+sd, 0)), Equal.cong(Nat, Array<U32>, d => Array.new(U32, d, 0), Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 3n+sd, e3), AR.new(U32, 3n+sd, 0)))  +r1 = Equal.cong(Array<U32>, LR.LRU<&2, V>, z => LR.put_slot(&2, V, cap, n, head, tail, free2, z, AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), "")}, ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, mT), 0, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), eM)  +r2 = Equal.cong(Array<String>, LR.LRU<&2, V>, z => LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), z, ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), "")}, AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), eK)  +r3 = Equal.cong(Array<Maybe<&2, V>>, LR.LRU<&2, V>, z => LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), z, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), eE)  +r4 = Equal.cong(Array<U32>, LR.LRU<&2, V>, z => LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), z, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), eL)  +ER = Equal.trans(LR.LRU<&2, V>, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), False{}), LR.put_slot(&2, V, cap, n, head, tail, free2, Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, mT), 0, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), "")}, ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), x1, Equal.trans(LR.LRU<&2, V>, LR.put_slot(&2, V, cap, n, head, tail, free2, Array.set(U32, Array.set(U32, Array.set(U32, AR.thaw(U32, mT), 0, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2, U32.inc(W32.nth0(AR.slots(U32, mT), 2n))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), "")}, ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), "")}, ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), r1, Equal.trans(LR.LRU<&2, V>, LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(W32.nth0(AR.slots(U32, mT), 2n)), "")}, ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), r2, Equal.trans(LR.LRU<&2, V>, LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), ANode{AR.thaw(Maybe<&2, V>, eT), LR.vac(&2, V, UD.v(W32.nth0(AR.slots(U32, mT), 2n)))}, ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), ANode{AR.thaw(U32, lkT), Array.new(U32, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 2n)), 3n), 0)}, W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), r3, r4))))  L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, z), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), False{}), Equal.sym(LR.LRU<&2, V>, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), False{}), LR.put_slot(&2, V, cap, n, head, tail, free2, AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))), 1n, U32.shl(W32.nth0(AR.slots(U32, mT), 1n))), 2n, U32.inc(W32.nth0(AR.slots(U32, mT), 2n)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{eT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{lkT, AR.trep(U32, 3n+sd, 0)}), W32.nth0(AR.slots(U32, mT), 0n), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), ER), ok2)# THEOREM (add, a full arena: it doubles and the fresh slot takes the entry)def ip_grow(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +free2: U32, +hf2: {U32.is_eq(free2, 0) == True{} : Bool}, +hfz: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)) == False{} : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), False{})):  match fl:    case Nil{}:      igr_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, free2, hf2, hr)    case Con{+s0, +tl}:      +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg)      +hf0 = L.and_left(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0))), ST.flok(~V, tl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))      +hs0 = N.lt_le_trans(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), L.and_left(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), hf0), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))      +ef = A.eq_of(free, LK.lnk(s0), ST.g_cfree(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, Con{s0, tl}, hg))      +hz0 = L.subst(U32, z => {U32.is_eq(z, 0) == True{} : Bool}, free, LK.lnk(s0), ef, hfz)      Empty.absurd(BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), False{})), L.false_true(Equal.trans(Bool, False{}, U32.is_eq(LK.lnk(s0), 0), True{}, Equal.sym(Bool, U32.is_eq(LK.lnk(s0), 0), False{}, UL.lnk_nz(one, h1, s0, sd, hsd, hs0)), hz0)))