proofs/containers/hash_table/hole.bend
bend-collections-laws-containers@1.0.0.0 · 327 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
6import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as HS
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/modn.bend as M
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_all.bend as PA
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insert.bend as IS
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/ring.bend as RG
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/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
23def 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
32def 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
39def 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
46def 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
54def 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
58def 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
70def 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
78def 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
89def 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
92def 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
99def 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
107def 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
119def 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
129def 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
138def 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
144def 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
153def 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
162def 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
173def 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
176def 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
185def 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
190def 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
207def 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
214def 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
222def 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
231def 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
237def 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
250def 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)), {==})))
257def 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
265def 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
274def 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
280def 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
283def 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
295def 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
303def 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
310def 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
317def 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
326def 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))