import Base
import ../../lib/logic.bend as L
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 ./ok.bend as OK
import ./reads.bend as RD
import ./find.bend as FI
import ./ends.bend as EN
import ./path.bend as P
import ./plug.bend as PG
import ./ord.bend as OR
import ./prim.bend as PR
import ./tree.bend as TR
import ./spath.bend as SP
import ../../lib/nat.bend as N
import ./alls.bend as AL
import ./dj.bend as DJ
import ./nbr.bend as NB
import ./xtr.bend as XT
import ./frame.bend as FRM
import ./succ.bend as SU
import ./unl.bend as UN
import ./rms.bend as RS
import ./rmd.bend as RMD
import ./putm.bend as PM
import ./dord.bend as DO
import ../../lib/nat_list.bend as NL

# remove over a good shadow: the search from the root ends at a path and a
# subtree; an empty subtree means the key is absent, a node is removed by its
# shape (no left child, no right child, or two children and its successor).
# The mirror refines the specification's remove. (source: tools/generators/tm_hand/rmv.src)


# ---- the shapes ----

# no left child
def rm_ua(~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}) -> 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))):
  RMD.rm_a(~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, UN.unl_a(~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, hr, RMD.ua_root(~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), RMD.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), hok, RMD.ua_hk(~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), ST.g_cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), RMD.ua_hul(~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)))

# a left child and no right one
def rm_ub(~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, +hj: {Nat.is_lt(0n, ST.rid(ch)) == True{} : Bool}, +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}) -> 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))):
  RMD.rm_b(~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, UN.unl_b(~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, hj, hr, L.subst(ST.Tr, z => {root == ST.rid(z) : Nat}, tg, PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}}), hplug, 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))), RMD.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), hok, RMD.ub_hk(~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), ST.g_cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), RMD.ub_hul(~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)))

# ---- two children: the successor ----


