proofs/containers/lru/room.bend source

proofs/containers/lru/room.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/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/table.bend as TBimport ../hash_table/cyc.bend as CYimport ../hash_table/inv.bend as IVimport ./state.bend as STimport ./basic.bend as BAimport ./meta.bend as MTimport ./tabsl.bend as TSimport ./idx.bend as IDimport ../../lib/word.bend as WDimport ../hash_table/grow.bend as GRimport ../hash_table/insu.bend as IUimport ../hash_table/insgrow.bend as IGimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# add, first step: room keeps the table at most half full for one more entry,# doubling it when needed (a rehash); the model is unchanged.# the state is roomy: one more entry keeps the table at most half fulldef roomy(~V: Data, sh: ST.Sh<V>) -> Bool:  match sh:    case ST.LS{+cap, +n, +head, +tail, +free, +mT, +k, +sd, +tabT, +ksT, +eT, +lkT, +sl, +fl}:      Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k))def RoomOK(~V: Data, +sh: ST.Sh<V>, r: LR.LRU<&2, V>) -> Type:  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : LR.LRU<&2, V>} & ({ST.model(~V, sh2) == ST.model(~V, sh) : SP.Lru<V>} & ({ST.good(~V, sh2) == True{} : Bool} & {roomy(~V, sh2) == True{} : Bool}))>def mk_room(~V: Data, +sh: ST.Sh<V>, -r: LR.LRU<&2, V>, +sh2: ST.Sh<V>, +e: {r == ST.real(~V, sh2) : LR.LRU<&2, V>}, +em: {ST.model(~V, sh2) == ST.model(~V, sh) : SP.Lru<V>}, +g: {ST.good(~V, sh2) == True{} : Bool}, +h: {roomy(~V, sh2) == True{} : Bool}) -> RoomOK(~V, sh, r):  (sh2, (e, (em, (g, h))))# the invariant from its components with the meta words nameddef good_mk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT2: AR.Tree<U32>, +a0: U32, +a1: U32, +a2: U32, +a6: U32, +a7: 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.goodF(~V, cap, n, head, tail, free, a0, a1, a2, a6, a7, True{}, k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, +e0: {W32.nth0(AR.slots(U32, mT2), 0n) == a0 : U32}, +e1: {W32.nth0(AR.slots(U32, mT2), 1n) == a1 : U32}, +e2: {W32.nth0(AR.slots(U32, mT2), 2n) == a2 : U32}, +e6: {W32.nth0(AR.slots(U32, mT2), 6n) == a6 : U32}, +e7: {W32.nth0(AR.slots(U32, mT2), 7n) == a7 : U32}, +hp: {AR.perfect(U32, 5n, mT2) == True{} : Bool}) -> {ST.good(~V, ST.LS{cap, n, head, tail, free, mT2, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}:  +g0 = L.subst(U32, z => {ST.goodF(~V, cap, n, head, tail, free, z, a1, a2, a6, a7, True{}, k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, a0, W32.nth0(AR.slots(U32, mT2), 0n), Equal.sym(U32, W32.nth0(AR.slots(U32, mT2), 0n), a0, e0), hg)  +g1 = L.subst(U32, z => {ST.goodF(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT2), 0n), z, a2, a6, a7, True{}, k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, a1, W32.nth0(AR.slots(U32, mT2), 1n), Equal.sym(U32, W32.nth0(AR.slots(U32, mT2), 1n), a1, e1), g0)  +g2 = L.subst(U32, z => {ST.goodF(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT2), 0n), W32.nth0(AR.slots(U32, mT2), 1n), z, a6, a7, True{}, k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, a2, W32.nth0(AR.slots(U32, mT2), 2n), Equal.sym(U32, W32.nth0(AR.slots(U32, mT2), 2n), a2, e2), g1)  +g6 = L.subst(U32, z => {ST.goodF(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT2), 0n), W32.nth0(AR.slots(U32, mT2), 1n), W32.nth0(AR.slots(U32, mT2), 2n), z, a7, True{}, k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, a6, W32.nth0(AR.slots(U32, mT2), 6n), Equal.sym(U32, W32.nth0(AR.slots(U32, mT2), 6n), a6, e6), g2)  +g7 = L.subst(U32, z => {ST.goodF(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT2), 0n), W32.nth0(AR.slots(U32, mT2), 1n), W32.nth0(AR.slots(U32, mT2), 2n), W32.nth0(AR.slots(U32, mT2), 6n), z, True{}, k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, a7, W32.nth0(AR.slots(U32, mT2), 7n), Equal.sym(U32, W32.nth0(AR.slots(U32, mT2), 7n), a7, e7), g6)  L.subst(Bool, z => {ST.goodF(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT2), 0n), W32.nth0(AR.slots(U32, mT2), 1n), W32.nth0(AR.slots(U32, mT2), 2n), W32.nth0(AR.slots(U32, mT2), 6n), W32.nth0(AR.slots(U32, mT2), 7n), z, k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, True{}, AR.perfect(U32, 5n, mT2), Equal.sym(Bool, AR.perfect(U32, 5n, mT2), True{}, hp), g7)# a meta word other than 6 and 7 is keptdef oth2(+mT: AR.Tree<U32>, +k: Nat, +hs1: {AR.slots(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))) == SC.update(U32, AR.slots(U32, mT), 6n, U32.inc(U32.shl(CY.msk(k)))) : List<&2, U32>}, +hs2: {AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))) == SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))) : List<&2, U32>}, +j: Nat, +n6: {Nat.is_eq(6n, j) == False{} : Bool}, +n7: {Nat.is_eq(7n, j) == False{} : Bool}) -> {W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), j) == W32.nth0(AR.slots(U32, mT), j) : U32}:  Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), j), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))), j), W32.nth0(AR.slots(U32, mT), j), MT.nth_other(AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), hs2, j, n7), MT.nth_other(mT, 6n, U32.inc(U32.shl(CY.msk(k))), AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), hs1, j, n6))# the model reads meta words 3, 4, 5 and 16 .. 25 onlydef model_m(~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>, +T2: AR.Tree<U32>, +hs1: {AR.slots(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))) == SC.update(U32, AR.slots(U32, mT), 6n, U32.inc(U32.shl(CY.msk(k)))) : List<&2, U32>}, +hs2: {AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))) == SC.update(U32, AR.slots(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))) : List<&2, U32>}) -> {ST.model(~V, ST.LS{cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+k, sd, T2, ksT, eT, lkT, sl, fl}) == ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) : SP.Lru<V>}:  +ec = BA.ctr_eq(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), AR.slots(U32, mT), oth2(mT, k, hs1, hs2, 16n, {==}, {==}), oth2(mT, k, hs1, hs2, 17n, {==}, {==}), oth2(mT, k, hs1, hs2, 18n, {==}, {==}), oth2(mT, k, hs1, hs2, 19n, {==}, {==}), oth2(mT, k, hs1, hs2, 20n, {==}, {==}), oth2(mT, k, hs1, hs2, 21n, {==}, {==}), oth2(mT, k, hs1, hs2, 22n, {==}, {==}), oth2(mT, k, hs1, hs2, 23n, {==}, {==}), oth2(mT, k, hs1, hs2, 24n, {==}, {==}), oth2(mT, k, hs1, hs2, 25n, {==}, {==}))  BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), 4n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))))), ST.ctr(AR.slots(U32, mT)), oth2(mT, k, hs1, hs2, 3n, {==}, {==}), BA.w64_eq(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), AR.slots(U32, mT), 4n, oth2(mT, k, hs1, hs2, 4n, {==}, {==}), oth2(mT, k, hs1, hs2, 5n, {==}, {==})), {==}, ec)# the grown table: the implementation's size word is the hash map'sdef tg_eq(~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}) -> {H.mv_fin(H.mv_go(U32.to_nat(U32.inc(CY.msk(k))), 0, U32.inc(U32.shl(CY.msk(k))), H.MV{AR.thaw(U32, tabT), Array.new(U32, U32.to_nat(U32.add(W32.nth0(AR.slots(U32, mT), 7n), 2)), 0)})) == H.grow_tab(CY.msk(k), U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), AR.thaw(U32, tabT)) : Array<U32>}:  +ek = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), k, 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, fl, hg))  +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, fl, hg))  +hk5 = L.subst(Nat, z => {Nat.is_lt(1n+z, SC.pow2(5n)) == True{} : Bool}, k, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), k, ek), N.lt_trans(1n+k, 31n, 32n, hk30, {==}))  +hk5b = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(5n)) == True{} : Bool}, k, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), k, ek), N.lt_trans(k, 30n, 32n, hk30, {==}))  +ei1 = W32.inc_val(one, h1, W32.nth0(AR.slots(U32, mT), 7n), W32.bound32(one, h1, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 5n, {==}, hk5b))  +hi1 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(5n)) == True{} : Bool}, 1n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), ei1), hk5)  +ei2 = W32.inc_val(one, h1, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), W32.bound32(one, h1, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 5n, {==}, hi1))  +ea0 = Equal.trans(Nat, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 2n), 1n+Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 1n), 2n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), N.add_succ(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 1n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 1n), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), Equal.trans(Nat, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 1n), 1n+Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 0n), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), N.add_succ(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 0n), UD.v(W32.nth0(AR.slots(U32, mT), 7n)), N.add_zero(UD.v(W32.nth0(AR.slots(U32, mT), 7n)))))))  +hb2 = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, 1n+UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 2n), Equal.trans(Nat, 1n+UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 2n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 2n), Equal.cong(Nat, Nat, z => 1n+z, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), ei1), Equal.sym(Nat, Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 2n), 2n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), ea0)), W32.bound32(one, h1, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 5n, {==}, hi1))  +ea = ID.add_val(one, h1, W32.nth0(AR.slots(U32, mT), 7n), 2, hb2)  +es = Equal.trans(Nat, UD.v(U32.add(W32.nth0(AR.slots(U32, mT), 7n), 2)), 2n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), UD.v(U32.inc(U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), Equal.trans(Nat, UD.v(U32.add(W32.nth0(AR.slots(U32, mT), 7n), 2)), Nat.add(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 2n), 2n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), ea, ea0), Equal.sym(Nat, UD.v(U32.inc(U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), 2n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), Equal.trans(Nat, UD.v(U32.inc(U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), 1n+UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 2n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), ei2, Equal.cong(Nat, Nat, z => 1n+z, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), ei1))))  Equal.cong(Nat, Array<U32>, d => H.mv_fin(H.mv_go(U32.to_nat(U32.inc(CY.msk(k))), 0, U32.inc(U32.shl(CY.msk(k))), H.MV{AR.thaw(U32, tabT), Array.new(U32, d, 0)})), UD.v(U32.add(W32.nth0(AR.slots(U32, mT), 7n), 2)), UD.v(U32.inc(U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), es)# the grown state, for any mask (kept symbolic so nothing unfolds)def gtb(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +KT: AR.Tree<String>, +ET: AR.Tree<Maybe<&2, V>>, +LT: AR.Tree<U32>, +TT: AR.Tree<U32>, +mask: U32, +MT: AR.Tree<U32>, +bits: U32, +er: {Array.get(U32, AR.thaw(U32, MT), 7) == (AR.thaw(U32, MT), bits) : Array<U32> & U32}, +XT: AR.Tree<U32>, +YT: AR.Tree<U32>, +ex: {Array.set(U32, Array.set(U32, AR.thaw(U32, MT), 6, U32.inc(U32.shl(mask))), 7, U32.inc(bits)) == AR.thaw(U32, XT) : Array<U32>}, +ey: {H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, U32.inc(U32.shl(mask)), H.MV{AR.thaw(U32, TT), Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})) == AR.thaw(U32, YT) : Array<U32>}) -> {LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), LR.grow_tab(AR.thaw(U32, MT), AR.thaw(U32, TT), mask, True{})) == LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (AR.thaw(U32, XT), AR.thaw(U32, YT))) : LR.LRU<&2, V>}:  +e1 = Equal.cong(Array<U32> & U32, LR.LRU<&2, V>, z => LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), LR.grow_tab_b(AR.thaw(U32, TT), mask, z)), Array.get(U32, AR.thaw(U32, MT), 7), (AR.thaw(U32, MT), bits), er)  +e2 = Equal.cong(Array<U32>, LR.LRU<&2, V>, z => LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (z, H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, U32.inc(U32.shl(mask)), H.MV{AR.thaw(U32, TT), Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})))), Array.set(U32, Array.set(U32, AR.thaw(U32, MT), 6, U32.inc(U32.shl(mask))), 7, U32.inc(bits)), AR.thaw(U32, XT), ex)  +e3 = Equal.cong(Array<U32>, LR.LRU<&2, V>, z => LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (AR.thaw(U32, XT), z)), H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, U32.inc(U32.shl(mask)), H.MV{AR.thaw(U32, TT), Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})), AR.thaw(U32, YT), ey)  Equal.trans(LR.LRU<&2, V>, LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), LR.grow_tab(AR.thaw(U32, MT), AR.thaw(U32, TT), mask, True{})), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (Array.set(U32, Array.set(U32, AR.thaw(U32, MT), 6, U32.inc(U32.shl(mask))), 7, U32.inc(bits)), H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, U32.inc(U32.shl(mask)), H.MV{AR.thaw(U32, TT), Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})))), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (AR.thaw(U32, XT), AR.thaw(U32, YT))), e1, Equal.trans(LR.LRU<&2, V>, LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (Array.set(U32, Array.set(U32, AR.thaw(U32, MT), 6, U32.inc(U32.shl(mask))), 7, U32.inc(bits)), H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, U32.inc(U32.shl(mask)), H.MV{AR.thaw(U32, TT), Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})))), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (AR.thaw(U32, XT), H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, U32.inc(U32.shl(mask)), H.MV{AR.thaw(U32, TT), Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})))), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, KT), AR.thaw(Maybe<&2, V>, ET), AR.thaw(U32, LT), (AR.thaw(U32, XT), AR.thaw(U32, YT))), e2, e3))def rm_g3(~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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cz)) == True{} : Bool}, +hov: {Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +htd: {UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))) == 1n+k : Nat}, -r: LR.LRU<&2, V>, +T2: AR.Tree<U32>, +hr: {GR.rinv(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k)) == True{} : Bool}, +erl: {r == ST.real(~V, ST.LS{cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+k, sd, T2, ksT, eT, lkT, sl, fl}) : LR.LRU<&2, V>}) -> RoomOK(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, r):  +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, fl, hg))  +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==})  +hk0 = L.and_right(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, fl, 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, fl, hg)  +a1 = UT.uset_a(5n, {==}, mT, pm, 6, {==}, U32.inc(U32.shl(CY.msk(k))))  +p1 = UT.uset_p(5n, mT, pm, 6n, U32.inc(U32.shl(CY.msk(k))))  +hs1 = UT.uset_s(5n, mT, pm, 6n, {==}, U32.inc(U32.shl(CY.msk(k))))  +a2 = UT.uset_a(5n, {==}, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), p1, 7, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))  +p2 = UT.uset_p(5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), p1, 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))  +hs2 = UT.uset_s(5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), p1, 7n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))  +lt = N.not_le_lt(Nat.double(1n+UD.v(n)), SC.pow2(k), IU.gt_true_nle(Nat.double(1n+UD.v(n)), SC.pow2(k), hov))  +hk29 = L.subst(Nat, z => {Nat.is_lt(k, z) == True{} : Bool}, cz, 29n, hcz, IG.pow2_lt_inv(k, cz, N.lt_le_trans(SC.pow2(k), Nat.double(1n+UD.v(n)), SC.pow2(cz), lt, hcap)))  +hck = L.and_intro(Nat.is_lt(1n+k, 30n), Nat.is_lt(0n, 1n+k), hk29, {==})  +hsdk = N.lt_trans(sd, k, 1n+k, ST.g_csdk(~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, fl, hg), N.lt_succ(k))  +hbits = L.subst(Nat, z => {Nat.is_eq(z, 1n+k) == True{} : Bool}, 1n+k, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), Equal.sym(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+k, htd), N.is_eq_refl(1n+k))  +eo = Equal.trans(Nat, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(TB.buckets(AR.slots(U32, T2), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), 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, fl, hg)), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, T2), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, T2), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), GR.r_5(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k), hr))))  +hcn = L.subst(Nat, z => {Nat.is_eq(UD.v(n), z) == True{} : Bool}, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, T2), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(1n+k)), eo, N.is_eq_refl(UD.v(n)))  +hld2 = N.le_trans(Nat.double(UD.v(n)), SC.pow2(k), SC.pow2(1n+k), 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, fl, hg), N.lt_le(SC.pow2(k), SC.pow2(1n+k), N.pow2_lt_succ(k)))  +gx = ST.good_intro(~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), CY.msk(1n+k), U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), True{}, 1n+k, sd, T2, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hck, hsdk, GR.r_1(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k), hr), 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, fl, hg), 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, fl, hg), 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, fl, hg), {==}, A.eq_refl(CY.msk(1n+k)), hbits, 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, fl, hg), 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, fl, hg), 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, fl, hg), GR.r_3(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k), hr), GR.r_2(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k), hr), GR.r_4(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k), hr), hcn, hld2, 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, fl, hg), TS.bsl_from(TB.buckets(AR.slots(U32, T2), AR.slots(String, ksT), SC.pow2(1n+k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(1n+k), GR.r_6(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k), hr), sl, AR.slots(U32, lkT), 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, fl, hg)), TS.has_to(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, T2), AR.slots(String, ksT), SC.pow2(1n+k)), SC.pow2(k), SC.pow2(1n+k), GR.r_7(tabT, AR.slots(String, ksT), k, sd, T2, SC.pow2(k), hr), AR.slots(U32, lkT), sl, 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, fl, hg)), 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, fl, 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, fl, 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, fl, 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, fl, 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, fl, hg), 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, fl, hg), 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, fl, 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, fl, hg), ST.g_cfll(~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, fl, hg), 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, fl, hg), ST.g_cfnd(~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, fl, 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, fl, hg))  +e6 = Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), 6n), W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))), 6n), CY.msk(1n+k), MT.nth_other(AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), hs2, 6n, {==}), Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))), 6n), U32.inc(U32.shl(CY.msk(k))), CY.msk(1n+k), MT.nth_same(5n, mT, pm, 6n, {==}, U32.inc(U32.shl(CY.msk(k))), AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), hs1), GR.msk_up(one, h1, k, hk31)))  +e7 = MT.nth_same(5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), p1, 7n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), hs2)  +g = good_mk(~V, cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), CY.msk(1n+k), U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), 1n+k, sd, T2, ksT, eT, lkT, sl, fl, gx, oth2(mT, k, hs1, hs2, 0n, {==}, {==}), oth2(mT, k, hs1, hs2, 1n, {==}, {==}), oth2(mT, k, hs1, hs2, 2n, {==}, {==}), e6, e7, p2)  +hro = N.double_le(1n+UD.v(n), SC.pow2(k), IU.over_c(one, h1, k, hk31, hk0, UD.v(n), 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, fl, hg)))  mk_room(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, r, ST.LS{cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+k, sd, T2, ksT, eT, lkT, sl, fl}, erl, model_m(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, T2, hs1, hs2), g, hro)def rm_g2(~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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cz)) == True{} : Bool}, +hov: {Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +htd: {UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))) == 1n+k : Nat}, -r: LR.LRU<&2, V>, +hr0: {r == LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), True{})) : LR.LRU<&2, V>}, go: GR.GrowOK(tabT, AR.slots(String, ksT), k, sd, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))) -> RoomOK(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, r):  match go:    case Tuple{+T2, Tuple{+e0, hr}}:      +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, fl, hg)      +G7 = UT.uget(5n, {==}, mT, pm, 7, {==})      +a1 = UT.uset_a(5n, {==}, mT, pm, 6, {==}, U32.inc(U32.shl(CY.msk(k))))      +p1 = UT.uset_p(5n, mT, pm, 6n, U32.inc(U32.shl(CY.msk(k))))      +hs1 = UT.uset_s(5n, mT, pm, 6n, {==}, U32.inc(U32.shl(CY.msk(k))))      +a2 = UT.uset_a(5n, {==}, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), p1, 7, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))      +p2 = UT.uset_p(5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), p1, 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))      +hs2 = UT.uset_s(5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), p1, 7n, {==}, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))      +eM = Equal.trans(Array<U32>, Array.set(U32, Array.set(U32, AR.thaw(U32, mT), 6, U32.inc(U32.shl(CY.msk(k)))), 7, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), Array.set(U32, AR.thaw(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))), 7, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), AR.thaw(U32, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)))), Equal.cong(Array<U32>, Array<U32>, z => Array.set(U32, z, 7, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), Array.set(U32, AR.thaw(U32, mT), 6, U32.inc(U32.shl(CY.msk(k)))), AR.thaw(U32, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k))))), a1), a2)      +eTb = Equal.trans(Array<U32>, H.mv_fin(H.mv_go(U32.to_nat(U32.inc(CY.msk(k))), 0, U32.inc(U32.shl(CY.msk(k))), H.MV{AR.thaw(U32, tabT), Array.new(U32, U32.to_nat(U32.add(W32.nth0(AR.slots(U32, mT), 7n), 2)), 0)})), H.grow_tab(CY.msk(k), U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), AR.thaw(U32, tabT)), AR.thaw(U32, T2), tg_eq(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1), e0)      +er = gtb(~V, cap, n, head, tail, free, ksT, eT, lkT, tabT, CY.msk(k), mT, W32.nth0(AR.slots(U32, mT), 7n), G7, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), T2, eM, eTb)      rm_g3(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, cz, hcz, hcap, hov, htd, r, T2, hr, Equal.trans(LR.LRU<&2, V>, r, LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), True{})), ST.real(~V, ST.LS{cap, n, head, tail, free, AR.upd(U32, 5n, AR.upd(U32, 5n, mT, 6n, U32.inc(U32.shl(CY.msk(k)))), 7n, U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+k, sd, T2, ksT, eT, lkT, sl, fl}), hr0, er))def rm_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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cz)) == True{} : Bool}, +hov: {Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}) -> RoomOK(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), True{}))):  +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, fl, hg))  +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==})  +hk0 = L.and_right(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, fl, hg))  +ek = N.eq_from_is_eq(UD.v(W32.nth0(AR.slots(U32, mT), 7n)), k, 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, fl, hg))  +hk5b = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(5n)) == True{} : Bool}, k, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), Equal.sym(Nat, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), k, ek), N.lt_trans(k, 30n, 32n, hk30, {==}))  +htd = Equal.trans(Nat, UD.v(U32.inc(W32.nth0(AR.slots(U32, mT), 7n))), 1n+UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 1n+k, W32.inc_val(one, h1, W32.nth0(AR.slots(U32, mT), 7n), W32.bound32(one, h1, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), 5n, {==}, hk5b)), Equal.cong(Nat, Nat, z => 1n+z, UD.v(W32.nth0(AR.slots(U32, mT), 7n)), k, ek))  +hlen = 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, fl, hg))  +hld = L.subst(Nat, z => {Nat.is_le(Nat.double(z), SC.pow2(k)) == True{} : Bool}, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), 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, fl, 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, fl, hg))  rm_g2(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, cz, hcz, hcap, hov, htd, LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), True{})), {==}, GR.grow_ok(one, h1, k, hk31, hk30, hk0, tabT, 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, fl, hg), AR.slots(String, ksT), sd, hlen, 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, fl, hg), 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, fl, hg), hld, U32.inc(W32.nth0(AR.slots(U32, mT), 7n)), htd))def rm_b(~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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cz)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)) == b : Bool}) -> RoomOK(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), b))):  match b:    case True{}:      rm_grow(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, cz, hcz, hcap, hb)    case False{}:      (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, ({==}, ({==}, (hg, IU.gt_false_le(Nat.double(1n+UD.v(n)), SC.pow2(k), hb)))))def room_f(~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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cz)) == True{} : Bool}) -> RoomOK(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, LR.room(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))):  +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, fl, hg))  +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==})  +hk0 = L.and_right(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, fl, hg))  +G6 = Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 6n)), (AR.thaw(U32, mT), CY.msk(k)), UT.uget(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, fl, hg), 6, {==}), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, mT), z), W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), A.eq_of(W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), 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, fl, hg))))  +E1 = Equal.cong(Array<U32> & U32, LR.LRU<&2, V>, r => LR.room_m(&2, V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), G6)  +E2 = Equal.cong(Bool, LR.LRU<&2, V>, b => LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), b)), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), IU.over_val(one, h1, k, hk31, hk0, n, 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, fl, hg)))  +E = Equal.trans(LR.LRU<&2, V>, LR.room(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))))), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)))), E1, E2)  L.subst(LR.LRU<&2, V>, z => RoomOK(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, z), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)))), LR.room(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), Equal.sym(LR.LRU<&2, V>, LR.room(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), LR.room_fin(&2, V, cap, n, head, tail, free, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), LR.grow_tab(AR.thaw(U32, mT), AR.thaw(U32, tabT), CY.msk(k), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)))), E), rm_b(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, cz, hcz, hcap, Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), {==}))# the state can take one more entry within 2^29 bucketsdef capok(~V: Data, sh: ST.Sh<V>, +cz: Nat) -> Bool:  match sh:    case ST.LS{+cap, +n, +head, +tail, +free, +mT, +k, +sd, +tabT, +ksT, +eT, +lkT, +sl, +fl}:      Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cz))# THEOREM: room keeps the model and the invariant and leaves room for one moredef room_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hcap: {capok(~V, sh, cz) == True{} : Bool}) -> RoomOK(~V, sh, LR.room(&2, V, ST.real(~V, sh))):  match sh:    case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}:      room_f(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, cz, hcz, hcap)