proofs/containers/lru/state.bend
bend-collections-laws-containers@1.0.0.0 · 583 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/hash_table.bend as S
7import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
10import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
11import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as IV
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
19import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
20
21# The LRU as a Data shadow: its U32 fields, the table exponent k (2^k
22# buckets), the arena exponent sd (2^sd slots), a mirror tree for each array,
23# and two ghost lists the implementation does not hold: sl, the live slots
24# from oldest to newest (the recency list), and fl, the free list in order.
25# real(sh) is the LRU<&2, V> the implementation holds.
26#
27# m meta words: 0 fresh, 1 size, 2 depth, 3 lifetime on, 4-5 lifetime,
28# 6 mask, 7 bits, 16 + 2c / 17 + 2c counter c
29# tab the hash map's bucket table (proofs/hash_table/table.bend decodes it)
30# lk eight words per slot: prev, next, check word, timed, deadline lo, hi
31
32type Sh<-V: Data> is Data:
33 LS{cap: U32, n: U32, head: U32, tail: U32, free: U32, mT: AR.Tree<U32>, k: Nat, sd: Nat, tabT: AR.Tree<U32>, ksT: AR.Tree<String>, eT: AR.Tree<Maybe<&2, V>>, lkT: AR.Tree<U32>, sl: List<&2, Nat>, fl: List<&2, Nat>}
34
35def real(~V: Data, sh: Sh<V>) -> LR.LRU<&2, V>:
36 match sh:
37 case LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}:
38 LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}
39
40# ---- slots and their words ----
41
42# the link of slot s
43
44# the link of the first slot of t, q for none
45
46# the link of the last slot of t, p for none
47
48# word o of slot s in lk
49def off(+s: Nat, +o: Nat) -> Nat:
50 Nat.add(Nat.double(Nat.double(Nat.double(s))), o)
51
52def lw(+ll: List<&2, U32>, +s: Nat, +o: Nat) -> U32:
53 W32.nth0(ll, off(s, o))
54
55# the segment sl: its first slot's prev is p, its last slot's next is q,
56# and consecutive slots are linked both ways
57def seg(+ll: List<&2, U32>, sl: List<&2, Nat>, +p: U32, +q: U32) -> Bool:
58 match sl:
59 case Nil{}:
60 True{}
61 case Con{+s, +t}:
62 Bool.and(U32.is_eq(lw(ll, s, 0n), p), Bool.and(U32.is_eq(lw(ll, s, 1n), LK.fst_or(t, q)), seg(ll, t, LK.lnk(s), q)))
63
64# the free list: each slot's next is the slot after it (0 for the last)
65def fll(+ll: List<&2, U32>, fl: List<&2, Nat>) -> Bool:
66 match fl:
67 case Nil{}:
68 True{}
69 case Con{+s, +t}:
70 Bool.and(U32.is_eq(lw(ll, s, 1n), LK.fst_or(t, 0)), fll(ll, t))
71
72
73def live(~V: Data, +el: List<&2, Maybe<&2, V>>, +s: Nat) -> Bool:
74 HT.some_b(~V, HT.nthm(~V, el, s))
75
76# ---- predicates on slots, and their conjunction over a list ----
77
78type SP1<-V: Data> is Data:
79 PLive{fr: Nat, el: List<&2, Maybe<&2, V>>}
80 PVac{fr: Nat, el: List<&2, Maybe<&2, V>>}
81 PHas{bs: List<&2, B.Bk>, m: Nat, ll: List<&2, U32>}
82 PNk{ll: List<&2, U32>, kl: List<&2, String>, key: String}
83
84# ---- the table and the slots ----
85
86# b is a full bucket with word w and link l
87def isbf(b: B.Bk, +w: U32, +l: U32) -> Bool:
88 match b:
89 case B.BE{}:
90 False{}
91 case B.BF{+w2, +l2, k}:
92 Bool.and(U32.is_eq(w2, w), U32.is_eq(l2, l))
93
94# some bucket below m is full with word w and link l
95def anyb(+bs: List<&2, B.Bk>, +m: Nat, +l: U32, +w: U32) -> Bool:
96 match m:
97 case 0n:
98 False{}
99 case 1n+j:
100 Bool.or(isbf(B.at(bs, j), w, l), anyb(bs, j, l, w))
101
102# a full bucket's slot is on the recency list and stores the bucket's word
103def bslb(+sl: List<&2, Nat>, +ll: List<&2, U32>, b: B.Bk) -> Bool:
104 match b:
105 case B.BE{}:
106 True{}
107 case B.BF{+w, +l, k}:
108 Bool.and(NL.memn(UD.v(H.slot(l)), sl), U32.is_eq(lw(ll, UD.v(H.slot(l)), 2n), w))
109
110def bsl(+bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +ll: List<&2, U32>, +m: Nat) -> Bool:
111 match m:
112 case 0n:
113 True{}
114 case 1n+j:
115 Bool.and(bslb(sl, ll, B.at(bs, j)), bsl(bs, sl, ll, j))
116
117# ---- the abstraction ----
118
119# the key of slot s: a one-character key is its check word, any other is
120# its stored String
121def skey(+ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat) -> String:
122 TB.keyof(lw(ll, s, 2n), TB.nths(kl, s))
123
124def sent_m(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, m: Maybe<&2, V>) -> List<&2, SP.Ent<V>>:
125 match m:
126 case None{}:
127 Nil{}
128 case Some{v}:
129 Con{SP.LE{skey(ll, kl, s), v, lw(ll, s, 3n), W.U64{lw(ll, s, 4n), lw(ll, s, 5n)}}, Nil{}}
130
131# the entries of the slots of sl, in order
132def es(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, sl: List<&2, Nat>) -> List<&2, SP.Ent<V>>:
133 match sl:
134 case Nil{}:
135 Nil{}
136 case Con{+s, t}:
137 SC.append(SP.Ent<V>, sent_m(~V, ll, kl, s, HT.nthm(~V, el, s)), es(~V, ll, kl, el, t))
138
139def w64(+ml: List<&2, U32>, +i: Nat) -> W.U64:
140 W.U64{W32.nth0(ml, i), W32.nth0(ml, 1n+i)}
141
142def ctr(+ml: List<&2, U32>) -> SP.Ctr:
143 SP.CT{w64(ml, 16n), w64(ml, 18n), w64(ml, 20n), w64(ml, 22n), w64(ml, 24n)}
144
145def modelF(~V: Data, +cap: U32, +mT: AR.Tree<U32>, +kl: List<&2, String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>) -> SP.Lru<V>:
146 SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), w64(AR.slots(U32, mT), 4n), es(~V, AR.slots(U32, lkT), kl, AR.slots(Maybe<&2, V>, eT), sl), ctr(AR.slots(U32, mT))}
147
148# the entries of a model
149def lru_es(~V: Data, l: SP.Lru<V>) -> List<&2, SP.Ent<V>>:
150 match l:
151 case SP.L{cap, on, life, es, c}:
152 es
153
154# the cache the shadow stands for
155def model(~V: Data, sh: Sh<V>) -> SP.Lru<V>:
156 match sh:
157 case LS{+cap, n, head, tail, free, +mT, k, sd, tabT, +ksT, +eT, +lkT, +sl, fl}:
158 modelF(~V, cap, mT, AR.slots(String, ksT), eT, lkT, sl)
159
160def sev(~V: Data, p: SP1<V>, +s: Nat) -> Bool:
161 match p:
162 case PLive{+fr, +el}:
163 Bool.and(Nat.is_lt(s, fr), live(~V, el, s))
164 case PVac{+fr, +el}:
165 Bool.and(Nat.is_lt(s, fr), Bool.not(live(~V, el, s)))
166 case PHas{+bs, +m, +ll}:
167 anyb(bs, m, LK.lnk(s), lw(ll, s, 2n))
168 case PNk{+ll, +kl, +key}:
169 Bool.not(S.str_eq(skey(ll, kl, s), key))
170
171# p holds for every slot of xs
172def sall(~V: Data, +p: SP1<V>, xs: List<&2, Nat>) -> Bool:
173 match xs:
174 case Nil{}:
175 True{}
176 case Con{+s, t}:
177 Bool.and(sev(~V, p, s), sall(~V, p, t))
178
179# every slot of xs is below fr and live
180def slok(~V: Data, xs: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>) -> Bool:
181 sall(~V, PLive{fr, el}, xs)
182
183# every slot of xs is below fr and vacant
184def flok(~V: Data, xs: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>) -> Bool:
185 sall(~V, PVac{fr, el}, xs)
186
187# every slot of sl has a bucket with its link and its stored check word
188def hasall(~V: Data, +bs: List<&2, B.Bk>, +m: Nat, +ll: List<&2, U32>, sl: List<&2, Nat>) -> Bool:
189 sall(~V, PHas{bs, m, ll}, sl)
190
191# no slot of sl has key
192def nokey(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, sl: List<&2, Nat>, +key: String) -> Bool:
193 sall(~V, PNk{ll, kl, key}, sl)
194
195# ---- the invariant (generated) ----
196# (tools/generators/lru_state.py)
197
198def ck(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
199 Bool.and(Nat.is_lt(k, 30n), Nat.is_lt(0n, k))
200
201def csdk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
202 Nat.is_lt(sd, k)
203
204def cpt(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
205 AR.perfect(U32, 1n+k, tabT)
206
207def cpk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
208 pk
209
210def cpe(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
211 AR.perfect(Maybe<&2, V>, sd, eT)
212
213def cpl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
214 AR.perfect(U32, 3n+sd, lkT)
215
216def cpm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
217 pm
218
219def cmask(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
220 U32.is_eq(mmk, CY.msk(k))
221
222def cbits(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
223 Nat.is_eq(UD.v(mbt), k)
224
225def csize(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
226 Nat.is_eq(UD.v(msz), SC.pow2(sd))
227
228def cdepth(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
229 Nat.is_eq(UD.v(mdp), sd)
230
231def cfresh(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
232 Nat.is_le(UD.v(fr), SC.pow2(sd))
233
234def cwell(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
235 B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k))
236
237def cclus(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
238 B.cluster(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k))
239
240def cuniq(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
241 B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k))}, SC.pow2(k))
242
243def cn(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
244 Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k)))
245
246def cload(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
247 Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k))
248
249def ccap(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
250 Bool.not(U32.is_eq(cap, 0))
251
252def cbsl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
253 bsl(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k))
254
255def chas(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
256 hasall(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), sl)
257
258def csl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
259 slok(~V, sl, UD.v(fr), AR.slots(Maybe<&2, V>, eT))
260
261def cnd(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
262 NL.nodupn(sl)
263
264def clen(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
265 Nat.is_eq(SC.length(Nat, sl), UD.v(n))
266
267def chead(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
268 U32.is_eq(head, LK.fst_or(sl, 0))
269
270def ctail(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
271 U32.is_eq(tail, LK.last_or(sl, 0))
272
273def cdll(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
274 seg(AR.slots(U32, lkT), sl, 0, 0)
275
276def ckeys(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
277 S.nodup(SP.keys_of(~V, es(~V, AR.slots(U32, lkT), kl, AR.slots(Maybe<&2, V>, eT), sl)))
278
279def cfree(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
280 U32.is_eq(free, LK.fst_or(fl, 0))
281
282def cfll(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
283 fll(AR.slots(U32, lkT), fl)
284
285def cfl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
286 flok(~V, fl, UD.v(fr), AR.slots(Maybe<&2, V>, eT))
287
288def cfnd(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
289 NL.nodupn(fl)
290
291def cfcnt(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
292 Nat.is_eq(Nat.add(SC.length(Nat, sl), SC.length(Nat, fl)), UD.v(fr))
293
294def gr30(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
295 Bool.and(cfnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), cfcnt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
296
297def gr29(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
298 Bool.and(cfl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr30(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
299
300def gr28(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
301 Bool.and(cfll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr29(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
302
303def gr27(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
304 Bool.and(cfree(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr28(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
305
306def gr26(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
307 Bool.and(ckeys(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr27(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
308
309def gr25(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
310 Bool.and(cdll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr26(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
311
312def gr24(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
313 Bool.and(ctail(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr25(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
314
315def gr23(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
316 Bool.and(chead(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr24(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
317
318def gr22(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
319 Bool.and(clen(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr23(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
320
321def gr21(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
322 Bool.and(cnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr22(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
323
324def gr20(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
325 Bool.and(csl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr21(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
326
327def gr19(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
328 Bool.and(chas(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr20(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
329
330def gr18(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
331 Bool.and(cbsl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr19(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
332
333def gr17(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
334 Bool.and(ccap(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr18(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
335
336def gr16(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
337 Bool.and(cload(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr17(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
338
339def gr15(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
340 Bool.and(cn(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr16(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
341
342def gr14(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
343 Bool.and(cuniq(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr15(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
344
345def gr13(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
346 Bool.and(cclus(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr14(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
347
348def gr12(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
349 Bool.and(cwell(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr13(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
350
351def gr11(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
352 Bool.and(cfresh(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr12(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
353
354def gr10(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
355 Bool.and(cdepth(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr11(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
356
357def gr9(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
358 Bool.and(csize(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr10(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
359
360def gr8(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
361 Bool.and(cbits(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr9(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
362
363def gr7(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
364 Bool.and(cmask(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr8(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
365
366def gr6(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
367 Bool.and(cpm(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr7(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
368
369def gr5(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
370 Bool.and(cpl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr6(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
371
372def gr4(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
373 Bool.and(cpe(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr5(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
374
375def gr3(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
376 Bool.and(cpk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr4(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
377
378def gr2(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
379 Bool.and(cpt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr3(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
380
381def gr1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
382 Bool.and(csdk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr2(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
383
384def goodF(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
385 Bool.and(ck(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr1(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl))
386
387def good(~V: Data, sh: Sh<V>) -> Bool:
388 match sh:
389 case LS{+cap, +n, +head, +tail, +free, +mT, +k, +sd, +tabT, +ksT, +eT, +lkT, +sl, +fl}:
390 goodF(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl)
391
392def gp1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr1(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
393 L.and_right(ck(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr1(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), g)
394
395def gp2(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr2(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
396 L.and_right(csdk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr2(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp1(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
397
398def gp3(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr3(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
399 L.and_right(cpt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr3(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp2(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
400
401def gp4(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr4(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
402 L.and_right(cpk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr4(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp3(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
403
404def gp5(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr5(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
405 L.and_right(cpe(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr5(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp4(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
406
407def gp6(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr6(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
408 L.and_right(cpl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr6(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp5(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
409
410def gp7(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr7(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
411 L.and_right(cpm(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr7(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp6(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
412
413def gp8(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr8(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
414 L.and_right(cmask(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr8(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp7(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
415
416def gp9(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr9(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
417 L.and_right(cbits(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr9(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp8(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
418
419def gp10(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr10(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
420 L.and_right(csize(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr10(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp9(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
421
422def gp11(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr11(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
423 L.and_right(cdepth(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr11(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp10(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
424
425def gp12(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr12(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
426 L.and_right(cfresh(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr12(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp11(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
427
428def gp13(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr13(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
429 L.and_right(cwell(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr13(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp12(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
430
431def gp14(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr14(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
432 L.and_right(cclus(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr14(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp13(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
433
434def gp15(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr15(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
435 L.and_right(cuniq(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr15(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp14(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
436
437def gp16(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr16(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
438 L.and_right(cn(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr16(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp15(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
439
440def gp17(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr17(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
441 L.and_right(cload(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr17(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp16(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
442
443def gp18(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr18(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
444 L.and_right(ccap(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr18(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp17(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
445
446def gp19(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr19(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
447 L.and_right(cbsl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr19(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp18(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
448
449def gp20(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr20(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
450 L.and_right(chas(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr20(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp19(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
451
452def gp21(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr21(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
453 L.and_right(csl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr21(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp20(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
454
455def gp22(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr22(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
456 L.and_right(cnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr22(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp21(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
457
458def gp23(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr23(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
459 L.and_right(clen(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr23(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp22(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
460
461def gp24(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr24(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
462 L.and_right(chead(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr24(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp23(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
463
464def gp25(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr25(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
465 L.and_right(ctail(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr25(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp24(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
466
467def gp26(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr26(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
468 L.and_right(cdll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr26(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp25(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
469
470def gp27(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr27(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
471 L.and_right(ckeys(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr27(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp26(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
472
473def gp28(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr28(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
474 L.and_right(cfree(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr28(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp27(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
475
476def gp29(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr29(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
477 L.and_right(cfll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr29(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp28(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
478
479def gp30(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {gr30(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
480 L.and_right(cfl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr30(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp29(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
481
482def gp31(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cfcnt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
483 L.and_right(cfnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), cfcnt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp30(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
484
485def g_ck(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {ck(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
486 L.and_left(ck(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr1(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), g)
487
488def g_csdk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {csdk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
489 L.and_left(csdk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr2(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp1(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
490
491def g_cpt(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cpt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
492 L.and_left(cpt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr3(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp2(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
493
494def g_cpk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cpk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
495 L.and_left(cpk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr4(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp3(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
496
497def g_cpe(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cpe(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
498 L.and_left(cpe(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr5(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp4(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
499
500def g_cpl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cpl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
501 L.and_left(cpl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr6(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp5(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
502
503def g_cpm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cpm(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
504 L.and_left(cpm(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr7(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp6(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
505
506def g_cmask(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cmask(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
507 L.and_left(cmask(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr8(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp7(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
508
509def g_cbits(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cbits(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
510 L.and_left(cbits(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr9(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp8(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
511
512def g_csize(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {csize(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
513 L.and_left(csize(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr10(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp9(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
514
515def g_cdepth(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cdepth(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
516 L.and_left(cdepth(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr11(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp10(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
517
518def g_cfresh(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cfresh(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
519 L.and_left(cfresh(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr12(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp11(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
520
521def g_cwell(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cwell(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
522 L.and_left(cwell(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr13(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp12(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
523
524def g_cclus(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cclus(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
525 L.and_left(cclus(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr14(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp13(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
526
527def g_cuniq(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cuniq(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
528 L.and_left(cuniq(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr15(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp14(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
529
530def g_cn(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cn(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
531 L.and_left(cn(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr16(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp15(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
532
533def g_cload(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cload(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
534 L.and_left(cload(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr17(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp16(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
535
536def g_ccap(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {ccap(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
537 L.and_left(ccap(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr18(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp17(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
538
539def g_cbsl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cbsl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
540 L.and_left(cbsl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr19(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp18(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
541
542def g_chas(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {chas(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
543 L.and_left(chas(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr20(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp19(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
544
545def g_csl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {csl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
546 L.and_left(csl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr21(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp20(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
547
548def g_cnd(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
549 L.and_left(cnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr22(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp21(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
550
551def g_clen(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {clen(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
552 L.and_left(clen(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr23(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp22(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
553
554def g_chead(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {chead(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
555 L.and_left(chead(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr24(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp23(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
556
557def g_ctail(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {ctail(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
558 L.and_left(ctail(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr25(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp24(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
559
560def g_cdll(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cdll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
561 L.and_left(cdll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr26(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp25(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
562
563def g_ckeys(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {ckeys(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
564 L.and_left(ckeys(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr27(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp26(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
565
566def g_cfree(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cfree(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
567 L.and_left(cfree(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr28(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp27(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
568
569def g_cfll(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cfll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
570 L.and_left(cfll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr29(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp28(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
571
572def g_cfl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cfl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
573 L.and_left(cfl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr30(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp29(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
574
575def g_cfnd(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cfnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
576 L.and_left(cfnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), cfcnt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gp30(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g))
577
578def g_cfcnt(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {cfcnt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
579 gp31(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g)
580
581# the invariant from its components
582def good_intro(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +fr: U32, +msz: U32, +mdp: U32, +mmk: U32, +mbt: U32, +pm: Bool, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +h_ck: {ck(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_csdk: {csdk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cpt: {cpt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cpk: {cpk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cpe: {cpe(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cpl: {cpl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cpm: {cpm(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cmask: {cmask(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cbits: {cbits(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_csize: {csize(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cdepth: {cdepth(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cfresh: {cfresh(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cwell: {cwell(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cclus: {cclus(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cuniq: {cuniq(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cn: {cn(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cload: {cload(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_ccap: {ccap(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cbsl: {cbsl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_chas: {chas(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_csl: {csl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cnd: {cnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_clen: {clen(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_chead: {chead(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_ctail: {ctail(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cdll: {cdll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_ckeys: {ckeys(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cfree: {cfree(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cfll: {cfll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cfl: {cfl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cfnd: {cfnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}, +h_cfcnt: {cfcnt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}) -> {goodF(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}:
583 L.and_intro(ck(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr1(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_ck, L.and_intro(csdk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr2(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_csdk, L.and_intro(cpt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr3(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cpt, L.and_intro(cpk(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr4(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cpk, L.and_intro(cpe(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr5(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cpe, L.and_intro(cpl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr6(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cpl, L.and_intro(cpm(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr7(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cpm, L.and_intro(cmask(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr8(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cmask, L.and_intro(cbits(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr9(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cbits, L.and_intro(csize(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr10(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_csize, L.and_intro(cdepth(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr11(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cdepth, L.and_intro(cfresh(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr12(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cfresh, L.and_intro(cwell(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr13(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cwell, L.and_intro(cclus(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr14(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cclus, L.and_intro(cuniq(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr15(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cuniq, L.and_intro(cn(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr16(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cn, L.and_intro(cload(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr17(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cload, L.and_intro(ccap(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr18(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_ccap, L.and_intro(cbsl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr19(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cbsl, L.and_intro(chas(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr20(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_chas, L.and_intro(csl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr21(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_csl, L.and_intro(cnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr22(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cnd, L.and_intro(clen(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr23(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_clen, L.and_intro(chead(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr24(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_chead, L.and_intro(ctail(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr25(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_ctail, L.and_intro(cdll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr26(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cdll, L.and_intro(ckeys(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr27(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_ckeys, L.and_intro(cfree(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr28(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cfree, L.and_intro(cfll(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr29(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cfll, L.and_intro(cfl(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), gr30(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cfl, L.and_intro(cfnd(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), cfcnt(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl), h_cfnd, h_cfcnt)))))))))))))))))))))))))))))))