import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
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 ./tree.bend as TR
import ./path.bend as P
import ./plug.bend as PG
import ./prim.bend as PR
import ./mirror.bend as MI
import ./ok.bend as OK
import ./find.bend as FI
import ./ends.bend as EN
import ./ord.bend as OR
import ./slot.bend as SL
import ./alls.bend as AL
import ./dj.bend as DJ
import ./agree.bend as AG
import ./dord.bend as DO
import ./idmv.bend as ID
import ./rmf.bend as RF
import ./rms.bend as RS
import ./frame.bend as FRM
import ../../lib/nat_list.bend as NL

# Removing a found key: the specification's del removes exactly the node's
# entry, and each shape of the node (no left child, no right child, two
# children) gives the unlink and the end of the removal their facts.
# (source: tools/generators/tm_hand/rmd.src)


# the node's entry leaves the entries
def del_hit(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +i: Nat, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +hW: {ST.ids(tg) == SC.append(Nat, xs, Con{i, ys}) : List<&2, Nat>}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, i))) == True{} : Bool}, +a0: Nat, +b0: Nat, +q0: Nat, +x: M.Node<K>, +m: Maybe<&2, V>, +hxi: {ST.nd(K, nl, i) == x : M.Node<K>}, +hmi: {ST.pv(V, pl, i) == m : Maybe<&2, V>}, +hx: {ST.is_node(K, x, a0, b0, q0) == True{} : Bool}, +hm: {ST.some2(V, m) == True{} : Bool}) -> {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl) : List<&2, M.Entry<K, V>>} & {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}:
  match x m:
    case M.Free{f} +m:
      Empty.absurd({S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl) : List<&2, M.Entry<K, V>>} & {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, L.false_true(hx))
    case M.N{c0, x1, x2, x3, key} None{}:
      Empty.absurd({S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl) : List<&2, M.Entry<K, V>>} & {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, L.false_true(hm))
    case M.N{+c0, +x1, +x2, +x3, +key} Some{+vi}:
      +e0 = L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry<K, V>>}, ST.ids(tg), SC.append(Nat, xs, Con{i, ys}), hW, {==})
      +e1 = FI.ents_app(~K, ~V, xs, Con{i, ys}, nl, pl)
      +eent = L.subst(Maybe<&2, V>, z => {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == ST.ent(K, V, M.N{c0, x1, x2, x3, key}, z) : Maybe<&2, M.Entry<K, V>>}, ST.pv(V, pl, i), Some{vi}, hmi, L.subst(M.Node<K>, z => {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == ST.ent(K, V, z, ST.pv(V, pl, i)) : Maybe<&2, M.Entry<K, V>>}, ST.nd(K, nl, i), M.N{c0, x1, x2, x3, key}, hxi, {==}))
      +e2 = L.subst(Maybe<&2, M.Entry<K, V>>, z => {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ys, nl, pl))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.cons_m(M.Entry<K, V>, z, ST.ents(~K, ~V, ys, nl, pl))) : List<&2, M.Entry<K, V>>}, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), Some{M.Entry{key, vi}}, eent, {==})
      +hE = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, xs, Con{i, ys}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl)}), e0, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, xs, Con{i, ys}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ys, nl, pl))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl)}), e1, e2))
      +hord = 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>, ST.ents(~K, ~V, xs, nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl)}), hE, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
      +hc = AG.iseq_eq(cmp(k, key), L.subst(M.Node<K>, z => {S.is_eq(TR.kc(~K, ~cmp, k, z)) == True{} : Bool}, ST.nd(K, nl, i), M.N{c0, x1, x2, x3, key}, hxi, hfin))
      +hlx = L.subst(K, z => {OR.ltall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, xs, nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, O.antisym(~K, ~cmp, o, k, key, hc)), OR.ord_mid_l(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, xs, nl, pl), M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl), hord))
      +eD = Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl)})), ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl), L.subst(List<&2, M.Entry<K, V>>, z => {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.del(~K, ~V, ~cmp, k, z) : List<&2, M.Entry<K, V>>}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl)}), hE, {==}), Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl)})), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.ents(~K, ~V, ys, nl, pl)), ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl), DO.del_mid(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, xs, nl, pl), M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl), hlx, hc), Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.ents(~K, ~V, ys, nl, pl)), FI.ents_app(~K, ~V, xs, ys, nl, pl))))
      (eD, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.ents(~K, ~V, ys, nl, pl)), S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.sym(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.ents(~K, ~V, ys, nl, pl)), Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl), ST.ents(~K, ~V, ys, nl, pl)), eD, FI.ents_app(~K, ~V, xs, ys, nl, pl))), DO.ord_drop(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, xs, nl, pl), M.Entry{key, vi}, ST.ents(~K, ~V, ys, nl, pl), hord)))