# the successor's node, its key and payload moved in, then its unlink
def rm_sr(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, 1n+ja, 1n+jb, x3, k0} : M.Node<K>}, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +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{}, ST.TN{1n+ja, aa, ab}}, c}), SC.append(Nat, ST.ids(ST.TN{1n+jb, ba, bb}), P.after(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}))) : List<&2, Nat>}, +hs0: {1n+si == ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})) : Nat}, +hlp: {PG.plug(cs, ST.TN{1n+si, ST.TE{}, sb}) == PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}) : ST.Tr}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}) : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+si, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+si, nl) == True{} : Bool}, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +ks: K, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}) -> 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+si))), ST.pv(V, pl, 1n+ui))):
  +hb = RMD.us_hb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, 1n+ja, 1n+jb, x3, ks, cs0, as0, bs0, qs0, hsn)
  %Equal.sym(ST.Sh<K, V> & Nat, MI.move_successor(~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, 1n+si), (ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, 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), SU.msucc_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl, nl, ui, c0, 1n+ja, 1n+jb, x3, k0, ks, hx, hb, 1n+si, cs0, as0, bs0, qs0, hsn)) : 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.unlink_target(~K, ~V, ~cmp, _), ST.pv(V, pl, 1n+ui)))
  +hn = RS.nd_old(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, cs, si, sb, hbc, hlw, hlb)
  +eo = RS.eo_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, cs, si, sb, hbc, hlw, hlb)
  +hold = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ST.TN{1n+ja, aa, ab})), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), eo, 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)))
  +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{})), RMD.us_lp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, 1n+ja, 1n+jb, x3, ks, cs0, as0, bs0, qs0, hsn), hb)
  +o1 = RS.oks_new(~K, ~V, ~cmp, ~o, nl, pl, ui, si, c0, 1n+ja, 1n+jb, x3, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, RS.us_s(c, ui, ST.TN{1n+ja, aa, ab}, cs, si, sb, hn), SC.append(Nat, P.before(c), ST.ids(ST.TN{1n+ja, aa, ab})), SC.append(Nat, ST.ids(sb), P.after(cs)), RS.ux_s(c, ui, ST.TN{1n+ja, aa, ab}, cs, si, sb, hn), RS.sx_s(c, ui, ST.TN{1n+ja, aa, ab}, cs, si, sb, hn), RS.ur_s(c, ui, ST.TN{1n+ja, aa, ab}, cs, si, sb, hn), RS.sr_s(c, ui, ST.TN{1n+ja, aa, ab}, cs, si, sb, hn), hold)
  +hk4 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, 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))) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ST.TN{1n+ja, aa, ab})), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), Equal.sym(List<&2, Nat>, 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(ST.TN{1n+ja, aa, ab})), 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, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, cs, si, sb, hbc, hlw, hlb)), o1)
  +mu = L.subst(List<&2, Nat>, z => {NL.memn(1n+ui, z) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ST.TN{1n+ja, aa, ab})), 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(ST.TN{1n+ja, aa, ab})), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), eo), DJ.mem_r(1n+ui, SC.append(Nat, P.before(c), ST.ids(ST.TN{1n+ja, aa, ab})), 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))})))
  +ms = L.subst(List<&2, Nat>, z => {NL.memn(1n+si, z) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ST.TN{1n+ja, aa, ab})), 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(ST.TN{1n+ja, aa, ab})), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), eo), DJ.mem_r(1n+si, SC.append(Nat, P.before(c), ST.ids(ST.TN{1n+ja, aa, ab})), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}, DJ.mem_tl(1n+si, 1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}, DJ.mem_hd(1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))))))
  +hfl4 = Equal.trans(Bool, ST.fll(~K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, ks}), fl), ST.fll(~K, nl, fl), True{}, FRM.fll_frame(~K, fl, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, ks}, DJ.dj_r(ST.ids(tg), fl, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), 1n+ui, mu)), ST.g_cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hin = AL.allin_mem(ST.ids(tg), SC.length(M.Node<K>, nl), 1n+si, 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)), ms)
  +hul4 = L.subst(Nat, z => {Nat.is_lt(si, z) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, ks})), Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, ks})), SC.length(M.Node<K>, nl), FRM.len_wr(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, ks})), N.succ_le_lt(si, SC.length(M.Node<K>, nl), L.and_right(Nat.is_lt(0n, 1n+si), Nat.is_le(1n+si, SC.length(M.Node<K>, nl)), hin)))
  +hroot = L.subst(ST.Tr, z => {root == ST.rid(z) : Nat}, PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}), PG.plug(cs, ST.TN{1n+si, ST.TE{}, sb}), Equal.sym(ST.Tr, PG.plug(cs, ST.TN{1n+si, ST.TE{}, sb}), PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}), hlp), L.subst(ST.Tr, z => {root == ST.rid(z) : Nat}, tg, PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), hplug, 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))))
  +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))), RS.ew_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, cs, si, sb, hbc, hlw, hlb), ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hr0 = Equal.trans(Bool, ST.rep(~K, ST.TN{1n+si, ST.TE{}, sb}, P.top(cs), PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, ks})), ST.rep(~K, ST.TN{1n+si, ST.TE{}, sb}, P.top(cs), nl), True{}, SU.rep_k(~K, nl, ui, c0, 1n+ja, 1n+jb, x3, k0, ks, hx, hb, ST.TN{1n+si, ST.TE{}, sb}, P.top(cs)), hlr)
  +hok4 = Equal.trans(Bool, P.ctxok(~K, cs, 1n+si, PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, ks})), P.ctxok(~K, cs, 1n+si, nl), True{}, SU.ctx_k(~K, nl, ui, c0, 1n+ja, 1n+jb, x3, k0, ks, hx, hb, cs, 1n+si), hlc)
  RMD.rm_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, cs, si, sb, hbc, hlw, hlb, hr, hfin, c0, 1n+ja, 1n+jb, x3, ks, cs0, as0, bs0, qs0, hsn, UN.unl_a(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, 1n+ui, M.N{c0, 1n+ja, 1n+jb, x3, 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, hr0, hroot, hnd0, hok4, hk4, hfl4, ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), hul4))

