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/balanced_search_tree/main.bend as S
import ../dynamic_array/layout.bend as LY
import ../dynamic_array/state.bend as DAS
import ../../../src/containers/balanced_search_tree.bend as M
import ../../../src/containers/dynamic_array.bend as D
import ./nsr.bend as NR
import ./mk.bend as MK
import ../../lib/nat_list.bend as NL

# The indexed TreeMap's shadow: the header, the node and payload lists (the
# arrays are their canonical blocks, one limit and depth for both; the node
# store is one block per node field, nsr.bend), a ghost
# tree of node ids and the free stack (ghost). Colours, links and keys are
# read from the node list. (generated by tools/generators/tm_state.py)

type Tr is Data:
  TE{}
  TN{id: Nat, left: Tr, right: Tr}

type Sh<-K: Data, -V: Data> is Data:
  SH{n: Nat, root: Nat, lo: Nat, hi: Nat, free: Nat, l: Nat, d: Nat, nl: List<&2, M.Node<K>>, pl: List<&2, Maybe<&2, V>>, t: Tr, fl: List<&2, Nat>}

def nodes(~K: Data, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>) -> M.NodeStore<K>:
  NR.real(~K, l, d, nl)

def pays(~V: Data, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>) -> D.DynArray<&2, Maybe<&2, V>>:
  DAS.real(Maybe<&2, V>, DAS.Sh{l, d, SC.length(Maybe<&2, V>, pl), MK.mk(Maybe<&2, V>, d, pl)})

def real(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sh: Sh<K, V>) -> M.TreeMap<K, V, cmp>:
  match sh:
    case SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:
      M.TM{n, root, lo, hi, free, nodes(~K, l, d, nl), pays(~V, l, d, pl)}

# ---- the ghost tree ----

def rid(t: Tr) -> Nat:
  match t:
    case TE{}:
      0n
    case TN{+i, l, r}:
      i

# the ids in key (in-)order
def ids(t: Tr) -> List<&2, Nat>:
  match t:
    case TE{}:
      Nil{}
    case TN{+i, l, r}:
      SC.append(Nat, ids(l), Con{i, ids(r)})

def fst0(xs: List<&2, Nat>) -> Nat:
  match xs:
    case Nil{}:
      0n
    case Con{+x, t}:
      x

def last0(xs: List<&2, Nat>) -> Nat:
  match xs:
    case Nil{}:
      0n
    case Con{+x, t}:
      match t:
        case Nil{}:
          x
        case Con{+y, +u}:
          last0(Con{y, u})

# ---- nodes read by id ----

def pk(-T: Type, +b: Bool, x: T, y: T) -> T:
  match b:
    case True{}:
      x
    case False{}:
      y

def nth_or(-X: Data, xs: List<&2, X>, +i: Nat, +dflt: X) -> X:
  match xs i:
    case Nil{} _:
      dflt
    case Con{x, t} 0n:
      x
    case Con{x, t} 1n+p:
      nth_or(X, t, p, dflt)

# the node of id (a free sentinel for 0 or an id out of range)
def nd(-K: Data, xs: List<&2, M.Node<K>>, +id: Nat) -> M.Node<K>:
  match id:
    case 0n:
      M.Free{0n}
    case 1n+i:
      nth_or(M.Node<K>, xs, i, M.Free{0n})

def pv(-V: Data, xs: List<&2, Maybe<&2, V>>, +id: Nat) -> Maybe<&2, V>:
  match id:
    case 0n:
      None{}
    case 1n+i:
      nth_or(Maybe<&2, V>, xs, i, None{})

def is_node(-K: Data, x: M.Node<K>, +a: Nat, +b: Nat, +p: Nat) -> Bool:
  match x:
    case M.Free{f}:
      False{}
    case M.N{c, +x1, +x2, +x3, k}:
      Bool.and(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(x3, p)))

def is_free(-K: Data, x: M.Node<K>, +q: Nat) -> Bool:
  match x:
    case M.Free{+f}:
      Nat.is_eq(f, q)
    case M.N{c, x1, x2, x3, k}:
      False{}

def is_red(-K: Data, x: M.Node<K>) -> Bool:
  match x:
    case M.Free{f}:
      False{}
    case M.N{+c, x1, x2, x3, k}:
      c

# every node of t links to its children's ids and to its parent p
def rep(~K: Data, t: Tr, +p: Nat, +xs: List<&2, M.Node<K>>) -> Bool:
  match t:
    case TE{}:
      True{}
    case TN{+i, +l, +r}:
      Bool.and(Nat.is_lt(0n, i), Bool.and(is_node(K, nd(K, xs, i), rid(l), rid(r), p), Bool.and(rep(~K, l, i, xs), rep(~K, r, i, xs))))

def some2(-V: Data, m: Maybe<&2, V>) -> Bool:
  match m:
    case None{}:
      False{}
    case Some{v}:
      True{}

# every node of t has a value
def pay(~V: Data, t: Tr, +ys: List<&2, Maybe<&2, V>>) -> Bool:
  match t:
    case TE{}:
      True{}
    case TN{+i, l, r}:
      Bool.and(some2(V, pv(V, ys, i)), Bool.and(pay(~V, l, ys), pay(~V, r, ys)))