# ---- no left child: the node's right subtree takes its place ----


# the facts of the unlink: the root, the ids with the free chain, the
# remaining ids' payloads, the free chain, the node in range
def ua_root(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {root == ST.rid(PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch})) : Nat}:
  Equal.trans(Nat, root, ST.rid(tg), ST.rid(PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch})), N.eq_from_is_eq(root, ST.rid(tg), ST.g_croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), L.subst(ST.Tr, z => {ST.rid(tg) == ST.rid(z) : Nat}, tg, PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}), hplug, {==}))

def ua_nd(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), fl)) == True{} : Bool}:
  L.subst(List<&2, Nat>, z => {NL.nodupn(SC.append(Nat, z, fl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))

def ua_nm(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {NL.memn(1n+ui, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))) == False{} : Bool}:
  DJ.dj_l(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, fl}, ID.mv_a(fl, c, ui, ch, ua_nd(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), 1n+ui, DJ.mem_hd(1n+ui, fl))


def ua_hk(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool}:
  +hb = SL.oks_split_l(~K, ~V, P.before(c), Con{1n+ui, SC.append(Nat, ST.ids(ch), P.after(c))}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc, EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))))
  +hy = L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+ui), ST.pv(V, pl, 1n+ui))), EN.oks(~K, ~V, SC.append(Nat, ST.ids(ch), P.after(c)), nl, pl), SL.oks_split_r(~K, ~V, P.before(c), Con{1n+ui, SC.append(Nat, ST.ids(ch), P.after(c))}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc, EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))))
  Equal.trans(Bool, EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})), EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), True{}, SL.oks_pex(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl, 1n+ui, None{}, ua_nm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), EN.oks_app(~K, ~V, nl, pl, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), hb, hy))

def ua_hul(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}:
  +hm = L.subst(List<&2, Nat>, z => {NL.memn(1n+ui, z) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), ST.ids(tg), Equal.sym(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc), DJ.mem_r(1n+ui, P.before(c), Con{1n+ui, SC.append(Nat, ST.ids(ch), P.after(c))}, DJ.mem_hd(1n+ui, SC.append(Nat, ST.ids(ch), P.after(c)))))
  +hin = AL.allin_mem(ST.ids(tg), SC.length(M.Node<K>, nl), 1n+ui, AL.allin_l(ST.ids(tg), fl, SC.length(M.Node<K>, nl), ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), hm)
  N.succ_le_lt(ui, SC.length(M.Node<K>, nl), L.and_right(Nat.is_lt(0n, 1n+ui), Nat.is_le(1n+ui, SC.length(M.Node<K>, nl)), hin))

def ua_hm(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {ST.some2(V, ST.pv(V, pl, 1n+ui)) == True{} : Bool}:
  FI.pay_node(~V, 1n+ui, ST.TE{}, ch, pl, SL.pay_oks(~K, ~V, ST.TN{1n+ui, ST.TE{}, ch}, nl, pl, SL.oks_split_l(~K, ~V, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c), nl, pl, SL.oks_split_r(~K, ~V, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c)), nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc, EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))))))


