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 ../../../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 ./agree.bend as AG
import ./setters.bend as SE
import ./rotm.bend as RM
import ./rotn.bend as RN
import ./rot.bend as RT
import ./rotp.bend as RP
import ./fix.bend as FX
import ./dj.bend as DJ
import ./spath.bend as SP
import ./idmv.bend as ID
import ./frame.bend as FRM
import ./mirror.bend as MI
import ./prim.bend as PR
import ./ends.bend as EN
import ./dfix.bend as DF
import ./nbr.bend as NB
import ../../lib/nat_list.bend as NL

# Unlinking a node with at most one child: its child's subtree takes its
# place under its parent (or becomes the root); the path then leads to the
# child, the ids lose the node, and the node joins the free chain.
# (source: tools/generators/tm_hand/unl.src)


# ---- reattaching: the child's subtree under the unlinked node's parent ----


# the child's links: its root now points up to q
def ratt_rep(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +q: Nat, +dr: Bool, +u: Nat, +ch: ST.Tr, +hr: {ST.rep(~K, ch, u, nl) == True{} : Bool}, +hq: {NL.memn(q, ST.ids(ch)) == False{} : Bool}, +hnd: {NL.nodupn(ST.ids(ch)) == True{} : Bool}) -> {ST.rep(~K, ch, q, SE.setp(K, RM.attn(K, nl, q, ST.rid(ch), dr), ST.rid(ch), q)) == True{} : Bool}:
  match ch:
    case ST.TE{}:
      {==}
    case ST.TN{+x, +cl, +cr}:
      +hqx = Pair.fst({Nat.is_eq(x, q) == False{} : Bool}, {NL.memn(q, ST.ids(cl)) == False{} : Bool} & {NL.memn(q, ST.ids(cr)) == False{} : Bool}, FRM.nm_node(q, x, cl, cr, hq))
      +hql = Pair.fst({NL.memn(q, ST.ids(cl)) == False{} : Bool}, {NL.memn(q, ST.ids(cr)) == False{} : Bool}, Pair.snd({Nat.is_eq(x, q) == False{} : Bool}, {NL.memn(q, ST.ids(cl)) == False{} : Bool} & {NL.memn(q, ST.ids(cr)) == False{} : Bool}, FRM.nm_node(q, x, cl, cr, hq)))
      +hqr = Pair.snd({NL.memn(q, ST.ids(cl)) == False{} : Bool}, {NL.memn(q, ST.ids(cr)) == False{} : Bool}, Pair.snd({Nat.is_eq(x, q) == False{} : Bool}, {NL.memn(q, ST.ids(cl)) == False{} : Bool} & {NL.memn(q, ST.ids(cr)) == False{} : Bool}, FRM.nm_node(q, x, cl, cr, hq)))
      +hxl = DJ.dj_l(ST.ids(cl), Con{x, ST.ids(cr)}, hnd, x, DJ.mem_hd(x, ST.ids(cr)))
      +hxr = DJ.nd_head(x, ST.ids(cr), DJ.ndr(ST.ids(cl), Con{x, ST.ids(cr)}, hnd))
      +e = Equal.trans(M.Node<K>, ST.nd(K, SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), x), SE.modp(K, ST.nd(K, RM.attn(K, nl, q, x, dr), x), q), SE.modp(K, ST.nd(K, nl, x), q), RN.hitp(K, RM.attn(K, nl, q, x, dr), x, q), L.subst(M.Node<K>, z => {SE.modp(K, ST.nd(K, RM.attn(K, nl, q, x, dr), x), q) == SE.modp(K, z, q) : M.Node<K>}, ST.nd(K, RM.attn(K, nl, q, x, dr), x), ST.nd(K, nl, x), RN.skipa(K, nl, q, x, dr, x, FRM.ne_sym(x, q, hqx)), {==}))
      +isn = L.subst(M.Node<K>, z => {ST.is_node(K, z, ST.rid(cl), ST.rid(cr), q) == True{} : Bool}, SE.modp(K, ST.nd(K, nl, x), q), ST.nd(K, SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), x), Equal.sym(M.Node<K>, ST.nd(K, SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), x), SE.modp(K, ST.nd(K, nl, x), q), e), RN.isn_p(K, ST.nd(K, nl, x), ST.rid(cl), ST.rid(cr), u, q, TR.rep_node(~K, x, cl, cr, u, nl, hr)))
      +hl = RT.rep_moved(~K, ~cmp, ~o, cl, x, nl, SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), AG.agr_trans(~K, ~cmp, ~o, ST.ids(cl), nl, RM.attn(K, nl, q, x, dr), SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), RN.attn_agr(~K, ~cmp, ~o, ST.ids(cl), nl, q, x, dr, hql), SE.setp_agr(~K, ~cmp, ~o, ST.ids(cl), RM.attn(K, nl, q, x, dr), x, q, hxl)), TR.rep_l(~K, x, cl, cr, u, nl, hr))
      +hrr = RT.rep_moved(~K, ~cmp, ~o, cr, x, nl, SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), AG.agr_trans(~K, ~cmp, ~o, ST.ids(cr), nl, RM.attn(K, nl, q, x, dr), SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), RN.attn_agr(~K, ~cmp, ~o, ST.ids(cr), nl, q, x, dr, hqr), SE.setp_agr(~K, ~cmp, ~o, ST.ids(cr), RM.attn(K, nl, q, x, dr), x, q, hxr)), TR.rep_r(~K, x, cl, cr, u, nl, hr))
      RT.rep_intro(~K, SE.setp(K, RM.attn(K, nl, q, x, dr), x, q), x, cl, cr, q, L.and_left(Nat.is_lt(0n, x), Bool.and(ST.is_node(K, ST.nd(K, nl, x), ST.rid(cl), ST.rid(cr), u), Bool.and(ST.rep(~K, cl, x, nl), ST.rep(~K, cr, x, nl))), hr), isn, hl, hrr)