def rm_sq(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, 1n+ja, 1n+jb, x3, k0} : M.Node<K>}, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +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{}, ST.TN{1n+ja, aa, ab}}, c}), SC.append(Nat, ST.ids(ST.TN{1n+jb, ba, bb}), P.after(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}))) : List<&2, Nat>}, +hs0: {1n+si == ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})) : Nat}, +hlp: {PG.plug(cs, ST.TN{1n+si, ST.TE{}, sb}) == PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}) : ST.Tr}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}) : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+si, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+si, nl) == True{} : Bool}, +y: M.Node<K>, +hy: {ST.nd(K, nl, 1n+si) == y : M.Node<K>}) -> 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+si))), ST.pv(V, pl, 1n+ui))):
  match y:
    case M.Free{f}:
      Empty.absurd(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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+si))), ST.pv(V, pl, 1n+ui))), L.false_true(L.subst(M.Node<K>, z => {ST.is_node(K, z, 0n, ST.rid(sb), P.top(cs)) == True{} : Bool}, ST.nd(K, nl, 1n+si), M.Free{f}, hy, TR.rep_node(~K, 1n+si, ST.TE{}, sb, P.top(cs), nl, hlr))))
    case M.N{+cs0, +as0, +bs0, +qs0, +ks}:
      rm_sr(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx, cs, si, sb, hlw, hs0, hlp, hlb, hlr, hlc, cs0, as0, bs0, qs0, ks, hy)


def rm_so(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, 1n+ja, 1n+jb, x3, k0} : M.Node<K>}, +cs: List<&2, P.Fr>, +s: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}), SC.append(Nat, ST.ids(ST.TN{1n+jb, ba, bb}), P.after(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}))) : List<&2, Nat>}, +hs0: {s == ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})) : Nat}, +hlp: {PG.plug(cs, ST.TN{s, ST.TE{}, sb}) == PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}) : ST.Tr}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}) : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{s, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, s, nl) == True{} : Bool}) -> 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb}))))), ST.pv(V, pl, 1n+ui))):
  match s:
    case 0n:
      Empty.absurd(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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb}))))), ST.pv(V, pl, 1n+ui))), L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), 0n, ST.rid(sb), P.top(cs)), Bool.and(True{}, ST.rep(~K, sb, 0n, nl))), hlr)))
    case 1n+si:
      %Equal.sym(Nat, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})), 1n+si, Equal.sym(Nat, 1n+si, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})), hs0)) : 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, _))), ST.pv(V, pl, 1n+ui)))
      rm_sq(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx, cs, si, sb, hlw, hs0, hlp, hlb, hlr, hlc, ST.nd(K, nl, 1n+si), {==})


def rm_sn(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, 1n+ja, 1n+jb, x3, k0} : M.Node<K>}, +cs: List<&2, P.Fr>, +s: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}), SC.append(Nat, ST.ids(ST.TN{1n+jb, ba, bb}), P.after(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}))) : List<&2, Nat>}, +hs0: {s == ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})) : Nat}, +hlp: {PG.plug(cs, ST.TN{s, ST.TE{}, sb}) == PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}) : ST.Tr}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}) : List<&2, Nat>}, r2: {ST.rep(~K, ST.TN{s, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool} & {P.ctxok(~K, cs, s, nl) == True{} : Bool}) -> 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb}))))), ST.pv(V, pl, 1n+ui))):
  match r2:
    case Tuple{hlr, hlc}:
      rm_so(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx, cs, s, sb, hlw, hs0, hlp, hlb, hlr, hlc)