def rm_a3(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +hd1: {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) : List<&2, M.Entry<K, V>>}, +hd2: {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui)), ST.pv(V, pl, 1n+ui))):
  +hnd = ID.mv_a(fl, c, ui, ch, ua_nd(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin))
  +hin = ID.ain_a(fl, c, ui, ch, SC.length(M.Node<K>, nl), L.subst(List<&2, Nat>, z => {ST.allin(SC.append(Nat, z, fl), SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc, ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
  +hln0 = L.subst(List<&2, Nat>, z => {Nat.is_eq(SC.length(Nat, SC.append(Nat, z, fl)), SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc, ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hln = L.subst(Nat, w => {Nat.is_eq(w, SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), fl)), SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, fl})), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, fl})), SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), fl)), ID.len_a(fl, c, ui, ch)), hln0)
  +en = Equal.trans(Nat, n, SC.length(Nat, ST.ids(tg)), 1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), Equal.trans(Nat, SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c)))), 1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(tg)) == SC.length(Nat, z) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))), hbc, {==}), ID.sz_a(fl, c, ui, ch)))
  +esub = Equal.trans(Nat, Nat.sub(n, 1n), Nat.sub(1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), L.subst(Nat, z => {Nat.sub(n, 1n) == Nat.sub(z, 1n) : Nat}, n, 1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), en, {==}), N.add_sub_cancel(1n, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))))
  +hsz = L.subst(Nat, z => {Nat.is_eq(z, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))) == True{} : Bool}, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), Nat.sub(n, 1n), Equal.sym(Nat, Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), esub), N.is_eq_refl(SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))))
  +hcpl = L.subst(Nat, z => {Nat.is_eq(z, SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.length(Maybe<&2, V>, pl), SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+ui, None{})), Equal.sym(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+ui, None{})), SC.length(Maybe<&2, V>, pl), SL.len_ex(V, pl, 1n+ui, None{})), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hdel = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SL.ents_pex(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl, 1n+ui, None{}, ua_nm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), Equal.sym(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), hd1))
  RF.rm_fin(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl, fl, c, ui, ch, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.pv(V, pl, 1n+ui), hdel, hd2, hnd, hin, hln, hsz, ST.g_cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), hcpl, r)

def rm_a2(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, dh: {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) : List<&2, M.Entry<K, V>>} & {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui)), ST.pv(V, pl, 1n+ui))):
  match dh:
    case Tuple{hd1, hd2}:
      rm_a3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin, hd1, hd2, r)

def rm_a(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ch}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui)), ST.pv(V, pl, 1n+ui))):
  rm_a2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin, del_hit(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, 1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), hbc, hfin, 0n, ST.rid(ch), P.top(c), ST.nd(K, nl, 1n+ui), ST.pv(V, pl, 1n+ui), {==}, {==}, TR.rep_node(~K, 1n+ui, ST.TE{}, ch, P.top(c), nl, hr), ua_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), r)

# ---- no right child: the node's left subtree takes its place ----


def ub_nd(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), fl)) == True{} : Bool}:
  L.subst(List<&2, Nat>, z => {NL.nodupn(SC.append(Nat, z, fl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), hbc, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))

def ub_nm(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {NL.memn(1n+ui, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))) == False{} : Bool}:
  DJ.dj_l(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, fl}, ID.mv_b(fl, c, ui, ch, ub_nd(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), 1n+ui, DJ.mem_hd(1n+ui, fl))

def ub_hk(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool}:
  +hq = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), Con{1n+ui, P.after(c)}), ID.wb_eq(fl, c, ui, ch), L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), hbc, EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))))
  +hb = SL.oks_split_l(~K, ~V, SC.append(Nat, P.before(c), ST.ids(ch)), Con{1n+ui, P.after(c)}, nl, pl, hq)
  +hy = L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+ui), ST.pv(V, pl, 1n+ui))), EN.oks(~K, ~V, P.after(c), nl, pl), SL.oks_split_r(~K, ~V, SC.append(Nat, P.before(c), ST.ids(ch)), Con{1n+ui, P.after(c)}, nl, pl, hq))
  +hI = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c)), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ID.i0_eq(fl, c, ui, ch), EN.oks_app(~K, ~V, nl, pl, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c), hb, hy))
  Equal.trans(Bool, EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})), EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), True{}, SL.oks_pex(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl, 1n+ui, None{}, ub_nm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), hI)