# the parent's frame after reattaching: x on the path's side where z0 was
def ratt_frame(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +nla: List<&2, M.Node<K>>, +x: Nat, +z0: Nat, +i: Nat, +lft: Bool, +s: ST.Tr, +u: List<&2, P.Fr>, +hc0: {P.ctxok(~K, Con{P.FR{1n+i, lft, s}, u}, z0, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == True{} : Bool}, +hags: {AG.agr(~K, ~cmp, ST.ids(s), nl, nla) == True{} : Bool}, +hagu: {AG.agr(~K, ~cmp, SC.append(Nat, P.before(u), P.after(u)), nl, nla) == True{} : Bool}, +hagq: {ST.nd(K, nl, 1n+i) == ST.nd(K, nla, 1n+i) : M.Node<K>}, +hq: {Nat.is_eq(x, 1n+i) == False{} : Bool}, +hxf: {NL.memn(x, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == False{} : Bool}) -> {P.ctxok(~K, Con{P.FR{1n+i, lft, s}, u}, x, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i)) == True{} : Bool}:
  +hk = L.and_left(P.cok1(~K, P.FR{1n+i, lft, s}, z0, P.top(u), nl), P.ctxok(~K, u, 1n+i, nl), hc0)
  +hu = L.and_right(P.cok1(~K, P.FR{1n+i, lft, s}, z0, P.top(u), nl), P.ctxok(~K, u, 1n+i, nl), hc0)
  +h0 = L.and_left(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, z0, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), z0), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk)
  +hqn = L.and_left(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, z0, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), z0), P.top(u)), ST.rep(~K, s, 1n+i, nl), L.and_right(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, z0, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), z0), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk))
  +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, z0, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), z0), P.top(u)), ST.rep(~K, s, 1n+i, nl), L.and_right(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, z0, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), z0), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk))
  +qs = Pair.fst({NL.memn(1n+i, ST.ids(s)) == False{} : Bool}, {NL.memn(1n+i, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, RT.fq_s(1n+i, lft, s, u, hnd))
  +qu = Pair.snd({NL.memn(1n+i, ST.ids(s)) == False{} : Bool}, {NL.memn(1n+i, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, RT.fq_s(1n+i, lft, s, u, hnd))
  +xs = Pair.fst({NL.memn(x, ST.ids(s)) == False{} : Bool}, {NL.memn(x, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, RT.fw_s(x, 1n+i, lft, s, u, hxf))
  +xu = Pair.snd({NL.memn(x, ST.ids(s)) == False{} : Bool}, {NL.memn(x, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, RT.fw_s(x, 1n+i, lft, s, u, hxf))
  +e1 = Equal.trans(M.Node<K>, ST.nd(K, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), 1n+i), ST.nd(K, RM.attn(K, nla, 1n+i, x, lft), 1n+i), RN.moda(K, ST.nd(K, nl, 1n+i), x, lft), RN.skipp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i, 1n+i, hq), Equal.trans(M.Node<K>, ST.nd(K, RM.attn(K, nla, 1n+i, x, lft), 1n+i), RN.moda(K, ST.nd(K, nla, 1n+i), x, lft), RN.moda(K, ST.nd(K, nl, 1n+i), x, lft), RN.hita(K, nla, i, x, lft), L.subst(M.Node<K>, z => {RN.moda(K, ST.nd(K, nla, 1n+i), x, lft) == RN.moda(K, z, x, lft) : M.Node<K>}, ST.nd(K, nla, 1n+i), ST.nd(K, nl, 1n+i), Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), ST.nd(K, nla, 1n+i), hagq), {==})))
  +rq = L.subst(M.Node<K>, z => {ST.is_node(K, z, ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)) == True{} : Bool}, RN.moda(K, ST.nd(K, nl, 1n+i), x, lft), ST.nd(K, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), 1n+i), Equal.sym(M.Node<K>, ST.nd(K, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), 1n+i), RN.moda(K, ST.nd(K, nl, 1n+i), x, lft), e1), RN.isn_a(K, ST.nd(K, nl, 1n+i), lft, z0, ST.rid(s), P.top(u), x, hqn))
  +hs2 = RT.rep_moved(~K, ~cmp, ~o, s, 1n+i, nl, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), AG.agr_trans(~K, ~cmp, ~o, ST.ids(s), nl, RM.attn(K, nla, 1n+i, x, lft), SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), AG.agr_trans(~K, ~cmp, ~o, ST.ids(s), nl, nla, RM.attn(K, nla, 1n+i, x, lft), hags, RN.attn_agr(~K, ~cmp, ~o, ST.ids(s), nla, 1n+i, x, lft, qs)), SE.setp_agr(~K, ~cmp, ~o, ST.ids(s), RM.attn(K, nla, 1n+i, x, lft), x, 1n+i, xs)), hs)
  +hu2 = Equal.trans(Bool, P.ctxok(~K, u, 1n+i, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i)), P.ctxok(~K, u, 1n+i, nl), True{}, AG.ctx_agr(~K, ~cmp, ~o, u, 1n+i, nl, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), AG.agr_trans(~K, ~cmp, ~o, SC.append(Nat, P.before(u), P.after(u)), nl, RM.attn(K, nla, 1n+i, x, lft), SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), AG.agr_trans(~K, ~cmp, ~o, SC.append(Nat, P.before(u), P.after(u)), nl, nla, RM.attn(K, nla, 1n+i, x, lft), hagu, RN.attn_agr(~K, ~cmp, ~o, SC.append(Nat, P.before(u), P.after(u)), nla, 1n+i, x, lft, qu)), SE.setp_agr(~K, ~cmp, ~o, SC.append(Nat, P.before(u), P.after(u)), RM.attn(K, nla, 1n+i, x, lft), x, 1n+i, xu))), hu)
  L.and_intro(P.cok1(~K, P.FR{1n+i, lft, s}, x, P.top(u), SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i)), P.ctxok(~K, u, 1n+i, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i)), L.and_intro(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i))), h0, L.and_intro(ST.is_node(K, ST.nd(K, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i), 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, SE.setp(K, RM.attn(K, nla, 1n+i, x, lft), x, 1n+i)), rq, hs2)), hu2)


