proofs/containers/hash_table/shift.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../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 ./words.bend as WRimport ./table.bend as TBimport ./buckets.bend as Bimport ./modn.bend as Mimport ./cyc.bend as CYimport ./arr.bend as AXimport ./inv.bend as IVimport ./probe_impl.bend as PIimport ./probe_all.bend as PAimport ./insm.bend as IMimport ./insa.bend as IAimport ./insert.bend as ISimport ./rehash.bend as RHimport ./grow.bend as GRimport ./ring.bend as RGimport ./hole.bend as HOimport ./rawins.bend as RIimport ./keys.bend as K2import ./delmv.bend as DMimport ../../lib/words32.bend as W32# del_at: the implementation's backward shift is the bucket-level one.# ---- writing one bucket, the key arena unchanged ----def d_other(+tb: List<&2, U32>, +kl: List<&2, String>, +e: Nat, +w: U32, +l: U32, +j: Nat, +hne: {Nat.is_eq(e, j) == False{} : Bool}) -> {TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, j) == TB.dec(tb, kl, j) : B.Bk}:  +wj = W32.nth0(tb, Nat.double(j))  Equal.trans(B.Bk, TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, j), TB.dec_c(wj, W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), 1n+Nat.double(j)), kl, U32.is_eq(wj, 0)), TB.dec(tb, kl, j), Equal.cong(U32, B.Bk, a => TB.dec_c(a, W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), 1n+Nat.double(j)), kl, U32.is_eq(a, 0)), W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), Nat.double(j)), wj, IA.w_other(tb, e, w, l, j, hne)), Equal.cong(U32, B.Bk, a => TB.dec_c(wj, a, kl, U32.is_eq(wj, 0)), W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), 1n+Nat.double(j)), W32.nth0(tb, 1n+Nat.double(j)), IA.l_other(tb, e, w, l, j, hne)))def d_at(+tb: List<&2, U32>, +kl: List<&2, String>, +e: Nat, +w: U32, +l: U32, +htb: {Nat.is_lt(1n+Nat.double(e), SC.length(U32, tb)) == True{} : Bool}) -> {TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, e) == TB.dec_c(w, l, kl, U32.is_eq(w, 0)) : B.Bk}:  Equal.trans(B.Bk, TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, e), TB.dec_c(w, W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), 1n+Nat.double(e)), kl, U32.is_eq(w, 0)), TB.dec_c(w, l, kl, U32.is_eq(w, 0)), Equal.cong(U32, B.Bk, a => TB.dec_c(a, W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), 1n+Nat.double(e)), kl, U32.is_eq(a, 0)), W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), Nat.double(e)), w, IA.w_same(tb, e, w, l, htb)), Equal.cong(U32, B.Bk, a => TB.dec_c(w, a, kl, U32.is_eq(w, 0)), W32.nth0(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), 1n+Nat.double(e)), l, IA.l_same(tb, e, w, l, htb)))def d_same(+tb: List<&2, U32>, +kl: List<&2, String>, +e: Nat, +w: U32, +l: U32, +n: Nat, +m: Nat, +i: Nat, +hei: {Nat.is_lt(e, i) == True{} : Bool}) -> {TB.dlist(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, m, i) == TB.dlist(tb, kl, m, i) : List<&2, B.Bk>}:  match m:    case 0n:      {==}    case 1n+p:      IA.con_eq(TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, i), TB.dec(tb, kl, i), TB.dlist(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, p, 1n+i), TB.dlist(tb, kl, p, 1n+i), d_other(tb, kl, e, w, l, i, N.is_eq_lt(e, i, hei)), d_same(tb, kl, e, w, l, n, p, 1n+i, N.lt_trans(e, i, 1n+i, hei, N.lt_succ(i))))def d_ins(+tb: List<&2, U32>, +kl: List<&2, String>, +e: Nat, +w: U32, +l: U32, +n: Nat, +htb: {Nat.is_lt(1n+Nat.double(e), SC.length(U32, tb)) == True{} : Bool}, +m: Nat, +i: Nat, +d: Nat, +hed: {Nat.add(i, d) == e : Nat}) -> {TB.dlist(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, m, i) == IM.bupd(TB.dlist(tb, kl, m, i), d, TB.dec_c(w, l, kl, U32.is_eq(w, 0))) : List<&2, B.Bk>}:  match m d:    case 0n _:      {==}    case 1n+p 0n:      +hie = Equal.trans(Nat, i, Nat.add(i, 0n), e, Equal.sym(Nat, Nat.add(i, 0n), i, N.add_zero(i)), hed)      +h0 = L.subst(Nat, z => {TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, z) == TB.dec_c(w, l, kl, U32.is_eq(w, 0)) : B.Bk}, e, i, Equal.sym(Nat, i, e, hie), d_at(tb, kl, e, w, l, htb))      +hei = L.subst(Nat, z => {Nat.is_lt(z, 1n+i) == True{} : Bool}, i, e, hie, N.lt_succ(i))      IA.con_eq(TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, i), TB.dec_c(w, l, kl, U32.is_eq(w, 0)), TB.dlist(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, p, 1n+i), TB.dlist(tb, kl, p, 1n+i), h0, d_same(tb, kl, e, w, l, n, p, 1n+i, hei))    case 1n+p 1n+q:      +he1 = Equal.trans(Nat, Nat.add(1n+i, q), Nat.add(i, 1n+q), e, Equal.sym(Nat, Nat.add(i, 1n+q), 1n+Nat.add(i, q), N.add_succ(i, q)), hed)      +hlt = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, Nat.add(1n+i, q), e, he1, N.le_lt_succ(i, Nat.add(i, q), N.le_add_right(i, q)))      IA.con_eq(TB.dec(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, i), TB.dec(tb, kl, i), TB.dlist(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, p, 1n+i), IM.bupd(TB.dlist(tb, kl, p, 1n+i), q, TB.dec_c(w, l, kl, U32.is_eq(w, 0))), d_other(tb, kl, e, w, l, i, N.is_eq_sym_false(i, e, N.is_eq_lt(i, e, hlt))), d_ins(tb, kl, e, w, l, n, htb, p, 1n+i, q, he1))# THEOREM: writing (w, l) into bucket e decodes as bucket e replaceddef put_dec(+tb: List<&2, U32>, +kl: List<&2, String>, +e: Nat, +w: U32, +l: U32, +n: Nat, +htb: {Nat.is_lt(1n+Nat.double(e), SC.length(U32, tb)) == True{} : Bool}) -> {TB.buckets(SC.update(U32, SC.update(U32, tb, Nat.double(e), w), 1n+Nat.double(e), l), kl, n) == IM.bupd(TB.buckets(tb, kl, n), e, TB.dec_c(w, l, kl, U32.is_eq(w, 0))) : List<&2, B.Bk>}:  d_ins(tb, kl, e, w, l, n, htb, n, 0n, e, {==})# ---- the loop state and invariant ----type DSt is Data:  DS{iU: U32, h: Nat, kU: U32, dk: Nat, T: AR.Tree<U32>}# the invariant; dq<i> names the conjunction of its components from i on,# so no statement repeats the rest of the chain (dp<i>: the invariant gives it)def dq10(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(Nat.is_le(dk, M.dist(1n+bp, h, e0)), Nat.is_lt(h, 1n+bp))def dq9(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(Nat.is_le(1n, dk), dq10(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq8(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(Bool.not(B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0))), dq9(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq7(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(Nat.is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp)), dq8(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq6(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(B.all_lt(B.PTo{V0, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp}, 1n+bp), dq7(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq5(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(B.all_lt(B.PFrom{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), V0, 1n+bp}, 1n+bp), dq6(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq4(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(B.all_lt(B.PUniq{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})}, 1n+bp), dq5(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq3(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(B.all_lt(B.PHole{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, CY.msk(K), h, dk}, 1n+bp), dq4(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq2(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(AR.perfect(U32, 1n+K, T), dq3(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dq1(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(Nat.is_eq(UD.v(kU), M.pos(1n+bp, h, dk)), dq2(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dinvF(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>) -> Bool:  Bool.and(Nat.is_eq(UD.v(iU), h), dq1(kl, K, bp, V0, e0, iU, h, kU, dk, T))def dp1(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq1(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(Nat.is_eq(UD.v(iU), h), dq1(kl, K, bp, V0, e0, iU, h, kU, dk, T), hq)def dp2(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq2(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(Nat.is_eq(UD.v(kU), M.pos(1n+bp, h, dk)), dq2(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp1(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp3(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq3(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(AR.perfect(U32, 1n+K, T), dq3(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp2(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp4(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq4(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(B.all_lt(B.PHole{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, CY.msk(K), h, dk}, 1n+bp), dq4(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp5(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq5(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(B.all_lt(B.PUniq{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})}, 1n+bp), dq5(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp4(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp6(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq6(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(B.all_lt(B.PFrom{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), V0, 1n+bp}, 1n+bp), dq6(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp5(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp7(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq7(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(B.all_lt(B.PTo{V0, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp}, 1n+bp), dq7(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp6(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp8(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq8(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(Nat.is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp)), dq8(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp7(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp9(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq9(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(Bool.not(B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0))), dq9(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp8(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp10(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {dq10(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_right(Nat.is_le(1n, dk), dq10(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp9(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def dp11(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(h, 1n+bp) == True{} : Bool}:  L.and_right(Nat.is_le(dk, M.dist(1n+bp, h, e0)), Nat.is_lt(h, 1n+bp), dp10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q1(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_eq(UD.v(iU), h) == True{} : Bool}:  L.and_left(Nat.is_eq(UD.v(iU), h), dq1(kl, K, bp, V0, e0, iU, h, kU, dk, T), hq)def q2(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_eq(UD.v(kU), M.pos(1n+bp, h, dk)) == True{} : Bool}:  L.and_left(Nat.is_eq(UD.v(kU), M.pos(1n+bp, h, dk)), dq2(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp1(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q3(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {AR.perfect(U32, 1n+K, T) == True{} : Bool}:  L.and_left(AR.perfect(U32, 1n+K, T), dq3(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp2(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q4(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {B.all_lt(B.PHole{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}:  L.and_left(B.all_lt(B.PHole{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, CY.msk(K), h, dk}, 1n+bp), dq4(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q5(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {B.all_lt(B.PUniq{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})}, 1n+bp) == True{} : Bool}:  L.and_left(B.all_lt(B.PUniq{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})}, 1n+bp), dq5(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp4(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q6(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {B.all_lt(B.PFrom{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), V0, 1n+bp}, 1n+bp) == True{} : Bool}:  L.and_left(B.all_lt(B.PFrom{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), V0, 1n+bp}, 1n+bp), dq6(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp5(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q7(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {B.all_lt(B.PTo{V0, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp}, 1n+bp) == True{} : Bool}:  L.and_left(B.all_lt(B.PTo{V0, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp}, 1n+bp), dq7(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp6(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q8(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp)) == True{} : Bool}:  L.and_left(Nat.is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp)), dq8(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp7(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q9(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Bool.not(B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0))) == True{} : Bool}:  L.and_left(Bool.not(B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0))), dq9(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp8(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q10(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_le(1n, dk) == True{} : Bool}:  L.and_left(Nat.is_le(1n, dk), dq10(kl, K, bp, V0, e0, iU, h, kU, dk, T), dp9(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q11(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_le(dk, M.dist(1n+bp, h, e0)) == True{} : Bool}:  L.and_left(Nat.is_le(dk, M.dist(1n+bp, h, e0)), Nat.is_lt(h, 1n+bp), dp10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq))def q12(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hq: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(h, 1n+bp) == True{} : Bool}:  dp11(kl, K, bp, V0, e0, iU, h, kU, dk, T, hq)def q_mk(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +h1: {Nat.is_eq(UD.v(iU), h) == True{} : Bool}, +h2: {Nat.is_eq(UD.v(kU), M.pos(1n+bp, h, dk)) == True{} : Bool}, +h3: {AR.perfect(U32, 1n+K, T) == True{} : Bool}, +h4: {B.all_lt(B.PHole{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}, +h5: {B.all_lt(B.PUniq{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})}, 1n+bp) == True{} : Bool}, +h6: {B.all_lt(B.PFrom{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), V0, 1n+bp}, 1n+bp) == True{} : Bool}, +h7: {B.all_lt(B.PTo{V0, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp}, 1n+bp) == True{} : Bool}, +h8: {Nat.is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp)) == True{} : Bool}, +h9: {Bool.not(B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0))) == True{} : Bool}, +h10: {Nat.is_le(1n, dk) == True{} : Bool}, +h11: {Nat.is_le(dk, M.dist(1n+bp, h, e0)) == True{} : Bool}, +h12: {Nat.is_lt(h, 1n+bp) == True{} : Bool}) -> {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}:  L.and_intro(Nat.is_eq(UD.v(iU), h), dq1(kl, K, bp, V0, e0, iU, h, kU, dk, T), h1, L.and_intro(Nat.is_eq(UD.v(kU), M.pos(1n+bp, h, dk)), dq2(kl, K, bp, V0, e0, iU, h, kU, dk, T), h2, L.and_intro(AR.perfect(U32, 1n+K, T), dq3(kl, K, bp, V0, e0, iU, h, kU, dk, T), h3, L.and_intro(B.all_lt(B.PHole{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, CY.msk(K), h, dk}, 1n+bp), dq4(kl, K, bp, V0, e0, iU, h, kU, dk, T), h4, L.and_intro(B.all_lt(B.PUniq{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})}, 1n+bp), dq5(kl, K, bp, V0, e0, iU, h, kU, dk, T), h5, L.and_intro(B.all_lt(B.PFrom{IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), V0, 1n+bp}, 1n+bp), dq6(kl, K, bp, V0, e0, iU, h, kU, dk, T), h6, L.and_intro(B.all_lt(B.PTo{V0, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp}, 1n+bp), dq7(kl, K, bp, V0, e0, iU, h, kU, dk, T), h7, L.and_intro(Nat.is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp)), dq8(kl, K, bp, V0, e0, iU, h, kU, dk, T), h8, L.and_intro(Bool.not(B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0))), dq9(kl, K, bp, V0, e0, iU, h, kU, dk, T), h9, L.and_intro(Nat.is_le(1n, dk), dq10(kl, K, bp, V0, e0, iU, h, kU, dk, T), h10, L.and_intro(Nat.is_le(dk, M.dist(1n+bp, h, e0)), Nat.is_lt(h, 1n+bp), h11, h12)))))))))))def dinv(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, st: DSt) -> Bool:  match st:    case DS{+iU, +h, +kU, +dk, +T}:      dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T)def dfuel(+bp: Nat, +e0: Nat, +f: Nat, st: DSt) -> Bool:  match st:    case DS{iU, +h, kU, +dk, T}:      Nat.is_lt(M.dist(1n+bp, h, e0), Nat.add(dk, f))# what the deletion leavesdef dfin(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>) -> Bool:  Bool.and(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))))def f1(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>, +h: {dfin(kl, K, bp, V0, Tf) == True{} : Bool}) -> {AR.perfect(U32, 1n+K, Tf) == True{} : Bool}:  L.and_left(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))), h)def f2(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>, +h: {dfin(kl, K, bp, V0, Tf) == True{} : Bool}) -> {B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}:  L.and_left(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))))), L.and_right(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))), h))def f3(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>, +h: {dfin(kl, K, bp, V0, Tf) == True{} : Bool}) -> {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp) == True{} : Bool}:  L.and_left(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))))), L.and_right(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))), h)))def f4(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>, +h: {dfin(kl, K, bp, V0, Tf) == True{} : Bool}) -> {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp) == True{} : Bool}:  L.and_left(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))))), L.and_right(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))), h))))def f5(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>, +h: {dfin(kl, K, bp, V0, Tf) == True{} : Bool}) -> {B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp) == True{} : Bool}:  L.and_left(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)), L.and_right(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))))), L.and_right(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))), h)))))def f6(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>, +h: {dfin(kl, K, bp, V0, Tf) == True{} : Bool}) -> {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)) == True{} : Bool}:  L.and_right(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)), L.and_right(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))))), L.and_right(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))), h)))))def f_mk(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>, +g1: {AR.perfect(U32, 1n+K, Tf) == True{} : Bool}, +g2: {B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +g3: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +g4: {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp) == True{} : Bool}, +g5: {B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp) == True{} : Bool}, +g6: {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)) == True{} : Bool}) -> {dfin(kl, K, bp, V0, Tf) == True{} : Bool}:  L.and_intro(AR.perfect(U32, 1n+K, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))))), g1, L.and_intro(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp, CY.msk(K)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))))), g2, L.and_intro(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp)}, 1n+bp), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)))), g3, L.and_intro(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), V0, 1n+bp}, 1n+bp), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp))), g4, L.and_intro(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp}, 1n+bp), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, 1n+bp), 1n+bp), IV.occn(V0, 1n+bp)), g5, g6)))))def DelOK(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +f: Nat, +iU: U32, +kU: U32, +T: AR.Tree<U32>) -> Type:  Sigma<&1, &1, AR.Tree<U32>, Tf => {H.shift(f, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), CY.msk(K), iU, kU) == AR.thaw(U32, Tf) : Array<U32>} & {dfin(kl, K, bp, V0, Tf) == True{} : Bool}>def DelOKs(+kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +f: Nat, st: DSt) -> Type:  match st:    case DS{+iU, h, +kU, dk, +T}:      DelOK(kl, K, bp, V0, f, iU, kU, T)# ---- one step ----def g_hdn(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(dk, 1n+bp) == True{} : Bool}:  N.le_lt_trans(dk, M.dist(1n+bp, h, e0), 1n+bp, q11(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), M.dist_lt(bp, h, e0))def g_hkn(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(M.pos(1n+bp, h, dk), 1n+bp) == True{} : Bool}:  M.pos_lt(bp, h, dk)def g_hkK(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(M.pos(1n+bp, h, dk), SC.pow2(K)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(M.pos(1n+bp, h, dk), z) == True{} : Bool}, 1n+bp, SC.pow2(K), hN, g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))def g_hhK(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(h, SC.pow2(K)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(h, z) == True{} : Bool}, 1n+bp, SC.pow2(K), hN, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))def g_hhk(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_eq(h, M.pos(1n+bp, h, dk)) == False{} : Bool}:  HO.h_ne_k(K, bp, hN, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dk, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hdn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))def g_ekv(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {UD.v(kU) == M.pos(1n+bp, h, dk) : Nat}:  N.eq_from_is_eq(UD.v(kU), M.pos(1n+bp, h, dk), q2(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))def g_eiv(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {UD.v(iU) == h : Nat}:  N.eq_from_is_eq(UD.v(iU), h, q1(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))def g_hh2(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(1n+Nat.double(UD.v(kU)), SC.pow2(1n+K)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(1n+Nat.double(z), SC.pow2(1n+K)) == True{} : Bool}, M.pos(1n+bp, h, dk), UD.v(kU), Equal.sym(Nat, UD.v(kU), M.pos(1n+bp, h, dk), g_ekv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), N.double_lt_bit(True{}, M.pos(1n+bp, h, dk), SC.pow2(K), g_hkK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def g_ews(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {UD.v(U32.shl(kU)) == Nat.double(M.pos(1n+bp, h, dk)) : Nat}:  Equal.trans(Nat, UD.v(U32.shl(kU)), Nat.double(UD.v(kU)), Nat.double(M.pos(1n+bp, h, dk)), AX.ix_w(kU, 1n+K, hK, g_hh2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(kU), M.pos(1n+bp, h, dk), g_ekv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def g_ewl(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {UD.v(U32.inc(U32.shl(kU))) == 1n+Nat.double(M.pos(1n+bp, h, dk)) : Nat}:  Equal.trans(Nat, UD.v(U32.inc(U32.shl(kU))), 1n+Nat.double(UD.v(kU)), 1n+Nat.double(M.pos(1n+bp, h, dk)), AX.ix_l(kU, 1n+K, hK, g_hh2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), UD.v(kU), M.pos(1n+bp, h, dk), g_ekv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def eqS(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU) == H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)) : H.Sh}:  +hi2 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+K)) == True{} : Bool}, Nat.double(M.pos(1n+bp, h, dk)), UD.v(U32.shl(kU)), Equal.sym(Nat, UD.v(U32.shl(kU)), Nat.double(M.pos(1n+bp, h, dk)), g_ews(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), N.lt_trans(Nat.double(M.pos(1n+bp, h, dk)), 1n+Nat.double(M.pos(1n+bp, h, dk)), SC.pow2(1n+K), N.lt_succ(Nat.double(M.pos(1n+bp, h, dk))), N.double_lt_bit(True{}, M.pos(1n+bp, h, dk), SC.pow2(K), g_hkK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))))  +g = AX.getw(1n+K, T, U32.shl(kU), hK, hi2, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))  Equal.trans(H.Sh, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), H.sh_w(CY.msk(K), iU, kU, (AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), UD.v(U32.shl(kU))))), H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), Equal.cong(Array<U32> & U32, H.Sh, r => H.sh_w(CY.msk(K), iU, kU, r), Array.get(U32, AR.thaw(U32, T), U32.shl(kU)), (AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), UD.v(U32.shl(kU)))), g), Equal.cong(Nat, H.Sh, z => H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), z), U32.is_eq(W32.nth0(AR.slots(U32, T), z), 0)), UD.v(U32.shl(kU)), Nat.double(M.pos(1n+bp, h, dk)), g_ews(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def eqL(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), False{}) == H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))) : H.Sh}:  +hi2 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+K)) == True{} : Bool}, 1n+Nat.double(M.pos(1n+bp, h, dk)), UD.v(U32.inc(U32.shl(kU))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(kU))), 1n+Nat.double(M.pos(1n+bp, h, dk)), g_ewl(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), N.double_lt_bit(True{}, M.pos(1n+bp, h, dk), SC.pow2(K), g_hkK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))  +g = AX.getw(1n+K, T, U32.inc(U32.shl(kU)), hK, hi2, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))  Equal.trans(H.Sh, H.sh_l(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K), iU, kU, Array.get(U32, AR.thaw(U32, T), U32.inc(U32.shl(kU)))), H.sh_l(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K), iU, kU, (AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), UD.v(U32.inc(U32.shl(kU)))))), H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), Equal.cong(Array<U32> & U32, H.Sh, r => H.sh_l(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K), iU, kU, r), Array.get(U32, AR.thaw(U32, T), U32.inc(U32.shl(kU))), (AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), UD.v(U32.inc(U32.shl(kU))))), g), Equal.cong(Nat, H.Sh, z => H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), z), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), UD.v(U32.inc(U32.shl(kU))), 1n+Nat.double(M.pos(1n+bp, h, dk)), g_ewl(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def at_k(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk)) == TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)) : B.Bk}:  Equal.trans(B.Bk, B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk)), B.at(TB.buckets(AR.slots(U32, T), kl, 1n+bp), M.pos(1n+bp, h, dk)), TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), IM.at_bupd_other(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}, M.pos(1n+bp, h, dk), g_hhk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), TB.at_buckets(AR.slots(U32, T), kl, 1n+bp, M.pos(1n+bp, h, dk), g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def sc_nr(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}) -> {WD.sc(K, one) == 1n+bp : Nat}:  Equal.trans(Nat, WD.sc(K, one), SC.pow2(K), 1n+bp, Equal.sym(Nat, SC.pow2(K), WD.sc(K, one), W32.pow_one(one, h1, K)), Equal.sym(Nat, 1n+bp, SC.pow2(K), hN))def lt_sc(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +x: U32, +v: Nat, +hx: {UD.v(x) == v : Nat}, +hv: {Nat.is_lt(v, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(UD.v(x), WD.sc(K, one)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(UD.v(x), z) == True{} : Bool}, 1n+bp, WD.sc(K, one), Equal.sym(Nat, WD.sc(K, one), 1n+bp, sc_nr(one, h1, kl, K, bp, V0, e0, hK, hN, he0)), L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, v, UD.v(x), Equal.sym(Nat, UD.v(x), v, hx), hv))def mdist(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +a: U32, +b: U32, +va: Nat, +vb: Nat, +ha: {UD.v(a) == va : Nat}, +hb: {UD.v(b) == vb : Nat}, +hva: {Nat.is_lt(va, 1n+bp) == True{} : Bool}, +hvb: {Nat.is_lt(vb, 1n+bp) == True{} : Bool}) -> {UD.v(U32.and(U32.sub(b, a), CY.msk(K))) == M.dist(1n+bp, va, vb) : Nat}:  +hkj = N.sub_add(32n, K, N.lt_le(K, 32n, N.lt_trans(K, 31n, 32n, hK, {==})))  +d0 = CY.dist(one, h1, K, Nat.sub(32n, K), hkj, a, b, lt_sc(one, h1, kl, K, bp, V0, e0, hK, hN, he0, a, va, ha, hva), lt_sc(one, h1, kl, K, bp, V0, e0, hK, hN, he0, b, vb, hb, hvb))  Equal.trans(Nat, UD.v(U32.and(U32.sub(b, a), CY.msk(K))), M.dist(WD.sc(K, one), UD.v(a), UD.v(b)), M.dist(1n+bp, va, vb), d0, Equal.trans(Nat, M.dist(WD.sc(K, one), UD.v(a), UD.v(b)), M.dist(1n+bp, UD.v(a), UD.v(b)), M.dist(1n+bp, va, vb), Equal.cong(Nat, Nat, z => M.dist(z, UD.v(a), UD.v(b)), WD.sc(K, one), 1n+bp, sc_nr(one, h1, kl, K, bp, V0, e0, hK, hN, he0)), Equal.trans(Nat, M.dist(1n+bp, UD.v(a), UD.v(b)), M.dist(1n+bp, va, UD.v(b)), M.dist(1n+bp, va, vb), Equal.cong(Nat, Nat, z => M.dist(1n+bp, z, UD.v(b)), UD.v(a), va, ha), Equal.cong(Nat, Nat, z => M.dist(1n+bp, va, z), UD.v(b), vb, hb))))# THEOREM: the implementation's move test compares the scanned bucket's distance from home with the gap'sdef mvv(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))) == Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk) : Bool}:  +hbl = L.subst(Nat, z => {Nat.is_lt(UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), z) == True{} : Bool}, SC.pow2(K), 1n+bp, Equal.sym(Nat, 1n+bp, SC.pow2(K), hN), PA.home_lt(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), K))  +dx = mdist(one, h1, kl, K, bp, V0, e0, hK, hN, he0, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K)), kU, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk), {==}, g_ekv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), hbl, g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))  +dy = Equal.trans(Nat, UD.v(U32.and(U32.sub(kU, iU), CY.msk(K))), M.dist(1n+bp, h, M.pos(1n+bp, h, dk)), dk, mdist(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, kU, h, M.pos(1n+bp, h, dk), g_eiv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), g_ekv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), HO.dist_k(K, bp, hN, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dk, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hdn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))  +x = U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K))  +y = U32.and(U32.sub(kU, iU), CY.msk(K))  Equal.trans(Bool, U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), Nat.is_ge(UD.v(x), UD.v(y)), Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), Equal.cong(Cmp, Bool, c => Cmp.is_ge(c), U32.cmp(x, y), Nat.cmp(UD.v(x), UD.v(y)), U.u32_cmp(x, y)), Equal.trans(Bool, Nat.is_ge(UD.v(x), UD.v(y)), Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), UD.v(y)), Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), Equal.cong(Nat, Bool, z => Nat.is_ge(z, UD.v(y)), UD.v(x), M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dx), Equal.cong(Nat, Bool, z => Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), z), UD.v(y), dk, dy)))def len_v(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {SC.length(B.Bk, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})) == 1n+bp : Nat}:  Equal.trans(Nat, SC.length(B.Bk, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})), SC.length(B.Bk, TB.buckets(AR.slots(U32, T), kl, 1n+bp)), 1n+bp, RG.len_bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), IA.len_dlist(AR.slots(U32, T), kl, 1n+bp, 0n))def lt_lv(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(x, SC.length(B.Bk, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}))) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(x, z) == True{} : Bool}, 1n+bp, SC.length(B.Bk, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})), Equal.sym(Nat, SC.length(B.Bk, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{})), 1n+bp, len_v(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), hx)def e_iu(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {iU == U32.from_nat(h) : U32}:  Equal.trans(U32, iU, U32.from_nat(UD.v(iU)), U32.from_nat(h), Equal.sym(U32, U32.from_nat(UD.v(iU)), iU, PI.from_v(iU, K, N.lt_le(K, 32n, N.lt_trans(K, 31n, 32n, hK, {==})), L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(K)) == True{} : Bool}, h, UD.v(iU), Equal.sym(Nat, UD.v(iU), h, g_eiv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))), Equal.cong(Nat, U32, z => U32.from_nat(z), UD.v(iU), h, g_eiv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def g_htb(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_lt(1n+Nat.double(h), SC.length(U32, AR.slots(U32, T))) == True{} : Bool}:  IS.len_lt(U32, 1n+K, T, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), 1n+Nat.double(h), N.double_lt_bit(True{}, h, SC.pow2(K), g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))def g_occk(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == c : Bool}) -> {B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk))) == Bool.not(c) : Bool}:  Equal.trans(Bool, B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk))), B.occ(TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0))), Bool.not(c), Equal.cong(B.Bk, Bool, y => B.occ(y), B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk)), TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), at_k(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), Equal.trans(Bool, B.occ(TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0))), Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), Bool.not(c), RI.occ_dec(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), Equal.cong(Bool, Bool, b => Bool.not(b), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0), c, hc)))# an empty scanned bucket: the gap is cleared and the deletion endsdef step_end(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == True{} : Bool}) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T):  +hz = g_occk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, True{}, hc)  +cl = HO.hole_end(K, bp, hN, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dk, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hdn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), hz, q4(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))  +ep = Equal.trans(Array<U32>, H.put_bucket(AR.thaw(U32, T), iU, 0, 0), H.put_bucket(AR.thaw(U32, T), U32.from_nat(h), 0, 0), AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), Equal.cong(U32, Array<U32>, i => H.put_bucket(AR.thaw(U32, T), i, 0, 0), iU, U32.from_nat(h), e_iu(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), GR.put_eq(K, hK, T, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), h, g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), 0, 0))  +eq = Equal.trans(Array<U32>, H.shift(1n+p, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), CY.msk(K), iU, kU), H.shift(1n+p, H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), CY.msk(K), iU, kU), AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), Equal.cong(H.Sh, Array<U32>, s => H.shift(1n+p, s, CY.msk(K), iU, kU), H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), eqS(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), Equal.trans(Array<U32>, H.shift(1n+p, H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), CY.msk(K), iU, kU), H.put_bucket(AR.thaw(U32, T), iU, 0, 0), AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), Equal.cong(Bool, Array<U32>, c => H.shift(1n+p, H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), c), CY.msk(K), iU, kU), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0), True{}, hc), ep))  +evc = 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(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(h), 0), 1n+Nat.double(h), 0), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), Equal.cong(List<&2, U32>, List<&2, B.Bk>, z => TB.buckets(z, kl, 1n+bp), AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(h), 0), 1n+Nat.double(h), 0), GR.put_slots(K, hK, T, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), h, g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), 0, 0)), put_dec(AR.slots(U32, T), kl, h, 0, 0, 1n+bp, g_htb(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))  (AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0), (eq, f_mk(kl, K, bp, V0, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0), GR.put_perf(K, hK, T, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), h, g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), 0, 0), L.subst(List<&2, B.Bk>, z => {B.cluster(z, 1n+bp, CY.msk(K)) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), Equal.sym(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(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), evc), cl), L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PUniq{z}, 1n+bp) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), Equal.sym(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(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), evc), q5(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PFrom{z, V0, 1n+bp}, 1n+bp) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), Equal.sym(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(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), evc), q6(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PTo{V0, z, 1n+bp}, 1n+bp) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), Equal.sym(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(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), evc), q7(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), L.subst(List<&2, B.Bk>, z => {Nat.is_eq(IV.occn(z, 1n+bp), IV.occn(V0, 1n+bp)) == True{} : Bool} , IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), Equal.sym(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(h))), 0), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), 0)), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), evc), q8(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))))# ---- facts shared by move and skip ----def g_hbk(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}) -> {B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk)) == B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))} : B.Bk}:  Equal.trans(B.Bk, B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk)), TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, at_k(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), Equal.cong(Bool, B.Bk, c => TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, c), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0), False{}, hc))def g_e0f(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0)) == False{} : Bool}:  K2.not_true_eq(B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0)), q9(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))def ne_occ_c(+bs: List<&2, B.Bk>, +x: Nat, +y: Nat, +hx: {B.occ(B.at(bs, x)) == True{} : Bool}, +hy: {B.occ(B.at(bs, y)) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(x, y) == c : Bool}) -> {c == False{} : Bool}:  match c:    case False{}:      {==}    case True{}:      Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, B.occ(B.at(bs, y)), False{}, L.subst(Nat, z => {True{} == B.occ(B.at(bs, z)) : Bool}, x, y, N.eq_from_is_eq(x, y, hc), Equal.sym(Bool, B.occ(B.at(bs, x)), True{}, hx)), hy)))def g_nke(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}) -> {Nat.is_eq(M.pos(1n+bp, h, dk), e0) == False{} : Bool}:  ne_occ_c(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), e0, Equal.trans(Bool, B.occ(B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk))), Bool.not(False{}), True{}, g_occk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, False{}, hc), {==}), g_e0f(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), Nat.is_eq(M.pos(1n+bp, h, dk), e0), {==})def dne_c(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}, +c: Bool, +hc2: {Nat.is_eq(dk, M.dist(1n+bp, h, e0)) == c : Bool}) -> {c == False{} : Bool}:  match c:    case False{}:      {==}    case True{}:      +eke = Equal.trans(Nat, M.pos(1n+bp, h, dk), M.pos(1n+bp, h, M.dist(1n+bp, h, e0)), e0, Equal.cong(Nat, Nat, z => M.pos(1n+bp, h, z), dk, M.dist(1n+bp, h, e0), N.eq_from_is_eq(dk, M.dist(1n+bp, h, e0), hc2)), M.pos_dist(bp, h, e0, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), he0))      Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_eq(M.pos(1n+bp, h, dk), e0), False{}, Equal.sym(Bool, Nat.is_eq(M.pos(1n+bp, h, dk), e0), True{}, IS.eq_is_eq(M.pos(1n+bp, h, dk), e0, eke)), g_nke(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc))))# the scanned bucket is full, so the empty e0 lies further ondef g_dlt(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}) -> {Nat.is_lt(dk, M.dist(1n+bp, h, e0)) == True{} : Bool}:  N.lt_or_eq(dk, M.dist(1n+bp, h, e0), q11(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dne_c(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc, Nat.is_eq(dk, M.dist(1n+bp, h, e0)), {==}))def g_nv(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {UD.v(H.bnext(kU, CY.msk(K))) == Nat.mod(1n+M.pos(1n+bp, h, dk), 1n+bp) : Nat}:  +hks = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, SC.pow2(K), WD.sc(K, one), W32.pow_one(one, h1, K), N.lt_le_trans(SC.pow2(K), SC.pow2(1n+K), WD.sc(32n, one), N.pow2_lt_succ(K), W32.pow_le32(one, h1, 1n+K, hK)))  +n1 = CY.next_val(one, h1, K, kU, hks, lt_sc(one, h1, kl, K, bp, V0, e0, hK, hN, he0, kU, M.pos(1n+bp, h, dk), g_ekv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))  Equal.trans(Nat, UD.v(H.bnext(kU, CY.msk(K))), Nat.mod(1n+UD.v(kU), WD.sc(K, one)), Nat.mod(1n+M.pos(1n+bp, h, dk), 1n+bp), n1, Equal.trans(Nat, Nat.mod(1n+UD.v(kU), WD.sc(K, one)), Nat.mod(1n+UD.v(kU), 1n+bp), Nat.mod(1n+M.pos(1n+bp, h, dk), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(1n+UD.v(kU), z), WD.sc(K, one), 1n+bp, sc_nr(one, h1, kl, K, bp, V0, e0, hK, hN, he0)), Equal.cong(Nat, Nat, z => Nat.mod(1n+z, 1n+bp), UD.v(kU), M.pos(1n+bp, h, dk), g_ekv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))))# the implementation reaches the move testdef eq_mv(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}) -> {H.shift(1n+p, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), CY.msk(K), iU, kU) == H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), CY.msk(K), iU, kU) : Array<U32>}:  Equal.trans(Array<U32>, H.shift(1n+p, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), CY.msk(K), iU, kU), H.shift(1n+p, H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), CY.msk(K), iU, kU), H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), CY.msk(K), iU, kU), Equal.cong(H.Sh, Array<U32>, s => H.shift(1n+p, s, CY.msk(K), iU, kU), H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), eqS(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), Equal.trans(Array<U32>, H.shift(1n+p, H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0)), CY.msk(K), iU, kU), H.shift(1n+p, H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), False{}), CY.msk(K), iU, kU), H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), CY.msk(K), iU, kU), Equal.cong(Bool, Array<U32>, c => H.shift(1n+p, H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), c), CY.msk(K), iU, kU), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0), False{}, hc), Equal.cong(H.Sh, Array<U32>, s => H.shift(1n+p, s, CY.msk(K), iU, kU), H.sh_if(AR.thaw(U32, T), CY.msk(K), iU, kU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), False{}), H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), eqL(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))))def nhe_c(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(h, e0) == c : Bool}) -> {c == False{} : Bool}:  match c:    case False{}:      {==}    case True{}:      +d0 = Equal.trans(Nat, M.dist(1n+bp, h, e0), M.dist(1n+bp, h, h), 0n, Equal.cong(Nat, Nat, z => M.dist(1n+bp, h, z), e0, h, Equal.sym(Nat, h, e0, N.eq_from_is_eq(h, e0, hc))), RG.dist_self(bp, h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))      +l0 = N.le_trans(1n, dk, 0n, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), L.subst(Nat, z => {Nat.is_le(dk, z) == True{} : Bool}, M.dist(1n+bp, h, e0), 0n, d0, q11(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))      Empty.absurd({True{} == False{} : Bool}, L.false_true(l0))# the gap is not the empty bucket aheaddef g_nhe(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {Nat.is_eq(h, e0) == False{} : Bool}:  nhe_c(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, Nat.is_eq(h, e0), {==})# ---- move ----def g_hzh(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}) -> {B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h) == B.BE{} : B.Bk}:  IM.at_bupd_same(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}, L.subst(Nat, z => {Nat.is_lt(h, z) == True{} : Bool}, 1n+bp, SC.length(B.Bk, TB.buckets(AR.slots(U32, T), kl, 1n+bp)), Equal.sym(Nat, SC.length(B.Bk, TB.buckets(AR.slots(U32, T), kl, 1n+bp)), 1n+bp, IA.len_dlist(AR.slots(U32, T), kl, 1n+bp, 0n)), q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))def ev2(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}) -> {IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}) == IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}) : List<&2, B.Bk>}:  +eb = 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(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(h), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), 1n+Nat.double(h), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), Equal.cong(List<&2, U32>, List<&2, B.Bk>, z => TB.buckets(z, kl, 1n+bp), AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(h), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), 1n+Nat.double(h), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), GR.put_slots(K, hK, T, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), h, g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), Equal.trans(List<&2, B.Bk>, TB.buckets(SC.update(U32, SC.update(U32, AR.slots(U32, T), Nat.double(h), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), 1n+Nat.double(h), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0))), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), put_dec(AR.slots(U32, T), kl, h, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), 1n+bp, g_htb(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), Equal.cong(Bool, List<&2, B.Bk>, c => IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, TB.dec_c(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), kl, c)), U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0), False{}, hc)))  +a1 = RG.bupd_comm(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, M.pos(1n+bp, h, dk), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, B.BE{}, g_hhk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))  +a2 = RG.bupd_comm(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, M.pos(1n+bp, h, dk), B.BE{}, B.BE{}, g_hhk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))  +a3 = RG.bupd_over(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), h, B.BE{}, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))})  Equal.trans(List<&2, B.Bk>, IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), Equal.cong(List<&2, B.Bk>, List<&2, B.Bk>, z => IM.bupd(z, M.pos(1n+bp, h, dk), B.BE{}), TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), eb), Equal.trans(List<&2, B.Bk>, IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), a1, Equal.sym(List<&2, B.Bk>, IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), Equal.trans(List<&2, B.Bk>, IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), h, B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), Equal.cong(List<&2, B.Bk>, List<&2, B.Bk>, z => IM.bupd(z, h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), h, B.BE{}), a2), a3))))def mv_fin(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}, +hm: {U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))) == True{} : Bool}, r: DelOK(kl, K, bp, V0, p, kU, H.bnext(kU, CY.msk(K)), AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T):  match r:    case Tuple{+Tf, Tuple{+e1, +hdf}}:      +s4 = Equal.cong(Bool, Array<U32>, c => H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), c), CY.msk(K), iU, kU), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), True{}, hm)      +s5 = Equal.cong(Array<U32>, Array<U32>, a => H.shift(p, H.sh_step(a, CY.msk(K), kU, H.bnext(kU, CY.msk(K))), CY.msk(K), kU, H.bnext(kU, CY.msk(K))), H.put_bucket(AR.thaw(U32, T), iU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), Equal.trans(Array<U32>, H.put_bucket(AR.thaw(U32, T), iU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), H.put_bucket(AR.thaw(U32, T), U32.from_nat(h), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), Equal.cong(U32, Array<U32>, i => H.put_bucket(AR.thaw(U32, T), i, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), iU, U32.from_nat(h), e_iu(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), GR.put_eq(K, hK, T, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), h, g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))))      (Tf, (Equal.trans(Array<U32>, H.shift(1n+p, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), CY.msk(K), iU, kU), H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), CY.msk(K), iU, kU), AR.thaw(U32, Tf), eq_mv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hc), Equal.trans(Array<U32>, H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), CY.msk(K), iU, kU), H.shift(p, H.sh_step(H.put_bucket(AR.thaw(U32, T), iU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), CY.msk(K), kU, H.bnext(kU, CY.msk(K))), CY.msk(K), kU, H.bnext(kU, CY.msk(K))), AR.thaw(U32, Tf), s4, Equal.trans(Array<U32>, H.shift(p, H.sh_step(H.put_bucket(AR.thaw(U32, T), iU, W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), CY.msk(K), kU, H.bnext(kU, CY.msk(K))), CY.msk(K), kU, H.bnext(kU, CY.msk(K))), H.shift(p, H.sh_step(AR.thaw(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), CY.msk(K), kU, H.bnext(kU, CY.msk(K))), CY.msk(K), kU, H.bnext(kU, CY.msk(K))), AR.thaw(U32, Tf), s5, e1))), hdf))def step_move(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hfu: {Nat.is_lt(M.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}, +hm: {U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))) == True{} : Bool}, rec: @+st2: DSt -> @+hi2: {dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2: {dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T):  +g = Equal.trans(Bool, Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), True{}, Equal.sym(Bool, U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), mvv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), hm)  +hmv = N.not_lt_le(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk, Equal.trans(Bool, Nat.is_lt(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), Bool.not(Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk)), False{}, WR.lt_ge(Nat.cmp(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk)), Equal.cong(Bool, Bool, b => Bool.not(b), Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), True{}, g)))  +hkn = g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)  +nke = g_nke(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)  +hhe = g_nhe(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)  +c2 = IS.eq_is_eq(UD.v(H.bnext(kU, CY.msk(K))), M.pos(1n+bp, M.pos(1n+bp, h, dk), 1n), Equal.trans(Nat, UD.v(H.bnext(kU, CY.msk(K))), Nat.mod(1n+M.pos(1n+bp, h, dk), 1n+bp), M.pos(1n+bp, M.pos(1n+bp, h, dk), 1n), g_nv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), 1n+M.pos(1n+bp, h, dk), Nat.add(M.pos(1n+bp, h, dk), 1n), Equal.sym(Nat, Nat.add(M.pos(1n+bp, h, dk), 1n), 1n+M.pos(1n+bp, h, dk), N.add_comm(M.pos(1n+bp, h, dk), 1n)))))  +c4 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PHole{z, 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, 1n+bp) == True{} : Bool} , IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), Equal.sym(List<&2, B.Bk>, IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), ev2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), HO.hole_move(K, bp, hN, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dk, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hdn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, g_hbk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc), {==}, hmv, lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, M.pos(1n+bp, h, dk), hkn), q4(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))  +c5 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PUniq{z}, 1n+bp) == True{} : Bool} , IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), Equal.sym(List<&2, B.Bk>, IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), ev2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), DM.uq_move(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, M.pos(1n+bp, h, dk), hkn, lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, M.pos(1n+bp, h, dk), hkn), q5(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))))), g_hbk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))))  +c6 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PFrom{z, V0, 1n+bp}, 1n+bp) == True{} : Bool} , IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), Equal.sym(List<&2, B.Bk>, IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), ev2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), DM.from_move(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, h, M.pos(1n+bp, h, dk), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, g_hbk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc), {==}, g_hzh(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), g_hhk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, M.pos(1n+bp, h, dk), g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), V0, 1n+bp, q6(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), hkn))  +c7 = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PTo{V0, z, 1n+bp}, 1n+bp) == True{} : Bool} , IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), Equal.sym(List<&2, B.Bk>, IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), ev2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), DM.to_move(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, h, M.pos(1n+bp, h, dk), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, g_hbk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc), {==}, g_hzh(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), g_hhk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, M.pos(1n+bp, h, dk), g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), V0, 1n+bp, q7(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))  +c8 = L.subst(List<&2, B.Bk>, z => {Nat.is_eq(IV.occn(z, 1n+bp), IV.occn(V0, 1n+bp)) == True{} : Bool} , IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), Equal.sym(List<&2, B.Bk>, IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), ev2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), IS.eq_is_eq(IV.occn(IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), 1n+bp), IV.occn(V0, 1n+bp), Equal.trans(Nat, IV.occn(IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), 1n+bp), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp), DM.occn_move(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, h, M.pos(1n+bp, h, dk), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, g_hbk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc), {==}, g_hzh(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), g_hhk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, M.pos(1n+bp, h, dk), g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), hkn, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), N.eq_from_is_eq(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp), IV.occn(V0, 1n+bp), q8(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))))  +c9 = L.subst(List<&2, B.Bk>, z => {Bool.not(B.occ(B.at(z, e0))) == True{} : Bool} , IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), Equal.sym(List<&2, B.Bk>, IM.bupd(TB.buckets(AR.slots(U32, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))), kl, 1n+bp), M.pos(1n+bp, h, dk), B.BE{}), IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), ev2(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), L.subst(B.Bk, y => {Bool.not(B.occ(y)) == True{} : Bool}, B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0), B.at(IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), e0), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk), B.BE{}), h, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}), e0), B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), e0), DM.at_vo(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), 1n+bp, h, M.pos(1n+bp, h, dk), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, g_hbk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc), {==}, g_hzh(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), g_hhk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), lt_lv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, M.pos(1n+bp, h, dk), g_hkn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), e0, hhe, nke)), q9(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)))  +dsum = HO.dist_split2(bp, h, M.pos(1n+bp, h, dk), e0, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), hkn, he0, L.subst(Nat, z => {Nat.is_lt(z, M.dist(1n+bp, h, e0)) == True{} : Bool}, dk, M.dist(1n+bp, h, M.pos(1n+bp, h, dk)), Equal.sym(Nat, M.dist(1n+bp, h, M.pos(1n+bp, h, dk)), dk, HO.dist_k(K, bp, hN, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dk, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hdn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi))), g_dlt(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)))  +dsum2 = Equal.trans(Nat, Nat.add(dk, M.dist(1n+bp, M.pos(1n+bp, h, dk), e0)), Nat.add(M.dist(1n+bp, h, M.pos(1n+bp, h, dk)), M.dist(1n+bp, M.pos(1n+bp, h, dk), e0)), M.dist(1n+bp, h, e0), Equal.cong(Nat, Nat, z => Nat.add(z, M.dist(1n+bp, M.pos(1n+bp, h, dk), e0)), dk, M.dist(1n+bp, h, M.pos(1n+bp, h, dk)), Equal.sym(Nat, M.dist(1n+bp, h, M.pos(1n+bp, h, dk)), dk, HO.dist_k(K, bp, hN, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dk, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hdn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)))), dsum)  +hf2 = RG.zy_lt(dk, 1n+p, M.dist(1n+bp, M.pos(1n+bp, h, dk), e0), L.subst(Nat, z => {Nat.is_lt(z, Nat.add(dk, 1n+p)) == True{} : Bool}, M.dist(1n+bp, h, e0), Nat.add(dk, M.dist(1n+bp, M.pos(1n+bp, h, dk), e0)), Equal.sym(Nat, Nat.add(dk, M.dist(1n+bp, M.pos(1n+bp, h, dk), e0)), M.dist(1n+bp, h, e0), dsum2), hfu))  +hi2 = q_mk(kl, K, bp, V0, e0, kU, M.pos(1n+bp, h, dk), H.bnext(kU, CY.msk(K)), 1n, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), q2(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), c2, GR.put_perf(K, hK, T, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), h, g_hhK(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))), c4, c5, c6, c7, c8, c9, {==}, HO.dist_pos1(bp, M.pos(1n+bp, h, dk), e0, hkn, he0, nke), hkn)  mv_fin(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hc, hm, rec(DS{kU, M.pos(1n+bp, h, dk), H.bnext(kU, CY.msk(K)), 1n, AR.upd(U32, 1n+K, AR.upd(U32, 1n+K, T, UD.v(U32.shl(U32.from_nat(h))), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk)))), UD.v(U32.inc(U32.shl(U32.from_nat(h)))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))))}, hi2, hf2))# ---- skip ----def sk_fin(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}, +hm: {U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))) == False{} : Bool}, r: DelOK(kl, K, bp, V0, p, iU, H.bnext(kU, CY.msk(K)), T)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T):  match r:    case Tuple{+Tf, Tuple{+e1, +hdf}}:      +s4 = Equal.cong(Bool, Array<U32>, c => H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), c), CY.msk(K), iU, kU), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), False{}, hm)      (Tf, (Equal.trans(Array<U32>, H.shift(1n+p, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, kU), CY.msk(K), iU, kU), H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), CY.msk(K), iU, kU), AR.thaw(U32, Tf), eq_mv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hc), Equal.trans(Array<U32>, H.shift(1n+p, H.sh_mv(AR.thaw(U32, T), W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K)))), CY.msk(K), iU, kU), H.shift(p, H.sh_step(AR.thaw(U32, T), CY.msk(K), iU, H.bnext(kU, CY.msk(K))), CY.msk(K), iU, H.bnext(kU, CY.msk(K))), AR.thaw(U32, Tf), s4, e1)), hdf))def step_skip(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hfu: {Nat.is_lt(M.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}, +hm: {U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))) == False{} : Bool}, rec: @+st2: DSt -> @+hi2: {dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2: {dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T):  +g = Equal.trans(Bool, Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), False{}, Equal.sym(Bool, U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), mvv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi)), hm)  +lt = Equal.trans(Bool, Nat.is_lt(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), Bool.not(Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk)), True{}, WR.lt_ge(Nat.cmp(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk)), Equal.cong(Bool, Bool, b => Bool.not(b), Nat.is_ge(M.dist(1n+bp, UD.v(HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), M.pos(1n+bp, h, dk)), dk), False{}, g))  +hsk = L.subst(B.Bk, y => {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), y), M.pos(1n+bp, h, dk)), dk) == True{} : Bool}, B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk)), Equal.sym(B.Bk, B.at(IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), M.pos(1n+bp, h, dk)), B.BF{W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk))), TB.keyof(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), TB.nths(kl, UD.v(H.slot(W32.nth0(AR.slots(U32, T), 1n+Nat.double(M.pos(1n+bp, h, dk)))))))}, g_hbk(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), lt)  +c2 = IS.eq_is_eq(UD.v(H.bnext(kU, CY.msk(K))), M.pos(1n+bp, h, 1n+dk), Equal.trans(Nat, UD.v(H.bnext(kU, CY.msk(K))), Nat.mod(1n+M.pos(1n+bp, h, dk), 1n+bp), M.pos(1n+bp, h, 1n+dk), g_nv(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), M.pos_next(bp, h, dk)))  +c4 = HO.hole_skip(K, bp, hN, IM.bupd(TB.buckets(AR.slots(U32, T), kl, 1n+bp), h, B.BE{}), h, q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), dk, q10(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), g_hdn(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi), hsk, q4(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))  +hf2 = L.subst(Nat, z => {Nat.is_lt(M.dist(1n+bp, h, e0), z) == True{} : Bool}, Nat.add(dk, 1n+p), 1n+Nat.add(dk, p), N.add_succ(dk, p), hfu)  +hi2 = q_mk(kl, K, bp, V0, e0, iU, h, H.bnext(kU, CY.msk(K)), 1n+dk, T, q1(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), c2, q3(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), c4, q5(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), q6(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), q7(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), q8(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), q9(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi), N.zero_le(dk), N.lt_succ_le_succ(dk, M.dist(1n+bp, h, e0), g_dlt(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, hc)), q12(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi))  sk_fin(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hc, hm, rec(DS{iU, h, H.bnext(kU, CY.msk(K)), 1n+dk, T}, hi2, hf2))# ---- dispatch and loop ----def step_mvc(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hfu: {Nat.is_lt(M.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool}, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == False{} : Bool}, +m: Bool, +hm: {U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))) == m : Bool}, rec: @+st2: DSt -> @+hi2: {dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2: {dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T):  match m:    case True{}:      step_move(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hfu, hc, hm, rec)    case False{}:      step_skip(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hfu, hc, hm, rec)def step_c(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +iU: U32, +h: Nat, +kU: U32, +dk: Nat, +T: AR.Tree<U32>, +hi: {dinvF(kl, K, bp, V0, e0, iU, h, kU, dk, T) == True{} : Bool}, +p: Nat, +hfu: {Nat.is_lt(M.dist(1n+bp, h, e0), Nat.add(dk, 1n+p)) == True{} : Bool}, +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0) == c : Bool}, rec: @+st2: DSt -> @+hi2: {dinv(kl, K, bp, V0, e0, st2) == True{} : Bool} -> @+hf2: {dfuel(bp, e0, p, st2) == True{} : Bool} -> DelOKs(kl, K, bp, V0, p, st2)) -> DelOK(kl, K, bp, V0, 1n+p, iU, kU, T):  match c:    case True{}:      step_end(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hc)    case False{}:      step_mvc(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hfu, hc, U32.is_ge(U32.and(U32.sub(kU, HS.bucket(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), CY.msk(K))), CY.msk(K)), U32.and(U32.sub(kU, iU), CY.msk(K))), {==}, rec)# THEOREM: the backward shift, run with enough fuel, ends with whole clustersdef loop(+one: Nat, +h1: {one == 1n : Nat}, +kl: List<&2, String>, +K: Nat, +bp: Nat, +V0: List<&2, B.Bk>, +e0: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +hN: {1n+bp == SC.pow2(K) : Nat}, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +f: Nat, +st: DSt, +hi: {dinv(kl, K, bp, V0, e0, st) == True{} : Bool}, +hfu: {dfuel(bp, e0, f, st) == True{} : Bool}) -> DelOKs(kl, K, bp, V0, f, st):  match f st:    case 0n DS{+iU, +h, +kU, +dk, +T}:      +lt = L.subst(Nat, z => {Nat.is_lt(M.dist(1n+bp, h, e0), z) == True{} : Bool}, Nat.add(dk, 0n), dk, N.add_zero(dk), hfu)      Empty.absurd(DelOK(kl, K, bp, V0, 0n, iU, kU, T), L.true_false(Equal.trans(Bool, True{}, Nat.is_le(dk, M.dist(1n+bp, h, e0)), False{}, Equal.sym(Bool, Nat.is_le(dk, M.dist(1n+bp, h, e0)), True{}, q11(kl, K, bp, V0, e0, iU, h, kU, dk, T, hi)), N.lt_not_le(M.dist(1n+bp, h, e0), dk, lt))))    case 1n+p DS{+iU, +h, +kU, +dk, +T}:      step_c(one, h1, kl, K, bp, V0, e0, hK, hN, he0, iU, h, kU, dk, T, hi, p, hfu, U32.is_eq(W32.nth0(AR.slots(U32, T), Nat.double(M.pos(1n+bp, h, dk))), 0), {==}, st2 => hi2 => hf2 => loop(one, h1, kl, K, bp, V0, e0, hK, hN, he0, p, st2, hi2, hf2))# ---- the start ----def cr_i(+bs: List<&2, B.Bk>, +n: Nat, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}) -> {B.implies(B.occ(B.at(bs, j)), B.anyeq(bs, n, B.at(bs, j))) == True{} : Bool}:  RH.imp_true(B.occ(B.at(bs, j)), B.anyeq(bs, n, B.at(bs, j)), RH.anyeq_intro(bs, n, B.at(bs, j), j, hj, RH.bk_refl(B.at(bs, j))))def from_refl(+bs: List<&2, B.Bk>, +n: Nat, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PFrom{bs, bs, 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.PFrom{bs, bs, n}, q), B.all_lt(B.PFrom{bs, bs, n}, q), cr_i(bs, n, q, hq), from_refl(bs, n, q, N.lt_le(q, n, hq)))def to_refl(+bs: List<&2, B.Bk>, +n: Nat, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PTo{bs, bs, 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.PTo{bs, bs, n}, q), B.all_lt(B.PTo{bs, bs, n}, q), cr_i(bs, n, q, hq), to_refl(bs, n, q, N.lt_le(q, n, hq)))def DelAt(+kl: List<&2, String>, +K: Nat, +bp: Nat, +OT: AR.Tree<U32>, +i: Nat) -> Type:  Sigma<&1, &1, AR.Tree<U32>, Tf => {H.del_at(AR.thaw(U32, OT), CY.msk(K), U32.from_nat(i)) == AR.thaw(U32, Tf) : Array<U32>} & {dfin(kl, K, bp, IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, B.BE{}), Tf) == True{} : Bool}>def d_hiK(+one: Nat, +h1: {one == 1n : Nat}, +K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+K, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool}) -> {Nat.is_lt(i, SC.pow2(K)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, 1n+bp, SC.pow2(K), hN, hi)def d_ev(+one: Nat, +h1: {one == 1n : Nat}, +K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+K, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool}) -> {UD.v(U32.from_nat(i)) == i : Nat}:  U.to_nat_from_nat(i, K, N.lt_le(K, 32n, N.lt_trans(K, 31n, 32n, hK, {==})), d_hiK(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi))def d_hlen(+one: Nat, +h1: {one == 1n : Nat}, +K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+K, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool}) -> {Nat.is_lt(i, SC.length(B.Bk, TB.buckets(AR.slots(U32, OT), kl, 1n+bp))) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, 1n+bp, SC.length(B.Bk, TB.buckets(AR.slots(U32, OT), kl, 1n+bp)), Equal.sym(Nat, SC.length(B.Bk, TB.buckets(AR.slots(U32, OT), kl, 1n+bp)), 1n+bp, IA.len_dlist(AR.slots(U32, OT), kl, 1n+bp, 0n)), hi)def d_kv(+one: Nat, +h1: {one == 1n : Nat}, +K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+K, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool}) -> {UD.v(H.bnext(U32.from_nat(i), CY.msk(K))) == M.pos(1n+bp, i, 1n) : Nat}:  +hks = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, SC.pow2(K), WD.sc(K, one), W32.pow_one(one, h1, K), N.lt_le_trans(SC.pow2(K), SC.pow2(1n+K), WD.sc(32n, one), N.pow2_lt_succ(K), W32.pow_le32(one, h1, 1n+K, hK)))  +scn = Equal.trans(Nat, WD.sc(K, one), SC.pow2(K), 1n+bp, Equal.sym(Nat, SC.pow2(K), WD.sc(K, one), W32.pow_one(one, h1, K)), Equal.sym(Nat, 1n+bp, SC.pow2(K), hN))  +hil = L.subst(Nat, z => {Nat.is_lt(UD.v(U32.from_nat(i)), z) == True{} : Bool}, SC.pow2(K), WD.sc(K, one), W32.pow_one(one, h1, K), L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(K)) == True{} : Bool}, i, UD.v(U32.from_nat(i)), Equal.sym(Nat, UD.v(U32.from_nat(i)), i, d_ev(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi)), d_hiK(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi)))  Equal.trans(Nat, UD.v(H.bnext(U32.from_nat(i), CY.msk(K))), Nat.mod(1n+UD.v(U32.from_nat(i)), WD.sc(K, one)), M.pos(1n+bp, i, 1n), CY.next_val(one, h1, K, U32.from_nat(i), hks, hil), Equal.trans(Nat, Nat.mod(1n+UD.v(U32.from_nat(i)), WD.sc(K, one)), Nat.mod(1n+i, 1n+bp), M.pos(1n+bp, i, 1n), Equal.trans(Nat, Nat.mod(1n+UD.v(U32.from_nat(i)), WD.sc(K, one)), Nat.mod(1n+UD.v(U32.from_nat(i)), 1n+bp), Nat.mod(1n+i, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(1n+UD.v(U32.from_nat(i)), z), WD.sc(K, one), 1n+bp, scn), Equal.cong(Nat, Nat, z => Nat.mod(1n+z, 1n+bp), UD.v(U32.from_nat(i)), i, d_ev(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi))), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), 1n+i, Nat.add(i, 1n), Equal.sym(Nat, Nat.add(i, 1n), 1n+i, N.add_comm(i, 1n)))))def z0_c(+O: List<&2, B.Bk>, +i: Nat, +e0: Nat, +hz0: {B.at(O, e0) == B.BE{} : B.Bk}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, e0) == c : Bool}) -> {Bool.not(B.occ(B.at(IM.bupd(O, i, B.BE{}), e0))) == True{} : Bool}:  match c:    case True{}:      L.subst(B.Bk, y => {Bool.not(B.occ(y)) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), e0), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), e0), B.BE{}, IM.at_bu_eq(O, i, B.BE{}, hlen, e0, hc)), {==})    case False{}:      L.subst(B.Bk, y => {Bool.not(B.occ(y)) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), e0), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), e0), B.BE{}, Equal.trans(B.Bk, B.at(IM.bupd(O, i, B.BE{}), e0), B.at(O, e0), B.BE{}, IM.at_bupd_other(O, i, B.BE{}, e0, hc), hz0)), {==})def d_fin(+one: Nat, +h1: {one == 1n : Nat}, +K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+K, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool}, +e0: Nat, lo: DelOK(kl, K, bp, IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, B.BE{}), 1n+bp, U32.from_nat(i), H.bnext(U32.from_nat(i), CY.msk(K)), OT)) -> DelAt(kl, K, bp, OT, i):  match lo:    case Tuple{+Tf, Tuple{+e1, +hdf}}:      +ef = Equal.trans(Nat, U32.to_nat(U32.inc(CY.msk(K))), SC.pow2(K), 1n+bp, PA.fuel_eq(one, h1, K, hK), Equal.sym(Nat, 1n+bp, SC.pow2(K), hN))      (Tf, (Equal.trans(Array<U32>, H.del_at(AR.thaw(U32, OT), CY.msk(K), U32.from_nat(i)), H.shift(1n+bp, H.sh_step(AR.thaw(U32, OT), CY.msk(K), U32.from_nat(i), H.bnext(U32.from_nat(i), CY.msk(K))), CY.msk(K), U32.from_nat(i), H.bnext(U32.from_nat(i), CY.msk(K))), AR.thaw(U32, Tf), Equal.cong(Nat, Array<U32>, f => H.shift(f, H.sh_step(AR.thaw(U32, OT), CY.msk(K), U32.from_nat(i), H.bnext(U32.from_nat(i), CY.msk(K))), CY.msk(K), U32.from_nat(i), H.bnext(U32.from_nat(i), CY.msk(K))), U32.to_nat(U32.inc(CY.msk(K))), 1n+bp, ef), e1), hdf))def d_e0(+one: Nat, +h1: {one == 1n : Nat}, +K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+K, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool}, e0p: IV.Empty0(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp)) -> DelAt(kl, K, bp, OT, i):  match e0p:    case Tuple{+e0, Tuple{+he0, +hz0}}:      +hlen = d_hlen(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi)      +nie = RH.ne_occ(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), e0, hz0, i, hoi, Nat.is_eq(e0, i), {==})      +hi0 = q_mk(kl, K, bp, IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, B.BE{}), e0, U32.from_nat(i), i, H.bnext(U32.from_nat(i), CY.msk(K)), 1n, OT, IS.eq_is_eq(UD.v(U32.from_nat(i)), i, d_ev(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi)), IS.eq_is_eq(UD.v(H.bnext(U32.from_nat(i), CY.msk(K))), M.pos(1n+bp, i, 1n), d_kv(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi)), pot, HO.hole_init(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), K, bp, hN, i, hi, hlen, cl, 1n+bp, N.le_refl(1n+bp)), DM.uq_rm(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, hlen, 1n+bp, huo, 1n+bp, N.le_refl(1n+bp)), from_refl(IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, B.BE{}), 1n+bp, 1n+bp, N.le_refl(1n+bp)), to_refl(IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, B.BE{}), 1n+bp, 1n+bp, N.le_refl(1n+bp)), N.is_eq_refl(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, B.BE{}), 1n+bp)), z0_c(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, e0, hz0, hlen, Nat.is_eq(i, e0), {==}), {==}, HO.dist_pos1(bp, i, e0, hi, he0, N.is_eq_sym_false(e0, i, nie)), hi)      +hf0 = N.lt_trans(M.dist(1n+bp, i, e0), 1n+bp, 1n+1n+bp, M.dist_lt(bp, i, e0), N.lt_succ(1n+bp))      d_fin(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi, e0, loop(one, h1, kl, K, bp, IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i, B.BE{}), e0, hK, hN, he0, 1n+bp, DS{U32.from_nat(i), i, H.bnext(U32.from_nat(i), CY.msk(K)), 1n, OT}, hi0, hf0))# THEOREM: deleting bucket i of a clustered table with a free bucket leaves a# clustered table of copies of the other bucketsdef del_ok(+one: Nat, +h1: {one == 1n : Nat}, +K: Nat, +hK: {Nat.is_lt(K, 31n) == True{} : Bool}, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +pot: {AR.perfect(U32, 1n+K, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, CY.msk(K)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, 1n+bp)}, 1n+bp) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), i)) == True{} : Bool}, +hem: {Nat.is_lt(IV.occn(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp), 1n+bp) == True{} : Bool}) -> DelAt(kl, K, bp, OT, i):  d_e0(one, h1, K, hK, bp, hN, kl, OT, pot, i, hi, cl, huo, hoi, IV.find_empty(TB.buckets(AR.slots(U32, OT), kl, 1n+bp), 1n+bp, hem))