import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/order.bend as O
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI
import ./ord.bend as OR
import ./reads.bend as RD
import ./cur.bend as CU
import ./cnx.bend as CX
import ./vsp.bend as VS
import ./vit.bend as VI

# A view's size: the mirror counts the steps of the view's cursor, forward
# from the first entry above the lower bound (backward from the last below
# the upper), until an entry is out of range; the count is the number of
# entries within. (source: tools/generators/tm_hand/vsz.src)


# ---- a step whose specification is known ----

def cnext(-K: Data, -V: Data, c: S.Cursor<K, V>) -> Maybe<&2, K>:
  match c:
    case S.CR{m, nx, cu, lo, hi, fw}:
      nx

def stp3(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hs: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hc2: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool}) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
  +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0), hsp), hs)
  +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe, heq)
  +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe, heq)
  +hk2 = Equal.sym(Maybe<&2, K>, a, CU.ck(~K, nl, y2), L.subst(S.Cursor<K, V>, q => {a == cnext(K, V, q) : Maybe<&2, K>}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, ec, {==}))
  +hm2 = L.subst(Maybe<&2, M.Entry<K, V>>, q => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, q) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, oe, o0, Equal.sym(Maybe<&2, M.Entry<K, V>>, o0, oe, eo), hm)
  (y2, (z2, (hm2, (hk2, hc2))))

def stp2(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool}) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
  match r:
    case Tuple{hs, hc2}:
      stp3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, cu, a, bb, o0, hsp, y2, z2, oe, hm, hs, hc2)

def stp(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, st: CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
  match st:
    case Tuple{+y2, Tuple{+z2, Tuple{+oe, Tuple{+hm, r}}}}:
      stp2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, cu, a, bb, o0, hsp, y2, z2, oe, hm, r)

# ---- the specification's step at an entry, either way ----


def find_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +es: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +hab: {es == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> {S.find_e(~K, ~V, ~cmp, k, es) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
  L.subst(List<&2, M.Entry<K, V>>, z => {S.find_e(~K, ~V, ~cmp, k, z) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, xa, M.Entry{k, v}, t, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, hord), O.refl(~K, ~cmp, ~o, k)))

def sp_f(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +hab: {es == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +cc: Maybe<&2, K>, +lo2: M.Bound<K>, +hi2: M.Bound<K>) -> {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, es}, Some{k}, cc, lo2, hi2, True{}}) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}:
  +efw = L.subst(List<&2, M.Entry<K, V>>, z => {S.first_where(~K, ~V, ~cmp, k, False{}, z) == S.head(M.Entry<K, V>, t) : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), CX.fw_mid(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, hord)))
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{M.Entry{k, v}}, find_at(~K, ~V, ~cmp, ~o, es, xa, k, v, t, hab, hord)) : {S.next_at(~K, ~V, ~cmp, l, es, cc, lo2, hi2, True{}, _) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, False{}, es), S.head(M.Entry<K, V>, t), efw) : {S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, _), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
  {==}

def sp_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +hab: {es == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +cc: Maybe<&2, K>, +lo2: M.Bound<K>, +hi2: M.Bound<K>) -> {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, es}, Some{k}, cc, lo2, hi2, False{}}) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}:
  +elw = L.subst(List<&2, M.Entry<K, V>>, z => {S.last_where(~K, ~V, ~cmp, k, False{}, z, None{}) == S.last(M.Entry<K, V>, xa) : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), CX.lw_mid(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, hord)))
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{M.Entry{k, v}}, find_at(~K, ~V, ~cmp, ~o, es, xa, k, v, t, hab, hord)) : {S.next_at(~K, ~V, ~cmp, l, es, cc, lo2, hi2, False{}, _) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, False{}, es, None{}), S.last(M.Entry<K, V>, xa), elw) : {S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, _), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
  {==}

# ---- forward ----


def szn2(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}:
  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}
  {==}

def szn(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
      szn2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, y2, z2, hm)

def szt2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {CU.ck(~K, nl, y2) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{hk2, hc2}:
      %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}
      +e2 = VS.cong(List<&2, M.Entry<K, V>>, Nat, q => Nat.add(SC.length(M.Entry<K, V>, q), c), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Con{M.Entry{k, v}, S.within(~K, ~V, ~cmp, lo2, hi2, t)}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, t, hb))
      +e3 = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c), 1n+Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), N.add_succ(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), Equal.sym(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), 1n+Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), e2))
      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)), kont(y2, z2, hc2, hk2), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), e3))