# the path leads to the reattached child
def ratt_ctx(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +nla: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +x: Nat, +z0: Nat, +hc0: {P.ctxok(~K, c, z0, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c), P.after(c))) == True{} : Bool}, +hag: {AG.agr(~K, ~cmp, SC.append(Nat, P.before(c), P.after(c)), nl, nla) == True{} : Bool}, +hxf: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}) -> {P.ctxok(~K, c, x, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c))) == True{} : Bool}:
  match c:
    case Nil{}:
      {==}
    case Con{P.FR{0n, +lft, +s}, +u}:
      Empty.absurd({P.ctxok(~K, Con{P.FR{0n, lft, s}, u}, x, SE.setp(K, RM.attn(K, nla, 0n, x, lft), x, 0n)) == True{} : Bool}, L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+0n), ST.pk(Nat, lft, z0, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), z0), P.top(u)), ST.rep(~K, s, 0n, nl)), L.and_left(P.cok1(~K, P.FR{0n, lft, s}, z0, P.top(u), nl), P.ctxok(~K, u, 0n, nl), hc0))))
    case Con{P.FR{1n+i, True{}, +s}, +u}:
      +h1 = AG.agr_r(~K, ~cmp, ~o, P.before(u), Con{1n+i, SC.append(Nat, ST.ids(s), P.after(u))}, nl, nla, hag)
      +h2 = L.and_right(AG.ndeq(~K, ~cmp, ST.nd(K, nl, 1n+i), ST.nd(K, nla, 1n+i)), AG.agr(~K, ~cmp, SC.append(Nat, ST.ids(s), P.after(u)), nl, nla), h1)
      +hq = N.is_eq_sym_false(x, 1n+i, DJ.ne_nm(x, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, True{}, s}, u}), P.after(Con{P.FR{1n+i, True{}, s}, u})), hxf, FX.q_in(1n+i, True{}, s, u)))
      ratt_frame(~K, ~cmp, ~o, nl, nla, x, z0, i, True{}, s, u, hc0, hnd, AG.agr_l(~K, ~cmp, ~o, ST.ids(s), P.after(u), nl, nla, h2), AG.agr_app(~K, ~cmp, ~o, P.before(u), P.after(u), nl, nla, AG.agr_l(~K, ~cmp, ~o, P.before(u), Con{1n+i, SC.append(Nat, ST.ids(s), P.after(u))}, nl, nla, hag), AG.agr_r(~K, ~cmp, ~o, ST.ids(s), P.after(u), nl, nla, h2)), AG.agr_head(~K, ~cmp, ~o, 1n+i, SC.append(Nat, ST.ids(s), P.after(u)), nl, nla, h1), N.is_eq_sym_false(1n+i, x, hq), hxf)
    case Con{P.FR{1n+i, False{}, +s}, +u}:
      +h1 = AG.agr_l(~K, ~cmp, ~o, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}})), P.after(u), nl, nla, hag)
      +h2 = AG.agr_r(~K, ~cmp, ~o, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}}), nl, nla, h1)
      +hq = N.is_eq_sym_false(x, 1n+i, DJ.ne_nm(x, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, False{}, s}, u}), P.after(Con{P.FR{1n+i, False{}, s}, u})), hxf, FX.q_in(1n+i, False{}, s, u)))
      ratt_frame(~K, ~cmp, ~o, nl, nla, x, z0, i, False{}, s, u, hc0, hnd, AG.agr_l(~K, ~cmp, ~o, ST.ids(s), Con{1n+i, Nil{}}, nl, nla, h2), AG.agr_app(~K, ~cmp, ~o, P.before(u), P.after(u), nl, nla, AG.agr_l(~K, ~cmp, ~o, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}}), nl, nla, h1), AG.agr_r(~K, ~cmp, ~o, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}})), P.after(u), nl, nla, hag)), AG.agr_head(~K, ~cmp, ~o, 1n+i, Nil{}, nl, nla, AG.agr_r(~K, ~cmp, ~o, ST.ids(s), Con{1n+i, Nil{}}, nl, nla, h2)), N.is_eq_sym_false(1n+i, x, hq), hxf)


