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/balanced_search_tree/main.bend as S
7	import ../dynamic_array/layout.bend as LY
8	import ../dynamic_array/state.bend as DAS
9	import ../../../src/containers/balanced_search_tree.bend as M
10	import ../../../src/containers/dynamic_array.bend as D
11	import ./nsr.bend as NR
12	import ./mk.bend as MK
13	import ../../lib/nat_list.bend as NL
14	
15	# The indexed TreeMap's shadow: the header, the node and payload lists (the
16	# arrays are their canonical blocks, one limit and depth for both; the node
17	# store is one block per node field, nsr.bend), a ghost
18	# tree of node ids and the free stack (ghost). Colours, links and keys are
19	# read from the node list. (generated by tools/generators/tm_state.py)
20	
21	type Tr is Data:
22	  TE{}
23	  TN{id: Nat, left: Tr, right: Tr}
24	
25	type Sh<-K: Data, -V: Data> is Data:
26	  SH{n: Nat, root: Nat, lo: Nat, hi: Nat, free: Nat, l: Nat, d: Nat, nl: List<&2, M.Node<K>>, pl: List<&2, Maybe<&2, V>>, t: Tr, fl: List<&2, Nat>}
27	
28	def nodes(~K: Data, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>) -> M.NodeStore<K>:
29	  NR.real(~K, l, d, nl)
30	
31	def pays(~V: Data, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>) -> D.DynArray<&2, Maybe<&2, V>>:
32	  DAS.real(Maybe<&2, V>, DAS.Sh{l, d, SC.length(Maybe<&2, V>, pl), MK.mk(Maybe<&2, V>, d, pl)})
33	
34	def real(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sh: Sh<K, V>) -> M.TreeMap<K, V, cmp>:
35	  match sh:
36	    case SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:
37	      M.TM{n, root, lo, hi, free, nodes(~K, l, d, nl), pays(~V, l, d, pl)}
38	
39	# ---- the ghost tree ----
40	
41	def rid(t: Tr) -> Nat:
42	  match t:
43	    case TE{}:
44	      0n
45	    case TN{+i, l, r}:
46	      i
47	
48	# the ids in key (in-)order
49	def ids(t: Tr) -> List<&2, Nat>:
50	  match t:
51	    case TE{}:
52	      Nil{}
53	    case TN{+i, l, r}:
54	      SC.append(Nat, ids(l), Con{i, ids(r)})
55	
56	def fst0(xs: List<&2, Nat>) -> Nat:
57	  match xs:
58	    case Nil{}:
59	      0n
60	    case Con{+x, t}:
61	      x
62	
63	def last0(xs: List<&2, Nat>) -> Nat:
64	  match xs:
65	    case Nil{}:
66	      0n
67	    case Con{+x, t}:
68	      match t:
69	        case Nil{}:
70	          x
71	        case Con{+y, +u}:
72	          last0(Con{y, u})
73	
74	# ---- nodes read by id ----
75	
76	def pk(-T: Type, +b: Bool, x: T, y: T) -> T:
77	  match b:
78	    case True{}:
79	      x
80	    case False{}:
81	      y
82	
83	def nth_or(-X: Data, xs: List<&2, X>, +i: Nat, +dflt: X) -> X:
84	  match xs i:
85	    case Nil{} _:
86	      dflt
87	    case Con{x, t} 0n:
88	      x
89	    case Con{x, t} 1n+p:
90	      nth_or(X, t, p, dflt)
91	
92	# the node of id (a free sentinel for 0 or an id out of range)
93	def nd(-K: Data, xs: List<&2, M.Node<K>>, +id: Nat) -> M.Node<K>:
94	  match id:
95	    case 0n:
96	      M.Free{0n}
97	    case 1n+i:
98	      nth_or(M.Node<K>, xs, i, M.Free{0n})
99	
100	def pv(-V: Data, xs: List<&2, Maybe<&2, V>>, +id: Nat) -> Maybe<&2, V>:
101	  match id:
102	    case 0n:
103	      None{}
104	    case 1n+i:
105	      nth_or(Maybe<&2, V>, xs, i, None{})
106	
107	def is_node(-K: Data, x: M.Node<K>, +a: Nat, +b: Nat, +p: Nat) -> Bool:
108	  match x:
109	    case M.Free{f}:
110	      False{}
111	    case M.N{c, +x1, +x2, +x3, k}:
112	      Bool.and(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(x3, p)))
113	
114	def is_free(-K: Data, x: M.Node<K>, +q: Nat) -> Bool:
115	  match x:
116	    case M.Free{+f}:
117	      Nat.is_eq(f, q)
118	    case M.N{c, x1, x2, x3, k}:
119	      False{}
120	
121	def is_red(-K: Data, x: M.Node<K>) -> Bool:
122	  match x:
123	    case M.Free{f}:
124	      False{}
125	    case M.N{+c, x1, x2, x3, k}:
126	      c
127	
128	# every node of t links to its children's ids and to its parent p
129	def rep(~K: Data, t: Tr, +p: Nat, +xs: List<&2, M.Node<K>>) -> Bool:
130	  match t:
131	    case TE{}:
132	      True{}
133	    case TN{+i, +l, +r}:
134	      Bool.and(Nat.is_lt(0n, i), Bool.and(is_node(K, nd(K, xs, i), rid(l), rid(r), p), Bool.and(rep(~K, l, i, xs), rep(~K, r, i, xs))))
135	
136	def some2(-V: Data, m: Maybe<&2, V>) -> Bool:
137	  match m:
138	    case None{}:
139	      False{}
140	    case Some{v}:
141	      True{}
142	
143	# every node of t has a value
144	def pay(~V: Data, t: Tr, +ys: List<&2, Maybe<&2, V>>) -> Bool:
145	  match t:
146	    case TE{}:
147	      True{}
148	    case TN{+i, l, r}:
149	      Bool.and(some2(V, pv(V, ys, i)), Bool.and(pay(~V, l, ys), pay(~V, r, ys)))
150	
151	# the free stack: each id is a free node pointing to the next (0 last)
152	def fll(~K: Data, +xs: List<&2, M.Node<K>>, fl: List<&2, Nat>) -> Bool:
153	  match fl:
154	    case Nil{}:
155	      True{}
156	    case Con{+f, +t}:
157	      Bool.and(is_free(K, nd(K, xs, f), fst0(t)), fll(~K, xs, t))
158	
159	# every id in 1..len
160	def allin(xs: List<&2, Nat>, +len: Nat) -> Bool:
161	  match xs:
162	    case Nil{}:
163	      True{}
164	    case Con{+x, t}:
165	      Bool.and(Bool.and(Nat.is_lt(0n, x), Nat.is_le(x, len)), allin(t, len))
166	
167	# ---- entries ----
168	
169	def ent(-K: Data, -V: Data, x: M.Node<K>, m: Maybe<&2, V>) -> Maybe<&2, M.Entry<K, V>>:
170	  match x m:
171	    case M.N{c, a, b, p, k} Some{v}:
172	      Some{M.Entry{k, v}}
173	    case _ _:
174	      None{}
175	
176	def cons_m(-X: Data, m: Maybe<&2, X>, xs: List<&2, X>) -> List<&2, X>:
177	  match m:
178	    case None{}:
179	      xs
180	    case Some{x}:
181	      Con{x, xs}
182	
183	# the entries of the ids, in order
184	def ents(~K: Data, ~V: Data, ix: List<&2, Nat>, +xs: List<&2, M.Node<K>>, +ys: List<&2, Maybe<&2, V>>) -> List<&2, M.Entry<K, V>>:
185	  match ix:
186	    case Nil{}:
187	      Nil{}
188	    case Con{+i, t}:
189	      cons_m(M.Entry<K, V>, ent(K, V, nd(K, xs, i), pv(V, ys, i)), ents(~K, ~V, t, xs, ys))
190	
191	# consecutive keys strictly increasing (the model invariant, stated in the spec)
192	def ordered(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, es: List<&2, M.Entry<K, V>>) -> Bool:
193	  S.ordered(~K, ~V, ~cmp, es)
194	
195	def root_black(~K: Data, t: Tr, +xs: List<&2, M.Node<K>>) -> Bool:
196	  match t:
197	    case TE{}:
198	      True{}
199	    case TN{+i, l, r}:
200	      Bool.not(is_red(K, nd(K, xs, i)))
201	
202	def model(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sh: Sh<K, V>) -> S.Model<K, V>:
203	  match sh:
204	    case SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:
205	      S.TM{l, ents(~K, ~V, ids(t), nl, pl)}
206	
207	# ---- the invariant ----
208	
209	def cl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
210	  Nat.is_le(l, 31n)
211	
212	def cd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
213	  Nat.is_le(d, l)
214	
215	def ccap(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
216	  Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d))
217	
218	def cpl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
219	  Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl))
220	
221	def crep(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
222	  rep(~K, t, 0n, nl)
223	
224	def cpay(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
225	  pay(~V, t, pl)
226	
227	def cfll(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
228	  fll(~K, nl, fl)
229	
230	def cnd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
231	  NL.nodupn(SC.append(Nat, ids(t), fl))
232	
233	def cin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
234	  allin(SC.append(Nat, ids(t), fl), SC.length(M.Node<K>, nl))
235	
236	def clen(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
237	  Nat.is_eq(SC.length(Nat, SC.append(Nat, ids(t), fl)), SC.length(M.Node<K>, nl))
238	
239	def cord(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
240	  ordered(~K, ~V, ~cmp, ents(~K, ~V, ids(t), nl, pl))
241	
242	def cblk(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
243	  root_black(~K, t, nl)
244	
245	def csz(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
246	  Nat.is_eq(n, SC.length(Nat, ids(t)))
247	
248	def croot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
249	  Nat.is_eq(root, rid(t))
250	
251	def clo(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
252	  Nat.is_eq(lo, fst0(ids(t)))
253	
254	def chi(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
255	  Nat.is_eq(hi, last0(ids(t)))
256	
257	def cfree(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
258	  Nat.is_eq(free, fst0(fl))
259	
260	def gr15(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
261	  Bool.and(chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
262	
263	def gr14(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
264	  Bool.and(clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
265	
266	def gr13(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
267	  Bool.and(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
268	
269	def gr12(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
270	  Bool.and(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
271	
272	def gr11(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
273	  Bool.and(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
274	
275	def gr10(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
276	  Bool.and(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
277	
278	def gr9(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
279	  Bool.and(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
280	
281	def gr8(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
282	  Bool.and(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
283	
284	def gr7(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
285	  Bool.and(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
286	
287	def gr6(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
288	  Bool.and(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
289	
290	def gr5(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
291	  Bool.and(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
292	
293	def gr4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
294	  Bool.and(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
295	
296	def gr3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
297	  Bool.and(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
298	
299	def gr2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
300	  Bool.and(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
301	
302	def gr1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
303	  Bool.and(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
304	
305	def goodF(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
306	  Bool.and(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))
307	
308	def good(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sh: Sh<K, V>) -> Bool:
309	  match sh:
310	    case SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:
311	      goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl)
312	
313	def gp1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
314	  L.and_right(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), g)
315	
316	def gp2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
317	  L.and_right(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
318	
319	def gp3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
320	  L.and_right(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
321	
322	def gp4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
323	  L.and_right(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
324	
325	def gp5(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
326	  L.and_right(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
327	
328	def gp6(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
329	  L.and_right(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
330	
331	def gp7(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
332	  L.and_right(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
333	
334	def gp8(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
335	  L.and_right(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
336	
337	def gp9(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
338	  L.and_right(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
339	
340	def gp10(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
341	  L.and_right(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
342	
343	def gp11(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
344	  L.and_right(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
345	
346	def gp12(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
347	  L.and_right(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
348	
349	def gp13(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
350	  L.and_right(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
351	
352	def gp14(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
353	  L.and_right(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
354	
355	def gp15(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
356	  L.and_right(clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
357	
358	def gp16(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
359	  L.and_right(chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
360	
361	def g_cl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
362	  L.and_left(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), g)
363	
364	def g_cd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
365	  L.and_left(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
366	
367	def g_ccap(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
368	  L.and_left(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
369	
370	def g_cpl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
371	  L.and_left(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
372	
373	def g_crep(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
374	  L.and_left(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
375	
376	def g_cpay(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
377	  L.and_left(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
378	
379	def g_cfll(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
380	  L.and_left(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
381	
382	def g_cnd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
383	  L.and_left(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
384	
385	def g_cin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
386	  L.and_left(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
387	
388	def g_clen(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
389	  L.and_left(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
390	
391	def g_cord(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
392	  L.and_left(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
393	
394	def g_cblk(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
395	  L.and_left(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
396	
397	def g_csz(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
398	  L.and_left(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
399	
400	def g_croot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
401	  L.and_left(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
402	
403	def g_clo(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
404	  L.and_left(clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
405	
406	def g_chi(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
407	  L.and_left(chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))
408	
409	def g_cfree(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
410	  gp16(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g)
411	
412	# the invariant from its components
413	def good_intro(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +h_cl: {cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cd: {cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_ccap: {ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cpl: {cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_crep: {crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cpay: {cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cfll: {cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cnd: {cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cin: {cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_clen: {clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cord: {cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cblk: {cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_csz: {csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_croot: {croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_clo: {clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_chi: {chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cfree: {cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
414	  L.and_intro(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cl, L.and_intro(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cd, L.and_intro(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_ccap, L.and_intro(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cpl, L.and_intro(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_crep, L.and_intro(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cpay, L.and_intro(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cfll, L.and_intro(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cnd, L.and_intro(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cin, L.and_intro(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_clen, L.and_intro(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cord, L.and_intro(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cblk, L.and_intro(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_csz, L.and_intro(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n,