proofs/containers/balanced_search_tree/state.bend
bend-collections-laws-containers@1.0.0.0 · 414 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as DAS
9import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
10import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as D
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsr.bend as NR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mk.bend as MK
13import bend-collections-laws-containers@1.0.0.0/proofs/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
21type Tr is Data:
22 TE{}
23 TN{id: Nat, left: Tr, right: Tr}
24
25type 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
28def nodes(~K: Data, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>) -> M.NodeStore<K>:
29 NR.real(~K, l, d, nl)
30
31def 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
34def 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
41def 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
49def 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
56def fst0(xs: List<&2, Nat>) -> Nat:
57 match xs:
58 case Nil{}:
59 0n
60 case Con{+x, t}:
61 x
62
63def 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
76def pk(-T: Type, +b: Bool, x: T, y: T) -> T:
77 match b:
78 case True{}:
79 x
80 case False{}:
81 y
82
83def 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)
93def 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
100def 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
107def 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
114def 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
121def 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
129def 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
136def 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
144def 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)
152def 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
160def 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
169def 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
176def 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
184def 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)
192def 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
195def 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
202def 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
209def 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
212def 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
215def 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
218def 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
221def 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
224def 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
227def 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
230def 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
233def 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
236def 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
239def 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
242def 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
245def 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
248def 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
251def 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
254def 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
257def 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
260def 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
263def 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
266def 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
269def 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
272def 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
275def 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
278def 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
281def 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
284def 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
287def 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
290def 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
293def 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
296def 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
299def 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
302def 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
305def 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
308def 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
313def 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
316def 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
319def 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
322def 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
325def 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
328def 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
331def 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
334def 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
337def 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
340def 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
343def 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
346def 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
349def 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
352def 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
355def 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
358def 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
361def 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
364def 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
367def 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
370def 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
373def 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
376def 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
379def 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
382def 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
385def 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
388def 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
391def 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
394def 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
397def 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
400def 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
403def 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
406def 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
409def 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
413def 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, root, lo, hi, free, l, d, nl, pl, t, fl), h_croot, L.and_intro(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), h_clo, L.and_intro(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), h_chi, h_cfree))))))))))))))))