1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32alg.bend as A 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/hash_table.bend as S 8 import ../../../spec/containers/lru.bend as SP 9 import ../../lib/u32div.bend as UD 10 import ../../../src/math/u64.bend as W 11 import ../../../src/containers/hash_table.bend as H 12 import ../../../src/containers/lru.bend as LR 13 import ../hash_table/table.bend as TB 14 import ../hash_table/buckets.bend as B 15 import ../hash_table/cyc.bend as CY 16 import ../hash_table/inv.bend as IV 17 import ../hash_table/keys.bend as K 18 import ./state.bend as ST 19 import ./basic.bend as BA 20 import ./bumpsh.bend as BS 21 import ./unlink.bend as UL 22 import ./meta.bend as MT 23 import ../../../src/math/hash.bend as HS 24 import ../hash_table/probe_all.bend as PA 25 26 import ./read.bend as RD 27 import ./ins.bend as IC 28 import ./insp.bend as IP 29 import ./pre.bend as PR 30 import ./room.bend as RO 31 import ../hash_table/arena.bend as AN 32 import ../hash_table/insgrow.bend as IG 33 import ./ins1.bend as I1 34 import ../../lib/u32.bend as U 35 import ../hash_table/insert.bend as IS 36 import ../hash_table/modn.bend as M 37 import ../../lib/links.bend as LK 38 import ../../lib/words32.bend as W32 39 import ../../lib/u32_tree.bend as UT 40 41 42 # add, a new key, a full arena: the arena doubles (a blank second half) and 43 # the new entry takes the next fresh slot. 44 45 46 47 # THEOREM: the doubled arena keeps the invariant 48 def gw_good(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +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}: 49 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg) 50 +hsd1 = UL.sd1(sd, hsd) 51 +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1) 52 +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)) 53 +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)) 54 +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)) 55 +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)) 56 +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) 57 +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))) 58 +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)) 59 +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) 60 +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)) 61 +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)) 62 +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)) 63 +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)) 64 +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)) 65 +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)) 66 +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)) 67 +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)) 68 +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) 69 +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)) 70 +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) 71 +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))) 72 +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))))) 73 +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)))) 74 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.sl 75 76 # ... and the model's entries 77 def gw_es(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +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>}: 78 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg) 79 +hsd1 = UL.sd1(sd, hsd) 80 +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1) 81 +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)) 82 +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)) 83 +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)) 84 +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)) 85 +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) 86 +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))) 87 +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)) 88 +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) 89 +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)) 90 +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)) 91 +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)) 92 +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)) 93 +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)) 94 +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)) 95 esg 96 97 98 def igr_n(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +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{})): 99 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Nil{}, hg) 100 +hsd1 = UL.sd1(sd, hsd) 101 +hsd32 = N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd1) 102 +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)) 103 +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)) 104 +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)) 105 +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)) 106 +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) 107 +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))) 108 +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)) 109 +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) 110 +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)) 111 +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)) 112 +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)) 113 +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)) 114 +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)) 115 +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)) 116 +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) 117 +gg = gw_good(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, hg, one, h1, hroom, hr) 118 +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) 119 +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) 120 +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) 121 +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) 122 +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)) 123 +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)) 124 +hd2 = N.lt_trans(1n+(1n+sd), 31n, 32n, N.lt_trans(1n+sd, k, 30n, hsdk2, hk30), {==}) 125 +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)) 126 +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)))) 127 +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)))) 128 +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.sl 129 +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))) 130 +q1 = UT.uset_p(5n, mT, pm, 0n, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))) 131 +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))) 132 +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))) 133 +t1 = UT.uset_s(5n, mT, pm, 0n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))) 134 +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))) 135 +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))) 136 +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)))) 137 +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)), {==})) 138 +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)), {==}) 139 +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))))) 140 +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 = 141 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) 142 +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.sl 143 +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 144 ok2 = L.subst(SP.Lru, 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) 145 +G2 = UT.uget(5n, {==}, mT, pm, 2, {==}) 146 +x1 = Equal.cong(Array & 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) 147 +m1 = UT.uset_a(5n, {==}, mT, pm, 0, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 0n))) 148 +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))) 149 +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))) 150 +eM = Equal.trans(Array, 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, Array, 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, 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, Array, 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)))) 151 +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)) 152 +eK = Equal.cong(Array, Array, 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, 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, d => Array.new(String, d, ""), UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, edp0), AR.new(String, sd, ""))) 153 +eE = Equal.cong(Array>, Array>, 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>, 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>, d => LR.vac(&2, V, d), UD.v(W32.nth0(AR.slots(U32, mT), 2n)), sd, edp0), PR.vac_eq(~V, sd))) 154 +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)) 155 +eL = Equal.cong(Array, Array, 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, 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, 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))) 156 +r1 = Equal.cong(Array, 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) 157 +r2 = Equal.cong(Array, 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) 158 +r3 = Equal.cong(Array>, 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) 159 +r4 = Equal.cong(Array, 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) 160 +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.LR 161 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 162 163 # THEOREM (add, a full arena: it doubles and the fresh slot takes the entry) 164 def ip_grow(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +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{})): 165 match fl: 166 case Nil{}: 167 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) 168 case Con{+s0, +tl}: 169 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg) 170 +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)) 171 +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)) 172 +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)) 173 +hz0 = L.subst(U32, z => {U32.is_eq(z, 0) == True{} : Bool}, free, LK.lnk(s0), ef, hfz) 174 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)))