# ---- the unlink, the recycling and the fix-up ----


def unl_core(~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>, +flf: List<&2, Nat>, +c: List<&2, P.Fr>, +ui: Nat, +tu: ST.Tr, +ch: ST.Tr, +hpar: {M.node_parent(~K, ST.nd(K, nl, 1n+ui)) == P.top(c) : Nat}, +hx: {M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))) == ST.rid(ch) : Nat}, +hdir: {Nat.is_eq(1n+ui, M.node_left(~K, ST.nd(K, nl, P.top(c)))) == SP.dir(c) : Bool}, +hr: {ST.rep(~K, ch, 1n+ui, nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +htu: {ST.rid(tu) == 1n+ui : Nat}, +hroot: {root == ST.rid(PG.plug(c, tu)) : Nat}, +m1: {NL.memn(P.top(c), ST.ids(ch)) == False{} : Bool}, +m2: {NL.nodupn(ST.ids(ch)) == True{} : Bool}, +m3: {NL.memn(ST.rid(ch), SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +m4: {NL.nodupn(SC.append(Nat, P.before(c), P.after(c))) == True{} : Bool}, +m5: {NL.memn(1n+ui, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))) == False{} : Bool}, +m6: {NL.memn(1n+ui, flf) == False{} : Bool}, +m7: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))) == True{} : Bool}, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) == True{} : Bool}, +hfl: {ST.fll(~K, nl, flf) == True{} : Bool}, +hfree: {Nat.is_eq(free, ST.fst0(flf)) == True{} : Bool}, +hul: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> 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, pl, tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, 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_, 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>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>:
  %Equal.sym(Nat, M.node_parent(~K, ST.nd(K, nl, 1n+ui)), P.top(c), hpar) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_repair(~K, ~V, ~cmp, MI.recycle(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _, M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))), Nat.is_eq(1n+ui, M.node_left(~K, ST.nd(K, nl, _)))), 1n+ui), M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))), _, M.node_red(~K, ST.nd(K, nl, 1n+ui))) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, 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_, 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>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>
  %Equal.sym(Bool, Nat.is_eq(1n+ui, M.node_left(~K, ST.nd(K, nl, P.top(c)))), SP.dir(c), hdir) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_repair(~K, ~V, ~cmp, MI.recycle(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, P.top(c), M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))), _), 1n+ui), M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))), P.top(c), M.node_red(~K, ST.nd(K, nl, 1n+ui))) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, 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_, 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>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>
  %Equal.sym(Nat, M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))), ST.rid(ch), hx) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_repair(~K, ~V, ~cmp, MI.recycle(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, P.top(c), _, SP.dir(c)), 1n+ui), _, P.top(c), M.node_red(~K, ST.nd(K, nl, 1n+ui))) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, 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_, 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>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>
  %Equal.sym(ST.Sh<K, V>, MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, P.top(c), ST.rid(ch), SP.dir(c)), ST.SH{n, RM.rootq(P.top(c), root, ST.rid(ch)), lo, hi, free, l, d, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), pl, tg, fl}, RM.attach_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, P.top(c), ST.rid(ch), SP.dir(c))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_repair(~K, ~V, ~cmp, MI.recycle(~K, ~V, ~cmp, _, 1n+ui), ST.rid(ch), P.top(c), M.node_red(~K, ST.nd(K, nl, 1n+ui))) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, 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_, 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>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>
  +m9 = DJ.nm_l(1n+ui, ST.ids(ch), P.after(c), DJ.nm_r(1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m5))
  +m8 = DJ.nm_app(1n+ui, P.before(c), P.after(c), DJ.nm_l(1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m5), DJ.nm_r(1n+ui, ST.ids(ch), P.after(c), DJ.nm_r(1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m5)))
  +el1 = Equal.trans(Nat, SC.length(M.Node<K>, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c))), SC.length(M.Node<K>, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c))), SC.length(M.Node<K>, nl), SE.setp_len(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), RP.attn_len(~K, nl, P.top(c), ST.rid(ch), SP.dir(c)))
  +el2 = Equal.trans(Nat, SC.length(M.Node<K>, PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free})), SC.length(M.Node<K>, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c))), SC.length(M.Node<K>, nl), FRM.len_wr(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), el1)
  +hul1 = L.subst(Nat, z => {Nat.is_lt(ui, z) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c))), Equal.sym(Nat, SC.length(M.Node<K>, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c))), SC.length(M.Node<K>, nl), el1), hul)
  +hfr = L.subst(M.Node<K>, z => {ST.is_free(K, z, ST.fst0(flf)) == True{} : Bool}, M.Free{free}, ST.nd(K, PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), 1n+ui), Equal.sym(M.Node<K>, ST.nd(K, PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), 1n+ui), M.Free{free}, FRM.nd_wr_same(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), ui, M.Free{free}, hul1)), hfree)
  +hf2 = Equal.trans(Bool, ST.fll(~K, PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), flf), ST.fll(~K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), flf), True{}, FRM.fll_frame(~K, flf, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}, m6), Equal.trans(Bool, ST.fll(~K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), flf), ST.fll(~K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), flf), True{}, SE.fll_setp(~K, flf, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), Equal.trans(Bool, ST.fll(~K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), flf), ST.fll(~K, nl, flf), True{}, RP.attn_fll(~K, flf, nl, P.top(c), ST.rid(ch), SP.dir(c)), hfl)))
  +h4 = 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))), PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), FRM.ents_frame(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), pl, 1n+ui, M.Free{free}, m5), 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))), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), SE.ents_setp(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), pl, ST.rid(ch), P.top(c)), RP.attn_ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), pl, nl, P.top(c), ST.rid(ch), SP.dir(c))))
  +h5 = Equal.trans(Bool, EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), pl), EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), pl), True{}, AG.oks_agr(~K, ~V, ~cmp, ~o, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), pl, AG.agr_wr(~K, ~cmp, ~o, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}, m5)), Equal.trans(Bool, EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), pl), EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), pl), True{}, SE.oks_setp(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), pl, ST.rid(ch), P.top(c)), Equal.trans(Bool, EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), pl), EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), True{}, RP.attn_oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), pl, nl, P.top(c), ST.rid(ch), SP.dir(c)), hk)))
  +i1 = Equal.trans(Bool, ST.rep(~K, ch, P.top(c), PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free})), ST.rep(~K, ch, P.top(c), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c))), True{}, FRM.rep_frame(~K, ch, P.top(c), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}, m9), ratt_rep(~K, ~cmp, ~o, nl, P.top(c), SP.dir(c), 1n+ui, ch, hr, m1, m2))
  +i2 = Equal.trans(Bool, P.ctxok(~K, c, ST.rid(ch), PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free})), P.ctxok(~K, c, ST.rid(ch), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c))), True{}, AG.ctx_agr(~K, ~cmp, ~o, c, ST.rid(ch), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), AG.agr_wr(~K, ~cmp, ~o, SC.append(Nat, P.before(c), P.after(c)), SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}, m8)), ratt_ctx(~K, ~cmp, ~o, nl, nl, c, ST.rid(ch), 1n+ui, hok, m4, AG.agr_refl(~K, ~cmp, ~o, SC.append(Nat, P.before(c), P.after(c)), nl), m3))
  DF.dloop(~K, ~V, ~cmp, ~o, Nat.sub(n, 1n), lo, hi, 1n+ui, l, d, pl, tg, fl, Con{1n+ui, flf}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), SC.length(M.Node<K>, nl), 1n+Nat.sub(n, 1n), RM.rootq(P.top(c), root, ST.rid(ch)), PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), c, ch, i1, i2, m7, {==}, RP.root_rot(~K, nl, c, 1n+ui, ST.rid(ch), tu, ch, root, htu, {==}, hok, hroot), h4, h5, L.and_intro(ST.is_free(K, ST.nd(K, PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), 1n+ui), ST.fst0(flf)), ST.fll(~K, PR.wr_nl(K, SE.setp(K, RM.attn(K, nl, P.top(c), ST.rid(ch), SP.dir(c)), ST.rid(ch), P.top(c)), 1n+ui, M.Free{free}), flf), hfr, hf2), el2, Bool.not(M.node_red(~K, ST.nd(K, nl, 1n+ui))))