def rm_sm(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, 1n+ja, 1n+jb, x3, k0} : M.Node<K>}, +cs: List<&2, P.Fr>, +s: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}), SC.append(Nat, ST.ids(ST.TN{1n+jb, ba, bb}), P.after(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}))) : List<&2, Nat>}, +hs0: {s == ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})) : Nat}, rest: {PG.plug(cs, ST.TN{s, ST.TE{}, sb}) == PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}) : ST.Tr} & ({P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}) : List<&2, Nat>} & ({ST.rep(~K, ST.TN{s, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool} & {P.ctxok(~K, cs, s, nl) == True{} : Bool}))) -> 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb}))))), ST.pv(V, pl, 1n+ui))):
  match rest:
    case Tuple{hlp, Tuple{hlb, r2}}:
      rm_sn(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx, cs, s, sb, hlw, hs0, hlp, hlb, r2)


def rm_sl(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, 1n+ja, 1n+jb, x3, k0} : M.Node<K>}, lm: Sigma<&1, &1, List<&2, P.Fr>, lc_ => Sigma<&1, &1, Nat, ls_ => Sigma<&1, &1, ST.Tr, lb_ => {SC.append(Nat, P.before(lc_), SC.append(Nat, ST.ids(ST.TN{ls_, ST.TE{}, lb_}), P.after(lc_))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}), SC.append(Nat, ST.ids(ST.TN{1n+jb, ba, bb}), P.after(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}))) : List<&2, Nat>} & ({ls_ == ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})) : Nat} & ({PG.plug(lc_, ST.TN{ls_, ST.TE{}, lb_}) == PG.plug(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, ST.TN{1n+jb, ba, bb}) : ST.Tr} & ({P.before(lc_) == P.before(Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}) : List<&2, Nat>} & ({ST.rep(~K, ST.TN{ls_, ST.TE{}, lb_}, P.top(lc_), nl) == True{} : Bool} & {P.ctxok(~K, lc_, ls_, nl) == True{} : Bool}))))>>>) -> 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb}))))), ST.pv(V, pl, 1n+ui))):
  match lm:
    case Tuple{+cs, Tuple{+s, Tuple{+sb, Tuple{hlw, Tuple{hs0, rest}}}}}:
      rm_sm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx, cs, s, sb, hlw, hs0, rest)

# the walk to the successor, and the path down to it
def rm_two(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, 1n+ja, 1n+jb, x3, k0} : M.Node<K>}) -> 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, 1n+ja, 1n+jb, x3, k0}))), ST.pv(V, pl, 1n+ui))):
  +hrb = TR.rep_r(~K, 1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, P.top(c), nl, hr)
  +en = Equal.trans(Nat, n, 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.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), 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)), 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.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c))), hbc, {==}))
  +hle = N.le_trans(TR.ht(ST.TN{1n+jb, ba, bb}), SC.length(Nat, ST.ids(ST.TN{1n+jb, ba, bb})), n, TR.ht_le(ST.TN{1n+jb, ba, bb}), L.subst(Nat, z => {Nat.is_le(SC.length(Nat, ST.ids(ST.TN{1n+jb, ba, bb})), z) == True{} : Bool}, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c)))), n, Equal.sym(Nat, n, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}}), P.after(c)))), en), RS.sublen(c, ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb})))
  +eext = Equal.trans(ST.Sh<K, V> & Nat, MI.extreme(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+jb, False{}), (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, MI.ext_loop(~K, 1n+n, nl, False{}, 1n+jb, M.child(~K, ST.nd(K, nl, 1n+jb), False{}))), (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb}))), XT.extreme_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl, 1n+jb, False{}), L.subst(Nat, z => {(ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, MI.ext_loop(~K, 1n+n, nl, False{}, 1n+jb, M.child(~K, ST.nd(K, nl, 1n+jb), False{}))) == (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, z) : ST.Sh<K, V> & Nat}, MI.ext_loop(~K, 1n+n, nl, False{}, 1n+jb, M.child(~K, ST.nd(K, nl, 1n+jb), False{})), ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb})), NB.ext_l(~K, nl, 1n+n, 1n+jb, ba, bb, 1n+ui, hrb, N.le_lt_succ(TR.ht(ST.TN{1n+jb, ba, bb}), n, hle)), {==}))
  %Equal.sym(ST.Sh<K, V> & Nat, MI.extreme(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, 1n+jb, False{}), (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.fst0(ST.ids(ST.TN{1n+jb, ba, bb}))), eext) : 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.unlink_target(~K, ~V, ~cmp, MI.successor_ready(~K, ~V, ~cmp, 1n+ui, _)), ST.pv(V, pl, 1n+ui)))
  rm_sl(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx, SU.lmost(~K, ~cmp, ~o, ba, nl, Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, 1n+jb, bb, hrb, Pair.fst({P.ctxok(~K, Con{P.FR{1n+ui, False{}, ST.TN{1n+ja, aa, ab}}, c}, 1n+jb, nl) == True{} : Bool}, {ST.rep(~K, ST.TN{1n+jb, ba, bb}, 1n+ui, nl) == True{} : Bool}, P.ok_r(~K, nl, c, 1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{1n+jb, ba, bb}, hr, hok))))