# the free stack: each id is a free node pointing to the next (0 last)
def fll(~K: Data, +xs: List<&2, M.Node<K>>, fl: List<&2, Nat>) -> Bool:
  match fl:
    case Nil{}:
      True{}
    case Con{+f, +t}:
      Bool.and(is_free(K, nd(K, xs, f), fst0(t)), fll(~K, xs, t))

# every id in 1..len
def allin(xs: List<&2, Nat>, +len: Nat) -> Bool:
  match xs:
    case Nil{}:
      True{}
    case Con{+x, t}:
      Bool.and(Bool.and(Nat.is_lt(0n, x), Nat.is_le(x, len)), allin(t, len))

# ---- entries ----

def ent(-K: Data, -V: Data, x: M.Node<K>, m: Maybe<&2, V>) -> Maybe<&2, M.Entry<K, V>>:
  match x m:
    case M.N{c, a, b, p, k} Some{v}:
      Some{M.Entry{k, v}}
    case _ _:
      None{}

def cons_m(-X: Data, m: Maybe<&2, X>, xs: List<&2, X>) -> List<&2, X>:
  match m:
    case None{}:
      xs
    case Some{x}:
      Con{x, xs}

# the entries of the ids, in order
def ents(~K: Data, ~V: Data, ix: List<&2, Nat>, +xs: List<&2, M.Node<K>>, +ys: List<&2, Maybe<&2, V>>) -> List<&2, M.Entry<K, V>>:
  match ix:
    case Nil{}:
      Nil{}
    case Con{+i, t}:
      cons_m(M.Entry<K, V>, ent(K, V, nd(K, xs, i), pv(V, ys, i)), ents(~K, ~V, t, xs, ys))

# consecutive keys strictly increasing (the model invariant, stated in the spec)
def ordered(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, es: List<&2, M.Entry<K, V>>) -> Bool:
  S.ordered(~K, ~V, ~cmp, es)

def root_black(~K: Data, t: Tr, +xs: List<&2, M.Node<K>>) -> Bool:
  match t:
    case TE{}:
      True{}
    case TN{+i, l, r}:
      Bool.not(is_red(K, nd(K, xs, i)))

def model(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sh: Sh<K, V>) -> S.Model<K, V>:
  match sh:
    case SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:
      S.TM{l, ents(~K, ~V, ids(t), nl, pl)}

# ---- the invariant ----

def cl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_le(l, 31n)

def cd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_le(d, l)

def ccap(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d))

def cpl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl))

def crep(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  rep(~K, t, 0n, nl)

def cpay(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  pay(~V, t, pl)

def cfll(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  fll(~K, nl, fl)

def cnd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  NL.nodupn(SC.append(Nat, ids(t), fl))

def cin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  allin(SC.append(Nat, ids(t), fl), SC.length(M.Node<K>, nl))

def clen(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_eq(SC.length(Nat, SC.append(Nat, ids(t), fl)), SC.length(M.Node<K>, nl))

def cord(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  ordered(~K, ~V, ~cmp, ents(~K, ~V, ids(t), nl, pl))

def cblk(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  root_black(~K, t, nl)

def csz(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_eq(n, SC.length(Nat, ids(t)))

def croot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_eq(root, rid(t))

def clo(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_eq(lo, fst0(ids(t)))

def chi(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_eq(hi, last0(ids(t)))

def cfree(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Nat.is_eq(free, fst0(fl))

def gr15(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr14(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr13(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr12(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr11(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr10(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr9(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr8(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr7(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr6(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr5(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def gr1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def goodF(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>) -> Bool:
  Bool.and(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl))

def good(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sh: Sh<K, V>) -> Bool:
  match sh:
    case SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:
      goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl)

def gp1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), g)

def gp2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp5(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp6(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp7(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp8(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp9(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp10(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp11(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp12(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp13(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp14(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp15(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def gp16(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_right(chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), g)

def g_cd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_ccap(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cpl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_crep(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cpay(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cfll(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cnd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_clen(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cord(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cblk(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_csz(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_croot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_clo(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_chi(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_left(chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gp15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g))

def g_cfree(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +g: {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  gp16(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, g)

# the invariant from its components
def good_intro(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: Tr, +fl: List<&2, Nat>, +h_cl: {cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cd: {cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_ccap: {ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cpl: {cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_crep: {crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cpay: {cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cfll: {cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cnd: {cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cin: {cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_clen: {clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cord: {cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cblk: {cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_csz: {csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_croot: {croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_clo: {clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_chi: {chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}, +h_cfree: {cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}) -> {goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}:
  L.and_intro(cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr1(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cl, L.and_intro(cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cd, L.and_intro(ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_ccap, L.and_intro(cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr4(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cpl, L.and_intro(crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr5(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_crep, L.and_intro(cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr6(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cpay, L.and_intro(cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr7(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cfll, L.and_intro(cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr8(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cnd, L.and_intro(cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr9(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cin, L.and_intro(clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr10(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_clen, L.and_intro(cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr11(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cord, L.and_intro(cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr12(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_cblk, L.and_intro(csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr13(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_csz, L.and_intro(croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr14(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_croot, L.and_intro(clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), gr15(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_clo, L.and_intro(chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl), h_chi, h_cfree))))))))))))))))