def ub_hul(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}:
  +hm0 = L.subst(List<&2, Nat>, z => {NL.memn(1n+ui, z) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), Con{1n+ui, P.after(c)}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), Con{1n+ui, P.after(c)}), ID.wb_eq(fl, c, ui, ch)), DJ.mem_r(1n+ui, SC.append(Nat, P.before(c), ST.ids(ch)), Con{1n+ui, P.after(c)}, DJ.mem_hd(1n+ui, P.after(c))))
  +hm = L.subst(List<&2, Nat>, z => {NL.memn(1n+ui, z) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), ST.ids(tg), Equal.sym(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), hbc), hm0)
  +hin = AL.allin_mem(ST.ids(tg), SC.length(M.Node<K>, nl), 1n+ui, AL.allin_l(ST.ids(tg), fl, SC.length(M.Node<K>, nl), ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), hm)
  N.succ_le_lt(ui, SC.length(M.Node<K>, nl), L.and_right(Nat.is_lt(0n, 1n+ui), Nat.is_le(1n+ui, SC.length(M.Node<K>, nl)), hin))

def ub_hm(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}) -> {ST.some2(V, ST.pv(V, pl, 1n+ui)) == True{} : Bool}:
  FI.pay_node(~V, 1n+ui, ch, ST.TE{}, pl, SL.pay_oks(~K, ~V, ST.TN{1n+ui, ch, ST.TE{}}, nl, pl, SL.oks_split_l(~K, ~V, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c), nl, pl, SL.oks_split_r(~K, ~V, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c)), nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), hbc, EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))))))


def rm_b3(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +hd1: {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c)), nl, pl) : List<&2, M.Entry<K, V>>}, +hd2: {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui)), ST.pv(V, pl, 1n+ui))):
  +hnd = ID.mv_b(fl, c, ui, ch, ub_nd(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin))
  +hin = ID.ain_b(fl, c, ui, ch, SC.length(M.Node<K>, nl), L.subst(List<&2, Nat>, z => {ST.allin(SC.append(Nat, z, fl), SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), hbc, ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
  +hln0 = L.subst(List<&2, Nat>, z => {Nat.is_eq(SC.length(Nat, SC.append(Nat, z, fl)), SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), hbc, ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hln = L.subst(Nat, w => {Nat.is_eq(w, SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), fl)), SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, fl})), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, fl})), SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), fl)), ID.len_b(fl, c, ui, ch)), hln0)
  +en = Equal.trans(Nat, n, SC.length(Nat, ST.ids(tg)), 1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), Equal.trans(Nat, SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c)))), 1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(tg)) == SC.length(Nat, z) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), hbc, {==}), ID.sz_b(fl, c, ui, ch)))
  +esub = Equal.trans(Nat, Nat.sub(n, 1n), Nat.sub(1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), L.subst(Nat, z => {Nat.sub(n, 1n) == Nat.sub(z, 1n) : Nat}, n, 1n+SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), en, {==}), N.add_sub_cancel(1n, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))))
  +hsz = L.subst(Nat, z => {Nat.is_eq(z, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))) == True{} : Bool}, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), Nat.sub(n, 1n), Equal.sym(Nat, Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), esub), N.is_eq_refl(SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))))
  +hcpl = L.subst(Nat, z => {Nat.is_eq(z, SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.length(Maybe<&2, V>, pl), SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+ui, None{})), Equal.sym(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+ui, None{})), SC.length(Maybe<&2, V>, pl), SL.len_ex(V, pl, 1n+ui, None{})), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hd1b = Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), hd1, L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c)), nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry<K, V>>}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c)), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ID.i0_eq(fl, c, ui, ch), {==}))
  +hdel = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SL.ents_pex(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl, 1n+ui, None{}, ub_nm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), Equal.sym(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), hd1b))
  RF.rm_fin(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl, fl, c, ui, ch, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.pv(V, pl, 1n+ui), hdel, hd2, hnd, hin, hln, hsz, ST.g_cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), hcpl, r)

def rm_b2(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, dh: {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c)), nl, pl) : List<&2, M.Entry<K, V>>} & {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui)), ST.pv(V, pl, 1n+ui))):
  match dh:
    case Tuple{hd1, hd2}:
      rm_b3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin, hd1, hd2, r)

