proofs/containers/doubly_linked_list/state.bend
bend-collections-laws-containers@1.0.0.0 · 316 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/doubly_linked_list.bend as S
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
8import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
9import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
10import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
14
15# The doubly linked list's shadow: the public list's fields, one mirror tree
16# per array (values, prev links, next links, generations), the ids of the
17# list in order and the free stack (both ghost). The storage's count is the
18# order's length, and its depth and capacity are the public ones.
19# (generated by tools/generators/dll_state.py)
20
21type Sh<-T: Data> is Data:
22 LS{tag: U32, cap: U32, fresh: U32, free: U32, head: U32, tail: U32, depth: Nat, vT: AR.Tree<Maybe<&2, T>>, pT: AR.Tree<U32>, nT: AR.Tree<U32>, gT: AR.Tree<U32>, sl: List<&2, Nat>, fl: List<&2, Nat>}
23
24def real(~T: Data, sh: Sh<T>) -> D.DList<T>:
25 match sh:
26 case LS{+tag, +cap, +fresh, +free, +head, +tail, +depth, +vT, +pT, +nT, +gT, +sl, +fl}:
27 D.DL{tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, AR.thaw(U32, gT)}
28
29def model(~T: Data, sh: Sh<T>) -> S.DS<T>:
30 match sh:
31 case LS{+tag, +cap, +fresh, +free, +head, +tail, +depth, +vT, +pT, +nT, +gT, +sl, +fl}:
32 S.DS{tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}
33
34# ---- links (lnk, fst_or, last_or, nodupn: the LRU's, proofs/containers/lru/state.bend) ----
35
36# the segment sl: its first id's prev is p, its last id's next is q, and
37# consecutive ids are linked both ways
38def seg(+pl: List<&2, U32>, +nl: List<&2, U32>, sl: List<&2, Nat>, +p: U32, +q: U32) -> Bool:
39 match sl:
40 case Nil{}:
41 True{}
42 case Con{+s, +t}:
43 Bool.and(U32.is_eq(W32.nth0(pl, s), p), Bool.and(U32.is_eq(W32.nth0(nl, s), LK.fst_or(t, q)), seg(pl, nl, t, LK.lnk(s), q)))
44
45# the free stack: each id's next is the id after it (0 for the last)
46def fll(+nl: List<&2, U32>, fl: List<&2, Nat>) -> Bool:
47 match fl:
48 case Nil{}:
49 True{}
50 case Con{+s, +t}:
51 Bool.and(U32.is_eq(W32.nth0(nl, s), LK.fst_or(t, 0)), fll(nl, t))
52
53def some_b(-T: Data, m: Maybe<&2, T>) -> Bool:
54 match m:
55 case None{}:
56 False{}
57 case Some{v}:
58 True{}
59
60def live(-T: Data, +vl: List<&2, Maybe<&2, T>>, +x: Nat) -> Bool:
61 some_b(T, S.val_of(T, vl, x))
62
63# every id of xs is below fr and live
64def slok(~T: Data, xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>) -> Bool:
65 match xs:
66 case Nil{}:
67 True{}
68 case Con{+x, t}:
69 Bool.and(Bool.and(Nat.is_lt(x, fr), live(T, vl, x)), slok(~T, t, fr, vl))
70
71# every id of xs is below fr and vacant
72def flok(~T: Data, xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>) -> Bool:
73 match xs:
74 case Nil{}:
75 True{}
76 case Con{+x, t}:
77 Bool.and(Bool.and(Nat.is_lt(x, fr), Bool.not(live(T, vl, x))), flok(~T, t, fr, vl))
78
79# every generation from index fr on is 0 (the ids not issued yet)
80def gz(gl: List<&2, U32>, +fr: Nat) -> Bool:
81 match gl fr:
82 case Nil{} _:
83 True{}
84 case Con{+g, +t} 0n:
85 Bool.and(U32.is_eq(g, 0), gz(t, 0n))
86 case Con{+g, +t} 1n+p:
87 gz(t, p)
88
89# every live value slot (index k on) is an id of sl
90def lvin(~T: Data, vl: List<&2, Maybe<&2, T>>, +k: Nat, +sl: List<&2, Nat>) -> Bool:
91 match vl:
92 case Nil{}:
93 True{}
94 case Con{m, t}:
95 Bool.and(Bool.or(Bool.not(some_b(T, m)), NL.memn(k, sl)), lvin(~T, t, 1n+k, sl))
96
97# ---- the invariant ----
98
99def cdep(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
100 Nat.is_lt(depth, 30n)
101
102def ccap(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
103 Nat.is_eq(UD.v(cap), SC.pow2(depth))
104
105def cpv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
106 AR.perfect(Maybe<&2, T>, depth, vT)
107
108def cpp(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
109 AR.perfect(U32, depth, pT)
110
111def cpn(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
112 AR.perfect(U32, depth, nT)
113
114def cpg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
115 AR.perfect(U32, depth, gT)
116
117def cfr(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
118 Nat.is_le(UD.v(fresh), UD.v(cap))
119
120def cseg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
121 seg(AR.slots(U32, pT), AR.slots(U32, nT), sl, 0, 0)
122
123def chead(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
124 U32.is_eq(head, LK.fst_or(sl, 0))
125
126def ctail(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
127 U32.is_eq(tail, LK.last_or(sl, 0))
128
129def cnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
130 NL.nodupn(sl)
131
132def csl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
133 slok(~T, sl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))
134
135def cfree(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
136 U32.is_eq(free, LK.fst_or(fl, 0))
137
138def cfll(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
139 fll(AR.slots(U32, nT), fl)
140
141def cfl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
142 flok(~T, fl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))
143
144def cfnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
145 NL.nodupn(fl)
146
147def cgz(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
148 gz(AR.slots(U32, gT), UD.v(fresh))
149
150def clv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
151 lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl)
152
153def gr16(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
154 Bool.and(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
155
156def gr15(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
157 Bool.and(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
158
159def gr14(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
160 Bool.and(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
161
162def gr13(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
163 Bool.and(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
164
165def gr12(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
166 Bool.and(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
167
168def gr11(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
169 Bool.and(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
170
171def gr10(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
172 Bool.and(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
173
174def gr9(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
175 Bool.and(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
176
177def gr8(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
178 Bool.and(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
179
180def gr7(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
181 Bool.and(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
182
183def gr6(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
184 Bool.and(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
185
186def gr5(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
187 Bool.and(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
188
189def gr4(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
190 Bool.and(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
191
192def gr3(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
193 Bool.and(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
194
195def gr2(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
196 Bool.and(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
197
198def gr1(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
199 Bool.and(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
200
201def goodF(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:
202 Bool.and(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))
203
204def good(~T: Data, sh: Sh<T>) -> Bool:
205 match sh:
206 case LS{+tag, +cap, +fresh, +free, +head, +tail, +depth, +vT, +pT, +nT, +gT, +sl, +fl}:
207 goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl)
208
209def gp1(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
210 L.and_right(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), g)
211
212def gp2(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
213 L.and_right(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
214
215def gp3(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
216 L.and_right(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
217
218def gp4(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
219 L.and_right(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
220
221def gp5(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
222 L.and_right(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
223
224def gp6(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
225 L.and_right(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
226
227def gp7(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
228 L.and_right(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
229
230def gp8(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
231 L.and_right(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
232
233def gp9(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
234 L.and_right(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
235
236def gp10(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
237 L.and_right(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
238
239def gp11(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
240 L.and_right(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
241
242def gp12(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
243 L.and_right(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
244
245def gp13(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
246 L.and_right(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
247
248def gp14(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
249 L.and_right(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
250
251def gp15(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
252 L.and_right(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
253
254def gp16(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
255 L.and_right(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
256
257def gp17(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
258 L.and_right(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
259
260def g_cdep(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
261 L.and_left(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), g)
262
263def g_ccap(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
264 L.and_left(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
265
266def g_cpv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
267 L.and_left(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
268
269def g_cpp(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
270 L.and_left(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
271
272def g_cpn(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
273 L.and_left(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
274
275def g_cpg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
276 L.and_left(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
277
278def g_cfr(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
279 L.and_left(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
280
281def g_cseg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
282 L.and_left(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
283
284def g_chead(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
285 L.and_left(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
286
287def g_ctail(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
288 L.and_left(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
289
290def g_cnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
291 L.and_left(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
292
293def g_csl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
294 L.and_left(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
295
296def g_cfree(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
297 L.and_left(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
298
299def g_cfll(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
300 L.and_left(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
301
302def g_cfl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
303 L.and_left(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
304
305def g_cfnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
306 L.and_left(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
307
308def g_cgz(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
309 L.and_left(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))
310
311def g_clv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
312 gp17(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g)
313
314# the invariant from its components
315def good_intro(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +h_cdep: {cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_ccap: {ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpv: {cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpp: {cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpn: {cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpg: {cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfr: {cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cseg: {cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_chead: {chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_ctail: {ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cnd: {cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_csl: {csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfree: {cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfll: {cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfl: {cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfnd: {cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cgz: {cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_clv: {clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:
316 L.and_intro(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cdep, L.and_intro(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_ccap, L.and_intro(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpv, L.and_intro(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpp, L.and_intro(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpn, L.and_intro(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpg, L.and_intro(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfr, L.and_intro(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cseg, L.and_intro(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_chead, L.and_intro(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_ctail, L.and_intro(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cnd, L.and_intro(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_csl, L.and_intro(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfree, L.and_intro(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfll, L.and_intro(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfl, L.and_intro(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfnd, L.and_intro(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cgz, h_clv)))))))))))))))))