# ---- the facts the unlink needs, from the tree's ----

def mid_c(+b: List<&2, Nat>, +s: List<&2, Nat>, +a: List<&2, Nat>, +q: Nat, +hnd: {NL.nodupn(SC.append(Nat, b, SC.append(Nat, s, a))) == True{} : Bool}, +hm: {NL.memn(q, SC.append(Nat, b, a)) == True{} : Bool}, +e: Bool, +he: {NL.memn(q, b) == e : Bool}) -> {NL.memn(q, s) == False{} : Bool}:
  match e:
    case True{}:
      DJ.nm_l(q, s, a, DJ.dj_r(b, SC.append(Nat, s, a), hnd, q, he))
    case False{}:
      +hor = Equal.trans(Bool, Bool.or(NL.memn(q, b), NL.memn(q, a)), NL.memn(q, SC.append(Nat, b, a)), True{}, Equal.sym(Bool, NL.memn(q, SC.append(Nat, b, a)), Bool.or(NL.memn(q, b), NL.memn(q, a)), NL.memn_app(q, b, a)), hm)
      +hqa = L.subst(Bool, w => {Bool.or(w, NL.memn(q, a)) == True{} : Bool}, NL.memn(q, b), False{}, he, hor)
      DJ.dj_l(s, a, DJ.ndr(b, SC.append(Nat, s, a), hnd), q, hqa)

