~/bend-docscommunity

proofs/containers/balanced_search_tree/state.bend source

proofs/containers/balanced_search_tree/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/balanced_search_tree/main.bend as Simport ../dynamic_array/layout.bend as LYimport ../dynamic_array/state.bend as DASimport ../../../src/containers/balanced_search_tree.bend as Mimport ../../../src/containers/dynamic_array.bend as Dimport ./nsr.bend as NRimport ./mk.bend as MKimport ../../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-)orderdef 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}:      xdef 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{}:      ydef 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 pdef 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 valuedef 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..lendef 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 orderdef 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 componentsdef 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))))))))))))))))