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 ../../../spec/containers/hash_table.bend as S
6	import ../../lib/u32div.bend as UD
7	import ../../../src/containers/hash_table.bend as H
8	import ./keys.bend as K
9	import ./table.bend as TB
10	import ./buckets.bend as B
11	import ./state.bend as ST
12	import ./lookup.bend as LK
13	import ./tools.bend as T
14	import ./speclem.bend as SL
15	import ./setv.bend as SV
16	import ./insm.bend as IM
17	import ./insa.bend as IA
18	import ./insf.bend as IF
19	import ./rehash.bend as RH
20	import ./delmv.bend as DM
21	import ./keysw.bend as KW
22	import ../../lib/nat_list.bend as NL
23	import ../../lib/words32.bend as W32
24	
25	# Facts for pop: after emptying the bucket i that holds key, the other keys
26	# look up as before, key is held nowhere, the model's keys have no repeats,
27	# and the vacated slot is free.
28	
29	
30	# ---- the emptied bucket, for a property true of every empty bucket ----
31	
32	def at_v0(+O: List<&2, B.Bk>, +i: Nat, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +j: Nat, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {B.at(IM.bupd(O, i, B.BE{}), j) == Bool.pick(B.Bk, c, B.BE{}, B.at(O, j)) : B.Bk}:
33	  match c:
34	    case True{}:
35	      IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)
36	    case False{}:
37	      IM.at_bupd_other(O, i, B.BE{}, j, hc)
38	
39	def well_rm_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{O, sd}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {B.wb(sd, B.at(IM.bupd(O, i, B.BE{}), j)) == True{} : Bool}:
40	  match c:
41	    case True{}:
42	      L.subst(B.Bk, y => {B.wb(sd, y) == 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)), {==})
43	    case False{}:
44	      L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), B.all_inst(B.PWell{O, sd}, n, hw, j, hj))
45	
46	def well_rm(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{O, sd}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PWell{IM.bupd(O, i, B.BE{}), sd}, m) == True{} : Bool}:
47	  match m:
48	    case 0n:
49	      {==}
50	    case 1n+q:
51	      +hq = N.succ_le_lt(q, n, hm)
52	      L.and_intro(B.wb(sd, B.at(IM.bupd(O, i, B.BE{}), q)), B.all_lt(B.PWell{IM.bupd(O, i, B.BE{}), sd}, q), well_rm_i(O, n, i, hi, hlen, sd, hw, q, hq, Nat.is_eq(i, q), {==}), well_rm(O, n, i, hi, hlen, sd, hw, q, N.lt_le(q, n, hq)))
53	
54	def wl_at(+obs: List<&2, B.Bk>, +sd: Nat, +j: Nat, +hw: {B.all_lt(B.PWell{obs, sd}, j) == True{} : Bool}, +b: B.Bk, e: RH.EqAt(obs, j, b)) -> {B.wb(sd, b) == True{} : Bool}:
55	  match e:
56	    case Tuple{+x, Tuple{+hx, +hb}}:
57	      L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.at(obs, x), b, hb, B.all_inst(B.PWell{obs, sd}, j, hw, x, hx))
58	
59	def wb_empty(+sd: Nat, +b: B.Bk, +h: {B.occ(b) == False{} : Bool}) -> {B.wb(sd, b) == True{} : Bool}:
60	  match b:
61	    case B.BE{}:
62	      {==}
63	    case B.BF{w, l, k}:
64	      Empty.absurd({B.wb(sd, B.BF{w, l, k}) == True{} : Bool}, L.true_false(h))
65	
66	def wlf_c(+nbs: List<&2, B.Bk>, +obs: List<&2, B.Bk>, +j: Nat, +n2: Nat, +hf: {B.all_lt(B.PFrom{nbs, obs, j}, n2) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{obs, sd}, j) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n2) == True{} : Bool}, +c: Bool, +hc: {B.occ(B.at(nbs, x)) == c : Bool}) -> {B.wb(sd, B.at(nbs, x)) == True{} : Bool}:
67	  match c:
68	    case False{}:
69	      wb_empty(sd, B.at(nbs, x), hc)
70	    case True{}:
71	      wl_at(obs, sd, j, hw, B.at(nbs, x), RH.from_at(nbs, obs, j, n2, hf, x, hx, hc))
72	
73	# THEOREM: copies of well-formed buckets are well formed
74	def well_from(+nbs: List<&2, B.Bk>, +obs: List<&2, B.Bk>, +j: Nat, +n2: Nat, +hf: {B.all_lt(B.PFrom{nbs, obs, j}, n2) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{obs, sd}, j) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n2) == True{} : Bool}) -> {B.all_lt(B.PWell{nbs, sd}, m) == True{} : Bool}:
75	  match m:
76	    case 0n:
77	      {==}
78	    case 1n+q:
79	      +hq = N.succ_le_lt(q, n2, hm)
80	      L.and_intro(B.wb(sd, B.at(nbs, q)), B.all_lt(B.PWell{nbs, sd}, q), wlf_c(nbs, obs, j, n2, hf, sd, hw, q, hq, B.occ(B.at(nbs, q)), {==}), well_from(nbs, obs, j, n2, hf, sd, hw, q, N.lt_le(q, n2, hq)))
81	
82	# ---- slots ----
83	
84	def nsb_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +t: Nat, +h: {ST.noslot(O, t, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(IM.bupd(O, i, B.BE{}), j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), j)))), t))) == True{} : Bool}:
85	  match c:
86	    case True{}:
87	      L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), t))) == 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)), {==})
88	    case False{}:
89	      L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), t))) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), IM.noslot_inst(O, t, n, h, j, hj))
90	
91	# THEOREM: emptying a bucket frees no slot another bucket was using
92	def ns_be(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +t: Nat, +h: {ST.noslot(O, t, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {ST.noslot(IM.bupd(O, i, B.BE{}), t, m) == True{} : Bool}:
93	  match m:
94	    case 0n:
95	      {==}
96	    case 1n+q:
97	      +hq = N.succ_le_lt(q, n, hm)
98	      L.and_intro(Bool.not(Bool.and(B.occ(B.at(IM.bupd(O, i, B.BE{}), q)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), q)))), t))), ST.noslot(IM.bupd(O, i, B.BE{}), t, q), nsb_i(O, n, i, hi, hlen, t, h, q, hq, Nat.is_eq(i, q), {==}), ns_be(O, n, i, hi, hlen, t, h, q, N.lt_le(q, n, hq)))
99	
100	
101	def pno_be_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +q: String, +hno: {B.all_lt(B.PNo{O, q}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), j))) == True{} : Bool}:
102	  match c:
103	    case True{}:
104	      L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == 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)), {==})
105	    case False{}:
106	      L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), B.all_inst(B.PNo{O, q}, n, hno, j, hj))
107	
108	def pno_be(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +q: String, +hno: {B.all_lt(B.PNo{O, q}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, m) == True{} : Bool}:
109	  match m:
110	    case 0n:
111	      {==}
112	    case 1n+p:
113	      +hp = N.succ_le_lt(p, n, hm)
114	      L.and_intro(Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), p))), B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, p), pno_be_i(O, n, i, hi, hlen, q, hno, p, hp, Nat.is_eq(i, p), {==}), pno_be(O, n, i, hi, hlen, q, hno, p, N.lt_le(p, n, hp)))
115	
116	def hold_eqk(+b: B.Bk, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}) -> {B.hold(key, b) == B.hold(q, b) : Bool}:
117	  match b:
118	    case B.BE{}:
119	      {==}
120	    case B.BF{w, l, +k}:
121	      SL.eq_tr2(k, key, q, hq)
122	
123	def pnq_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), j))) == True{} : Bool}:
124	  match c:
125	    case True{}:
126	      L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == 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)), {==})
127	    case False{}:
128	      +o = LK.other(O, n, key, huq, i, hi, hk, j, hj, N.is_eq_sym_false(i, j, hc))
129	      L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), L.subst(Bool, x => {Bool.not(x) == True{} : Bool}, B.hold(key, B.at(O, j)), B.hold(q, B.at(O, j)), hold_eqk(B.at(O, j), key, q, hq), o))
130	
131	# THEOREM: once its bucket is emptied, the removed key is held nowhere
132	def pno_rmq(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, m) == True{} : Bool}:
133	  match m:
134	    case 0n:
135	      {==}
136	    case 1n+p:
137	      +hp = N.succ_le_lt(p, n, hm)
138	      L.and_intro(Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), p))), B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, p), pnq_i(O, n, i, hi, hlen, huq, key, hk, q, hq, p, hp, Nat.is_eq(i, p), {==}), pno_rmq(O, n, i, hi, hlen, huq, key, hk, q, hq, p, N.lt_le(p, n, hp)))
139	
140	def lkr_h(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +mm: Maybe<&2, V>, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, e0: T.Holder(O, q, n)) -> {S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q) == S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q) : Maybe<&2, V>}:
141	  match e0:
142	    case Tuple{+j, Tuple{+hj, +hkj}}:
143	      +hji = SV.neq_hold(O, key, q, i, j, hk, hq, hkj, Nat.is_eq(j, i), {==})
144	      +eat = IM.at_bupd_other(O, i, B.BE{}, j, N.is_eq_sym_false(j, i, hji))
145	      +hkj2 = L.subst(B.Bk, y => {B.hold(q, y) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat), hkj)
146	      +sj = UD.v(H.slot(B.lnk(B.at(O, j))))
147	      +hne = N.is_eq_sym_false(sj, UD.v(H.slot(B.lnk(B.at(O, i)))), T.slot_ne(O, n, huq, i, j, hi, hj, hji, B.hold_occ(key, B.at(O, i), hk), B.hold_occ(q, B.at(O, j), hkj)))
148	      Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), j))))), S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), LK.lookup_hit(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), q, n, DM.uq_rm(O, i, hlen, n, huq, n, N.le_refl(n)), j, hj, hkj2), Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), j))))), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), sj), S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), Equal.cong(B.Bk, Maybe<&2, V>, y => ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), UD.v(H.slot(B.lnk(y)))), B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat), Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), sj), ST.nthm(~V, vsl, sj), S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), T.nthm_upd_other(~V, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), sj, mm, hne), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), ST.nthm(~V, vsl, sj), LK.lookup_hit(~V, O, vsl, q, n, huq, j, hj, hkj)))))
149	
150	def lkr_c(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +mm: Maybe<&2, V>, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +d: Bool, +hd: {B.all_lt(B.PNo{O, q}, n) == d : Bool}) -> {S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q) == S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q) : Maybe<&2, V>}:
151	  match d:
152	    case True{}:
153	      Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q), None{}, S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), LK.lookup_none(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), q, n, pno_be(O, n, i, hi, hlen, q, hd, n, N.le_refl(n))), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), None{}, LK.lookup_none(~V, O, vsl, q, n, hd)))
154	    case False{}:
155	      lkr_h(~V, O, n, i, hi, hlen, huq, key, hk, vsl, mm, q, hq, T.find_hold(O, q, n, hd))
156	
157	# THEOREM: emptying key's bucket and its slot leaves every other key's lookup
158	def lk_rm(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +mm: Maybe<&2, V>, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}) -> {S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q) == S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q) : Maybe<&2, V>}:
159	  lkr_c(~V, O, n, i, hi, hlen, huq, key, hk, vsl, mm, q, hq, B.all_lt(B.PNo{O, q}, n), {==})
160	
161	# ---- liveness with the slot vacated ----
162	
163	def lvr_b(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +s: Nat, +fr: Nat, +b: B.Bk, +h: {B.live_b(ST.lvs(~V, vsl), fr, b) == True{} : Bool}, +hne: {Bool.not(Bool.and(B.occ(b), Nat.is_eq(UD.v(H.slot(B.lnk(b))), s))) == True{} : Bool}) -> {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, b) == True{} : Bool}:
164	  match b:
165	    case B.BE{}:
166	      {==}
167	    case B.BF{w, +l, k}:
168	      +t = UD.v(H.slot(l))
169	      +ne = N.is_eq_sym_false(t, s, K.not_true_eq(Nat.is_eq(t, s), hne))
170	      +e = Equal.trans(Bool, B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), t), ST.some_b(~V, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t)), B.nthb(ST.lvs(~V, vsl), t), ST.lvs_nth(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t), Equal.trans(Bool, ST.some_b(~V, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t)), ST.some_b(~V, ST.nthm(~V, vsl, t)), B.nthb(ST.lvs(~V, vsl), t), Equal.cong(Maybe<&2, V>, Bool, m => ST.some_b(~V, m), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t), ST.nthm(~V, vsl, t), T.nthm_upd_other(~V, vsl, s, t, None{}, ne)), Equal.sym(Bool, B.nthb(ST.lvs(~V, vsl), t), ST.some_b(~V, ST.nthm(~V, vsl, t)), ST.lvs_nth(~V, vsl, t))))
171	      L.and_intro(B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), t), Nat.is_lt(t, fr), Equal.trans(Bool, B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), t), B.nthb(ST.lvs(~V, vsl), t), True{}, e, L.and_left(B.nthb(ST.lvs(~V, vsl), t), Nat.is_lt(t, fr), h)), L.and_right(B.nthb(ST.lvs(~V, vsl), t), Nat.is_lt(t, fr), h))
172	
173	def lvr_i(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +hl: {B.all_lt(B.PLive{O, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +s: Nat, +hns: {ST.noslot(IM.bupd(O, i, B.BE{}), s, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, B.at(IM.bupd(O, i, B.BE{}), j)) == True{} : Bool}:
174	  match c:
175	    case True{}:
176	      L.subst(B.Bk, y => {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, y) == 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)), {==})
177	    case False{}:
178	      +eat = IM.at_bupd_other(O, i, B.BE{}, j, hc)
179	      +hne = L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), s))) == True{} : Bool}, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat, IM.noslot_inst(IM.bupd(O, i, B.BE{}), s, n, hns, j, hj))
180	      L.subst(B.Bk, y => {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, y) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat), lvr_b(~V, vsl, s, fr, B.at(O, j), B.all_inst(B.PLive{O, ST.lvs(~V, vsl), fr}, n, hl, j, hj), hne))
181	
182	# THEOREM: the other buckets stay live once the removed slot is vacant
183	def live_rm(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +hl: {B.all_lt(B.PLive{O, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +s: Nat, +hns: {ST.noslot(IM.bupd(O, i, B.BE{}), s, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PLive{IM.bupd(O, i, B.BE{}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr}, m) == True{} : Bool}:
184	  match m:
185	    case 0n:
186	      {==}
187	    case 1n+q:
188	      +hq = N.succ_le_lt(q, n, hm)
189	      L.and_intro(B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, B.at(IM.bupd(O, i, B.BE{}), q)), B.all_lt(B.PLive{IM.bupd(O, i, B.BE{}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr}, q), lvr_i(~V, O, n, i, hi, hlen, vsl, fr, hl, s, hns, q, hq, Nat.is_eq(i, q), {==}), live_rm(~V, O, n, i, hi, hlen, vsl, fr, hl, s, hns, q, N.lt_le(q, n, hq)))
190	
191	# ---- the free list after pushing the vacated slot ----
192	
193	def subl_refl(+xs: List<&2, Nat>) -> {IF.subl(xs, xs) == True{} : Bool}:
194	  match xs:
195	    case Nil{}:
196	      {==}
197	    case Con{+x, +t}:
198	      L.and_intro(NL.memn(x, Con{x, t}), IF.subl(t, Con{x, t}), L.subst(Bool, b => {Bool.or(b, NL.memn(x, t)) == True{} : Bool}, True{}, Nat.is_eq(x, x), Equal.sym(Bool, Nat.is_eq(x, x), True{}, N.is_eq_refl(x)), {==}), IF.subl_cons(t, t, x, subl_refl(t)))
199	
200	def mem_self(+t: Nat, +xs: List<&2, Nat>) -> {NL.memn(t, Con{t, xs}) == True{} : Bool}:
201	  L.subst(Bool, b => {Bool.or(b, NL.memn(t, xs)) == True{} : Bool}, True{}, Nat.is_eq(t, t), Equal.sym(Bool, Nat.is_eq(t, t), True{}, N.is_eq_refl(t)), {==})
202	
203	
204	# the two orders of visiting s and t
205	def subl_sw(+s: Nat, +t: Nat, +seen: List<&2, Nat>) -> {IF.subl(Con{t, Con{s, seen}}, Con{s, Con{t, seen}}) == True{} : Bool}:
206	  L.and_intro(NL.memn(t, Con{s, Con{t, seen}}), IF.subl(Con{s, seen}, Con{s, Con{t, seen}}), IF.mem_cons(t, s, Con{t, seen}, mem_self(t, seen)), L.and_intro(NL.memn(s, Con{s, Con{t, seen}}), IF.subl(seen, Con{s, Con{t, seen}}), mem_self(s, Con{t, seen}), IF.subl_cons(seen, Con{t, seen}, s, IF.subl_cons(seen, seen, t, subl_refl(seen)))))
207	
208	
209	# THEOREM: the old free list is still valid after pushing the vacated slot
210	def fl_pr(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +Vf: List<&2, B.Bk>, +hf: {B.all_lt(B.PFrom{Vf, IM.bupd(O, i, B.BE{}), n}, n) == True{} : Bool}, +hoi: {B.occ(B.at(O, i)) == True{} : Bool}, +nxl: List<&2, U32>, +fv: U32, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>, +h: {ST.fl_ok(O, n, nxl, cnt, f, fr, seen) == True{} : Bool}) -> {ST.fl_ok(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), cnt, f, fr, Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}) == True{} : Bool}:
211	  match cnt:
212	    case 0n:
213	      h
214	    case 1n+p:
215	      +x1 = Bool.not(U32.is_eq(f, 0))
216	      +y = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen))))
217	      +tl = ST.fl_ok(O, n, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})
218	      +z = Bool.and(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))
219	      +a2 = L.and_left(y, tl, L.and_right(x1, Bool.and(y, tl), h))
220	      +a5 = L.and_right(y, tl, L.and_right(x1, Bool.and(y, tl), h))
221	      +ns = L.and_left(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
222	      +nm = L.and_right(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
223	      +ne = IM.slot_other(B.at(O, i), UD.v(H.slot(f)), hoi, IM.noslot_inst(O, UD.v(H.slot(f)), n, ns, i, hi))
224	      +ns2 = RH.ns_from(Vf, IM.bupd(O, i, B.BE{}), n, n, hf, UD.v(H.slot(f)), ns_be(O, n, i, hi, hlen, UD.v(H.slot(f)), ns, n, N.le_refl(n)), n, N.le_refl(n))
225	      +nm2 = L.subst(Bool, b => {Bool.not(Bool.or(b, NL.memn(UD.v(H.slot(f)), seen))) == True{} : Bool}, False{}, Nat.is_eq(UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f))), Equal.sym(Bool, Nat.is_eq(UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f))), False{}, ne), nm)
226	      +enx = W32.nth0_upd_other(nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f)), fv, ne)
227	      +r0 = fl_pr(O, n, i, hi, hlen, Vf, hf, hoi, nxl, fv, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}, a5)
228	      +r1 = L.subst(U32, g => {ST.fl_ok(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), p, g, fr, Con{UD.v(H.slot(B.lnk(B.at(O, i)))), Con{UD.v(H.slot(f)), seen}}) == True{} : Bool}, W32.nth0(nxl, UD.v(H.slot(f))), W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), Equal.sym(U32, W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), W32.nth0(nxl, UD.v(H.slot(f))), enx), r0)
229	      +r2 = IF.fl_weak(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), p, W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), fr, Con{UD.v(H.slot(B.lnk(B.at(O, i)))), Con{UD.v(H.slot(f)), seen}}, Con{UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}}, subl_sw(UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f)), seen), r1)
230	      +y2 = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(Vf, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}))))
231	      +tl2 = ST.fl_ok(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), p, W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}})
232	      L.and_intro(x1, Bool.and(y2, tl2), L.and_left(x1, Bool.and(y, tl), h), L.and_intro(y2, tl2, L.and_intro(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(Vf, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}))), L.and_left(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2), L.and_intro(ST.noslot(Vf, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen})), ns2, nm2)), r2))
233	
234	# ---- the model's keys have no repeats ----
235	
236	def mk_b(+key: String, +b: B.Bk, +r: List<&2, String>, +hnh: {Bool.not(B.hold(key, b)) == True{} : Bool}, +hr: {S.mem(key, r) == False{} : Bool}) -> {S.mem(key, SC.append(String, KW.kof(b), r)) == False{} : Bool}:
237	  match b:
238	    case B.BE{}:
239	      hr
240	    case B.BF{w, l, +k}:
241	      L.subst(Bool, x => {Bool.or(x, S.mem(key, r)) == False{} : Bool}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, K.not_true_eq(S.str_eq(k, key), hnh)), hr)
242	
243	def mem_kb(+bs: List<&2, B.Bk>, +key: String, +m: Nat, +j: Nat, +h: {LK.nob(bs, key, m, j) == True{} : Bool}) -> {S.mem(key, KW.kb(bs, m, j)) == False{} : Bool}:
244	  match m:
245	    case 0n:
246	      {==}
247	    case 1n+p:
248	      mk_b(key, B.at(bs, j), KW.kb(bs, p, 1n+j), L.and_left(Bool.not(B.hold(key, B.at(bs, j))), LK.nob(bs, key, p, 1n+j), h), mem_kb(bs, key, p, 1n+j, L.and_right(Bool.not(B.hold(key, B.at(bs, j))), LK.nob(bs, key, p, 1n+j), h)))
249	
250	def nd_b(+bs: List<&2, B.Bk>, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +p: Nat, +hjm: {Nat.is_le(Nat.add(1n+j, p), n) == True{} : Bool}, +b: B.Bk, +hb: {B.at(bs, j) == b : B.Bk}, +hr: {S.nodup(KW.kb(bs, p, 1n+j)) == True{} : Bool}) -> {S.nodup(SC.append(String, KW.kof(b), KW.kb(bs, p, 1n+j))) == True{} : Bool}:
251	  match b:
252	    case B.BE{}:
253	      hr
254	    case B.BF{w, l, +k}:
255	      +hk = L.subst(B.Bk, y => {B.hold(k, y) == True{} : Bool}, B.BF{w, l, k}, B.at(bs, j), Equal.sym(B.Bk, B.at(bs, j), B.BF{w, l, k}, hb), K.str_refl(k))
256	      +nm = mem_kb(bs, k, p, 1n+j, LK.nob_past(bs, n, k, huq, j, hj, hk, p, 1n+j, hjm, N.lt_succ(j)))
257	      L.and_intro(Bool.not(S.mem(k, KW.kb(bs, p, 1n+j))), S.nodup(KW.kb(bs, p, 1n+j)), IM.not_f(S.mem(k, KW.kb(bs, p, 1n+j)), nm), hr)
258	
259	def nodup_kb(+bs: List<&2, B.Bk>, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}) -> {S.nodup(KW.kb(bs, m, j)) == True{} : Bool}:
260	  match m:
261	    case 0n:
262	      {==}
263	    case 1n+p:
264	      +hj = IA.idx_lt(j, p, n, hjm)
265	      +hjm2 = IA.idx_next(j, p, n, hjm)
266	      nd_b(bs, n, huq, j, hj, p, hjm2, B.at(bs, j), {==}, nodup_kb(bs, n, huq, p, 1n+j, hjm2))
267	
268	# THEOREM: the model of a table with unique keys has no repeated key
269	def nodup_model(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +n: Nat, +hl: {B.all_lt(B.PLive{bs, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}) -> {S.nodup(S.keys(~V, ST.absm(~V, bs, vsl, n, 0n))) == True{} : Bool}:
270	  L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, KW.kb(bs, n, 0n), S.keys(~V, ST.absm(~V, bs, vsl, n, 0n)), Equal.sym(List<&2, String>, S.keys(~V, ST.absm(~V, bs, vsl, n, 0n)), KW.kb(bs, n, 0n), KW.keys_absm(~V, bs, vsl, fr, n, hl, n, 0n, N.le_refl(n))), nodup_kb(bs, n, huq, n, 0n, N.le_refl(n)))
271	
272	# ---- a key cell no bucket uses ----
273	
274	def kd_i(+tb: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +n: Nat, +hns: {ST.noslot(TB.buckets(tb, kl, n), s, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {Bool.not(Bool.and(B.occ(TB.dec(tb, kl, i)), Nat.is_eq(UD.v(H.slot(B.lnk(TB.dec(tb, kl, i)))), s))) == True{} : Bool}:
275	  L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), s))) == True{} : Bool}, B.at(TB.buckets(tb, kl, n), i), TB.dec(tb, kl, i), TB.at_buckets(tb, kl, n, i, hi), IM.noslot_inst(TB.buckets(tb, kl, n), s, n, hns, i, hi))
276	
277	def kd(+tb: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +sk: String, +n: Nat, +hns: {ST.noslot(TB.buckets(tb, kl, n), s, n) == True{} : Bool}, +m: Nat, +i: Nat, +hmi: {Nat.is_le(Nat.add(i, m), n) == True{} : Bool}) -> {TB.dlist(tb, SC.update(String, kl, s, sk), m, i) == TB.dlist(tb, kl, m, i) : List<&2, B.Bk>}:
278	  match m:
279	    case 0n:
280	      {==}
281	    case 1n+p:
282	      +hi = IA.idx_lt(i, p, n, hmi)
283	      IA.con_eq(TB.dec(tb, SC.update(String, kl, s, sk), i), TB.dec(tb, kl, i), TB.dlist(tb, SC.update(String, kl, s, sk), p, 1n+i), TB.dlist(tb, kl, p, 1n+i), IA.dec_same_c(W32.nth0(tb, Nat.double(i)), W32.nth0(tb, 1n+Nat.double(i)), kl, s, sk, U32.is_eq(W32.nth0(tb, Nat.double(i)), 0), kd_i(tb, kl, s, n, hns, i, hi)), kd(tb, kl, s, sk, n, hns, p, 1n+i, IA.idx_next(i, p, n, hmi)))
284	
285	# THEOREM: rewriting a key cell no bucket uses leaves every bucket
286	def bs_key(+tb: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +sk: String, +n: Nat, +hns: {ST.noslot(TB.buckets(tb, kl, n), s, n) == True{} : Bool}) -> {TB.buckets(tb, SC.update(String, kl, s, sk), n) == TB.buckets(tb, kl, n) : List<&2, B.Bk>}:
287	  kd(tb, kl, s, sk, n, hns, n, 0n, N.le_refl(n))