1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/array.bend as AR
5	import ../../../spec/lib/common.bend as SC
6	import ../../../spec/containers/hash_table.bend as S
7	import ../../lib/u32div.bend as UD
8	import ../../../src/containers/hash_table.bend as H
9	import ./table.bend as TB
10	import ./buckets.bend as B
11	import ./cyc.bend as CY
12	import ./inv.bend as IV
13	import ../../lib/nat_list.bend as NL
14	import ../../lib/words32.bend as W32
15	
16	# The hash map as a Data shadow: its U32 fields, the table and arena
17	# exponents k (2^k buckets) and sd (2^sd slots), and a mirror tree for each
18	# array. real(sh) is the HashMap<&2, V> the implementation holds.
19	
20	type Sh<-V: Data> is Data:
21	  HS{n: U32, k: Nat, td: U32, fresh: U32, sz: U32, sd: Nat, sdU: U32, free: U32, tabT: AR.Tree<U32>, ksT: AR.Tree<String>, vsT: AR.Tree<Maybe<&2, V>>, nxT: AR.Tree<U32>}
22	
23	def real(~V: Data, sh: Sh<V>) -> H.HashMap<&2, V>:
24	  match sh:
25	    case HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}:
26	      H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}
27	
28	# ---- the abstraction ----
29	
30	def some_b(~V: Data, m: Maybe<&2, V>) -> Bool:
31	  match m:
32	    case None{}:
33	      False{}
34	    case Some{v}:
35	      True{}
36	
37	def lvs(~V: Data, vsl: List<&2, Maybe<&2, V>>) -> List<&2, Bool>:
38	  match vsl:
39	    case Nil{}:
40	      Nil{}
41	    case Con{m, t}:
42	      Con{some_b(~V, m), lvs(~V, t)}
43	
44	def nthm(~V: Data, vsl: List<&2, Maybe<&2, V>>, +i: Nat) -> Maybe<&2, V>:
45	  match vsl i:
46	    case Nil{} _:
47	      None{}
48	    case Con{m, t} 0n:
49	      m
50	    case Con{m, t} 1n+p:
51	      nthm(~V, t, p)
52	
53	def ent_m(~V: Data, +k: String, m: Maybe<&2, V>) -> List<&2, S.Entry<V>>:
54	  match m:
55	    case None{}:
56	      Nil{}
57	    case Some{v}:
58	      Con{S.E{k, v}, Nil{}}
59	
60	# the entry of a bucket
61	def ent(~V: Data, b: B.Bk, +vsl: List<&2, Maybe<&2, V>>) -> List<&2, S.Entry<V>>:
62	  match b:
63	    case B.BE{}:
64	      Nil{}
65	    case B.BF{w, +l, +k}:
66	      ent_m(~V, k, nthm(~V, vsl, UD.v(H.slot(l))))
67	
68	# the entries of buckets j .. j + m - 1, in bucket order
69	def absm(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +m: Nat, +j: Nat) -> List<&2, S.Entry<V>>:
70	  match m:
71	    case 0n:
72	      Nil{}
73	    case 1n+p:
74	      SC.append(S.Entry<V>, ent(~V, B.at(bs, j), vsl), absm(~V, bs, vsl, p, 1n+j))
75	
76	def bsof(~V: Data, sh: Sh<V>) -> List<&2, B.Bk>:
77	  match sh:
78	    case HS{n, +k, td, fresh, sz, sd, sdU, free, +tabT, +ksT, vsT, nxT}:
79	      TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))
80	
81	def model(~V: Data, sh: Sh<V>) -> List<&2, S.Entry<V>>:
82	  match sh:
83	    case HS{n, +k, td, fresh, sz, sd, sdU, free, +tabT, +ksT, +vsT, nxT}:
84	      absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)
85	
86	# ---- the invariant ----
87	# stated over the stored keys' slot list kl and their tree's perfectness pk,
88	# so that a read that swaps a key out and back keeps it
89	
90	
91	# no full bucket among the first m uses slot s
92	def noslot(+bs: List<&2, B.Bk>, +s: Nat, +m: Nat) -> Bool:
93	  match m:
94	    case 0n:
95	      True{}
96	    case 1n+j:
97	      Bool.and(Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), s))), noslot(bs, s, j))
98	
99	# the free list from link f has exactly cnt links: each slot on it is below
100	# fresh, used by no bucket and not repeated, and the list ends after them
101	def fl_ok(+bs: List<&2, B.Bk>, +nb: Nat, +nxl: List<&2, U32>, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>) -> Bool:
102	  match cnt:
103	    case 0n:
104	      U32.is_eq(f, 0)
105	    case 1n+p:
106	      Bool.and(Bool.not(U32.is_eq(f, 0)), Bool.and(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))), fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})))
107	
108	def ck(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
109	  Bool.and(Nat.is_lt(k, 31n), Nat.is_lt(0n, k))
110	
111	def csd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
112	  Nat.is_lt(sd, 32n)
113	
114	def cpt(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
115	  AR.perfect(U32, 1n+k, tabT)
116	
117	def cpk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
118	  pk
119	
120	def cpv(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
121	  AR.perfect(Maybe<&2, V>, sd, vsT)
122	
123	def cpn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
124	  AR.perfect(U32, sd, nxT)
125	
126	def ctd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
127	  Nat.is_eq(UD.v(td), 1n+k)
128	
129	def csz(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
130	  Nat.is_eq(UD.v(sz), SC.pow2(sd))
131	
132	def csdu(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
133	  Nat.is_eq(UD.v(sdU), sd)
134	
135	def cwell(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
136	  B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k))
137	
138	def cclus(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
139	  B.cluster(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k))
140	
141	def cuniq(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
142	  B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k))}, SC.pow2(k))
143	
144	def cn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
145	  Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k)))
146	
147	def cload(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
148	  Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k))
149	
150	def clive(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
151	  B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh)}, SC.pow2(k))
152	
153	def cfresh(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
154	  Nat.is_le(UD.v(fresh), UD.v(sz))
155	
156	def cfree(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
157	  Bool.and(Nat.is_le(UD.v(n), UD.v(fresh)), fl_ok(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}))
158	
159	def csdk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
160	  Nat.is_lt(sd, k)
161	
162	def gr16(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
163	  Bool.and(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
164	
165	def gr15(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
166	  Bool.and(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
167	
168	def gr14(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
169	  Bool.and(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
170	
171	def gr13(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
172	  Bool.and(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
173	
174	def gr12(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
175	  Bool.and(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
176	
177	def gr11(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
178	  Bool.and(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
179	
180	def gr10(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
181	  Bool.and(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
182	
183	def gr9(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
184	  Bool.and(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
185	
186	def gr8(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
187	  Bool.and(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
188	
189	def gr7(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
190	  Bool.and(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
191	
192	def gr6(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
193	  Bool.and(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
194	
195	def gr5(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
196	  Bool.and(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
197	
198	def gr4(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
199	  Bool.and(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
200	
201	def gr3(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
202	  Bool.and(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
203	
204	def gr2(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
205	  Bool.and(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
206	
207	def gr1(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
208	  Bool.and(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
209	
210	def goodF(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:
211	  Bool.and(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))
212	
213	def good(~V: Data, sh: Sh<V>) -> Bool:
214	  match sh:
215	    case HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:
216	      goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT)
217	
218	def gp1(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
219	  L.and_right(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), g)
220	
221	def gp2(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
222	  L.and_right(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
223	
224	def gp3(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
225	  L.and_right(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
226	
227	def gp4(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
228	  L.and_right(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
229	
230	def gp5(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
231	  L.and_right(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
232	
233	def gp6(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
234	  L.and_right(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
235	
236	def gp7(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
237	  L.and_right(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
238	
239	def gp8(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
240	  L.and_right(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
241	
242	def gp9(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
243	  L.and_right(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
244	
245	def gp10(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
246	  L.and_right(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
247	
248	def gp11(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
249	  L.and_right(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
250	
251	def gp12(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
252	  L.and_right(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
253	
254	def gp13(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
255	  L.and_right(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
256	
257	def gp14(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
258	  L.and_right(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
259	
260	def gp15(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
261	  L.and_right(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
262	
263	def gp16(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
264	  L.and_right(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
265	
266	def gp17(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
267	  L.and_right(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
268	
269	def g_ck(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
270	  L.and_left(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), g)
271	
272	def g_csd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
273	  L.and_left(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
274	
275	def g_cpt(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
276	  L.and_left(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
277	
278	def g_cpk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
279	  L.and_left(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
280	
281	def g_cpv(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
282	  L.and_left(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
283	
284	def g_cpn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
285	  L.and_left(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
286	
287	def g_ctd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
288	  L.and_left(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
289	
290	def g_csz(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
291	  L.and_left(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
292	
293	def g_csdu(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
294	  L.and_left(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
295	
296	def g_cwell(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
297	  L.and_left(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
298	
299	def g_cclus(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
300	  L.and_left(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
301	
302	def g_cuniq(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
303	  L.and_left(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
304	
305	def g_cn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
306	  L.and_left(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
307	
308	def g_cload(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
309	  L.and_left(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
310	
311	def g_clive(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
312	  L.and_left(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
313	
314	def g_cfresh(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
315	  L.and_left(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
316	
317	def g_cfree(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
318	  L.and_left(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))
319	
320	def g_csdk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:
321	  gp17(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g)
322	
323	# the invariant from its components
324	def good_intro(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +h_ck: {ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csd: {csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpt: {cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpk: {cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpv: {cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpn: {cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_ctd: {ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csz: {csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csdu: {csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cwell: {cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cclus: {cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cuniq: {cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cn: {cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cload: {cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_clive: {clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cfresh: {cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cfree: {cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csdk: {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {goodF(~V, n, k, td, fresh
325	  L.and_intro(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_ck, L.and_intro(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csd, L.and_intro(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpt, L.and_intro(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpk, L.and_intro(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpv, L.and_intro(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpn, L.and_intro(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_ctd, L.and_intro(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csz, L.and_intro(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csdu, L.and_intro(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cwell, L.and_intro(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cclus, L.and_intro(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cuniq, L.and_intro(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, 
326	
327	# ---- slot values ----
328	
329	def lvs_nth(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +i: Nat) -> {B.nthb(lvs(~V, vsl), i) == some_b(~V, nthm(~V, vsl, i)) : Bool}:
330	  match vsl i:
331	    case Nil{} _:
332	      {==}
333	    case Con{m, t} 0n:
334	      {==}
335	    case Con{m, t} 1n+p:
336	      lvs_nth(~V, t, p)
337	
338	def nthm_some(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}) -> {SC.nth(Maybe<&2, V>, vsl, i) == Some{nthm(~V, vsl, i)} : Maybe<&2, Maybe<&2, V>>}:
339	  match vsl i:
340	    case Nil{} _:
341	      Empty.absurd({SC.nth(Maybe<&2, V>, Nil{}, i) == Some{nthm(~V, Nil{}, i)} : Maybe<&2, Maybe<&2, V>>}, N.lt_zero_absurd(i, h))
342	    case Con{m, t} 0n:
343	      {==}
344	    case Con{m, t} 1n+p:
345	      nthm_some(~V, t, p, h)