import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/doubly_linked_list.bend as E
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../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 ways
def 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 live
def 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 vacant
def 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 sl
def 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 components
def good_intro(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +h_cdep: {cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_ccap: {ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpv: {cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpp: {cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpn: {cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cpg: {cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfr: {cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cseg: {cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_chead: {chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_ctail: {ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cnd: {cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_csl: {csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfree: {cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfll: {cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfl: {cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cfnd: {cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_cgz: {cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h_clv: {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)))))))))))))))))