1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../lib/u32div.bend as UD
6	import ../../../src/math/hash.bend as HS
7	import ./buckets.bend as B
8	import ./modn.bend as M
9	import ./cyc.bend as CY
10	import ./probe_all.bend as PA
11	import ./insm.bend as IM
12	import ./insert.bend as IS
13	import ./ring.bend as RG
14	import ./rehash.bend as RH
15	
16	# Backward-shift deletion at the bucket level. While the gap left by the
17	# removed bucket travels forward, every full bucket's path is full except
18	# possibly at the gap h, and only buckets at least dk past h have paths
19	# through h. When the scan meets an empty bucket, no path goes through the
20	# gap, so the clusters are whole again.
21	
22	
23	def hb_lt(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +b: B.Bk) -> {Nat.is_lt(B.hb(CY.msk(K), b), 1n+bp) == True{} : Bool}:
24	  match b:
25	    case B.BE{}:
26	      N.succ_le_lt(0n, 1n+bp, N.zero_le(bp))
27	    case B.BF{+w, l, k}:
28	      L.subst(Nat, z => {Nat.is_lt(UD.v(HS.bucket(w, CY.msk(K))), z) == True{} : Bool}, SC.pow2(K), 1n+bp, Equal.sym(Nat, 1n+bp, SC.pow2(K), hN), PA.home_lt(w, K))
29	
30	# ---- paths full except at h ----
31	
32	def ox_c(+bs: List<&2, B.Bk>, +n: Nat, +a: Nat, +h: Nat, +q: Nat, +hp: {Bool.and(Bool.or(Nat.is_eq(h, M.pos(n, a, q)), B.occ(B.at(bs, M.pos(n, a, q)))), B.opx(bs, n, a, q, h)) == True{} : Bool}, +t: Nat, +ht: {Nat.is_lt(t, 1n+q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(t, q) == c : Bool}, rec: @hlt: {Nat.is_lt(t, q) == True{} : Bool} -> {Bool.or(Nat.is_eq(h, M.pos(n, a, t)), B.occ(B.at(bs, M.pos(n, a, t)))) == True{} : Bool}) -> {Bool.or(Nat.is_eq(h, M.pos(n, a, t)), B.occ(B.at(bs, M.pos(n, a, t)))) == True{} : Bool}:
33	  match c:
34	    case True{}:
35	      L.subst(Nat, z => {Bool.or(Nat.is_eq(h, M.pos(n, a, z)), B.occ(B.at(bs, M.pos(n, a, z)))) == True{} : Bool}, q, t, Equal.sym(Nat, t, q, N.eq_from_is_eq(t, q, hc)), L.and_left(Bool.or(Nat.is_eq(h, M.pos(n, a, q)), B.occ(B.at(bs, M.pos(n, a, q)))), B.opx(bs, n, a, q, h), hp))
36	    case False{}:
37	      rec(N.lt_or_eq(t, q, N.lt_succ_le(t, q, ht), hc))
38	
39	def opx_inst(+bs: List<&2, B.Bk>, +n: Nat, +a: Nat, +m: Nat, +h: Nat, +hp: {B.opx(bs, n, a, m, h) == True{} : Bool}, +t: Nat, +ht: {Nat.is_lt(t, m) == True{} : Bool}) -> {Bool.or(Nat.is_eq(h, M.pos(n, a, t)), B.occ(B.at(bs, M.pos(n, a, t)))) == True{} : Bool}:
40	  match m:
41	    case 0n:
42	      Empty.absurd({Bool.or(Nat.is_eq(h, M.pos(n, a, t)), B.occ(B.at(bs, M.pos(n, a, t)))) == True{} : Bool}, N.lt_zero_absurd(t, ht))
43	    case 1n+q:
44	      ox_c(bs, n, a, h, q, hp, t, ht, Nat.is_eq(t, q), {==}, hlt => opx_inst(bs, n, a, q, h, L.and_right(Bool.or(Nat.is_eq(h, M.pos(n, a, q)), B.occ(B.at(bs, M.pos(n, a, q)))), B.opx(bs, n, a, q, h), hp), t, hlt))
45	
46	def opx_pre(+bs: List<&2, B.Bk>, +n: Nat, +a: Nat, +m: Nat, +h: Nat, +hp: {B.opx(bs, n, a, m, h) == True{} : Bool}, +m2: Nat, +hm: {Nat.is_le(m2, m) == True{} : Bool}) -> {B.opx(bs, n, a, m2, h) == True{} : Bool}:
47	  match m2:
48	    case 0n:
49	      {==}
50	    case 1n+s:
51	      +hs = N.succ_le_lt(s, m, hm)
52	      L.and_intro(Bool.or(Nat.is_eq(h, M.pos(n, a, s)), B.occ(B.at(bs, M.pos(n, a, s)))), B.opx(bs, n, a, s, h), opx_inst(bs, n, a, m, h, hp, s, hs), opx_pre(bs, n, a, m, h, hp, s, N.lt_le(s, m, hs)))
53	
54	def or_f(+x: Bool, +y: Bool, +h: {Bool.or(x, y) == True{} : Bool}, +hx: {x == False{} : Bool}) -> {y == True{} : Bool}:
55	  L.subst(Bool, z => {Bool.or(z, y) == True{} : Bool}, x, False{}, hx, h)
56	
57	# a path that does not reach h is full
58	def occ_of_opx(+bs: List<&2, B.Bk>, +bp: Nat, +a: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +h: Nat, +m: Nat, +hm: {Nat.is_le(m, 1n+bp) == True{} : Bool}, +hp: {B.opx(bs, 1n+bp, a, m, h) == True{} : Bool}, +hn: {Nat.is_lt(M.dist(1n+bp, a, h), m) == False{} : Bool}) -> {B.occpath(bs, 1n+bp, a, m) == True{} : Bool}:
59	  match m:
60	    case 0n:
61	      {==}
62	    case 1n+s:
63	      +d = M.dist(1n+bp, a, h)
64	      +hd = N.not_lt_le(d, 1n+s, hn)
65	      +hsd = N.lt_le_trans(s, 1n+s, d, N.lt_succ(s), hd)
66	      +hne = N.is_eq_sym_false(M.pos(1n+bp, a, s), h, RG.pos_ne(bp, a, s, h, ha, N.lt_le_trans(s, 1n+s, 1n+bp, N.lt_succ(s), hm), N.is_eq_lt(s, d, hsd)))
67	      +x = Bool.or(Nat.is_eq(h, M.pos(1n+bp, a, s)), B.occ(B.at(bs, M.pos(1n+bp, a, s))))
68	      L.and_intro(B.occ(B.at(bs, M.pos(1n+bp, a, s))), B.occpath(bs, 1n+bp, a, s), or_f(Nat.is_eq(h, M.pos(1n+bp, a, s)), B.occ(B.at(bs, M.pos(1n+bp, a, s))), L.and_left(x, B.opx(bs, 1n+bp, a, s, h), hp), hne), occ_of_opx(bs, bp, a, ha, h, s, N.lt_le(s, 1n+bp, N.lt_le_trans(s, 1n+s, 1n+bp, N.lt_succ(s), hm)), L.and_right(x, B.opx(bs, 1n+bp, a, s, h), hp), N.le_not_lt(d, s, N.lt_le(s, d, hsd))))
69	
70	def ooc_bit(+bs: List<&2, B.Bk>, +i: Nat, +p: Nat, +ho: {B.occ(B.at(bs, p)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, p) == c : Bool}) -> {Bool.or(c, B.occ(B.at(IM.bupd(bs, i, B.BE{}), p))) == True{} : Bool}:
71	  match c:
72	    case True{}:
73	      {==}
74	    case False{}:
75	      L.subst(B.Bk, y => {Bool.or(False{}, B.occ(y)) == True{} : Bool}, B.at(bs, p), B.at(IM.bupd(bs, i, B.BE{}), p), Equal.sym(B.Bk, B.at(IM.bupd(bs, i, B.BE{}), p), B.at(bs, p), IM.at_bupd_other(bs, i, B.BE{}, p, hc)), ho)
76	
77	# emptying bucket i leaves every full path full except at i
78	def opx_of_occ(+bs: List<&2, B.Bk>, +i: Nat, +n: Nat, +a: Nat, +m: Nat, +hp: {B.occpath(bs, n, a, m) == True{} : Bool}) -> {B.opx(IM.bupd(bs, i, B.BE{}), n, a, m, i) == True{} : Bool}:
79	  match m:
80	    case 0n:
81	      {==}
82	    case 1n+s:
83	      +p = M.pos(n, a, s)
84	      L.and_intro(Bool.or(Nat.is_eq(i, p), B.occ(B.at(IM.bupd(bs, i, B.BE{}), p))), B.opx(IM.bupd(bs, i, B.BE{}), n, a, s, i), L.subst(Bool, c => {Bool.or(c, B.occ(B.at(IM.bupd(bs, i, B.BE{}), p))) == True{} : Bool}, Nat.is_eq(i, p), Nat.is_eq(i, p), {==}, ooc_bit(bs, i, p, L.and_left(B.occ(B.at(bs, p)), B.occpath(bs, n, a, s), hp), Nat.is_eq(i, p), {==})), opx_of_occ(bs, i, n, a, s, L.and_right(B.occ(B.at(bs, p)), B.occpath(bs, n, a, s), hp)))
85	
86	# ---- moving bucket k into the gap h ----
87	
88	
89	def hlen2(+V: List<&2, B.Bk>, +h: Nat, +k: Nat, +b: B.Bk, +hbo: {B.occ(b) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}) -> {Nat.is_lt(h, SC.length(B.Bk, IM.bupd(V, k, B.BE{}))) == True{} : Bool}:
90	  L.subst(Nat, z => {Nat.is_lt(h, z) == True{} : Bool}, SC.length(B.Bk, V), SC.length(B.Bk, IM.bupd(V, k, B.BE{})), Equal.sym(Nat, SC.length(B.Bk, IM.bupd(V, k, B.BE{})), SC.length(B.Bk, V), RG.len_bupd(V, k, B.BE{})), hlen)
91	
92	def mv_h2(+V: List<&2, B.Bk>, +h: Nat, +k: Nat, +b: B.Bk, +hbo: {B.occ(b) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +p: Nat, +c: Bool, +hc: {Nat.is_eq(h, p) == c : Bool}, +hold: {Bool.or(c, B.occ(B.at(V, p))) == True{} : Bool}, +hck: {Nat.is_eq(k, p) == False{} : Bool}) -> {Bool.or(False{}, B.occ(B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p))) == True{} : Bool}:
93	  match c:
94	    case True{}:
95	      L.subst(B.Bk, y => {B.occ(y) == True{} : Bool}, b, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), b, IM.at_bu_eq(IM.bupd(V, k, B.BE{}), h, b, hlen2(V, h, k, b, hbo, hlen), p, hc)), hbo)
96	    case False{}:
97	      L.subst(B.Bk, y => {B.occ(y) == True{} : Bool}, B.at(V, p), B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), B.at(V, p), Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p), B.at(IM.bupd(V, k, B.BE{}), p), B.at(V, p), IM.at_bupd_other(IM.bupd(V, k, B.BE{}), h, b, p, hc), IM.at_bupd_other(V, k, B.BE{}, p, hck))), hold)
98	
99	def mv_h(+V: List<&2, B.Bk>, +h: Nat, +k: Nat, +b: B.Bk, +hbo: {B.occ(b) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +p: Nat, +c: Bool, +hc: {Nat.is_eq(h, p) == c : Bool}, +hold: {Bool.or(c, B.occ(B.at(V, p))) == True{} : Bool}, +ck: Bool, +hck: {Nat.is_eq(k, p) == ck : Bool}) -> {Bool.or(ck, B.occ(B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p))) == True{} : Bool}:
100	  match ck:
101	    case True{}:
102	      {==}
103	    case False{}:
104	      mv_h2(V, h, k, b, hbo, hlen, p, c, hc, hold, hck)
105	
106	# THEOREM: after the move, paths are full except at the new gap k
107	def opx_move(+V: List<&2, B.Bk>, +h: Nat, +k: Nat, +b: B.Bk, +hbo: {B.occ(b) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +n: Nat, +a: Nat, +m: Nat, +hp: {B.opx(V, n, a, m, h) == True{} : Bool}) -> {B.opx(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, a, m, k) == True{} : Bool}:
108	  match m:
109	    case 0n:
110	      {==}
111	    case 1n+s:
112	      +p = M.pos(n, a, s)
113	      +x = Bool.or(Nat.is_eq(h, p), B.occ(B.at(V, p)))
114	      L.and_intro(Bool.or(Nat.is_eq(k, p), B.occ(B.at(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), p))), B.opx(IM.bupd(IM.bupd(V, k, B.BE{}), h, b), n, a, s, k), mv_h(V, h, k, b, hbo, hlen, p, Nat.is_eq(h, p), {==}, L.and_left(x, B.opx(V, n, a, s, h), hp), Nat.is_eq(k, p), {==}), opx_move(V, h, k, b, hbo, hlen, n, a, s, L.and_right(x, B.opx(V, n, a, s, h), hp)))
115	
116	# ---- more ring facts ----
117	
118	# a path from a through h to j: its length splits at h
119	def dist_split2(+bp: Nat, +a: Nat, +h: Nat, +j: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hlt: {Nat.is_lt(M.dist(1n+bp, a, h), M.dist(1n+bp, a, j)) == True{} : Bool}) -> {Nat.add(M.dist(1n+bp, a, h), M.dist(1n+bp, h, j)) == M.dist(1n+bp, a, j) : Nat}:
120	  +x = M.dist(1n+bp, a, h)
121	  +m = M.dist(1n+bp, a, j)
122	  +r = Nat.sub(m, x)
123	  +exr = N.sub_add(m, x, N.lt_le(x, m, hlt))
124	  +hr = N.le_lt_trans(r, m, 1n+bp, L.subst(Nat, z => {Nat.is_le(r, z) == True{} : Bool}, Nat.add(r, x), m, Equal.trans(Nat, Nat.add(r, x), Nat.add(x, r), m, N.add_comm(r, x), exr), N.le_add_right(r, x)), M.dist_lt(bp, a, j))
125	  +pj = Equal.trans(Nat, M.pos(1n+bp, h, r), M.pos(1n+bp, M.pos(1n+bp, a, x), r), j, Equal.cong(Nat, Nat, z => M.pos(1n+bp, z, r), h, M.pos(1n+bp, a, x), Equal.sym(Nat, M.pos(1n+bp, a, x), h, M.pos_dist(bp, a, h, ha, hh))), Equal.trans(Nat, M.pos(1n+bp, M.pos(1n+bp, a, x), r), M.pos(1n+bp, a, Nat.add(x, r)), j, RG.pos_add(bp, a, x, r), Equal.trans(Nat, M.pos(1n+bp, a, Nat.add(x, r)), M.pos(1n+bp, a, m), j, Equal.cong(Nat, Nat, z => M.pos(1n+bp, a, z), Nat.add(x, r), m, exr), M.pos_dist(bp, a, j, ha, hj))))
126	  +dr = Equal.trans(Nat, M.dist(1n+bp, h, j), M.dist(1n+bp, h, M.pos(1n+bp, h, r)), r, Equal.cong(Nat, Nat, z => M.dist(1n+bp, h, z), j, M.pos(1n+bp, h, r), Equal.sym(Nat, M.pos(1n+bp, h, r), j, pj)), M.dist_pos(bp, h, r, hh, hr))
127	  Equal.trans(Nat, Nat.add(x, M.dist(1n+bp, h, j)), Nat.add(x, r), m, Equal.cong(Nat, Nat, z => Nat.add(x, z), M.dist(1n+bp, h, j), r, dr), exr)
128	
129	def dp_c(+bp: Nat, +i: Nat, +j: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hne: {Nat.is_eq(i, j) == False{} : Bool}, +d: Nat, +hd: {M.dist(1n+bp, i, j) == d : Nat}) -> {Nat.is_le(1n, d) == True{} : Bool}:
130	  match d:
131	    case 0n:
132	      +e = RG.eq_of_dist0(bp, i, j, hi, hj, hd)
133	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_eq(i, j), False{}, Equal.sym(Bool, Nat.is_eq(i, j), True{}, IS.eq_is_eq(i, j, e)), hne)))
134	    case 1n+p:
135	      N.zero_le(p)
136	
137	# distinct buckets are at least one step apart
138	def dist_pos1(+bp: Nat, +i: Nat, +j: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hne: {Nat.is_eq(i, j) == False{} : Bool}) -> {Nat.is_le(1n, M.dist(1n+bp, i, j)) == True{} : Bool}:
139	  dp_c(bp, i, j, hi, hj, hne, M.dist(1n+bp, i, j), {==})
140	
141	# ---- the hole invariant: start ----
142	
143	
144	def h0_o(+O: List<&2, B.Bk>, +K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +x: B.Bk, +hx: {B.implies(B.occ(x), B.occpath(O, 1n+bp, B.hb(CY.msk(K), x), M.dist(1n+bp, B.hb(CY.msk(K), x), j))) == True{} : Bool}, +o: Bool, +ho: {B.occ(x) == o : Bool}) -> {B.implies(o, Bool.and(B.opx(IM.bupd(O, i, B.BE{}), 1n+bp, B.hb(CY.msk(K), x), M.dist(1n+bp, B.hb(CY.msk(K), x), j), i), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), x), i), M.dist(1n+bp, B.hb(CY.msk(K), x), j)), Nat.is_le(1n, M.dist(1n+bp, i, j))))) == True{} : Bool}:
145	  match o:
146	    case False{}:
147	      {==}
148	    case True{}:
149	      +op = B.imp_elim(B.occ(x), B.occpath(O, 1n+bp, B.hb(CY.msk(K), x), M.dist(1n+bp, B.hb(CY.msk(K), x), j)), hx, ho)
150	      L.and_intro(B.opx(IM.bupd(O, i, B.BE{}), 1n+bp, B.hb(CY.msk(K), x), M.dist(1n+bp, B.hb(CY.msk(K), x), j), i), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), x), i), M.dist(1n+bp, B.hb(CY.msk(K), x), j)), Nat.is_le(1n, M.dist(1n+bp, i, j))), opx_of_occ(O, i, 1n+bp, B.hb(CY.msk(K), x), M.dist(1n+bp, B.hb(CY.msk(K), x), j), op), RH.imp_true(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), x), i), M.dist(1n+bp, B.hb(CY.msk(K), x), j)), Nat.is_le(1n, M.dist(1n+bp, i, j)), dist_pos1(bp, i, j, hi, hj, hij)))
151	
152	
153	def h0_i(+O: List<&2, B.Bk>, +K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +cl: {B.cluster(O, 1n+bp, CY.msk(K)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {B.eval(B.PHole{IM.bupd(O, i, B.BE{}), 1n+bp, CY.msk(K), i, 1n}, j) == True{} : Bool}:
154	  match c:
155	    case True{}:
156	      L.subst(B.Bk, y => {B.implies(B.occ(y), Bool.and(B.opx(IM.bupd(O, i, B.BE{}), 1n+bp, B.hb(CY.msk(K), y), M.dist(1n+bp, B.hb(CY.msk(K), y), j), i), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), y), i), M.dist(1n+bp, B.hb(CY.msk(K), y), j)), Nat.is_le(1n, M.dist(1n+bp, i, j))))) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.BE{}, IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)), {==})
157	    case False{}:
158	      +x = B.at(O, j)
159	      L.subst(B.Bk, y => {B.implies(B.occ(y), Bool.and(B.opx(IM.bupd(O, i, B.BE{}), 1n+bp, B.hb(CY.msk(K), y), M.dist(1n+bp, B.hb(CY.msk(K), y), j), i), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), y), i), M.dist(1n+bp, B.hb(CY.msk(K), y), j)), Nat.is_le(1n, M.dist(1n+bp, i, j))))) == True{} : Bool}, x, B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), x, IM.at_bupd_other(O, i, B.BE{}, j, hc)), L.subst(Bool, o => {B.implies(o, Bool.and(B.opx(IM.bupd(O, i, B.BE{}), 1n+bp, B.hb(CY.msk(K), x), M.dist(1n+bp, B.hb(CY.msk(K), x), j), i), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), x), i), M.dist(1n+bp, B.hb(CY.msk(K), x), j)), Nat.is_le(1n, M.dist(1n+bp, i, j))))) == True{} : Bool}, B.occ(x), B.occ(x), {==}, h0_o(O, K, bp, hN, i, hi, j, hj, hc, x, B.all_inst(B.PClus{O, 1n+bp, CY.msk(K)}, 1n+bp, cl, j, hj), B.occ(x), {==})))
160	
161	# THEOREM: emptying a bucket of a clustered table starts the invariant
162	def hole_init(+O: List<&2, B.Bk>, +K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +i: Nat, +hi: {Nat.is_lt(i, 1n+bp) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +cl: {B.cluster(O, 1n+bp, CY.msk(K)) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, 1n+bp) == True{} : Bool}) -> {B.all_lt(B.PHole{IM.bupd(O, i, B.BE{}), 1n+bp, CY.msk(K), i, 1n}, m) == True{} : Bool}:
163	  match m:
164	    case 0n:
165	      {==}
166	    case 1n+q:
167	      +hq = N.succ_le_lt(q, 1n+bp, hm)
168	      L.and_intro(B.eval(B.PHole{IM.bupd(O, i, B.BE{}), 1n+bp, CY.msk(K), i, 1n}, q), B.all_lt(B.PHole{IM.bupd(O, i, B.BE{}), 1n+bp, CY.msk(K), i, 1n}, q), h0_i(O, K, bp, hN, i, hi, hlen, cl, q, hq, Nat.is_eq(i, q), {==}), hole_init(O, K, bp, hN, i, hi, hlen, cl, q, N.lt_le(q, 1n+bp, hq)))
169	
170	# ---- the scan position ----
171	
172	
173	def dist_k(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}) -> {M.dist(1n+bp, h, M.pos(1n+bp, h, dk)) == dk : Nat}:
174	  M.dist_pos(bp, h, dk, hh, hdn)
175	
176	def hk_c(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(h, M.pos(1n+bp, h, dk)) == c : Bool}) -> {c == False{} : Bool}:
177	  match c:
178	    case False{}:
179	      {==}
180	    case True{}:
181	      +e = Equal.trans(Nat, 0n, M.dist(1n+bp, h, h), dk, Equal.sym(Nat, M.dist(1n+bp, h, h), 0n, RG.dist_self(bp, h, hh)), Equal.trans(Nat, M.dist(1n+bp, h, h), M.dist(1n+bp, h, M.pos(1n+bp, h, dk)), dk, Equal.cong(Nat, Nat, z => M.dist(1n+bp, h, z), h, M.pos(1n+bp, h, dk), N.eq_from_is_eq(h, M.pos(1n+bp, h, dk), hc)), dist_k(K, bp, hN, V, h, hh, dk, hd1, hdn)))
182	      Empty.absurd({True{} == False{} : Bool}, L.false_true(L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, dk, 0n, Equal.sym(Nat, 0n, dk, e), hd1)))
183	
184	# the scan position is not the gap
185	def h_ne_k(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}) -> {Nat.is_eq(h, M.pos(1n+bp, h, dk)) == False{} : Bool}:
186	  hk_c(K, bp, hN, V, h, hh, dk, hd1, hdn, Nat.is_eq(h, M.pos(1n+bp, h, dk)), {==})
187	
188	# ---- end: the scan met an empty bucket ----
189	
190	def e_bad(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hz: {B.occ(B.at(V, M.pos(1n+bp, h, dk))) == False{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hoj: {B.occ(B.at(V, j)) == True{} : Bool}, +hop: {B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h) == True{} : Bool}, +hlt: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)) == True{} : Bool}, +hge: {Nat.is_le(dk, M.dist(1n+bp, h, j)) == True{} : Bool}, +c3: Bool, +hc3: {Nat.is_eq(dk, M.dist(1n+bp, h, j)) == c3 : Bool}) -> Empty:
191	  match c3:
192	    case True{}:
193	      +ejk = Equal.trans(Nat, j, M.pos(1n+bp, h, M.dist(1n+bp, h, j)), M.pos(1n+bp, h, dk), Equal.sym(Nat, M.pos(1n+bp, h, M.dist(1n+bp, h, j)), j, M.pos_dist(bp, h, j, hh, hj)), Equal.cong(Nat, Nat, z => M.pos(1n+bp, h, z), M.dist(1n+bp, h, j), dk, Equal.sym(Nat, dk, M.dist(1n+bp, h, j), N.eq_from_is_eq(dk, M.dist(1n+bp, h, j), hc3))))
194	      L.true_false(Equal.trans(Bool, True{}, B.occ(B.at(V, M.pos(1n+bp, h, dk))), False{}, L.subst(Nat, z => {True{} == B.occ(B.at(V, z)) : Bool}, j, M.pos(1n+bp, h, dk), ejk, Equal.sym(Bool, B.occ(B.at(V, j)), True{}, hoj)), hz))
195	    case False{}:
196	      +a = B.hb(CY.msk(K), B.at(V, j))
197	      +ha = hb_lt(K, bp, hN, B.at(V, j))
198	      +x = M.dist(1n+bp, a, h)
199	      +ds = dist_split2(bp, a, h, j, ha, hh, hj, hlt)
200	      +hlt2 = N.lt_or_eq(dk, M.dist(1n+bp, h, j), hge, hc3)
201	      +ht = L.subst(Nat, z => {Nat.is_lt(Nat.add(x, dk), z) == True{} : Bool}, Nat.add(x, M.dist(1n+bp, h, j)), M.dist(1n+bp, a, j), ds, N.lt_add_left(dk, M.dist(1n+bp, h, j), x, hlt2))
202	      +pt = Equal.trans(Nat, M.pos(1n+bp, a, Nat.add(x, dk)), M.pos(1n+bp, M.pos(1n+bp, a, x), dk), M.pos(1n+bp, h, dk), Equal.sym(Nat, M.pos(1n+bp, M.pos(1n+bp, a, x), dk), M.pos(1n+bp, a, Nat.add(x, dk)), RG.pos_add(bp, a, x, dk)), Equal.cong(Nat, Nat, z => M.pos(1n+bp, z, dk), M.pos(1n+bp, a, x), h, M.pos_dist(bp, a, h, ha, hh)))
203	      +oi = L.subst(Nat, z => {Bool.or(Nat.is_eq(h, z), B.occ(B.at(V, z))) == True{} : Bool}, M.pos(1n+bp, a, Nat.add(x, dk)), M.pos(1n+bp, h, dk), pt, opx_inst(V, 1n+bp, a, M.dist(1n+bp, a, j), h, hop, Nat.add(x, dk), ht))
204	      L.true_false(Equal.trans(Bool, True{}, B.occ(B.at(V, M.pos(1n+bp, h, dk))), False{}, Equal.sym(Bool, B.occ(B.at(V, M.pos(1n+bp, h, dk))), True{}, or_f(Nat.is_eq(h, M.pos(1n+bp, h, dk)), B.occ(B.at(V, M.pos(1n+bp, h, dk))), oi, h_ne_k(K, bp, hN, V, h, hh, dk, hd1, hdn))), hz))
205	
206	
207	def e_c(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hz: {B.occ(B.at(V, M.pos(1n+bp, h, dk))) == False{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hoj: {B.occ(B.at(V, j)) == True{} : Bool}, +hop: {B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h) == True{} : Bool}, +himp: {B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j))) == True{} : Bool}, +c2: Bool, +hc2: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)) == c2 : Bool}) -> {B.occpath(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)) == True{} : Bool}:
208	  match c2:
209	    case False{}:
210	      occ_of_opx(V, bp, B.hb(CY.msk(K), B.at(V, j)), hb_lt(K, bp, hN, B.at(V, j)), h, M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), N.lt_le(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), 1n+bp, M.dist_lt(bp, B.hb(CY.msk(K), B.at(V, j)), j)), hop, hc2)
211	    case True{}:
212	      Empty.absurd({B.occpath(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)) == True{} : Bool}, e_bad(K, bp, hN, V, h, hh, dk, hd1, hdn, hz, j, hj, hoj, hop, hc2, B.imp_elim(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j)), himp, hc2), Nat.is_eq(dk, M.dist(1n+bp, h, j)), {==}))
213	
214	def e_o(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hz: {B.occ(B.at(V, M.pos(1n+bp, h, dk))) == False{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +h0: {B.eval(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, j) == True{} : Bool}, +o: Bool, +ho: {B.occ(B.at(V, j)) == o : Bool}) -> {B.implies(o, B.occpath(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j))) == True{} : Bool}:
215	  match o:
216	    case False{}:
217	      {==}
218	    case True{}:
219	      +hx = B.imp_elim(B.occ(B.at(V, j)), Bool.and(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j)))), h0, ho)
220	      e_c(K, bp, hN, V, h, hh, dk, hd1, hdn, hz, j, hj, ho, L.and_left(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j))), hx), L.and_right(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j))), hx), Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), {==})
221	
222	def hole_end_m(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hz: {B.occ(B.at(V, M.pos(1n+bp, h, dk))) == False{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, 1n+bp) == True{} : Bool}) -> {B.all_lt(B.PClus{V, 1n+bp, CY.msk(K)}, m) == True{} : Bool}:
223	  match m:
224	    case 0n:
225	      {==}
226	    case 1n+j:
227	      +hj = N.succ_le_lt(j, 1n+bp, hm)
228	      L.and_intro(B.eval(B.PClus{V, 1n+bp, CY.msk(K)}, j), B.all_lt(B.PClus{V, 1n+bp, CY.msk(K)}, j), L.subst(Bool, o => {B.implies(o, B.occpath(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j))) == True{} : Bool}, B.occ(B.at(V, j)), B.occ(B.at(V, j)), {==}, e_o(K, bp, hN, V, h, hh, dk, hd1, hdn, hz, j, hj, B.all_inst(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp, hv, j, hj), B.occ(B.at(V, j)), {==})), hole_end_m(K, bp, hN, V, h, hh, dk, hd1, hdn, hz, hv, j, N.lt_le(j, 1n+bp, hj)))
229	
230	# THEOREM: when the scan meets an empty bucket, the clusters are whole
231	def hole_end(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hz: {B.occ(B.at(V, M.pos(1n+bp, h, dk))) == False{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}) -> {B.cluster(V, 1n+bp, CY.msk(K)) == True{} : Bool}:
232	  hole_end_m(K, bp, hN, V, h, hh, dk, hd1, hdn, hz, hv, 1n+bp, N.le_refl(1n+bp))
233	
234	# ---- skip: the scanned bucket's path does not reach the gap ----
235	
236	
237	def s_ne(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hskip: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, M.pos(1n+bp, h, dk))), M.pos(1n+bp, h, dk)), dk) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hc2: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)) == True{} : Bool}, +c3: Bool, +hc3: {Nat.is_eq(dk, M.dist(1n+bp, h, j)) == c3 : Bool}) -> {c3 == False{} : Bool}:
238	  match c3:
239	    case False{}:
240	      {==}
241	    case True{}:
242	      +edj = N.eq_from_is_eq(dk, M.dist(1n+bp, h, j), hc3)
243	      +ejk = Equal.trans(Nat, M.pos(1n+bp, h, dk), M.pos(1n+bp, h, M.dist(1n+bp, h, j)), j, Equal.cong(Nat, Nat, z => M.pos(1n+bp, h, z), dk, M.dist(1n+bp, h, j), edj), M.pos_dist(bp, h, j, hh, hj))
244	      +hs2 = L.subst(Nat, z => {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, z)), z), dk) == True{} : Bool}, M.pos(1n+bp, h, dk), j, ejk, hskip)
245	      +ds = dist_split2(bp, B.hb(CY.msk(K), B.at(V, j)), h, j, hb_lt(K, bp, hN, B.at(V, j)), hh, hj, hc2)
246	      +le = L.subst(Nat, z => {Nat.is_le(z, M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)) == True{} : Bool}, M.dist(1n+bp, h, j), dk, Equal.sym(Nat, dk, M.dist(1n+bp, h, j), edj), L.subst(Nat, z => {Nat.is_le(M.dist(1n+bp, h, j), z) == True{} : Bool}, Nat.add(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, h, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), ds, L.subst(Nat, z => {Nat.is_le(M.dist(1n+bp, h, j), z) == True{} : Bool}, Nat.add(M.dist(1n+bp, h, j), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h)), Nat.add(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, h, j)), N.add_comm(M.dist(1n+bp, h, j), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h)), N.le_add_right(M.dist(1n+bp, h, j), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h)))))
247	      Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), False{}, Equal.sym(Bool, Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), True{}, le), N.lt_not_le(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), dk, hs2))))
248	
249	
250	def s_imp(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hskip: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, M.pos(1n+bp, h, dk))), M.pos(1n+bp, h, dk)), dk) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +himp: {B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j))) == True{} : Bool}, +c2: Bool, +hc2: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)) == c2 : Bool}) -> {B.implies(c2, Nat.is_le(1n+dk, M.dist(1n+bp, h, j))) == True{} : Bool}:
251	  match c2:
252	    case False{}:
253	      {==}
254	    case True{}:
255	      +le1 = B.imp_elim(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j)), himp, hc2)
256	      N.lt_succ_le_succ(dk, M.dist(1n+bp, h, j), N.lt_or_eq(dk, M.dist(1n+bp, h, j), le1, s_ne(K, bp, hN, V, h, hh, dk, hd1, hdn, hskip, j, hj, hc2, Nat.is_eq(dk, M.dist(1n+bp, h, j)), {==})))
257	def sk_o(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hskip: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, M.pos(1n+bp, h, dk))), M.pos(1n+bp, h, dk)), dk) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +h0: {B.eval(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, j) == True{} : Bool}, +o: Bool, +ho: {B.occ(B.at(V, j)) == o : Bool}) -> {B.implies(o, Bool.and(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(1n+dk, M.dist(1n+bp, h, j))))) == True{} : Bool}:
258	  match o:
259	    case False{}:
260	      {==}
261	    case True{}:
262	      +hx = B.imp_elim(B.occ(B.at(V, j)), Bool.and(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j)))), h0, ho)
263	      L.and_intro(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(1n+dk, M.dist(1n+bp, h, j))), L.and_left(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j))), hx), s_imp(K, bp, hN, V, h, hh, dk, hd1, hdn, hskip, j, hj, L.and_right(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j))), hx), Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), {==}))
264	
265	def hole_skip_m(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hskip: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, M.pos(1n+bp, h, dk))), M.pos(1n+bp, h, dk)), dk) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, 1n+bp) == True{} : Bool}) -> {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, 1n+dk}, m) == True{} : Bool}:
266	  match m:
267	    case 0n:
268	      {==}
269	    case 1n+j:
270	      +hj = N.succ_le_lt(j, 1n+bp, hm)
271	      L.and_intro(B.eval(B.PHole{V, 1n+bp, CY.msk(K), h, 1n+dk}, j), B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, 1n+dk}, j), L.subst(Bool, o => {B.implies(o, Bool.and(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(1n+dk, M.dist(1n+bp, h, j))))) == True{} : Bool}, B.occ(B.at(V, j)), B.occ(B.at(V, j)), {==}, sk_o(K, bp, hN, V, h, hh, dk, hd1, hdn, hskip, j, hj, B.all_inst(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp, hv, j, hj), B.occ(B.at(V, j)), {==})), hole_skip_m(K, bp, hN, V, h, hh, dk, hd1, hdn, hskip, hv, j, N.lt_le(j, 1n+bp, hj)))
272	
273	# THEOREM: skipping a bucket whose path starts after the gap keeps the invariant one step further
274	def hole_skip(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +hskip: {Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, M.pos(1n+bp, h, dk))), M.pos(1n+bp, h, dk)), dk) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}) -> {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, 1n+dk}, 1n+bp) == True{} : Bool}:
275	  hole_skip_m(K, bp, hN, V, h, hh, dk, hd1, hdn, hskip, hv, 1n+bp, N.le_refl(1n+bp))
276	
277	# ---- move: the scanned bucket's path reaches the gap ----
278	
279	
280	def hkk(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +b: B.Bk, +hbk: {B.at(V, M.pos(1n+bp, h, dk)) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hmv: {Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(M.pos(1n+bp, h, dk), SC.length(B.Bk, V)) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(M.pos(1n+bp, h, dk), 1n+bp) == True{} : Bool}:
281	  M.pos_lt(bp, h, dk)
282	
283	def m_at_h(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +b: B.Bk, +hbk: {B.at(V, M.pos(1n+bp, h, dk)) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hmv: {Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(M.pos(1n+bp, h, dk), SC.length(B.Bk, V)) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}) -> {B.eval(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, h) == True{} : Bool}:
284	  +hk0 = L.subst(B.Bk, y => {B.implies(B.occ(y), Bool.and(B.opx(V, 1n+bp, B.hb(CY.msk(K), y), M.dist(1n+bp, B.hb(CY.msk(K), y), M.pos(1n+bp, h, dk)), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), y), h), M.dist(1n+bp, B.hb(CY.msk(K), y), M.pos(1n+bp, h, dk))), Nat.is_le(dk, M.dist(1n+bp, h, M.pos(1n+bp, h, dk)))))) == True{} : Bool}, B.at(V, M.pos(1n+bp, h, dk)), b, hbk, B.all_inst(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp, hv, M.pos(1n+bp, h, dk), hkk(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv)))
285	  +hx = B.imp_elim(B.occ(b), Bool.and(B.opx(V, 1n+bp, B.hb(CY.msk(K), b), M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk)), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), b), h), M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))), Nat.is_le(dk, M.dist(1n+bp, h, M.pos(1n+bp, h, dk))))), hk0, hbo)
286	  +hop = L.and_left(B.opx(V, 1n+bp, B.hb(CY.msk(K), b), M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk)), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), b), h), M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))), Nat.is_le(dk, M.dist(1n+bp, h, M.pos(1n+bp, h, dk)))), hx)
287	  +hle = L.subst(Nat, z => {Nat.is_le(z, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == 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, dist_k(K, bp, hN, V, h, hh, dk, hd1, hdn)), hmv)
288	  +ds = RG.dist_split(bp, B.hb(CY.msk(K), b), h, M.pos(1n+bp, h, dk), hb_lt(K, bp, hN, b), hh, hkk(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv), hle)
289	  +hl2 = L.subst(Nat, z => {Nat.is_le(M.dist(1n+bp, B.hb(CY.msk(K), b), h), z) == True{} : Bool}, Nat.add(M.dist(1n+bp, B.hb(CY.msk(K), b), h), M.dist(1n+bp, h, M.pos(1n+bp, h, dk))), M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk)), ds, N.le_add_right(M.dist(1n+bp, B.hb(CY.msk(K), b), h), M.dist(1n+bp, h, M.pos(1n+bp, h, dk))))
290	  +op2 = opx_move(V, h, M.pos(1n+bp, h, dk), b, hbo, hlen, 1n+bp, B.hb(CY.msk(K), b), M.dist(1n+bp, B.hb(CY.msk(K), b), h), opx_pre(V, 1n+bp, B.hb(CY.msk(K), b), M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk)), h, hop, M.dist(1n+bp, B.hb(CY.msk(K), b), h), hl2))
291	  +le1 = dist_pos1(bp, M.pos(1n+bp, h, dk), h, hkk(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv), hh, N.is_eq_sym_false(h, M.pos(1n+bp, h, dk), h_ne_k(K, bp, hN, V, h, hh, dk, hd1, hdn)))
292	  +r = RH.imp_true(B.occ(b), Bool.and(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), b), M.dist(1n+bp, B.hb(CY.msk(K), b), h), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), b), h)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), h)))), L.and_intro(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), b), M.dist(1n+bp, B.hb(CY.msk(K), b), h), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), b), h)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), h))), op2, RH.imp_true(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), b), h)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), h)), le1)))
293	  L.subst(B.Bk, y => {B.implies(B.occ(y), Bool.and(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), y), M.dist(1n+bp, B.hb(CY.msk(K), y), h), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), y), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), y), h)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), h))))) == True{} : Bool}, b, B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), h), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), h), b, IM.at_bupd_same(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b, hlen2(V, h, M.pos(1n+bp, h, dk), b, hbo, hlen))), r)
294	
295	def m_o(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +b: B.Bk, +hbk: {B.at(V, M.pos(1n+bp, h, dk)) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hmv: {Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(M.pos(1n+bp, h, dk), SC.length(B.Bk, V)) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hkj: {Nat.is_eq(M.pos(1n+bp, h, dk), j) == False{} : Bool}, +h0: {B.eval(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, j) == True{} : Bool}, +o: Bool, +ho: {B.occ(B.at(V, j)) == o : Bool}) -> {B.implies(o, Bool.and(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), j))))) == True{} : Bool}:
296	  match o:
297	    case False{}:
298	      {==}
299	    case True{}:
300	      +hx = B.imp_elim(B.occ(B.at(V, j)), Bool.and(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j)))), h0, ho)
301	      L.and_intro(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), j))), opx_move(V, h, M.pos(1n+bp, h, dk), b, hbo, hlen, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), L.and_left(B.opx(V, 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), h), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), h), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(dk, M.dist(1n+bp, h, j))), hx)), RH.imp_true(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), j)), dist_pos1(bp, M.pos(1n+bp, h, dk), j, hkk(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv), hj, hkj)))
302	
303	def m_k(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +b: B.Bk, +hbk: {B.at(V, M.pos(1n+bp, h, dk)) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hmv: {Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(M.pos(1n+bp, h, dk), SC.length(B.Bk, V)) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +hc: {Nat.is_eq(h, j) == False{} : Bool}, +ck: Bool, +hck: {Nat.is_eq(M.pos(1n+bp, h, dk), j) == ck : Bool}) -> {B.eval(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, j) == True{} : Bool}:
304	  match ck:
305	    case True{}:
306	      L.subst(B.Bk, y => {B.implies(B.occ(y), Bool.and(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), y), M.dist(1n+bp, B.hb(CY.msk(K), y), j), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), y), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), y), j)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), j))))) == True{} : Bool}, B.BE{}, B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), j), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), j), B.BE{}, Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), j), B.at(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), j), B.BE{}, IM.at_bupd_other(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b, j, hc), IM.at_bu_eq(V, M.pos(1n+bp, h, dk), B.BE{}, hlk, j, hck))), {==})
307	    case False{}:
308	      L.subst(B.Bk, y => {B.implies(B.occ(y), Bool.and(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), y), M.dist(1n+bp, B.hb(CY.msk(K), y), j), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), y), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), y), j)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), j))))) == True{} : Bool}, B.at(V, j), B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), j), Equal.sym(B.Bk, B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), j), B.at(V, j), Equal.trans(B.Bk, B.at(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), j), B.at(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), j), B.at(V, j), IM.at_bupd_other(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b, j, hc), IM.at_bupd_other(V, M.pos(1n+bp, h, dk), B.BE{}, j, hck))), L.subst(Bool, o => {B.implies(o, Bool.and(B.opx(IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j), M.pos(1n+bp, h, dk)), B.implies(Nat.is_lt(M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), M.pos(1n+bp, h, dk)), M.dist(1n+bp, B.hb(CY.msk(K), B.at(V, j)), j)), Nat.is_le(1n, M.dist(1n+bp, M.pos(1n+bp, h, dk), j))))) == True{} : Bool}, B.occ(B.at(V, j)), B.occ(B.at(V, j)), {==}, m_o(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv, j, hj, hck, B.all_inst(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp, hv, j, hj), B.occ(B.at(V, j)), {==})))
309	
310	def m_i(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +b: B.Bk, +hbk: {B.at(V, M.pos(1n+bp, h, dk)) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hmv: {Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(M.pos(1n+bp, h, dk), SC.length(B.Bk, V)) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(h, j) == c : Bool}) -> {B.eval(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, j) == True{} : Bool}:
311	  match c:
312	    case True{}:
313	      L.subst(Nat, z => {B.eval(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, z) == True{} : Bool}, h, j, N.eq_from_is_eq(h, j, hc), m_at_h(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv))
314	    case False{}:
315	      m_k(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv, j, hj, hc, Nat.is_eq(M.pos(1n+bp, h, dk), j), {==})
316	
317	def hole_move_m(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +b: B.Bk, +hbk: {B.at(V, M.pos(1n+bp, h, dk)) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hmv: {Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(M.pos(1n+bp, h, dk), SC.length(B.Bk, V)) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, 1n+bp) == True{} : Bool}) -> {B.all_lt(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, m) == True{} : Bool}:
318	  match m:
319	    case 0n:
320	      {==}
321	    case 1n+j:
322	      +hj = N.succ_le_lt(j, 1n+bp, hm)
323	      L.and_intro(B.eval(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, j), B.all_lt(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, j), m_i(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv, j, hj, Nat.is_eq(h, j), {==}), hole_move_m(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv, j, N.lt_le(j, 1n+bp, hj)))
324	
325	# THEOREM: moving the scanned bucket into the gap moves the gap to it
326	def hole_move(+K: Nat, +bp: Nat, +hN: {1n+bp == SC.pow2(K) : Nat}, +V: List<&2, B.Bk>, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +dk: Nat, +hd1: {Nat.is_le(1n, dk) == True{} : Bool}, +hdn: {Nat.is_lt(dk, 1n+bp) == True{} : Bool}, +b: B.Bk, +hbk: {B.at(V, M.pos(1n+bp, h, dk)) == b : B.Bk}, +hbo: {B.occ(b) == True{} : Bool}, +hmv: {Nat.is_le(dk, M.dist(1n+bp, B.hb(CY.msk(K), b), M.pos(1n+bp, h, dk))) == True{} : Bool}, +hlen: {Nat.is_lt(h, SC.length(B.Bk, V)) == True{} : Bool}, +hlk: {Nat.is_lt(M.pos(1n+bp, h, dk), SC.length(B.Bk, V)) == True{} : Bool}, +hv: {B.all_lt(B.PHole{V, 1n+bp, CY.msk(K), h, dk}, 1n+bp) == True{} : Bool}) -> {B.all_lt(B.PHole{IM.bupd(IM.bupd(V, M.pos(1n+bp, h, dk), B.BE{}), h, b), 1n+bp, CY.msk(K), M.pos(1n+bp, h, dk), 1n}, 1n+bp) == True{} : Bool}:
327	  hole_move_m(K, bp, hN, V, h, hh, dk, hd1, hdn, b, hbk, hbo, hmv, hlen, hlk, hv, 1n+bp, N.le_refl(1n+bp))