proofs/containers/hash_table/grow.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../lib/u32alg.bend as Aimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../lib/word.bend as WDimport ../../lib/u32div.bend as UDimport ../../../src/math/hash.bend as HSimport ../../../src/containers/hash_table.bend as Himport ./keys.bend as Kimport ./table.bend as TBimport ./buckets.bend as Bimport ./modn.bend as Mimport ./cyc.bend as CYimport ./arr.bend as AXimport ./inv.bend as IVimport ./state.bend as STimport ./probe_all.bend as PAimport ./insm.bend as IMimport ./insa.bend as IAimport ./rawins.bend as RIimport ./rehash.bend as RHimport ./insert.bend as ISimport ../../lib/words32.bend as W32# Growing the table: grow_tab moves every full old bucket into a table of# twice the buckets; the result holds copies of exactly the old buckets and# keeps the table invariants.def mskv(+k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}) -> {Nat.add(UD.v(CY.msk(k)), 1n) == SC.pow2(k) : Nat}:  Equal.trans(Nat, Nat.add(UD.v(CY.msk(k)), 1n), Nat.add(WD.uw(32n, WD.mask(32n, k)), 1n), SC.pow2(k), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), UD.v(CY.msk(k)), WD.uw(32n, WD.mask(32n, k)), UD.vw(WD.mask(32n, k))), PA.mask_val(32n, k, hk))# THEOREM: the grown mask is the mask of twice the bucketsdef msk_up(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, 31n) == True{} : Bool}) -> {U32.inc(U32.shl(CY.msk(k))) == CY.msk(1n+k) : U32}:  +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk, {==}))  +a0 = mskv(k, hk32)  +v0lt = L.subst(Nat, z => {Nat.is_lt(UD.v(CY.msk(k)), z) == True{} : Bool}, Nat.add(UD.v(CY.msk(k)), 1n), SC.pow2(k), a0, L.subst(Nat, z => {Nat.is_lt(UD.v(CY.msk(k)), z) == True{} : Bool}, 1n+UD.v(CY.msk(k)), Nat.add(UD.v(CY.msk(k)), 1n), Equal.sym(Nat, Nat.add(UD.v(CY.msk(k)), 1n), 1n+UD.v(CY.msk(k)), N.add_comm(UD.v(CY.msk(k)), 1n)), N.lt_succ(UD.v(CY.msk(k)))))  +es = U.shl_value(CY.msk(k), 1n+k, N.lt_le(1n+k, 32n, hk), N.double_lt(UD.v(CY.msk(k)), SC.pow2(k), v0lt))  +hb = L.subst(Nat, z => {Nat.is_lt(1n+z, WD.sc(32n, one)) == True{} : Bool}, Nat.double(UD.v(CY.msk(k))), UD.v(U32.shl(CY.msk(k))), Equal.sym(Nat, UD.v(U32.shl(CY.msk(k))), Nat.double(UD.v(CY.msk(k))), es), N.lt_le_trans(1n+Nat.double(UD.v(CY.msk(k))), SC.pow2(1n+k), WD.sc(32n, one), N.double_lt_bit(True{}, UD.v(CY.msk(k)), SC.pow2(k), v0lt), W32.pow_le32(one, h1, 1n+k, hk)))  +ei = Equal.trans(Nat, UD.v(U32.inc(U32.shl(CY.msk(k)))), 1n+UD.v(U32.shl(CY.msk(k))), 1n+Nat.double(UD.v(CY.msk(k))), W32.inc_val(one, h1, U32.shl(CY.msk(k)), hb), Equal.cong(Nat, Nat, z => 1n+z, UD.v(U32.shl(CY.msk(k))), Nat.double(UD.v(CY.msk(k))), es))  +a1 = mskv(1n+k, N.lt_le(1n+k, 32n, hk))  +e2 = Equal.trans(Nat, Nat.add(UD.v(CY.msk(1n+k)), 1n), SC.pow2(1n+k), Nat.add(1n+Nat.double(UD.v(CY.msk(k))), 1n), a1, Equal.trans(Nat, Nat.double(SC.pow2(k)), Nat.double(Nat.add(UD.v(CY.msk(k)), 1n)), Nat.add(1n+Nat.double(UD.v(CY.msk(k))), 1n), Equal.cong(Nat, Nat, z => Nat.double(z), SC.pow2(k), Nat.add(UD.v(CY.msk(k)), 1n), Equal.sym(Nat, Nat.add(UD.v(CY.msk(k)), 1n), SC.pow2(k), a0)), Equal.sym(Nat, Nat.add(1n+Nat.double(UD.v(CY.msk(k))), 1n), Nat.double(Nat.add(UD.v(CY.msk(k)), 1n)), PA.dbl_step(UD.v(CY.msk(k))))))  +e3 = A.add_cancel_r(UD.v(CY.msk(1n+k)), 1n+Nat.double(UD.v(CY.msk(k))), 1n, e2)  U.injective(U32.inc(U32.shl(CY.msk(k))), CY.msk(1n+k), Equal.trans(Nat, UD.v(U32.inc(U32.shl(CY.msk(k)))), 1n+Nat.double(UD.v(CY.msk(k))), UD.v(CY.msk(1n+k)), ei, Equal.sym(Nat, UD.v(CY.msk(1n+k)), 1n+Nat.double(UD.v(CY.msk(k))), e3)))# ---- writing one bucket of a tree ----def p_ev(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {UD.v(U32.from_nat(e)) == e : Nat}:  U.to_nat_from_nat(e, K, N.lt_le(K, 32n, N.lt_trans(K, 31n, 32n, hK, {==})), he)def p_h(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {Nat.is_lt(1n+Nat.double(UD.v(U32.from_nat(e))), SC.pow2(1n+K)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+K)) == True{} : Bool}, e, UD.v(U32.from_nat(e)), Equal.sym(Nat, UD.v(U32.from_nat(e)), e, p_ev(K, hK, T, pt, e, he, w, l)), N.double_lt_bit(True{}, e, SC.pow2(K), he))def p_i1(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {UD.v(U32.shl(U32.from_nat(e))) == Nat.double(e) : Nat}:  Equal.trans(Nat, UD.v(U32.shl(U32.from_nat(e))), Nat.double(UD.v(U32.from_nat(e))), Nat.double(e), AX.ix_w(U32.from_nat(e), 1n+K, hK, p_h(K, hK, T, pt, e, he, w, l)), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(U32.from_nat(e)), e, p_ev(K, hK, T, pt, e, he, w, l)))def p_i2(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {UD.v(U32.inc(U32.shl(U32.from_nat(e)))) == 1n+Nat.double(e) : Nat}:  Equal.trans(Nat, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), 1n+Nat.double(UD.v(U32.from_nat(e))), 1n+Nat.double(e), AX.ix_l(U32.from_nat(e), 1n+K, hK, p_h(K, hK, T, pt, e, he, w, l)), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), UD.v(U32.from_nat(e)), e, p_ev(K, hK, T, pt, e, he, w, l)))def p_h1(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {Nat.is_lt(UD.v(U32.shl(U32.from_nat(e))), SC.pow2(1n+K)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+K)) == True{} : Bool}, Nat.double(e), UD.v(U32.shl(U32.from_nat(e))), Equal.sym(Nat, UD.v(U32.shl(U32.from_nat(e))), Nat.double(e), p_i1(K, hK, T, pt, e, he, w, l)), N.lt_trans(Nat.double(e), 1n+Nat.double(e), SC.pow2(1n+K), N.lt_succ(Nat.double(e)), N.double_lt_bit(True{}, e, SC.pow2(K), he)))def p_h2(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {Nat.is_lt(UD.v(U32.inc(U32.shl(U32.from_nat(e)))), SC.pow2(1n+K)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+K)) == True{} : Bool}, 1n+Nat.double(e), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), 1n+Nat.double(e), p_i2(K, hK, T, pt, e, he, w, l)), N.double_lt_bit(True{}, e, SC.pow2(K), he))def put_perf(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {AR.perfect(U32, 1n+K, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) == True{} : Bool}:  AR.upd_perfect(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l, AR.upd_perfect(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w, pt))# THEOREM: writing bucket e is the tree update at 2e and 2e + 1def put_eq(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {H.put_bucket(AR.thaw(U32, T), U32.from_nat(e), w, l) == AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) : Array<U32>}:  +p1 = AR.upd_perfect(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w, pt)  +s1 = AR.set(U32, 1n+K, T, U32.shl(U32.from_nat(e)), w, W32.nth0(AR.slots(U32, T), UD.v(U32.shl(U32.from_nat(e)))), hK, p_h1(K, hK, T, pt, e, he, w, l), W32.nth_some(AR.slots(U32, T), UD.v(U32.shl(U32.from_nat(e))), IS.len_lt(U32, 1n+K, T, pt, UD.v(U32.shl(U32.from_nat(e))), p_h1(K, hK, T, pt, e, he, w, l))), pt)  +s2 = AR.set(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), U32.inc(U32.shl(U32.from_nat(e))), l, W32.nth0(AR.slots(U32, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w)), UD.v(U32.inc(U32.shl(U32.from_nat(e))))), hK, p_h2(K, hK, T, pt, e, he, w, l), W32.nth_some(AR.slots(U32, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), IS.len_lt(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), p1, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), p_h2(K, hK, T, pt, e, he, w, l))), p1)  Equal.trans(Array<U32>, H.put_bucket(AR.thaw(U32, T), U32.from_nat(e), w, l), Array.set(U32, AR.thaw(U32, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w)), U32.inc(U32.shl(U32.from_nat(e))), l), AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)), Equal.cong(Array<U32>, Array<U32>, a => Array.set(U32, a, U32.inc(U32.shl(U32.from_nat(e))), l), Array.set(U32, AR.thaw(U32, T), U32.shl(U32.from_nat(e)), w), AR.thaw(U32, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w)), s1), s2)def put_slots(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32) -> {AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) == SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l) : List<&2, U32>}:  +p1 = AR.upd_perfect(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w, pt)  +e1 = AR.upd_slots(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l, p_h2(K, hK, T, pt, e, he, w, l), p1)  +e2 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l), AR.slots(U32, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w)), SC.update(U32, AR.slots(U32, T), UD.v(U32.shl(U32.from_nat(e))), w), AR.upd_slots(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w, p_h1(K, hK, T, pt, e, he, w, l), pt))  +e3 = Equal.cong(Nat, List<&2, U32>, z => SC.update(U32, SC.update(U32, AR.slots(U32, T), z, w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l), UD.v(U32.shl(U32.from_nat(e))), Nat.double(e), p_i1(K, hK, T, pt, e, he, w, l))  +e4 = Equal.cong(Nat, List<&2, U32>, z => SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), z, l), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), 1n+Nat.double(e), p_i2(K, hK, T, pt, e, he, w, l))  Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)), SC.update(U32, AR.slots(U32, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l), SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), e1, Equal.trans(List<&2, U32>, SC.update(U32, AR.slots(U32, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l), SC.update(U32, SC.update(U32, AR.slots(U32, T), UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l), SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), e2, Equal.trans(List<&2, U32>, SC.update(U32, SC.update(U32, AR.slots(U32, T), UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l), SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l), SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), e3, e4)))# THEOREM: the written tree decodes to the buckets with bucket e filled, the# key read from the unchanged arenadef put_bs(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(K)) == True{} : Bool}, +w: U32, +l: U32, +kl: List<&2, String>, +n: Nat, +hns: {ST.noslot(TB.buckets(AR.slots(U32, T), kl, n), UD.v(H.slot(l)), n) == True{} : Bool}, +hw0: {U32.is_eq(w, 0) == False{} : Bool}, +hkl: {Nat.is_lt(UD.v(H.slot(l)), SC.length(String, kl)) == True{} : Bool}) -> {TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)), kl, n) == IM.bupd(TB.buckets(AR.slots(U32, T), kl, n), e, B.BF{w, l, TB.keyof(w, TB.nths(kl, UD.v(H.slot(l))))}) : List<&2, B.Bk>}:  +htb = IS.len_lt(U32, 1n+K, T, pt, 1n+Nat.double(e), N.double_lt_bit(True{}, e, SC.pow2(K), he))  +bp = IA.buckets_put(AR.slots(U32, T), kl, e, w, l, TB.nths(kl, UD.v(H.slot(l))), n, hns, hw0, htb, hkl)  +ek = TB.upd_self(kl, UD.v(H.slot(l)))  Equal.trans(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)), kl, n), TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), kl, n), IM.bupd(TB.buckets(AR.slots(U32, T), kl, n), e, B.BF{w, l, TB.keyof(w, TB.nths(kl, UD.v(H.slot(l))))}), Equal.cong(List<&2, U32>, List<&2, B.Bk>, z => TB.buckets(z, kl, n), AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), l)), SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), put_slots(K, hK, T, pt, e, he, w, l)), Equal.trans(List<&2, B.Bk>, TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), kl, n), TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), SC.update(String, kl, UD.v(H.slot(l)), TB.nths(kl, UD.v(H.slot(l)))), n), IM.bupd(TB.buckets(AR.slots(U32, T), kl, n), e, B.BF{w, l, TB.keyof(w, TB.nths(kl, UD.v(H.slot(l))))}), Equal.cong(List<&2, String>, List<&2, B.Bk>, z => TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(e), w), 1n+Nat.double(e), l), z, n), kl, SC.update(String, kl, UD.v(H.slot(l)), TB.nths(kl, UD.v(H.slot(l)))), Equal.sym(List<&2, String>, SC.update(String, kl, UD.v(H.slot(l)), TB.nths(kl, UD.v(H.slot(l)))), kl, ek)), bp))# ---- the empty table ----def nth0_rep(+m: Nat, +x: Nat) -> {W32.nth0(SC.replicate(U32, m, 0), x) == 0 : U32}:  match m x:    case 0n _:      {==}    case 1n+p 0n:      {==}    case 1n+p 1n+q:      nth0_rep(p, q)def nth0_z(+d: Nat, +x: Nat) -> {W32.nth0(AR.slots(U32, AR.trep(U32, d, 0)), x) == 0 : U32}:  Equal.trans(U32, W32.nth0(AR.slots(U32, AR.trep(U32, d, 0)), x), W32.nth0(SC.replicate(U32, SC.pow2(d), 0), x), 0, Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, x), AR.slots(U32, AR.trep(U32, d, 0)), SC.replicate(U32, SC.pow2(d), 0), AR.trep_slots(U32, d, 0)), nth0_rep(SC.pow2(d), x))def at_z(+d: Nat, +kl: List<&2, String>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), i) == B.BE{} : B.Bk}:  Equal.trans(B.Bk, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), i), TB.dec(AR.slots(U32, AR.trep(U32, d, 0)), kl, i), B.BE{}, TB.at_buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n, i, hi), Equal.cong(U32, B.Bk, a => TB.dec_c(a, W32.nth0(AR.slots(U32, AR.trep(U32, d, 0)), 1n+Nat.double(i)), kl, U32.is_eq(a, 0)), W32.nth0(AR.slots(U32, AR.trep(U32, d, 0)), Nat.double(i)), 0, nth0_z(d, Nat.double(i))))def z_clus(+d: Nat, +kl: List<&2, String>, +n: Nat, +mask: U32, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PClus{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), n, mask}, m) == True{} : Bool}:  match m:    case 0n:      {==}    case 1n+q:      +hq = N.succ_le_lt(q, n, hm)      L.and_intro(B.eval(B.PClus{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), n, mask}, q), B.all_lt(B.PClus{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), n, mask}, q), L.subst(B.Bk, x => {B.implies(B.occ(x), B.occpath(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), n, B.hb(mask, x), M.dist(n, B.hb(mask, x), q))) == True{} : Bool}, B.BE{}, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), Equal.sym(B.Bk, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), B.BE{}, at_z(d, kl, n, q, hq)), {==}), z_clus(d, kl, n, mask, q, N.lt_le(q, n, hq)))def z_well(+d: Nat, +kl: List<&2, String>, +n: Nat, +sd: Nat, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), sd}, m) == True{} : Bool}:  match m:    case 0n:      {==}    case 1n+q:      +hq = N.succ_le_lt(q, n, hm)      L.and_intro(B.eval(B.PWell{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), sd}, q), B.all_lt(B.PWell{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), sd}, q), L.subst(B.Bk, x => {B.wb(sd, x) == True{} : Bool}, B.BE{}, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), Equal.sym(B.Bk, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), B.BE{}, at_z(d, kl, n, q, hq)), {==}), z_well(d, kl, n, sd, q, N.lt_le(q, n, hq)))def z_uniq(+d: Nat, +kl: List<&2, String>, +n: Nat, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n)}, m) == True{} : Bool}:  match m:    case 0n:      {==}    case 1n+q:      +hq = N.succ_le_lt(q, n, hm)      L.and_intro(B.eval(B.PUniq{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n)}, q), B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n)}, q), L.subst(B.Bk, x => {B.uq_b(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q, x) == True{} : Bool}, B.BE{}, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), Equal.sym(B.Bk, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), B.BE{}, at_z(d, kl, n, q, hq)), {==}), z_uniq(d, kl, n, q, N.lt_le(q, n, hq)))def z_from(+d: Nat, +kl: List<&2, String>, +n: Nat, +src: List<&2, B.Bk>, +j: Nat, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), src, j}, m) == True{} : Bool}:  match m:    case 0n:      {==}    case 1n+q:      +hq = N.succ_le_lt(q, n, hm)      L.and_intro(B.eval(B.PFrom{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), src, j}, q), B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), src, j}, q), L.subst(B.Bk, x => {B.implies(B.occ(x), B.anyeq(src, j, x)) == True{} : Bool}, B.BE{}, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), Equal.sym(B.Bk, B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), B.BE{}, at_z(d, kl, n, q, hq)), {==}), z_from(d, kl, n, src, j, q, N.lt_le(q, n, hq)))def z_occn(+d: Nat, +kl: List<&2, String>, +n: Nat, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {IV.occn(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), m) == 0n : Nat}:  match m:    case 0n:      {==}    case 1n+q:      +hq = N.succ_le_lt(q, n, hm)      Equal.trans(Nat, Nat.add(IV.bitv(B.occ(B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q))), IV.occn(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q)), Nat.add(IV.bitv(B.occ(B.BE{})), IV.occn(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q)), 0n, Equal.cong(B.Bk, Nat, x => Nat.add(IV.bitv(B.occ(x)), IV.occn(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q)), B.at(TB.buckets(AR.slots(U32, AR.trep(U32, d, 0)), kl, n), q), B.BE{}, at_z(d, kl, n, q, hq)), z_occn(d, kl, n, q, N.lt_le(q, n, hq)))# the rehash loop invariant after moving old buckets 0 .. j - 1def rinv(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat) -> Bool:  Bool.and(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))))def r_1(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {AR.perfect(U32, 2n+k, NT) == True{} : Bool}:  L.and_left(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h)def r_2(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)) == True{} : Bool}:  L.and_left(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))))), L.and_right(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h))def r_3(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)) == True{} : Bool}:  L.and_left(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))))), L.and_right(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h)))def r_4(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)) == True{} : Bool}:  L.and_left(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))), L.and_right(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))))), L.and_right(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h))))def r_5(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)) == True{} : Bool}:  L.and_left(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))), L.and_right(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))))), L.and_right(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h)))))def r_6(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)) == True{} : Bool}:  L.and_left(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j), L.and_right(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))), L.and_right(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))))), L.and_right(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h))))))def r_7(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j) == True{} : Bool}:  L.and_right(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j), L.and_right(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))), L.and_right(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))))), L.and_right(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h))))))def r_mk(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree<U32>, +j: Nat, +h1: {AR.perfect(U32, 2n+k, NT) == True{} : Bool}, +h2: {B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)) == True{} : Bool}, +h3: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)) == True{} : Bool}, +h4: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)) == True{} : Bool}, +h5: {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)) == True{} : Bool}, +h6: {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)) == True{} : Bool}, +h7: {B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j) == True{} : Bool}) -> {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}:  L.and_intro(AR.perfect(U32, 2n+k, NT), Bool.and(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))))), h1, L.and_intro(B.cluster(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), CY.msk(1n+k)), Bool.and(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))))), h2, L.and_intro(B.all_lt(B.PWell{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), sd}, SC.pow2(1n+k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)))), h3, L.and_intro(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))}, SC.pow2(1n+k)), Bool.and(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j))), h4, L.and_intro(Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j)), h5, L.and_intro(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j}, SC.pow2(1n+k)), B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)}, j), h6, h7))))))# ---- one step of the move loop ----def StepOK(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +j: Nat, +kk: U32, +NT: AR.Tree<U32>) -> Type:  Sigma<&1, &1, AR.Tree<U32>, T2 => {H.mv_step(kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}) == H.MV{AR.thaw(U32, OT), AR.thaw(U32, T2)} : H.Mv} & {rinv(OT, kl, k, sd, T2, 1n+j) == True{} : Bool}>def s_hh(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {Nat.is_lt(1n+Nat.double(UD.v(kk)), SC.pow2(1n+k)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+k)) == True{} : Bool}, j, UD.v(kk), Equal.sym(Nat, UD.v(kk), j, hkk), N.double_lt_bit(True{}, j, SC.pow2(k), hj))def s_ew(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {UD.v(U32.shl(kk)) == Nat.double(j) : Nat}:  Equal.trans(Nat, UD.v(U32.shl(kk)), Nat.double(UD.v(kk)), Nat.double(j), AX.ix_w(kk, 1n+k, hk31, s_hh(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr)), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(kk), j, hkk))def s_el(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {UD.v(U32.inc(U32.shl(kk))) == 1n+Nat.double(j) : Nat}:  Equal.trans(Nat, UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(UD.v(kk)), 1n+Nat.double(j), AX.ix_l(kk, 1n+k, hk31, s_hh(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr)), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), UD.v(kk), j, hkk))def eqA(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {H.mv_step(kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}) == H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0)) : H.Mv}:  +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(j), UD.v(U32.shl(kk)), Equal.sym(Nat, UD.v(U32.shl(kk)), Nat.double(j), s_ew(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr)), N.lt_trans(Nat.double(j), 1n+Nat.double(j), SC.pow2(1n+k), N.lt_succ(Nat.double(j)), N.double_lt_bit(True{}, j, SC.pow2(k), hj)))  +ga = AX.getw(1n+k, OT, U32.shl(kk), hk31, hi, pot)  Equal.trans(H.Mv, H.mv_step(kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}), H.mv_w(kk, AR.thaw(U32, NT), CY.msk(1n+k), (AR.thaw(U32, OT), W32.nth0(AR.slots(U32, OT), UD.v(U32.shl(kk))))), H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0)), Equal.cong(Array<U32> & U32, H.Mv, r => H.mv_w(kk, AR.thaw(U32, NT), CY.msk(1n+k), r), Array.get(U32, AR.thaw(U32, OT), U32.shl(kk)), (AR.thaw(U32, OT), W32.nth0(AR.slots(U32, OT), UD.v(U32.shl(kk)))), ga), Equal.cong(Nat, H.Mv, z => H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), z), U32.is_eq(W32.nth0(AR.slots(U32, OT), z), 0)), UD.v(U32.shl(kk)), Nat.double(j), s_ew(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr)))def eqB(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), False{}) == H.MV{AR.thaw(U32, OT), H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))} : H.Mv}:  +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(j), UD.v(U32.inc(U32.shl(kk))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(j), s_el(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr)), N.double_lt_bit(True{}, j, SC.pow2(k), hj))  +gb = AX.getw(1n+k, OT, U32.inc(U32.shl(kk)), hk31, hi, pot)  Equal.trans(H.Mv, H.mv_l(W32.nth0(AR.slots(U32, OT), Nat.double(j)), AR.thaw(U32, NT), CY.msk(1n+k), Array.get(U32, AR.thaw(U32, OT), U32.inc(U32.shl(kk)))), H.mv_l(W32.nth0(AR.slots(U32, OT), Nat.double(j)), AR.thaw(U32, NT), CY.msk(1n+k), (AR.thaw(U32, OT), W32.nth0(AR.slots(U32, OT), UD.v(U32.inc(U32.shl(kk)))))), H.MV{AR.thaw(U32, OT), H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))}, Equal.cong(Array<U32> & U32, H.Mv, r => H.mv_l(W32.nth0(AR.slots(U32, OT), Nat.double(j)), AR.thaw(U32, NT), CY.msk(1n+k), r), Array.get(U32, AR.thaw(U32, OT), U32.inc(U32.shl(kk))), (AR.thaw(U32, OT), W32.nth0(AR.slots(U32, OT), UD.v(U32.inc(U32.shl(kk))))), gb), Equal.cong(Nat, H.Mv, z => H.MV{AR.thaw(U32, OT), H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), z))}, UD.v(U32.inc(U32.shl(kk))), 1n+Nat.double(j), s_el(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr)))def s_occ(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)) == Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0)) : Bool}:  RI.occ_flag(AR.slots(U32, OT), kl, SC.pow2(k), j, hj)# an empty old bucket: nothing movesdef step_skip(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0) == True{} : Bool}) -> StepOK(OT, kl, k, sd, j, kk, NT):  +ho = Equal.trans(Bool, B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0)), False{}, s_occ(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr), Equal.cong(Bool, Bool, b => Bool.not(b), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0), True{}, hc))  +e5 = Equal.trans(Nat, IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j), N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), r_5(OT, kl, k, sd, NT, j, hr)), Equal.cong(Bool, Nat, o => Nat.add(IV.bitv(o), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), False{}, B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), Equal.sym(Bool, B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), False{}, ho)))  +eq = Equal.trans(H.Mv, H.mv_step(kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}), H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0)), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}, eqA(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr), Equal.cong(Bool, H.Mv, c => H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), c), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0), True{}, hc))  (NT, (eq, r_mk(OT, kl, k, sd, NT, 1n+j, r_1(OT, kl, k, sd, NT, j, hr), r_2(OT, kl, k, sd, NT, j, hr), r_3(OT, kl, k, sd, NT, j, hr), r_4(OT, kl, k, sd, NT, j, hr), IS.eq_is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j), e5), RH.from_skip(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j, SC.pow2(1n+k), r_6(OT, kl, k, sd, NT, j, hr), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))), RH.to_skip(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), j, SC.pow2(1n+k), ho, r_7(OT, kl, k, sd, NT, j, hr)))))def s_hb(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0) == False{} : Bool}) -> {B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j) == B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))} : B.Bk}:  Equal.trans(B.Bk, B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), TB.dec(AR.slots(U32, OT), kl, j), B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, TB.at_buckets(AR.slots(U32, OT), kl, SC.pow2(k), j, hj), Equal.cong(Bool, B.Bk, c => TB.dec_c(W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), kl, c), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0), False{}, hc))def step_e(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0) == False{} : Bool}, +pno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, SC.pow2(1n+k)) == True{} : Bool}, +nsl: {ST.noslot(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), SC.pow2(1n+k)) == True{} : Bool}, fe: RI.FirstE(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), UD.v(HS.bucket(W32.nth0(AR.slots(U32, OT), Nat.double(j)), CY.msk(1n+k))))) -> StepOK(OT, kl, k, sd, j, kk, NT):  match fe:    case Tuple{+e, Tuple{+he, Tuple{+hz, hp0}}}:      +hp = {hp0 : {B.occpath(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), UD.v(HS.bucket(W32.nth0(AR.slots(U32, OT), Nat.double(j)), CY.msk(1n+k))), M.dist(SC.pow2(1n+k), UD.v(HS.bucket(W32.nth0(AR.slots(U32, OT), Nat.double(j)), CY.msk(1n+k))), e)) == True{} : Bool}}      +hb = s_hb(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, hc)      +hwb = L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, hb, B.all_inst(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k), hwo, j, hj))      +hkl = L.subst(Nat, z => {Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), z) == True{} : Bool}, SC.pow2(sd), SC.length(String, kl), Equal.sym(Nat, SC.length(String, kl), SC.pow2(sd), hlen), L.and_left(Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), SC.pow2(sd)), Bool.and(U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), K.kword(TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))))))), Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), 0))), hwb))      +rw = RI.raw_ok(one, h1, 1n+k, hk30, NT, r_1(OT, kl, k, sd, NT, j, hr), kl, W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), e, he, hz, hp)      +pe = put_eq(1n+k, hk30, NT, r_1(OT, kl, k, sd, NT, j, hr), e, he, W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))      +eq = Equal.trans(H.Mv, H.mv_step(kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}), H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0)), H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))}, eqA(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr), Equal.trans(H.Mv, H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0)), H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), False{}), H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))}, Equal.cong(Bool, H.Mv, c => H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), c), U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0), False{}, hc), Equal.trans(H.Mv, H.mv_if(kk, AR.thaw(U32, OT), AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), False{}), H.MV{AR.thaw(U32, OT), H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))}, H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))}, eqB(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr), Equal.cong(Array<U32>, H.Mv, a => H.MV{AR.thaw(U32, OT), a}, H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))), AR.thaw(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), Equal.trans(Array<U32>, H.ins_raw(AR.thaw(U32, NT), CY.msk(1n+k), W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))), H.put_bucket(AR.thaw(U32, NT), U32.from_nat(e), W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))), AR.thaw(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), rw, pe)))))      +bse = put_bs(1n+k, hk30, NT, r_1(OT, kl, k, sd, NT, j, hr), e, he, W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), kl, SC.pow2(1n+k), nsl, hc, hkl)      +hel = L.subst(Nat, z => {Nat.is_lt(e, z) == True{} : Bool}, SC.pow2(1n+k), SC.length(B.Bk, TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))), Equal.sym(Nat, SC.length(B.Bk, TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k))), SC.pow2(1n+k), IA.len_dlist(AR.slots(U32, NT), kl, SC.pow2(1n+k), 0n)), he)      +e5 = Equal.trans(Nat, IV.occn(IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), SC.pow2(1n+k)), 1n+IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j), IM.occn_up(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, {==}, hel, hz, SC.pow2(1n+k), he), Equal.trans(Nat, 1n+IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), 1n+IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j), Equal.cong(Nat, Nat, z => 1n+z, IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), r_5(OT, kl, k, sd, NT, j, hr))), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j), 1n+IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), Equal.cong(B.Bk, Nat, y => Nat.add(IV.bitv(B.occ(y)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j)), B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, hb))))      +c2 = L.subst(List<&2, B.Bk>, z => {B.cluster(z, SC.pow2(1n+k), CY.msk(1n+k)) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), bse), IM.clus_up(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, {==}, hel, SC.pow2(1n+k), CY.msk(1n+k), hp, r_2(OT, kl, k, sd, NT, j, hr)))      +c3 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PWell{z, sd}, SC.pow2(1n+k)) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), bse), IM.well_up(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, hel, sd, hwb, SC.pow2(1n+k), r_3(OT, kl, k, sd, NT, j, hr), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))))      +c4 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PUniq{z}, SC.pow2(1n+k)) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), bse), IM.uq_up(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, hel, W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))))), SC.pow2(1n+k), he, r_4(OT, kl, k, sd, NT, j, hr), pno, nsl))      +c5 = L.subst(List<&2, B.Bk>, z => {Nat.is_eq(IV.occn(z, SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j)) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), bse), IS.eq_is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j), e5))      +c6 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PFrom{z, TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 1n+j}, SC.pow2(1n+k)) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), bse), RH.from_mv(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j, SC.pow2(1n+k), e, hel, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, hb, r_6(OT, kl, k, sd, NT, j, hr), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))))      +c7 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PTo{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), z, SC.pow2(1n+k)}, 1n+j) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), kl, SC.pow2(1n+k)), IM.bupd(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), e, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}), bse), RH.to_mv(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j, SC.pow2(1n+k), e, hel, B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, hb, hz, he, r_7(OT, kl, k, sd, NT, j, hr)))      (AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))), (eq, r_mk(OT, kl, k, sd, AR.upd(U32, 2n+k, AR.upd(U32, 2n+k, NT, UD.v(U32.shl(U32.from_nat(e))), W32.nth0(AR.slots(U32, OT), Nat.double(j))), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))), 1n+j, put_perf(1n+k, hk30, NT, r_1(OT, kl, k, sd, NT, j, hr), e, he, W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))), c2, c3, c4, c5, c6, c7)))# a full old bucket: it moves to the first empty bucket of its pathdef step_mv(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0) == False{} : Bool}) -> StepOK(OT, kl, k, sd, j, kk, NT):  +hb = s_hb(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, hc)  +hu = L.subst(B.Bk, y => {B.uq_b(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j, y) == True{} : Bool}, B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), B.BF{W32.nth0(AR.slots(U32, OT), Nat.double(j)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j))))))}, hb, B.all_inst(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k), huo, j, hj))  +nohb = L.and_left(B.nohb(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))))), j), B.nolb(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), j), hu)  +nolb = L.and_right(B.nohb(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))))), j), B.nolb(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), j), hu)  +pno = RH.pno_from(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j, SC.pow2(1n+k), r_6(OT, kl, k, sd, NT, j, hr), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))))), nohb, SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k)))  +nsl = RH.ns_from(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j, SC.pow2(1n+k), r_6(OT, kl, k, sd, NT, j, hr), UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))), RH.noslot_nolb(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)), j, nolb), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k)))  +ol = N.le_trans(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k)), SC.pow2(k), hoc, N.le_trans(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k)), Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k), N.double_self_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), hld))  +hem = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), r_5(OT, kl, k, sd, NT, j, hr))), N.le_lt_trans(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), SC.pow2(k), SC.pow2(1n+k), ol, N.pow2_lt_succ(k)))  step_e(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, hc, pno, nsl, RI.find_e(TB.buckets(AR.slots(U32, NT), kl, SC.pow2(1n+k)), SC.pow2(1n+k), N.succ_le_lt(0n, SC.pow2(1n+k), N.pow2_pos(1n+k)), CY.msk(1n+k), TB.keyof(W32.nth0(AR.slots(U32, OT), Nat.double(j)), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, OT), 1n+Nat.double(j)))))), UD.v(HS.bucket(W32.nth0(AR.slots(U32, OT), Nat.double(j)), CY.msk(1n+k))), PA.home_lt(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 1n+k), r_2(OT, kl, k, sd, NT, j, hr), pno, hem))def step_c(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0) == c : Bool}) -> StepOK(OT, kl, k, sd, j, kk, NT):  match c:    case True{}:      step_skip(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, hc)    case False{}:      step_mv(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, hc)# THEOREM: one step of the move loop keeps the loop invariantdef step(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hoc: {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))) == True{} : Bool}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> StepOK(OT, kl, k, sd, j, kk, NT):  step_c(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, U32.is_eq(W32.nth0(AR.slots(U32, OT), Nat.double(j)), 0), {==})# ---- the loop ----def occn_le(+bs: List<&2, B.Bk>, +j: Nat, +d: Nat) -> {Nat.is_le(IV.occn(bs, j), IV.occn(bs, Nat.add(j, d))) == True{} : Bool}:  match d:    case 0n:      L.subst(Nat, z => {Nat.is_le(IV.occn(bs, j), IV.occn(bs, z)) == True{} : Bool}, j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), N.le_refl(IV.occn(bs, j)))    case 1n+q:      +x = IV.occn(bs, Nat.add(j, q))      +b = IV.bitv(B.occ(B.at(bs, Nat.add(j, q))))      +h1 = N.le_trans(IV.occn(bs, j), x, Nat.add(b, x), occn_le(bs, j, q), L.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, Nat.add(x, b), Nat.add(b, x), N.add_comm(x, b), N.le_add_right(x, b)))      L.subst(Nat, z => {Nat.is_le(IV.occn(bs, j), IV.occn(bs, z)) == True{} : Bool}, 1n+Nat.add(j, q), Nat.add(j, 1n+q), Equal.sym(Nat, Nat.add(j, 1n+q), 1n+Nat.add(j, q), N.add_succ(j, q)), h1)def LoopOK(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +f: Nat, +kk: U32, +NT: AR.Tree<U32>) -> Type:  Sigma<&1, &1, AR.Tree<U32>, T2 => {H.mv_go(f, kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}) == H.MV{AR.thaw(U32, OT), AR.thaw(U32, T2)} : H.Mv} & {rinv(OT, kl, k, sd, T2, SC.pow2(k)) == True{} : Bool}>def loop_s2(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +p: Nat, +kk: U32, +NT: AR.Tree<U32>, +T2: AR.Tree<U32>, +e1: {H.mv_step(kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}) == H.MV{AR.thaw(U32, OT), AR.thaw(U32, T2)} : H.Mv}, lo: LoopOK(OT, kl, k, sd, p, U32.inc(kk), T2)) -> LoopOK(OT, kl, k, sd, 1n+p, kk, NT):  match lo:    case Tuple{+T3, Tuple{+e2, +hr3}}:      (T3, (Equal.trans(H.Mv, H.mv_go(1n+p, kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}), H.mv_go(p, U32.inc(kk), CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, T2)}), H.MV{AR.thaw(U32, OT), AR.thaw(U32, T3)}, Equal.cong(H.Mv, H.Mv, m => H.mv_go(p, U32.inc(kk), CY.msk(1n+k), m), H.mv_step(kk, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, NT)}), H.MV{AR.thaw(U32, OT), AR.thaw(U32, T2)}, e1), e2), hr3))def loop_s(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +p: Nat, +j: Nat, +kk: U32, +NT: AR.Tree<U32>, st: StepOK(OT, kl, k, sd, j, kk, NT), rec: @+T2: AR.Tree<U32> -> @+hr2: {rinv(OT, kl, k, sd, T2, 1n+j) == True{} : Bool} -> LoopOK(OT, kl, k, sd, p, U32.inc(kk), T2)) -> LoopOK(OT, kl, k, sd, 1n+p, kk, NT):  match st:    case Tuple{+T2, Tuple{+e1, +hr2}}:      loop_s2(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, p, kk, NT, T2, e1, rec(T2, hr2))# THEOREM: the loop moves the remaining old buckets keeping the invariantdef loop(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +f: Nat, +j: Nat, +hjf: {Nat.add(j, f) == SC.pow2(k) : Nat}, +kk: U32, +hkk: {UD.v(kk) == j : Nat}, +NT: AR.Tree<U32>, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> LoopOK(OT, kl, k, sd, f, kk, NT):  match f:    case 0n:      +ej = Equal.trans(Nat, j, Nat.add(j, 0n), SC.pow2(k), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hjf)      (NT, ({==}, L.subst(Nat, z => {rinv(OT, kl, k, sd, NT, z) == True{} : Bool}, j, SC.pow2(k), ej, hr)))    case 1n+p:      +hN = Equal.trans(Nat, 1n+Nat.add(j, p), Nat.add(j, 1n+p), SC.pow2(k), Equal.sym(Nat, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p)), hjf)      +hj = L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, 1n+Nat.add(j, p), SC.pow2(k), hN, N.le_lt_succ(j, Nat.add(j, p), N.le_add_right(j, p)))      +hoc = L.subst(Nat, z => {Nat.is_le(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j), IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), z)) == True{} : Bool}, Nat.add(j, 1n+p), SC.pow2(k), hjf, occn_le(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), j, 1n+p))      +hb = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(k)) == True{} : Bool}, j, UD.v(kk), Equal.sym(Nat, UD.v(kk), j, hkk), hj)      +hk2 = Equal.trans(Nat, UD.v(U32.inc(kk)), 1n+UD.v(kk), 1n+j, W32.inc_val(one, h1, kk, W32.bound32(one, h1, UD.v(kk), k, hk31, hb)), Equal.cong(Nat, Nat, z => 1n+z, UD.v(kk), j, hkk))      +hjf2 = Equal.trans(Nat, Nat.add(1n+j, p), 1n+Nat.add(j, p), SC.pow2(k), {==}, hN)      loop_s(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, p, j, kk, NT, step(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr), T2 => hr2 => loop(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, p, 1n+j, hjf2, U32.inc(kk), hk2, T2, hr2))def GrowOK(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +td: U32) -> Type:  Sigma<&1, &1, AR.Tree<U32>, T2 => {H.grow_tab(CY.msk(k), td, AR.thaw(U32, OT)) == AR.thaw(U32, T2) : Array<U32>} & {rinv(OT, kl, k, sd, T2, SC.pow2(k)) == True{} : Bool}>def grow_fin(+OT: AR.Tree<U32>, +kl: List<&2, String>, +k: Nat, +sd: Nat, +td: U32, +e0: {H.grow_tab(CY.msk(k), td, AR.thaw(U32, OT)) == H.mv_fin(H.mv_go(SC.pow2(k), 0, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.trep(U32, 2n+k, 0))})) : Array<U32>}, lo: LoopOK(OT, kl, k, sd, SC.pow2(k), 0, AR.trep(U32, 2n+k, 0))) -> GrowOK(OT, kl, k, sd, td):  match lo:    case Tuple{+T2, Tuple{+e1, +hr}}:      (T2, (Equal.trans(Array<U32>, H.grow_tab(CY.msk(k), td, AR.thaw(U32, OT)), H.mv_fin(H.mv_go(SC.pow2(k), 0, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.trep(U32, 2n+k, 0))})), AR.thaw(U32, T2), e0, Equal.cong(H.Mv, Array<U32>, m => H.mv_fin(m), H.mv_go(SC.pow2(k), 0, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.trep(U32, 2n+k, 0))}), H.MV{AR.thaw(U32, OT), AR.thaw(U32, T2)}, e1)), hr))# THEOREM: growing the table yields a table of twice the buckets holding a# copy of every full old bucket and nothing else, with the table invariantsdef grow_ok(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk30: {Nat.is_lt(1n+k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +kl: List<&2, String>, +sd: Nat, +hlen: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +hwo: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hld: {Nat.is_le(Nat.double(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k))), SC.pow2(k)) == True{} : Bool}, +td: U32, +htd: {UD.v(td) == 1n+k : Nat}) -> GrowOK(OT, kl, k, sd, td):  +htd5 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(5n)) == True{} : Bool}, 1n+k, UD.v(td), Equal.sym(Nat, UD.v(td), 1n+k, htd), N.lt_trans(1n+k, 31n, 32n, hk30, {==}))  +etd = Equal.trans(Nat, UD.v(U32.inc(td)), 1n+UD.v(td), 2n+k, W32.inc_val(one, h1, td, W32.bound32(one, h1, UD.v(td), 5n, {==}, htd5)), Equal.cong(Nat, Nat, z => 1n+z, UD.v(td), 1n+k, htd))  +ea = Equal.trans(Array<U32>, Array.new(U32, UD.v(U32.inc(td)), 0), Array.new(U32, 2n+k, 0), AR.thaw(U32, AR.trep(U32, 2n+k, 0)), Equal.cong(Nat, Array<U32>, d => Array.new(U32, d, 0), UD.v(U32.inc(td)), 2n+k, etd), AR.new(U32, 2n+k, 0))  +e0 = Equal.trans(Array<U32>, H.grow_tab(CY.msk(k), td, AR.thaw(U32, OT)), H.mv_fin(H.mv_go(SC.pow2(k), 0, U32.inc(U32.shl(CY.msk(k))), H.MV{AR.thaw(U32, OT), Array.new(U32, UD.v(U32.inc(td)), 0)})), H.mv_fin(H.mv_go(SC.pow2(k), 0, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.trep(U32, 2n+k, 0))})), Equal.cong(Nat, Array<U32>, f => H.mv_fin(H.mv_go(f, 0, U32.inc(U32.shl(CY.msk(k))), H.MV{AR.thaw(U32, OT), Array.new(U32, UD.v(U32.inc(td)), 0)})), UD.v(U32.inc(CY.msk(k))), SC.pow2(k), PA.fuel_eq(one, h1, k, hk31)), Equal.trans(Array<U32>, H.mv_fin(H.mv_go(SC.pow2(k), 0, U32.inc(U32.shl(CY.msk(k))), H.MV{AR.thaw(U32, OT), Array.new(U32, UD.v(U32.inc(td)), 0)})), H.mv_fin(H.mv_go(SC.pow2(k), 0, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), Array.new(U32, UD.v(U32.inc(td)), 0)})), H.mv_fin(H.mv_go(SC.pow2(k), 0, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), AR.thaw(U32, AR.trep(U32, 2n+k, 0))})), Equal.cong(U32, Array<U32>, m => H.mv_fin(H.mv_go(SC.pow2(k), 0, m, H.MV{AR.thaw(U32, OT), Array.new(U32, UD.v(U32.inc(td)), 0)})), U32.inc(U32.shl(CY.msk(k))), CY.msk(1n+k), msk_up(one, h1, k, hk31)), Equal.cong(Array<U32>, Array<U32>, a => H.mv_fin(H.mv_go(SC.pow2(k), 0, CY.msk(1n+k), H.MV{AR.thaw(U32, OT), a})), Array.new(U32, UD.v(U32.inc(td)), 0), AR.thaw(U32, AR.trep(U32, 2n+k, 0)), ea)))  +h0 = r_mk(OT, kl, k, sd, AR.trep(U32, 2n+k, 0), 0n, AR.trep_perfect(U32, 2n+k, 0), z_clus(2n+k, kl, SC.pow2(1n+k), CY.msk(1n+k), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))), z_well(2n+k, kl, SC.pow2(1n+k), sd, SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))), z_uniq(2n+k, kl, SC.pow2(1n+k), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))), IS.eq_is_eq(IV.occn(TB.buckets(AR.slots(U32, AR.trep(U32, 2n+k, 0)), kl, SC.pow2(1n+k)), SC.pow2(1n+k)), 0n, z_occn(2n+k, kl, SC.pow2(1n+k), SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k)))), z_from(2n+k, kl, SC.pow2(1n+k), TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), 0n, SC.pow2(1n+k), N.le_refl(SC.pow2(1n+k))), {==})  grow_fin(OT, kl, k, sd, td, e0, loop(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, SC.pow2(k), 0n, {==}, 0, {==}, AR.trep(U32, 2n+k, 0), h0))