def rm_b(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, PR.ex_pl(V, pl, 1n+ui, None{})) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, PR.ex_pl(V, pl, 1n+ui, None{})) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+ui)), ST.pv(V, pl, 1n+ui))):
  rm_b2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin, del_hit(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, 1n+ui, SC.append(Nat, P.before(c), ST.ids(ch)), P.after(c), Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ch, ST.TE{}}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ch)), Con{1n+ui, P.after(c)}), hbc, ID.wb_eq(fl, c, ui, ch)), hfin, ST.rid(ch), 0n, P.top(c), ST.nd(K, nl, 1n+ui), ST.pv(V, pl, 1n+ui), {==}, {==}, TR.rep_node(~K, 1n+ui, ch, ST.TE{}, P.top(c), nl, hr), ub_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ch, hbc, hplug, hr, hok, hfin)), r)

# ---- two children: the successor's key and payload move in, it leaves ----


def us_hm(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{1n+ui, ta, tb}, P.top(c), nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}) -> {ST.some2(V, ST.pv(V, pl, 1n+ui)) == True{} : Bool}:
  FI.pay_node(~V, 1n+ui, ta, tb, pl, SL.pay_oks(~K, ~V, ST.TN{1n+ui, ta, tb}, nl, pl, SL.oks_split_l(~K, ~V, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c), nl, pl, SL.oks_split_r(~K, ~V, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)), nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), hbc, EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))))))

def us_hb(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{1n+ui, ta, tb}, P.top(c), nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}) -> {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}:
  +hm = L.subst(List<&2, Nat>, z => {NL.memn(1n+ui, z) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), ST.ids(tg), Equal.sym(List<&2, Nat>, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), RS.eo_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb)), DJ.mem_r(1n+ui, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}, DJ.mem_hd(1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))})))
  +hin = AL.allin_mem(ST.ids(tg), SC.length(M.Node<K>, nl), 1n+ui, AL.allin_l(ST.ids(tg), fl, SC.length(M.Node<K>, nl), ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), hm)
  N.succ_le_lt(ui, SC.length(M.Node<K>, nl), L.and_right(Nat.is_lt(0n, 1n+ui), Nat.is_le(1n+ui, SC.length(M.Node<K>, nl)), hin))

# the payload list's length through the exchanges
def us_lp(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{1n+ui, ta, tb}, P.top(c), nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}) -> {SC.length(M.Node<K>, nl) == SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})) : Nat}:
  Equal.sym(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), SC.length(M.Node<K>, nl), Equal.trans(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+ui, None{})), SC.length(M.Node<K>, nl), SL.len_ex(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), Equal.trans(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+ui, None{})), SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), SL.len_ex(V, pl, 1n+ui, None{}), N.eq_from_is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))))