def rm_tt(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{ja, aa, ab}, ST.TN{jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{ja, aa, ab}, ST.TN{jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{ja, aa, ab}, ST.TN{jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, ja, jb, x3, k0} : M.Node<K>}) -> 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, ja, jb, x3, k0}))), ST.pv(V, pl, 1n+ui))):
  match ja jb:
    case 0n +jb:
      Empty.absurd(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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, 0n, jb, x3, k0}))), ST.pv(V, pl, 1n+ui))), L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.rid(aa), ST.rid(ab), 1n+ui), Bool.and(ST.rep(~K, aa, 0n, nl), ST.rep(~K, ab, 0n, nl))), TR.rep_l(~K, 1n+ui, ST.TN{0n, aa, ab}, ST.TN{jb, ba, bb}, P.top(c), nl, hr))))
    case 1n+ja 0n:
      Empty.absurd(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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, 1n+ja, 0n, x3, k0}))), ST.pv(V, pl, 1n+ui))), L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.rid(ba), ST.rid(bb), 1n+ui), Bool.and(ST.rep(~K, ba, 0n, nl), ST.rep(~K, bb, 0n, nl))), TR.rep_r(~K, 1n+ui, ST.TN{1n+ja, aa, ab}, ST.TN{0n, ba, bb}, P.top(c), nl, hr))))
    case 1n+ja 1n+jb:
      rm_two(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx)

def rm_et(~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, +jb: Nat, +ba: ST.Tr, +bb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, ST.TN{jb, ba, bb}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TE{}, ST.TN{jb, ba, bb}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ST.TN{jb, ba, bb}}, 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}, +c0: Bool, +x3: Nat, +k0: K) -> 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, 0n, jb, x3, k0}))), ST.pv(V, pl, 1n+ui))):
  match jb:
    case 0n:
      Empty.absurd(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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, 0n, 0n, x3, k0}))), ST.pv(V, pl, 1n+ui))), L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.rid(ba), ST.rid(bb), 1n+ui), Bool.and(ST.rep(~K, ba, 0n, nl), ST.rep(~K, bb, 0n, nl))), TR.rep_r(~K, 1n+ui, ST.TE{}, ST.TN{0n, ba, bb}, P.top(c), nl, hr))))
    case 1n+j:
      rm_ua(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ST.TN{1n+j, ba, bb}, hbc, hplug, hr, hok, hfin)

