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 ./putm.bend as PM
import ./rmv.bend as RV
import ./mokx.bend as MX

# remove_if_equal: the found value compared with the expected one; equal,
# the node is removed as remove removes it, the answer true; otherwise, or
# absent, nothing changes. (source: tools/generators/tm_hand/rmi.src)


# equal or not: removed, or left
def rmi_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V, +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: {SP.fin(~K, ~cmp, k, ST.TN{1n+ui, a, b}, nl) == True{} : Bool}, +vi: V, +hmi: {ST.pv(V, pl, 1n+ui) == Some{vi} : Maybe<&2, V>}, +bq: Bool) -> OK.MOK(~K, ~V, ~cmp, Bool, S.pick(S.Model<K, V> & Bool, bq, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, True{}), (S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, False{})), MI.remove_if_apply(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui, e, bq)):
  match bq:
    case False{}:
      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (False{}, ({==}, ({==}, hg))))
    case True{}:
      %Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+ui), Some{vi}, hmi) : OK.MOK(~K, ~V, ~cmp, Bool, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, True{}), MI.changed_value(~K, ~V, ~cmp, (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)))), _)))
      MX.cv_mok(~K, ~V, ~cmp, 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)))), vi, L.subst(Maybe<&2, V>, z => 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))}, z), (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)))), z)), ST.pv(V, pl, 1n+ui), Some{vi}, hmi, RV.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), {==})))

# a node found: its value
def rmi_h(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V, +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: {SP.fin(~K, ~cmp, k, ST.TN{1n+ui, a, b}, nl) == 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>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+ui) == m : Maybe<&2, V>}, +hm: {ST.some2(V, m) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+ui, P.top(c), SP.dir(c)}))):
  match m:
    case None{}:
      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+ui, P.top(c), SP.dir(c)}))), L.false_true(hm))
    case Some{+vi}:
      %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vi}, Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+ui), Some{vi}, 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), hmi)) : OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, _), MI.remove_if_value(~K, ~V, ~cmp, ~eq, 1n+ui, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.pv(V, pl, 1n+ui))))
      %Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+ui), Some{vi}, hmi) : OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, Some{vi}), MI.remove_if_value(~K, ~V, ~cmp, ~eq, 1n+ui, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _)))
      rmi_b(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, c, ui, a, b, hbc, hplug, hr, hok, hfin, vi, hmi, eq(vi, e))

def rmi_tn(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (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:
      rmi_h(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, 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, ST.pv(V, pl, 1n+ui), {==}, PM.tn_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+ui, a, b, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, a, b}), P.after(c))), hwh, hk0)))

def rmi_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V, +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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (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{}:
      %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, Bool, S.remove_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, _), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, False{}))
      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (False{}, ({==}, ({==}, hg))))
    case ST.TN{+i, +a, +b}:
      rmi_tn(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, c, i, a, b, hfd, hwh, hplug, hr, hokc, hfin)

def rmi_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V, +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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (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}:
      rmi_t(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, c, t, hfd, hwh, hplug, hr, hokc, hb, ha, hfin)

def rmi_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V, +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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _)))
      rmi_c2(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, 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 rmi_sp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V, +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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (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}}:
      rmi_c(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, c, t, r)

def rmi_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +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, +e: V) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, e)):
  +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, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, _))
  rmi_sp(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, 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, {==}, {==}))