# a member of the lists around s is not in s
def mid_nm(+b: List<&2, Nat>, +s: List<&2, Nat>, +a: List<&2, Nat>, +q: Nat, +hnd: {NL.nodupn(SC.append(Nat, b, SC.append(Nat, s, a))) == True{} : Bool}, +hm: {NL.memn(q, SC.append(Nat, b, a)) == True{} : Bool}) -> {NL.memn(q, s) == False{} : Bool}:
  mid_c(b, s, a, q, hnd, hm, NL.memn(q, b), {==})

# the parent is not in the subtree
def top_nm(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +t: ST.Tr, +p: Nat, +hr: {ST.rep(~K, t, p, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}) -> {NL.memn(P.top(c), ST.ids(t)) == False{} : Bool}:
  match c:
    case Nil{}:
      RT.zero_ids(~K, nl, t, p, hr)
    case Con{P.FR{+q, +lft, +s}, +c1}:
      mid_nm(P.before(Con{P.FR{q, lft, s}, c1}), ST.ids(t), P.after(Con{P.FR{q, lft, s}, c1}), q, hnd, FX.q_in(q, lft, s, c1))

# the subtree's root is not on the path
def rid_nm(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +t: ST.Tr, +z: Nat, +hok: {P.ctxok(~K, c, z, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}) -> {NL.memn(ST.rid(t), SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}:
  match t:
    case ST.TE{}:
      RT.zero_ctx(~K, nl, c, z, hok)
    case ST.TN{+j, +tl, +tr}:
      +mj = P.mem_root(j, tl, tr)
      DJ.nm_app(j, P.before(c), P.after(c), DJ.dj_l(P.before(c), SC.append(Nat, ST.ids(ST.TN{j, tl, tr}), P.after(c)), hnd, j, DJ.mem_l(j, ST.ids(ST.TN{j, tl, tr}), P.after(c), mj)), DJ.dj_r(ST.ids(ST.TN{j, tl, tr}), P.after(c), DJ.ndr(P.before(c), SC.append(Nat, ST.ids(ST.TN{j, tl, tr}), P.after(c)), hnd), j, mj))

def une(+ui: Nat, +s: ST.Tr, +h: {NL.memn(1n+ui, ST.ids(s)) == False{} : Bool}) -> {Bool.not(Nat.is_eq(1n+ui, ST.rid(s))) == True{} : Bool}:
  match s:
    case ST.TE{}:
      {==}
    case ST.TN{+j, +sl, +sr}:
      +e = FRM.ne_sym(j, 1n+ui, Pair.fst({Nat.is_eq(j, 1n+ui) == False{} : Bool}, {NL.memn(1n+ui, ST.ids(sl)) == False{} : Bool} & {NL.memn(1n+ui, ST.ids(sr)) == False{} : Bool}, FRM.nm_node(1n+ui, j, sl, sr, h)))
      L.subst(Bool, w => {Bool.not(w) == True{} : Bool}, False{}, Nat.is_eq(1n+ui, j), Equal.sym(Bool, Nat.is_eq(1n+ui, j), False{}, e), {==})

# the side the node hangs on is the path's
def udir(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +ui: Nat, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hu: {NL.memn(1n+ui, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}) -> {Nat.is_eq(1n+ui, M.node_left(~K, ST.nd(K, nl, P.top(c)))) == SP.dir(c) : Bool}:
  match c:
    case Nil{}:
      {==}
    case Con{P.FR{+q, +lft, +s}, +c1}:
      +hk = L.and_left(P.cok1(~K, P.FR{q, lft, s}, 1n+ui, P.top(c1), nl), P.ctxok(~K, c1, q, nl), hok)
      +isn = L.and_left(ST.is_node(K, ST.nd(K, nl, q), ST.pk(Nat, lft, 1n+ui, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), 1n+ui), P.top(c1)), ST.rep(~K, s, q, nl), L.and_right(Nat.is_lt(0n, q), Bool.and(ST.is_node(K, ST.nd(K, nl, q), ST.pk(Nat, lft, 1n+ui, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), 1n+ui), P.top(c1)), ST.rep(~K, s, q, nl)), hk))
      %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, q)), ST.pk(Nat, lft, 1n+ui, ST.rid(s)), NB.child_eq(~K, ST.nd(K, nl, q), ST.pk(Nat, lft, 1n+ui, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), 1n+ui), P.top(c1), False{}, isn)) : {Nat.is_eq(1n+ui, _) == lft : Bool}
      FX.eq_pk(1n+ui, lft, ST.rid(s), une(ui, s, Pair.fst({NL.memn(1n+ui, ST.ids(s)) == False{} : Bool}, {NL.memn(1n+ui, SC.append(Nat, P.before(c1), P.after(c1))) == False{} : Bool}, RT.fw_s(1n+ui, q, lft, s, c1, hu))))

