1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/array.bend as AR
5	import ../../../spec/lib/common.bend as SC
6	import ../../../spec/containers/doubly_linked_list.bend as S
7	import ../../lib/u32div.bend as UD
8	import ../../../src/containers/doubly_linked_list.bend as D
9	import ../../../src/containers/internal/dlist_storage.bend as R
10	import ../../../src/containers/types/doubly_linked_list.bend as E
11	import ../../lib/nat_list.bend as NL
12	import ../../lib/links.bend as LK
13	import ../../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	
21	type 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	
24	def 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	
29	def 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
38	def 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)
46	def 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	
53	def some_b(-T: Data, m: Maybe<&2, T>) -> Bool:
54	  match m:
55	    case None{}:
56	      False{}
57	    case Some{v}:
58	      True{}
59	
60	def 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
64	def 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
72	def 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)
80	def 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
90	def 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	
99	def 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	
102	def 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	
105	def 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	
108	def 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	
111	def 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	
114	def 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	
117	def 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	
120	def 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	
123	def 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	
126	def 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	
129	def 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	
132	def 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	
135	def 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	
138	def 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	
141	def 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	
144	def 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	
147	def 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	
150	def 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	
153	def 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	
156	def 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	
159	def 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	
162	def 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	
165	def 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	
168	def 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	
171	def 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	
174	def 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	
177	def 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	
180	def 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	
183	def 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	
186	def 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	
189	def 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	
192	def 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	
195	def 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	
198	def 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	
201	def 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	
204	def 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	
209	def 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	
212	def 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	
215	def 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	
218	def 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	
221	def 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	
224	def 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	
227	def 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	
230	def 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	
233	def 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	
236	def 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	
239	def 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	
242	def 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	
245	def 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	
248	def 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	
251	def 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	
254	def 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	
257	def 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	
260	def 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	
263	def 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	
266	def 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	
269	def 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	
272	def 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	
275	def 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	
278	def 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	
281	def 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	
284	def 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	
287	def 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	
290	def 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	
293	def 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	
296	def 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	
299	def 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	
302	def 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	
305	def 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	
308	def 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	
311	def 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
315	def 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: {c
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