def szt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
      szt2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, y2, z2, hm, r2, kont)

def szs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}
  +hbu = VS.bu_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal), hb)
  +ho = OR.ord_app_r(~K, ~V, ~cmp, xa, Con{M.Entry{k, v}, t}, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
  +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), S.within(~K, ~V, ~cmp, lo2, hi2, t), Nil{}, VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, t, hb), VS.wnil(~K, ~V, ~cmp, ~o, lo2, hi2, k, t, hbu, OR.ord_gt(~K, ~V, ~cmp, ~o, t, M.Entry{k, v}, ho)))
  Equal.sym(MI.MView<K, V> & Nat, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, c), VS.cong(List<&2, M.Entry<K, V>>, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, q), c)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Nil{}, hw))

def szs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
      szs2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, y2, z2, hm)

def szc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == True{} : Bool}, +hk: {CU.ck(~K, nl, nx) == Some{k} : Maybe<&2, K>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
  match b:
    case True{}:
      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), sp_f(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), xa, k, v, t, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_t(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), hb))
      szt(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, Some{M.Entry{k, v}}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, True{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, hk, {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)), kont)
    case False{}:
      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), sp_f(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), xa, k, v, t, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_f(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), hb))
      szs(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, True{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, hk, {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)))


# the count forward: the entries within from the cursor on
def szf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == True{} : Bool}, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, bs) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.head(M.Entry<K, V>, bs)) : Maybe<&2, K>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, bs) == True{} : Bool}, +c: Nat) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, bs), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, bs)), c)) : MI.MView<K, V> & Nat}:
  match bs:
    case Nil{}:
      szn(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, True{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, None{}, CU.ck(~K, nl, nx), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, nx), None{}, hk), {==}), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)))
    case Con{M.Entry{+k, +v}, +t}:
      szc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hc, hk, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, ky => kz => kc => kk => szf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, t, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), ky, kz, kc, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), SC.append(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), t), hab, Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), t), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), LL.append_assoc(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}, t))), kk, L.and_right(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal), 1n+c))

# ---- backward: the entries before the cursor, reversed ----


def sbn2(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}:
  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}
  {==}

def sbn(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
      sbn2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, y2, z2, hm)

# the entries within the reversal of e before t: those of t's, then e's
def wl_snoc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +t: List<&2, M.Entry<K, V>>, +k: K, +v: V) -> {S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})) == SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})) : List<&2, M.Entry<K, V>>}:
  Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}), LL.snoc_append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), VS.within_app(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}))

def sbt2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {CU.ck(~K, nl, y2) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{hk2, hc2}:
      %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}
      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}), wl_snoc(~K, ~V, ~cmp, lo2, hi2, t, k, v), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), q), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}}), Con{M.Entry{k, v}, Nil{}}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)))
      +el = Equal.trans(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}})), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}), ew), LL.length_append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}))
      +e3 = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), Nat.add(Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c), Equal.sym(Nat, Nat.add(Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), N.add_assoc(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n, c)), VS.cong(Nat, Nat, q => Nat.add(q, c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), el)))
      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c)), kont(y2, z2, hc2, hk2), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c), e3))

def sbt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
      sbt2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, y2, z2, hm, r2, kont)

def sbs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}
  +hal = VS.al_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu), hb)
  +ho = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hw1 = VS.wnil_lt(~K, ~V, ~cmp, ~o, lo2, hi2, k, SC.reverse(M.Entry<K, V>, t), hal, OR.ord_mid_l(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, ho))
  +hw2 = VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)
  +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), Nil{}, wl_snoc(~K, ~V, ~cmp, lo2, hi2, t, k, v), L.subst(List<&2, M.Entry<K, V>>, q => {SC.append(M.Entry<K, V>, q, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})) == Nil{} : List<&2, M.Entry<K, V>>}, Nil{}, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Nil{}, hw1), hw2))
  Equal.sym(MI.MView<K, V> & Nat, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, c), VS.cong(List<&2, M.Entry<K, V>>, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, q), c)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Nil{}, hw))

def sbs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
      sbs2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, y2, z2, hm)