def rm_te2(~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, +ja: Nat, +aa: ST.Tr, +ab: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TN{ja, aa, ab}, ST.TE{}}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, ST.TN{ja, aa, ab}, ST.TE{}}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, ST.TN{ja, aa, ab}, 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}, +c0: Bool, +x3: Nat, +k0: K) -> 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, ja, 0n, x3, k0}))), ST.pv(V, pl, 1n+ui))):
  match ja:
    case 0n:
      Empty.absurd(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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, 0n, 0n, x3, k0}))), ST.pv(V, pl, 1n+ui))), L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.rid(aa), ST.rid(ab), 1n+ui), Bool.and(ST.rep(~K, aa, 0n, nl), ST.rep(~K, ab, 0n, nl))), TR.rep_l(~K, 1n+ui, ST.TN{0n, aa, ab}, ST.TE{}, P.top(c), nl, hr))))
    case 1n+j:
      rm_ub(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ST.TN{1n+j, aa, ab}, {==}, hbc, hplug, hr, hok, hfin)

# the node's shape
def rm_ab(~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, +a: ST.Tr, +b: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, a, b}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, a, b}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, a, b}, 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}, +c0: Bool, +x3: Nat, +k0: K, +hx: {ST.nd(K, nl, 1n+ui) == M.N{c0, ST.rid(a), ST.rid(b), x3, k0} : M.Node<K>}) -> 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, ST.rid(a), ST.rid(b), x3, k0}))), ST.pv(V, pl, 1n+ui))):
  match a b:
    case ST.TE{} ST.TE{}:
      rm_ua(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ST.TE{}, hbc, hplug, hr, hok, hfin)
    case ST.TE{} ST.TN{+jb, +ba, +bb}:
      rm_et(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0)
    case ST.TN{+ja, +aa, +ab} ST.TE{}:
      rm_te2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, hbc, hplug, hr, hok, hfin, c0, x3, k0)
    case ST.TN{+ja, +aa, +ab} ST.TN{+jb, +ba, +bb}:
      rm_tt(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, ja, aa, ab, jb, ba, bb, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx)

# the node read: its links are the tree's
def rm_x(~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, +a: ST.Tr, +b: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, a, b}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, a, b}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, a, b}, 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}, +x: M.Node<K>, +hxi: {ST.nd(K, nl, 1n+ui) == x : M.Node<K>}) -> 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, x))), ST.pv(V, pl, 1n+ui))):
  match x:
    case M.Free{f}:
      Empty.absurd(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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.Free{f}))), ST.pv(V, pl, 1n+ui))), L.false_true(L.subst(M.Node<K>, z => {ST.is_node(K, z, ST.rid(a), ST.rid(b), P.top(c)) == True{} : Bool}, ST.nd(K, nl, 1n+ui), M.Free{f}, hxi, TR.rep_node(~K, 1n+ui, a, b, P.top(c), nl, hr))))
    case M.N{+c0, +x1, +x2, +x3, +k0}:
      +hn = L.subst(M.Node<K>, z => {ST.is_node(K, z, ST.rid(a), ST.rid(b), P.top(c)) == True{} : Bool}, ST.nd(K, nl, 1n+ui), M.N{c0, x1, x2, x3, k0}, hxi, TR.rep_node(~K, 1n+ui, a, b, P.top(c), nl, hr))
      +e1 = N.eq_from_is_eq(x1, ST.rid(a), L.and_left(Nat.is_eq(x1, ST.rid(a)), Bool.and(Nat.is_eq(x2, ST.rid(b)), Nat.is_eq(x3, P.top(c))), hn))
      +e2 = N.eq_from_is_eq(x2, ST.rid(b), L.and_left(Nat.is_eq(x2, ST.rid(b)), Nat.is_eq(x3, P.top(c)), L.and_right(Nat.is_eq(x1, ST.rid(a)), Bool.and(Nat.is_eq(x2, ST.rid(b)), Nat.is_eq(x3, P.top(c))), hn)))
      +hx = L.subst(Nat, z => {ST.nd(K, nl, 1n+ui) == M.N{c0, z, ST.rid(b), x3, k0} : M.Node<K>}, x1, ST.rid(a), e1, L.subst(Nat, z => {ST.nd(K, nl, 1n+ui) == M.N{c0, x1, z, x3, k0} : M.Node<K>}, x2, ST.rid(b), e2, hxi))
      %Equal.sym(Nat, x1, ST.rid(a), e1) : 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, _, x2, x3, k0}))), ST.pv(V, pl, 1n+ui)))
      %Equal.sym(Nat, x2, ST.rid(b), e2) : 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.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, ST.rid(a), _, x3, k0}))), ST.pv(V, pl, 1n+ui)))
      rm_ab(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, a, b, hbc, hplug, hr, hok, hfin, c0, x3, k0, hx)