def rm_s3(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{1n+ui, ta, tb}, P.top(c), nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, +hd1: {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}), nl, pl) : List<&2, M.Entry<K, V>>}, +hd2: {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl}, 1n+si) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+si, l, d, fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+si, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl}, 1n+si)), ST.pv(V, pl, 1n+ui))):
  +hnd = RS.nd_old(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb)
  +hb = us_hb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hsn)
  +hbp = L.subst(Nat, z => {Nat.is_lt(ui, z) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), us_lp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hsn), hb)
  +hus = RS.us_s(c, ui, ta, cs, si, sb, hnd)
  +enew = RS.ents_new(~K, ~V, nl, pl, ui, si, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, hus, SC.append(Nat, P.before(c), ST.ids(ta)), SC.append(Nat, ST.ids(sb), P.after(cs)), RS.ux_s(c, ui, ta, cs, si, sb, hnd), RS.sx_s(c, ui, ta, cs, si, sb, hnd), RS.ur_s(c, ui, ta, cs, si, sb, hnd), RS.sr_s(c, ui, ta, cs, si, sb, hnd))
  +hdel = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == ST.ents(~K, ~V, z, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) : List<&2, M.Entry<K, V>>}, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}), RS.en_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb), {==}), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}), nl, pl), S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), enew, Equal.sym(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}), nl, pl), hd1)))
  +ews = RS.ew_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb)
  +hnd0 = L.subst(List<&2, Nat>, z => {NL.nodupn(SC.append(Nat, z, fl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), ews, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +elw = FRM.len_wr(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})
  +hin = ID.ain_a(fl, cs, si, sb, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), L.subst(Nat, w => {ST.allin(SC.append(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), fl), w) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), SC.length(M.Node<K>, nl), elw), L.subst(List<&2, Nat>, z => {ST.allin(SC.append(Nat, z, fl), SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), ews, ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))))
  +hln0 = L.subst(List<&2, Nat>, z => {Nat.is_eq(SC.length(Nat, SC.append(Nat, z, fl)), SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), ews, ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hln1 = L.subst(Nat, w => {Nat.is_eq(w, SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), fl)), SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), Con{1n+si, fl})), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), Con{1n+si, fl})), SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), fl)), ID.len_a(fl, cs, si, sb)), hln0)
  +hln = L.subst(Nat, w => {Nat.is_eq(SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), Con{1n+si, fl})), w) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), SC.length(M.Node<K>, nl), elw), hln1)
  +en = Equal.trans(Nat, n, SC.length(Nat, ST.ids(tg)), 1n+SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs)))), N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), Equal.trans(Nat, SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs)))), 1n+SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs)))), L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(tg)) == SC.length(Nat, z) : Nat}, ST.ids(tg), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), ews, {==}), ID.sz_a(fl, cs, si, sb)))
  +esub = Equal.trans(Nat, Nat.sub(n, 1n), Nat.sub(1n+SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs)))), 1n), SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs)))), L.subst(Nat, z => {Nat.sub(n, 1n) == Nat.sub(z, 1n) : Nat}, n, 1n+SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs)))), en, {==}), N.add_sub_cancel(1n, SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))))))
  +hsz = L.subst(Nat, z => {Nat.is_eq(z, SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))))) == True{} : Bool}, SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs)))), Nat.sub(n, 1n), Equal.sym(Nat, Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs)))), esub), N.is_eq_refl(SC.length(Nat, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))))))
  +hcap = L.subst(Nat, w => {Nat.is_le(w, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), SC.length(M.Node<K>, nl), elw), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +elp = Equal.trans(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), SC.length(M.Node<K>, nl), SL.len_ex(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), Equal.sym(Nat, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), us_lp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hsn)))
  +hcpl = L.subst(Nat, w => {Nat.is_eq(SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), w) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})), SC.length(M.Node<K>, nl), elw), L.subst(Nat, w => {Nat.is_eq(w, SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), Equal.sym(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), SC.length(M.Node<K>, nl), elp), N.is_eq_refl(SC.length(M.Node<K>, nl))))
  RF.rm_fin(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl, fl, cs, si, sb, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.pv(V, pl, 1n+ui), hdel, hd2, ID.mv_a(fl, cs, si, sb, hnd0), hin, hln, hsz, ST.g_cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), hcap, hcpl, r)

def rm_s2(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{1n+ui, ta, tb}, P.top(c), nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, dh: {S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}), nl, pl) : List<&2, M.Entry<K, V>>} & {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl}, 1n+si) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+si, l, d, fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+si, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl}, 1n+si)), ST.pv(V, pl, 1n+ui))):
  match dh:
    case Tuple{hd1, hd2}:
      rm_s3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hsn, hd1, hd2, r)

def rm_s(~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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{1n+ui, ta, tb}, P.top(c), nl) == True{} : Bool}, +hfin: {S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, 1n+ui))) == True{} : Bool}, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl}, 1n+si) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+si, l, d, fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == ST.ents(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), fn_, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+si, fl}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks})) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+ui)), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), tg, fl}, 1n+si)), ST.pv(V, pl, 1n+ui))):
  rm_s2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hsn, del_hit(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, 1n+ui, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}, RS.eo_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb), hfin, ST.rid(ta), ST.rid(tb), P.top(c), ST.nd(K, nl, 1n+ui), ST.pv(V, pl, 1n+ui), {==}, {==}, TR.rep_node(~K, 1n+ui, ta, tb, P.top(c), nl, hr), us_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hsn)), r)