~/bend-docscommunity

proofs/containers/doubly_linked_list/state.bend source

proofs/containers/doubly_linked_list/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/doubly_linked_list.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/containers/doubly_linked_list.bend as Dimport ../../../src/containers/internal/dlist_storage.bend as Rimport ../../../src/containers/types/doubly_linked_list.bend as Eimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32# The doubly linked list's shadow: the public list's fields, one mirror tree# per array (values, prev links, next links, generations), the ids of the# list in order and the free stack (both ghost). The storage's count is the# order's length, and its depth and capacity are the public ones.# (generated by tools/generators/dll_state.py)type Sh<-T: Data> is Data:  LS{tag: U32, cap: U32, fresh: U32, free: U32, head: U32, tail: U32, depth: Nat, vT: AR.Tree<Maybe<&2, T>>, pT: AR.Tree<U32>, nT: AR.Tree<U32>, gT: AR.Tree<U32>, sl: List<&2, Nat>, fl: List<&2, Nat>}def real(~T: Data, sh: Sh<T>) -> D.DList<T>:  match sh:    case LS{+tag, +cap, +fresh, +free, +head, +tail, +depth, +vT, +pT, +nT, +gT, +sl, +fl}:      D.DL{tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, AR.thaw(U32, gT)}def model(~T: Data, sh: Sh<T>) -> S.DS<T>:  match sh:    case LS{+tag, +cap, +fresh, +free, +head, +tail, +depth, +vT, +pT, +nT, +gT, +sl, +fl}:      S.DS{tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}# ---- links (lnk, fst_or, last_or, nodupn: the LRU's, proofs/containers/lru/state.bend) ----# the segment sl: its first id's prev is p, its last id's next is q, and# consecutive ids are linked both waysdef seg(+pl: List<&2, U32>, +nl: 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(W32.nth0(pl, s), p), Bool.and(U32.is_eq(W32.nth0(nl, s), LK.fst_or(t, q)), seg(pl, nl, t, LK.lnk(s), q)))# the free stack: each id's next is the id after it (0 for the last)def fll(+nl: List<&2, U32>, fl: List<&2, Nat>) -> Bool:  match fl:    case Nil{}:      True{}    case Con{+s, +t}:      Bool.and(U32.is_eq(W32.nth0(nl, s), LK.fst_or(t, 0)), fll(nl, t))def some_b(-T: Data, m: Maybe<&2, T>) -> Bool:  match m:    case None{}:      False{}    case Some{v}:      True{}def live(-T: Data, +vl: List<&2, Maybe<&2, T>>, +x: Nat) -> Bool:  some_b(T, S.val_of(T, vl, x))# every id of xs is below fr and livedef slok(~T: Data, xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>) -> Bool:  match xs:    case Nil{}:      True{}    case Con{+x, t}:      Bool.and(Bool.and(Nat.is_lt(x, fr), live(T, vl, x)), slok(~T, t, fr, vl))# every id of xs is below fr and vacantdef flok(~T: Data, xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>) -> Bool:  match xs:    case Nil{}:      True{}    case Con{+x, t}:      Bool.and(Bool.and(Nat.is_lt(x, fr), Bool.not(live(T, vl, x))), flok(~T, t, fr, vl))# every generation from index fr on is 0 (the ids not issued yet)def gz(gl: List<&2, U32>, +fr: Nat) -> Bool:  match gl fr:    case Nil{} _:      True{}    case Con{+g, +t} 0n:      Bool.and(U32.is_eq(g, 0), gz(t, 0n))    case Con{+g, +t} 1n+p:      gz(t, p)# every live value slot (index k on) is an id of sldef lvin(~T: Data, vl: List<&2, Maybe<&2, T>>, +k: Nat, +sl: List<&2, Nat>) -> Bool:  match vl:    case Nil{}:      True{}    case Con{m, t}:      Bool.and(Bool.or(Bool.not(some_b(T, m)), NL.memn(k, sl)), lvin(~T, t, 1n+k, sl))# ---- the invariant ----def cdep(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Nat.is_lt(depth, 30n)def ccap(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Nat.is_eq(UD.v(cap), SC.pow2(depth))def cpv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  AR.perfect(Maybe<&2, T>, depth, vT)def cpp(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  AR.perfect(U32, depth, pT)def cpn(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  AR.perfect(U32, depth, nT)def cpg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  AR.perfect(U32, depth, gT)def cfr(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Nat.is_le(UD.v(fresh), UD.v(cap))def cseg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  seg(AR.slots(U32, pT), AR.slots(U32, nT), sl, 0, 0)def chead(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  U32.is_eq(head, LK.fst_or(sl, 0))def ctail(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  U32.is_eq(tail, LK.last_or(sl, 0))def cnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  NL.nodupn(sl)def csl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  slok(~T, sl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))def cfree(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  U32.is_eq(free, LK.fst_or(fl, 0))def cfll(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  fll(AR.slots(U32, nT), fl)def cfl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  flok(~T, fl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))def cfnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  NL.nodupn(fl)def cgz(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  gz(AR.slots(U32, gT), UD.v(fresh))def clv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl)def gr16(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr15(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr14(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr13(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr12(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr11(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr10(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr9(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr8(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr7(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr6(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr5(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr4(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr3(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr2(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def gr1(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def goodF(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>) -> Bool:  Bool.and(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl))def good(~T: Data, sh: Sh<T>) -> Bool:  match sh:    case LS{+tag, +cap, +fresh, +free, +head, +tail, +depth, +vT, +pT, +nT, +gT, +sl, +fl}:      goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl)def gp1(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), g)def gp2(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp3(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp4(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp5(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp6(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp7(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp8(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp9(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp10(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp11(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp12(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp13(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp14(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp15(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp16(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def gp17(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_right(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cdep(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), g)def g_ccap(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cpv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cpp(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cpn(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cpg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cfr(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cseg(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_chead(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_ctail(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_csl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cfree(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cfll(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cfl(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cfnd(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_cgz(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_left(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gp16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g))def g_clv(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +g: {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  gp17(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, g)# the invariant from its componentsdef good_intro(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +h_cdep: {cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_ccap: {ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpv: {cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpp: {cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpn: {cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpg: {cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfr: {cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cseg: {cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_chead: {chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_ctail: {ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cnd: {cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_csl: {csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfree: {cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfll: {cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfl: {cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfnd: {cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cgz: {cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_clv: {clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}:  L.and_intro(cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr1(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cdep, L.and_intro(ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr2(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_ccap, L.and_intro(cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr3(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpv, L.and_intro(cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr4(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpp, L.and_intro(cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr5(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpn, L.and_intro(cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr6(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cpg, L.and_intro(cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr7(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfr, L.and_intro(cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr8(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cseg, L.and_intro(chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr9(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_chead, L.and_intro(ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr10(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_ctail, L.and_intro(cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr11(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cnd, L.and_intro(csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr12(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_csl, L.and_intro(cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr13(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfree, L.and_intro(cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr14(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfll, L.and_intro(cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr15(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfl, L.and_intro(cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), gr16(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cfnd, L.and_intro(cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl), h_cgz, h_clv)))))))))))))))))