# the child the unlink picks
def hx_a(~K: Data, +nl: List<&2, M.Node<K>>, +ui: Nat, +ch: ST.Tr, +q: Nat, +hn: {ST.is_node(K, ST.nd(K, nl, 1n+ui), 0n, ST.rid(ch), q) == True{} : Bool}) -> {M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))) == ST.rid(ch) : Nat}:
  %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, 1n+ui)), 0n, NB.child_eq(~K, ST.nd(K, nl, 1n+ui), 0n, ST.rid(ch), q, False{}, hn)) : {M.pick(Nat, Nat.is_lt(0n, _), _, M.node_right(~K, ST.nd(K, nl, 1n+ui))) == ST.rid(ch) : Nat}
  %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, 1n+ui)), ST.rid(ch), NB.child_eq(~K, ST.nd(K, nl, 1n+ui), 0n, ST.rid(ch), q, True{}, hn)) : {M.pick(Nat, False{}, 0n, _) == ST.rid(ch) : Nat}
  {==}

def hx_b(~K: Data, +nl: List<&2, M.Node<K>>, +ui: Nat, +ch: ST.Tr, +q: Nat, +hn: {ST.is_node(K, ST.nd(K, nl, 1n+ui), ST.rid(ch), 0n, q) == True{} : Bool}, +hj: {Nat.is_lt(0n, ST.rid(ch)) == True{} : Bool}) -> {M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, ST.nd(K, nl, 1n+ui))), M.node_left(~K, ST.nd(K, nl, 1n+ui)), M.node_right(~K, ST.nd(K, nl, 1n+ui))) == ST.rid(ch) : Nat}:
  %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, 1n+ui)), ST.rid(ch), NB.child_eq(~K, ST.nd(K, nl, 1n+ui), ST.rid(ch), 0n, q, False{}, hn)) : {M.pick(Nat, Nat.is_lt(0n, _), _, M.node_right(~K, ST.nd(K, nl, 1n+ui))) == ST.rid(ch) : Nat}
  %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, 1n+ui)), 0n, NB.child_eq(~K, ST.nd(K, nl, 1n+ui), ST.rid(ch), 0n, q, True{}, hn)) : {M.pick(Nat, Nat.is_lt(0n, ST.rid(ch)), ST.rid(ch), _) == ST.rid(ch) : Nat}
  %Equal.sym(Bool, Nat.is_lt(0n, ST.rid(ch)), True{}, hj) : {M.pick(Nat, _, ST.rid(ch), 0n) == ST.rid(ch) : Nat}
  {==}

