proofs/containers/lru/state.bend source

proofs/containers/lru/state.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/math/u64.bend as Wimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/table.bend as TBimport ../hash_table/buckets.bend as Bimport ../hash_table/cyc.bend as CYimport ../hash_table/inv.bend as IVimport ../hash_table/state.bend as HTimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32# The LRU as a Data shadow: its U32 fields, the table exponent k (2^k# buckets), the arena exponent sd (2^sd slots), a mirror tree for each array,# and two ghost lists the implementation does not hold: sl, the live slots# from oldest to newest (the recency list), and fl, the free list in order.# real(sh) is the LRU<&2, V> the implementation holds.##   m    meta words: 0 fresh, 1 size, 2 depth, 3 lifetime on, 4-5 lifetime,#        6 mask, 7 bits, 16 + 2c / 17 + 2c counter c#   tab  the hash map's bucket table (proofs/hash_table/table.bend decodes it)#   lk   eight words per slot: prev, next, check word, timed, deadline lo, hitype Sh<-V: Data> is Data:  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>}def real(~V: Data, sh: Sh<V>) -> LR.LRU<&2, V>:  match sh:    case LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}:      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)}# ---- slots and their words ----# the link of slot s# the link of the first slot of t, q for none# the link of the last slot of t, p for none# word o of slot s in lkdef off(+s: Nat, +o: Nat) -> Nat:  Nat.add(Nat.double(Nat.double(Nat.double(s))), o)def lw(+ll: List<&2, U32>, +s: Nat, +o: Nat) -> U32:  W32.nth0(ll, off(s, o))# the segment sl: its first slot's prev is p, its last slot's next is q,# and consecutive slots are linked both waysdef seg(+ll: List<&2, U32>, sl: List<&2, Nat>, +p: U32, +q: U32) -> Bool:  match sl:    case Nil{}:      True{}    case Con{+s, +t}:      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)))# the free list: each slot's next is the slot after it (0 for the last)def fll(+ll: List<&2, U32>, fl: List<&2, Nat>) -> Bool:  match fl:    case Nil{}:      True{}    case Con{+s, +t}:      Bool.and(U32.is_eq(lw(ll, s, 1n), LK.fst_or(t, 0)), fll(ll, t))def live(~V: Data, +el: List<&2, Maybe<&2, V>>, +s: Nat) -> Bool:  HT.some_b(~V, HT.nthm(~V, el, s))# ---- predicates on slots, and their conjunction over a list ----type SP1<-V: Data> is Data:  PLive{fr: Nat, el: List<&2, Maybe<&2, V>>}  PVac{fr: Nat, el: List<&2, Maybe<&2, V>>}  PHas{bs: List<&2, B.Bk>, m: Nat, ll: List<&2, U32>}  PNk{ll: List<&2, U32>, kl: List<&2, String>, key: String}# ---- the table and the slots ----# b is a full bucket with word w and link ldef isbf(b: B.Bk, +w: U32, +l: U32) -> Bool:  match b:    case B.BE{}:      False{}    case B.BF{+w2, +l2, k}:      Bool.and(U32.is_eq(w2, w), U32.is_eq(l2, l))# some bucket below m is full with word w and link ldef anyb(+bs: List<&2, B.Bk>, +m: Nat, +l: U32, +w: U32) -> Bool:  match m:    case 0n:      False{}    case 1n+j:      Bool.or(isbf(B.at(bs, j), w, l), anyb(bs, j, l, w))# a full bucket's slot is on the recency list and stores the bucket's worddef bslb(+sl: List<&2, Nat>, +ll: List<&2, U32>, b: B.Bk) -> Bool:  match b:    case B.BE{}:      True{}    case B.BF{+w, +l, k}:      Bool.and(NL.memn(UD.v(H.slot(l)), sl), U32.is_eq(lw(ll, UD.v(H.slot(l)), 2n), w))def bsl(+bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +ll: List<&2, U32>, +m: Nat) -> Bool:  match m:    case 0n:      True{}    case 1n+j:      Bool.and(bslb(sl, ll, B.at(bs, j)), bsl(bs, sl, ll, j))# ---- the abstraction ----# the key of slot s: a one-character key is its check word, any other is# its stored Stringdef skey(+ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat) -> String:  TB.keyof(lw(ll, s, 2n), TB.nths(kl, s))def sent_m(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, m: Maybe<&2, V>) -> List<&2, SP.Ent<V>>:  match m:    case None{}:      Nil{}    case Some{v}:      Con{SP.LE{skey(ll, kl, s), v, lw(ll, s, 3n), W.U64{lw(ll, s, 4n), lw(ll, s, 5n)}}, Nil{}}# the entries of the slots of sl, in orderdef 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>>:  match sl:    case Nil{}:      Nil{}    case Con{+s, t}:      SC.append(SP.Ent<V>, sent_m(~V, ll, kl, s, HT.nthm(~V, el, s)), es(~V, ll, kl, el, t))def w64(+ml: List<&2, U32>, +i: Nat) -> W.U64:  W.U64{W32.nth0(ml, i), W32.nth0(ml, 1n+i)}def ctr(+ml: List<&2, U32>) -> SP.Ctr:  SP.CT{w64(ml, 16n), w64(ml, 18n), w64(ml, 20n), w64(ml, 22n), w64(ml, 24n)}def 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>:  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))}# the entries of a modeldef lru_es(~V: Data, l: SP.Lru<V>) -> List<&2, SP.Ent<V>>:  match l:    case SP.L{cap, on, life, es, c}:      es# the cache the shadow stands fordef model(~V: Data, sh: Sh<V>) -> SP.Lru<V>:  match sh:    case LS{+cap, n, head, tail, free, +mT, k, sd, tabT, +ksT, +eT, +lkT, +sl, fl}:      modelF(~V, cap, mT, AR.slots(String, ksT), eT, lkT, sl)def sev(~V: Data, p: SP1<V>, +s: Nat) -> Bool:  match p:    case PLive{+fr, +el}:      Bool.and(Nat.is_lt(s, fr), live(~V, el, s))    case PVac{+fr, +el}:      Bool.and(Nat.is_lt(s, fr), Bool.not(live(~V, el, s)))    case PHas{+bs, +m, +ll}:      anyb(bs, m, LK.lnk(s), lw(ll, s, 2n))    case PNk{+ll, +kl, +key}:      Bool.not(S.str_eq(skey(ll, kl, s), key))# p holds for every slot of xsdef sall(~V: Data, +p: SP1<V>, xs: List<&2, Nat>) -> Bool:  match xs:    case Nil{}:      True{}    case Con{+s, t}:      Bool.and(sev(~V, p, s), sall(~V, p, t))# every slot of xs is below fr and livedef slok(~V: Data, xs: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>) -> Bool:  sall(~V, PLive{fr, el}, xs)# every slot of xs is below fr and vacantdef flok(~V: Data, xs: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>) -> Bool:  sall(~V, PVac{fr, el}, xs)# every slot of sl has a bucket with its link and its stored check worddef hasall(~V: Data, +bs: List<&2, B.Bk>, +m: Nat, +ll: List<&2, U32>, sl: List<&2, Nat>) -> Bool:  sall(~V, PHas{bs, m, ll}, sl)# no slot of sl has keydef nokey(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, sl: List<&2, Nat>, +key: String) -> Bool:  sall(~V, PNk{ll, kl, key}, sl)# ---- the invariant (generated) ----# (tools/generators/lru_state.py)def 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:  Bool.and(Nat.is_lt(k, 30n), Nat.is_lt(0n, k))def 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:  Nat.is_lt(sd, k)def 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:  AR.perfect(U32, 1n+k, tabT)def 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:  pkdef 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:  AR.perfect(Maybe<&2, V>, sd, eT)def 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:  AR.perfect(U32, 3n+sd, lkT)def 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:  pmdef 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:  U32.is_eq(mmk, CY.msk(k))def 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:  Nat.is_eq(UD.v(mbt), k)def 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:  Nat.is_eq(UD.v(msz), SC.pow2(sd))def 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:  Nat.is_eq(UD.v(mdp), sd)def 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:  Nat.is_le(UD.v(fr), SC.pow2(sd))def 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:  B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k))def 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:  B.cluster(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k))def 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:  B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k))}, SC.pow2(k))def 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:  Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k)))def 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:  Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k))def 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:  Bool.not(U32.is_eq(cap, 0))def 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:  bsl(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k))def 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:  hasall(~V, TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), sl)def 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:  slok(~V, sl, UD.v(fr), AR.slots(Maybe<&2, V>, eT))def 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:  NL.nodupn(sl)def 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:  Nat.is_eq(SC.length(Nat, sl), UD.v(n))def 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:  U32.is_eq(head, LK.fst_or(sl, 0))def 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:  U32.is_eq(tail, LK.last_or(sl, 0))def 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:  seg(AR.slots(U32, lkT), sl, 0, 0)def 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:  S.nodup(SP.keys_of(~V, es(~V, AR.slots(U32, lkT), kl, AR.slots(Maybe<&2, V>, eT), sl)))def 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:  U32.is_eq(free, LK.fst_or(fl, 0))def 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:  fll(AR.slots(U32, lkT), fl)def 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:  flok(~V, fl, UD.v(fr), AR.slots(Maybe<&2, V>, eT))def 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:  NL.nodupn(fl)def 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:  Nat.is_eq(Nat.add(SC.length(Nat, sl), SC.length(Nat, fl)), UD.v(fr))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def 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:  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))def good(~V: Data, sh: Sh<V>) -> Bool:  match sh:    case LS{+cap, +n, +head, +tail, +free, +mT, +k, +sd, +tabT, +ksT, +eT, +lkT, +sl, +fl}:      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)def 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}:  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)def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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)def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  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))def 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}:  gp31(~V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl, g)# the invariant from its componentsdef 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}:  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)))))))))))))))))))))))))))))))