# a node found: its payload is the lookup
def rm_u(~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, +a: ST.Tr, +b: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, a, b}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, a, b}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, a, b}, 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}, +hfd: {ST.pv(V, pl, 1n+ui) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+ui, P.top(c), SP.dir(c)}))):
  %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+ui), Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+ui), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd)) : 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))}, _), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, ST.nd(K, nl, 1n+ui)))), ST.pv(V, pl, 1n+ui)))
  rm_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, a, b, hbc, hplug, hr, hok, hfin, ST.nd(K, nl, 1n+ui), {==})

# ---- absent, or found ----

def rm_te(~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>, +hfd: {None{} == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))):
  %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}, Equal.sym(Maybe<&2, V>, None{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd)) : 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.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, None{}))
  %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, ST.ids(tg), nl, pl), DO.del_absent(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl), Equal.sym(Maybe<&2, V>, None{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd))) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, _}, None{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, None{}))
  (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (None{}, ({==}, ({==}, hg))))

def rm_tn(~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>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +hfd: {ST.pv(V, pl, i) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{i, a, b}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{i, a, b}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, i, nl) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, ST.TN{i, a, b}, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{i, P.top(c), SP.dir(c)}))):
  match i:
    case 0n:
      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))), PM.tn_zero(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, a, b, hr))
    case 1n+ui:
      rm_u(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, a, b, PM.tn_hbc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+ui, a, b, hwh), hplug, hr, hok, hfin, hfd)

def rm_t(~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, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, +ha: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))):
  match t:
    case ST.TE{}:
      rm_te(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, hfd)
    case ST.TN{+i, +a, +b}:
      rm_tn(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, i, a, b, hfd, hwh, hplug, hr, hokc, hfin)

def rm_c2(~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, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, r2: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))):
  match r2:
    case Tuple{ha, hfin}:
      rm_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, hk0, c, t, hfd, hwh, hplug, hr, hokc, hb, ha, hfin)

def rm_c(~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, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, r: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))):
  match r:
    case Tuple{hts, Tuple{hwh, Tuple{hplug, Tuple{hr, Tuple{hokc, Tuple{hb, r2}}}}}}:
      +hts2 = hts
      %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _)))
      rm_c2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, hk0, c, t, L.subst(M.Search, z => {ST.pv(V, pl, FI.sfound(z)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2, FI.tfind(~K, ~V, ~cmp, ~o, nl, pl, tg, 0n, False{}, k, 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), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), hwh, hplug, hr, hokc, hb, r2)

def rm_sp(~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, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, P.Fr>, c => Sigma<&1, &1, ST.Tr, t => {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))):
  match sp:
    case Tuple{+c, Tuple{+t, r}}:
      rm_c(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, hk0, c, t, r)

def rm_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.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k)):
  +ean = LL.append_nil(Nat, ST.ids(tg))
  +hk1 = 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))
  +hk0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), ean), hk1)
  +ho0 = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), ean), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  %Equal.sym(ST.Sh<K, V> & M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), RD.search_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove_found(~K, ~V, ~cmp, _))
  rm_sp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, hk0, SP.spath(~K, ~V, ~cmp, ~o, nl, pl, tg, Nil{}, k, 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), ho0, hk0, {==}, {==}))