# ---- the two shapes: no left child, or a left child and no right one ----


def unl_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>, +flf: List<&2, Nat>, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hr0: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, ch}, P.top(c), nl) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c, ST.TN{1n+ui, ST.TE{}, ch})) : Nat}, +hnd0: {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))), flf)) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) == True{} : Bool}, +hfl: {ST.fll(~K, nl, flf) == True{} : Bool}, +hfree: {Nat.is_eq(free, ST.fst0(flf)) == True{} : Bool}, +hul: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> 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, pl, tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, 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_, 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>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>:
  +hn = TR.rep_node(~K, 1n+ui, ST.TE{}, ch, P.top(c), nl, hr0)
  +hmv = ID.mv_a(flf, c, ui, ch, hnd0)
  +m7 = DJ.ndl(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}, hmv)
  +m5 = DJ.dj_l(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}, hmv, 1n+ui, DJ.mem_hd(1n+ui, flf))
  +hr = TR.rep_r(~K, 1n+ui, ST.TE{}, ch, P.top(c), nl, hr0)
  unl_core(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, flf, c, ui, ST.TN{1n+ui, ST.TE{}, ch}, ch, NB.parent_eq(~K, ST.nd(K, nl, 1n+ui), 0n, ST.rid(ch), P.top(c), hn), hx_a(~K, nl, ui, ch, P.top(c), hn), udir(~K, ~cmp, ~o, nl, c, ui, hok, DJ.nm_app(1n+ui, P.before(c), P.after(c), DJ.nm_l(1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m5), DJ.nm_r(1n+ui, ST.ids(ch), P.after(c), DJ.nm_r(1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m5)))), hr, hok, {==}, hroot, top_nm(~K, ~cmp, ~o, nl, c, ch, 1n+ui, hr, m7), DJ.ndl(ST.ids(ch), P.after(c), DJ.ndr(P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m7)), rid_nm(~K, ~cmp, ~o, nl, c, ch, 1n+ui, hok, m7), RT.nd_drop(P.before(c), ST.ids(ch), P.after(c), m7), m5, DJ.nd_head(1n+ui, flf, DJ.ndr(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}, hmv)), m7, hk, hfl, hfree, hul)

def unl_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>, +flf: List<&2, Nat>, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +hj: {Nat.is_lt(0n, ST.rid(ch)) == True{} : Bool}, +hr0: {ST.rep(~K, ST.TN{1n+ui, ch, ST.TE{}}, P.top(c), nl) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c, ST.TN{1n+ui, ch, ST.TE{}})) : Nat}, +hnd0: {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))), flf)) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) == True{} : Bool}, +hfl: {ST.fll(~K, nl, flf) == True{} : Bool}, +hfree: {Nat.is_eq(free, ST.fst0(flf)) == True{} : Bool}, +hul: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> 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, pl, tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, 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_, 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>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>:
  +hn = TR.rep_node(~K, 1n+ui, ch, ST.TE{}, P.top(c), nl, hr0)
  +hmv = ID.mv_b(flf, c, ui, ch, hnd0)
  +m7 = DJ.ndl(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}, hmv)
  +m5 = DJ.dj_l(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}, hmv, 1n+ui, DJ.mem_hd(1n+ui, flf))
  +hr = TR.rep_l(~K, 1n+ui, ch, ST.TE{}, P.top(c), nl, hr0)
  unl_core(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, flf, c, ui, ST.TN{1n+ui, ch, ST.TE{}}, ch, NB.parent_eq(~K, ST.nd(K, nl, 1n+ui), ST.rid(ch), 0n, P.top(c), hn), hx_b(~K, nl, ui, ch, P.top(c), hn, hj), udir(~K, ~cmp, ~o, nl, c, ui, hok, DJ.nm_app(1n+ui, P.before(c), P.after(c), DJ.nm_l(1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m5), DJ.nm_r(1n+ui, ST.ids(ch), P.after(c), DJ.nm_r(1n+ui, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m5)))), hr, hok, {==}, hroot, top_nm(~K, ~cmp, ~o, nl, c, ch, 1n+ui, hr, m7), DJ.ndl(ST.ids(ch), P.after(c), DJ.ndr(P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)), m7)), rid_nm(~K, ~cmp, ~o, nl, c, ch, 1n+ui, hok, m7), RT.nd_drop(P.before(c), ST.ids(ch), P.after(c), m7), m5, DJ.nd_head(1n+ui, flf, DJ.ndr(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}, hmv)), m7, hk, hfl, hfree, hul)