def sbc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == True{} : Bool}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))) : Maybe<&2, K>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
  match b:
    case True{}:
      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), sp_b(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.reverse(M.Entry<K, V>, t), k, v, bs, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_t(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), hb))
      sbt(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, Some{M.Entry{k, v}}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, False{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, nx), S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Some{k}, hk, VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Some{M.Entry{k, v}}, LL.last_snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)), kont)
    case False{}:
      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), sp_b(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.reverse(M.Entry<K, V>, t), k, v, bs, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_f(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), hb))
      sbs(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, False{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, nx), S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Some{k}, hk, VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Some{M.Entry{k, v}}, LL.last_snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)))


# the count backward: the entries within before the cursor
def szb(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +rr: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == True{} : Bool}, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr), bs) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr))) : Maybe<&2, K>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, rr) == True{} : Bool}, +c: Nat) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, rr), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, rr))), c)) : MI.MView<K, V> & Nat}:
  match rr:
    case Nil{}:
      sbn(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, False{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, None{}, CU.ck(~K, nl, nx), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, nx), None{}, hk), {==}), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)))
    case Con{M.Entry{+k, +v}, +t}:
      sbc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), hbu, c, hc, hk, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, ky => kz => kc => kk => szb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, t, Con{M.Entry{k, v}, bs}, ky, kz, kc, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), kk, L.and_right(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu), 1n+c))

# ---- the view's size ----


def vsf2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>})) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{hal, Tuple{hwa, hfb}}:
      %Equal.sym(ST.Sh<K, V> & Nat, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, True{}, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
      +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), LL.length_append(M.Entry<K, V>, xa, xb), N.add_comm(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)))
      %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+_, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
      +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), h2, Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), VS.start_fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.head(M.Entry<K, V>, xb), hfb)))
      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), VS.within_app(~K, ~V, ~cmp, lo2, hi2, xa, xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, q, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xa), Nil{}, hwa)))
      +ec = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), N.add_zero(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), ew)))
      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))), szf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, SC.length(M.Entry<K, V>, xa), xb, xa, j, 0n, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, True{}), hab, hk, hal, 0n), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), ec))

def vsf1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match sp:
    case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}:
      vsf2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)

def vsb2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>})) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{hbu, Tuple{hwb, hlb}}:
      %Equal.sym(ST.Sh<K, V> & Nat, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, False{}, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
      +err = LL.spec_rev_rev(M.Entry<K, V>, xa)
      +hab2 = L.subst(List<&2, M.Entry<K, V>>, q => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, q, xb) : List<&2, M.Entry<K, V>>}, xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err), hab)
      +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), LL.length_append(M.Entry<K, V>, xa, xb), VS.cong(Nat, Nat, q => Nat.add(q, SC.length(M.Entry<K, V>, xb)), SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(Nat, SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xa), LL.length_rev(M.Entry<K, V>, xa))))
      %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+_, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
      +hk0 = Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), VS.start_lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last(M.Entry<K, V>, xa), Equal.trans(Maybe<&2, M.Entry<K, V>>, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}), S.last(M.Entry<K, V>, xa), hlb, OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, xa)))))
      +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), h2, hk0), VS.cong(List<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, S.last(M.Entry<K, V>, q)), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err)))
      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), VS.within_app(~K, ~V, ~cmp, lo2, hi2, xa, xb), Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), Nil{}), S.within(~K, ~V, ~cmp, lo2, hi2, xa), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), q), S.within(~K, ~V, ~cmp, lo2, hi2, xb), Nil{}, hwb), LL.append_nil(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa))), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err)))))
      +ec = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), N.add_zero(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), ew)))
      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))), szb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, SC.length(M.Entry<K, V>, xb), SC.reverse(M.Entry<K, V>, xa), xb, j, 0n, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, False{}), hab2, hk, VS.allbu_rev(~K, ~V, ~cmp, hi2, xa, hbu), 0n), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), ec))

def vsb1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>}))>>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match sp:
    case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}:
      vsb2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)


def vrf2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{h2, h3}:
      vsf1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_fal(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))

def vrf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+j, Tuple{+h1, r2}}:
      vrf2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)

def vrb2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{h2, h3}:
      vsb1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_lbu(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))

def vrb(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match r:
    case Tuple{+j, Tuple{+h1, r2}}:
      vrb2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)

# the mirror's size of a view: the number of entries within
def view_size_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
  match d2:
    case True{}:
      vrb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, hi2, False{}))
    case False{}:
      vrf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, True{}))