1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32.bend as U 5 import ../../lib/u32alg.bend as A 6 import ../../lib/array.bend as AR 7 import ../../../spec/lib/common.bend as SC 8 import ../../lib/word.bend as WD 9 import ../../lib/u32div.bend as UD 10 import ../../../src/math/hash.bend as HS 11 import ../../../src/containers/hash_table.bend as H 12 import ./keys.bend as K 13 import ./table.bend as TB 14 import ./buckets.bend as B 15 import ./modn.bend as M 16 import ./cyc.bend as CY 17 import ./arr.bend as AX 18 import ./inv.bend as IV 19 import ./state.bend as ST 20 import ./probe_all.bend as PA 21 import ./insm.bend as IM 22 import ./insa.bend as IA 23 import ./rawins.bend as RI 24 import ./rehash.bend as RH 25 import ./insert.bend as IS 26 import ../../lib/words32.bend as W32 27 28 # Growing the table: grow_tab moves every full old bucket into a table of 29 # twice the buckets; the result holds copies of exactly the old buckets and 30 # keeps the table invariants. 31 32 33 def mskv(+k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}) -> {Nat.add(UD.v(CY.msk(k)), 1n) == SC.pow2(k) : Nat}: 34 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)) 35 36 37 # THEOREM: the grown mask is the mask of twice the buckets 38 def 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}: 39 +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk, {==})) 40 +a0 = mskv(k, hk32) 41 +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))))) 42 +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)) 43 +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))) 44 +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)) 45 +a1 = mskv(1n+k, N.lt_le(1n+k, 32n, hk)) 46 +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)))))) 47 +e3 = A.add_cancel_r(UD.v(CY.msk(1n+k)), 1n+Nat.double(UD.v(CY.msk(k))), 1n, e2) 48 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))) 49 50 # ---- writing one bucket of a tree ---- 51 52 53 def p_ev(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 54 U.to_nat_from_nat(e, K, N.lt_le(K, 32n, N.lt_trans(K, 31n, 32n, hK, {==})), he) 55 56 def p_h(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 57 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)) 58 59 def p_i1(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 60 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))) 61 62 def p_i2(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 63 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))) 64 65 def p_h1(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 66 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))) 67 68 def p_h2(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 69 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)) 70 71 def put_perf(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 72 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)) 73 74 # THEOREM: writing bucket e is the tree update at 2e and 2e + 1 75 def put_eq(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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}: 76 +p1 = AR.upd_perfect(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w, pt) 77 +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) 78 +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) 79 Equal.trans(Array, 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, Array, 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) 80 81 82 def put_slots(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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>}: 83 +p1 = AR.upd_perfect(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(e))), w, pt) 84 +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) 85 +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)) 86 +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)) 87 +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)) 88 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))) 89 90 91 # THEOREM: the written tree decodes to the buckets with bucket e filled, the 92 # key read from the unchanged arena 93 def put_bs(+K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +T: AR.Tree, +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>}: 94 +htb = IS.len_lt(U32, 1n+K, T, pt, 1n+Nat.double(e), N.double_lt_bit(True{}, e, SC.pow2(K), he)) 95 +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) 96 +ek = TB.upd_self(kl, UD.v(H.slot(l))) 97 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)) 98 99 # ---- the empty table ---- 100 101 def nth0_rep(+m: Nat, +x: Nat) -> {W32.nth0(SC.replicate(U32, m, 0), x) == 0 : U32}: 102 match m x: 103 case 0n _: 104 {==} 105 case 1n+p 0n: 106 {==} 107 case 1n+p 1n+q: 108 nth0_rep(p, q) 109 110 111 def nth0_z(+d: Nat, +x: Nat) -> {W32.nth0(AR.slots(U32, AR.trep(U32, d, 0)), x) == 0 : U32}: 112 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)) 113 114 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}: 115 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)))) 116 117 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}: 118 match m: 119 case 0n: 120 {==} 121 case 1n+q: 122 +hq = N.succ_le_lt(q, n, hm) 123 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))) 124 125 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}: 126 match m: 127 case 0n: 128 {==} 129 case 1n+q: 130 +hq = N.succ_le_lt(q, n, hm) 131 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))) 132 133 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}: 134 match m: 135 case 0n: 136 {==} 137 case 1n+q: 138 +hq = N.succ_le_lt(q, n, hm) 139 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))) 140 141 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}: 142 match m: 143 case 0n: 144 {==} 145 case 1n+q: 146 +hq = N.succ_le_lt(q, n, hm) 147 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))) 148 149 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}: 150 match m: 151 case 0n: 152 {==} 153 case 1n+q: 154 +hq = N.succ_le_lt(q, n, hm) 155 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))) 156 157 158 # the rehash loop invariant after moving old buckets 0 .. j - 1 159 def rinv(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +j: Nat) -> Bool: 160 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))))))) 161 162 def r_1(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +j: Nat, +h: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {AR.perfect(U32, 2n+k, NT) == True{} : Bool}: 163 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) 164 165 def r_2(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +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}: 166 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)) 167 168 def r_3(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +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}: 169 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(A 170 171 def r_4(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +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}: 172 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 173 174 def r_5(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +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}: 175 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, 176 177 def r_6(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +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}: 178 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( 179 180 def r_7(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +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}: 181 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 182 183 def r_mk(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +NT: AR.Tree, +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}: 184 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{T 185 186 # ---- one step of the move loop ---- 187 188 189 def StepOK(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +j: Nat, +kk: U32, +NT: AR.Tree) -> Type: 190 Sigma<&1, &1, AR.Tree, 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}> 191 192 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, +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, +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}: 193 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)) 194 195 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, +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, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {UD.v(U32.shl(kk)) == Nat.double(j) : Nat}: 196 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)) 197 198 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, +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, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> {UD.v(U32.inc(U32.shl(kk))) == 1n+Nat.double(j) : Nat}: 199 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)) 200 201 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, +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, +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}: 202 +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))) 203 +ga = AX.getw(1n+k, OT, U32.shl(kk), hk31, hi, pot) 204 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, 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))) 205 206 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, +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, +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}: 207 +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)) 208 +gb = AX.getw(1n+k, OT, U32.inc(U32.shl(kk)), hk31, hi, pot) 209 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, 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))) 210 211 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, +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, +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}: 212 RI.occ_flag(AR.slots(U32, OT), kl, SC.pow2(k), j, hj) 213 214 # an empty old bucket: nothing moves 215 def 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, +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, +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): 216 +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)) 217 +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))) 218 +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)) 219 (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))))) 220 221 222 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, +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, +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}: 223 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)) 224 225 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, +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, +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): 226 match fe: 227 case Tuple{+e, Tuple{+he, Tuple{+hz, hp0}}}: 228 +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}} 229 +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) 230 +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)) 231 +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)) 232 +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) 233 +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))) 234 +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), 235 +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) 236 +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) 237 +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)))) 238 +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))) 239 +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)))) 240 +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)) 241 +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)) 242 +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)))) 243 +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))) 244 (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))) 245 246 # a full old bucket: it moves to the first empty bucket of its path 247 def 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, +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, +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): 248 +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) 249 +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)) 250 +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) 251 +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) 252 +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))) 253 +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))) 254 +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)) 255 +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))) 256 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)) 257 258 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, +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, +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): 259 match c: 260 case True{}: 261 step_skip(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, hc) 262 case False{}: 263 step_mv(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, j, hj, hoc, kk, hkk, NT, hr, hc) 264 265 # THEOREM: one step of the move loop keeps the loop invariant 266 def 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, +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, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> StepOK(OT, kl, k, sd, j, kk, NT): 267 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), {==}) 268 269 # ---- the loop ---- 270 271 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}: 272 match d: 273 case 0n: 274 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))) 275 case 1n+q: 276 +x = IV.occn(bs, Nat.add(j, q)) 277 +b = IV.bitv(B.occ(B.at(bs, Nat.add(j, q)))) 278 +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))) 279 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) 280 281 def LoopOK(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +f: Nat, +kk: U32, +NT: AR.Tree) -> Type: 282 Sigma<&1, &1, AR.Tree, 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}> 283 284 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, +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, +T2: AR.Tree, +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): 285 match lo: 286 case Tuple{+T3, Tuple{+e2, +hr3}}: 287 (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)) 288 289 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, +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, st: StepOK(OT, kl, k, sd, j, kk, NT), rec: @+T2: AR.Tree -> @+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): 290 match st: 291 case Tuple{+T2, Tuple{+e1, +hr2}}: 292 loop_s2(one, h1, k, hk31, hk30, hk0, OT, pot, kl, sd, hlen, hwo, huo, hld, p, kk, NT, T2, e1, rec(T2, hr2)) 293 294 # THEOREM: the loop moves the remaining old buckets keeping the invariant 295 def 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, +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, +hr: {rinv(OT, kl, k, sd, NT, j) == True{} : Bool}) -> LoopOK(OT, kl, k, sd, f, kk, NT): 296 match f: 297 case 0n: 298 +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) 299 (NT, ({==}, L.subst(Nat, z => {rinv(OT, kl, k, sd, NT, z) == True{} : Bool}, j, SC.pow2(k), ej, hr))) 300 case 1n+p: 301 +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) 302 +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))) 303 +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)) 304 +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) 305 +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)) 306 +hjf2 = Equal.trans(Nat, Nat.add(1n+j, p), 1n+Nat.add(j, p), SC.pow2(k), {==}, hN) 307 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)) 308 309 310 def GrowOK(+OT: AR.Tree, +kl: List<&2, String>, +k: Nat, +sd: Nat, +td: U32) -> Type: 311 Sigma<&1, &1, AR.Tree, T2 => {H.grow_tab(CY.msk(k), td, AR.thaw(U32, OT)) == AR.thaw(U32, T2) : Array} & {rinv(OT, kl, k, sd, T2, SC.pow2(k)) == True{} : Bool}> 312 313 def grow_fin(+OT: AR.Tree, +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}, lo: LoopOK(OT, kl, k, sd, SC.pow2(k), 0, AR.trep(U32, 2n+k, 0))) -> GrowOK(OT, kl, k, sd, td): 314 match lo: 315 case Tuple{+T2, Tuple{+e1, +hr}}: 316 (T2, (Equal.trans(Array, 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, 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)) 317 318 # THEOREM: growing the table yields a table of twice the buckets holding a 319 # copy of every full old bucket and nothing else, with the table invariants 320 def 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, +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): 321 +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, {==})) 322 +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)) 323 +ea = Equal.trans(Array, 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, d => Array.new(U32, d, 0), UD.v(U32.inc(td)), 2n+k, etd), AR.new(U32, 2n+k, 0)) 324 +e0 = Equal.trans(Array, 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, 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, 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, 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, Array, 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))) 325 +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))), {==}) 326 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))