import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/order.bend as O
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./tree.bend as TR
import ./path.bend as P
import ./prim.bend as PR
import ./find.bend as FI
import ./ends.bend as EN
import ./slot.bend as SL
import ./dj.bend as DJ
import ./agree.bend as AG
import ./frame.bend as FRM
import ../../lib/nat_list.bend as NL

# Removing a node with two children: its successor s (the leftmost node of
# its right subtree) gives the node its key and payload and is unlinked.
# The ids split around the node and s; the new node list and payloads give
# the remaining ids the entries the old ones had without the node's.
# (source: tools/generators/tm_hand/rms.src)


# ---- the ids: before the node, the node, the successor, the rest ----

def eb_s(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}) -> {P.before(cs) == SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}) : List<&2, Nat>}:
  Equal.trans(List<&2, Nat>, P.before(cs), P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}), hlb, Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}), P.before(Con{P.FR{1n+ui, False{}, ta}, c}), LL.append_assoc(Nat, P.before(c), ST.ids(ta), Con{1n+ui, Nil{}})))

# the old ids through the successor's path
def ew_s(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}) -> {ST.ids(tg) == SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) : List<&2, Nat>}:
  Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), hbc, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), P.ids_r(c, 1n+ui, ta, tb), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))), hlw)))

def eo_s(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}) -> {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}) : List<&2, Nat>}:
  +e1 = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, z, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}) : List<&2, Nat>}, P.before(cs), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}), eb_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb), {==})
  Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), ew_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))), SC.append(Nat, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}), Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), e1, LL.append_assoc(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))})))

# the remaining ids
def en_s(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}) -> {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))) == SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}) : List<&2, Nat>}:
  +e1 = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))) == SC.append(Nat, z, SC.append(Nat, ST.ids(sb), P.after(cs))) : List<&2, Nat>}, P.before(cs), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}), eb_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb), {==})
  Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(sb), P.after(cs))), SC.append(Nat, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}), SC.append(Nat, ST.ids(sb), P.after(cs))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}), e1, LL.append_assoc(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Nil{}}, SC.append(Nat, ST.ids(sb), P.after(cs))))

# ---- no repeats: the node and the successor are apart from the rest ----

def nd_old(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))) : List<&2, Nat>}, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+si, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Con{P.FR{1n+ui, False{}, ta}, c}), SC.append(Nat, ST.ids(tb), P.after(Con{P.FR{1n+ui, False{}, ta}, c}))) : List<&2, Nat>}, +hlb: {P.before(cs) == P.before(Con{P.FR{1n+ui, False{}, ta}, c}) : List<&2, Nat>}) -> {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}})) == True{} : Bool}:
  L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}), eo_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, ui, ta, tb, cs, si, sb, hbc, hlw, hlb), DJ.ndl(ST.ids(tg), fl, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))

def ux_s(+c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +h: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}})) == True{} : Bool}) -> {NL.memn(1n+ui, SC.append(Nat, P.before(c), ST.ids(ta))) == False{} : Bool}:
  DJ.dj_l(SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}, h, 1n+ui, DJ.mem_hd(1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}))

def sx_s(+c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +h: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}})) == True{} : Bool}) -> {NL.memn(1n+si, SC.append(Nat, P.before(c), ST.ids(ta))) == False{} : Bool}:
  DJ.dj_l(SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}, h, 1n+si, 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)))))

def ut_s(+c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +h: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}})) == True{} : Bool}) -> {NL.memn(1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}) == False{} : Bool}:
  DJ.nd_head(1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}, DJ.ndr(SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}, h))

def sr_s(+c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +h: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}})) == True{} : Bool}) -> {NL.memn(1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))) == False{} : Bool}:
  DJ.nd_head(1n+si, SC.append(Nat, ST.ids(sb), P.after(cs)), DJ.nd_tail(1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}, DJ.ndr(SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}}, h)))

def ur_s(+c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +h: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}})) == True{} : Bool}) -> {NL.memn(1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))) == False{} : Bool}:
  DJ.nm_ct(1n+ui, 1n+si, SC.append(Nat, ST.ids(sb), P.after(cs)), ut_s(c, ui, ta, cs, si, sb, h))

def us_s(+c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +cs: List<&2, P.Fr>, +si: Nat, +sb: ST.Tr, +h: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(ta)), Con{1n+ui, Con{1n+si, SC.append(Nat, ST.ids(sb), P.after(cs))}})) == True{} : Bool}) -> {Nat.is_eq(1n+ui, 1n+si) == False{} : Bool}:
  FRM.ne_sym(1n+si, 1n+ui, DJ.nm_ch(1n+ui, 1n+si, SC.append(Nat, ST.ids(sb), P.after(cs)), ut_s(c, ui, ta, cs, si, sb, h)))

# ---- the moved key and payload ----


# ids away from the node and the successor keep their entries
def ents_rest(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +ui: Nat, +si: Nat, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hb: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}, +hbp: {Nat.is_lt(ui, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}))) == True{} : Bool}, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, +hus: {Nat.is_eq(1n+ui, 1n+si) == False{} : Bool}, +xs: List<&2, Nat>, +hu: {NL.memn(1n+ui, xs) == False{} : Bool}, +hs: {NL.memn(1n+si, xs) == False{} : Bool}) -> {ST.ents(~K, ~V, xs, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
  Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, xs, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, xs, nl, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, xs, nl, pl), FRM.ents_frame(~K, ~V, xs, nl, 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)), 1n+ui, M.N{c0, a0, b0, q0, ks}, hu), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, xs, nl, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, xs, nl, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), ST.ents(~K, ~V, xs, nl, pl), SL.ents_pex(~K, ~V, xs, nl, 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), hu), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, xs, nl, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), ST.ents(~K, ~V, xs, nl, PR.ex_pl(V, pl, 1n+ui, None{})), ST.ents(~K, ~V, xs, nl, pl), SL.ents_pex(~K, ~V, xs, nl, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}, hs), SL.ents_pex(~K, ~V, xs, nl, pl, 1n+ui, None{}, hu))))

def oks_rest(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +ui: Nat, +si: Nat, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hb: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}, +hbp: {Nat.is_lt(ui, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}))) == True{} : Bool}, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, +hus: {Nat.is_eq(1n+ui, 1n+si) == False{} : Bool}, +xs: List<&2, Nat>, +hu: {NL.memn(1n+ui, xs) == False{} : Bool}, +hs: {NL.memn(1n+si, xs) == False{} : Bool}) -> {EN.oks(~K, ~V, xs, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
  Equal.trans(Bool, EN.oks(~K, ~V, xs, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), EN.oks(~K, ~V, xs, nl, 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))), EN.oks(~K, ~V, xs, nl, pl), AG.oks_agr(~K, ~V, ~cmp, ~o, xs, nl, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), AG.agr_wr(~K, ~cmp, ~o, xs, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}, hu)), Equal.trans(Bool, EN.oks(~K, ~V, xs, nl, 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))), EN.oks(~K, ~V, xs, nl, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), EN.oks(~K, ~V, xs, nl, pl), SL.oks_pex(~K, ~V, xs, nl, 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), hu), Equal.trans(Bool, EN.oks(~K, ~V, xs, nl, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{})), EN.oks(~K, ~V, xs, nl, PR.ex_pl(V, pl, 1n+ui, None{})), EN.oks(~K, ~V, xs, nl, pl), SL.oks_pex(~K, ~V, xs, nl, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}, hs), SL.oks_pex(~K, ~V, xs, nl, pl, 1n+ui, None{}, hu))))

# an entry reads only the key
def ent_key(-K: Data, -V: Data, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +ks: K, +m: Maybe<&2, V>) -> {ST.ent(K, V, M.N{c0, a0, b0, q0, ks}, m) == ST.ent(K, V, M.N{cs0, as0, bs0, qs0, ks}, m) : Maybe<&2, M.Entry<K, V>>}:
  match m:
    case None{}:
      {==}
    case Some{+v}:
      {==}

# the node now holds the successor's entry
def ent_mv(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +ui: Nat, +si: Nat, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hb: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}, +hbp: {Nat.is_lt(ui, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}))) == True{} : Bool}, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, +hus: {Nat.is_eq(1n+ui, 1n+si) == False{} : Bool}) -> {ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)) == ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)) : Maybe<&2, M.Entry<K, V>>}:
  %Equal.sym(M.Node<K>, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), M.N{c0, a0, b0, q0, ks}, FRM.nd_wr_same(K, nl, ui, M.N{c0, a0, b0, q0, ks}, hb)) : {ST.ent(K, V, _, ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)) == ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)) : Maybe<&2, M.Entry<K, V>>}
  %Equal.sym(Maybe<&2, V>, ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui), ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si), SL.pv_ex_same(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si), hbp)) : {ST.ent(K, V, M.N{c0, a0, b0, q0, ks}, _) == ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)) : Maybe<&2, M.Entry<K, V>>}
  %Equal.sym(Maybe<&2, V>, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si), ST.pv(V, pl, 1n+si), SL.pv_ex_other(V, pl, 1n+ui, None{}, 1n+si, hus)) : {ST.ent(K, V, M.N{c0, a0, b0, q0, ks}, _) == ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)) : Maybe<&2, M.Entry<K, V>>}
  %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+si), M.N{cs0, as0, bs0, qs0, ks}, hsn) : {ST.ent(K, V, M.N{c0, a0, b0, q0, ks}, ST.pv(V, pl, 1n+si)) == ST.ent(K, V, _, ST.pv(V, pl, 1n+si)) : Maybe<&2, M.Entry<K, V>>}
  ent_key(K, V, c0, a0, b0, q0, cs0, as0, bs0, qs0, ks, ST.pv(V, pl, 1n+si))


# the remaining ids' entries: the old ones without the node's
def ents_new(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +ui: Nat, +si: Nat, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hb: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}, +hbp: {Nat.is_lt(ui, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}))) == True{} : Bool}, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, +hus: {Nat.is_eq(1n+ui, 1n+si) == False{} : Bool}, +xa: List<&2, Nat>, +rr: List<&2, Nat>, +hux: {NL.memn(1n+ui, xa) == False{} : Bool}, +hsx: {NL.memn(1n+si, xa) == False{} : Bool}, +hur: {NL.memn(1n+ui, rr) == False{} : Bool}, +hsr: {NL.memn(1n+si, rr) == False{} : Bool}) -> {ST.ents(~K, ~V, SC.append(Nat, xa, Con{1n+ui, rr}), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == ST.ents(~K, ~V, SC.append(Nat, xa, Con{1n+si, rr}), nl, pl) : List<&2, M.Entry<K, V>>}:
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, xa, Con{1n+ui, rr}), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, Con{1n+ui, rr}, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)))), FI.ents_app(~K, ~V, xa, Con{1n+ui, rr}, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)))) : {_ == ST.ents(~K, ~V, SC.append(Nat, xa, Con{1n+si, rr}), nl, pl) : List<&2, M.Entry<K, V>>}
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, xa, Con{1n+si, rr}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, nl, pl), ST.ents(~K, ~V, Con{1n+si, rr}, nl, pl)), FI.ents_app(~K, ~V, xa, Con{1n+si, rr}, nl, pl)) : {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)), ST.ents(~K, ~V, rr, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))))) == _ : List<&2, M.Entry<K, V>>}
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, xa, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, xa, nl, pl), ents_rest(~K, ~V, nl, pl, ui, si, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, hus, xa, hux, hsx)) : {SC.append(M.Entry<K, V>, _, ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)), ST.ents(~K, ~V, rr, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)), ST.ents(~K, ~V, rr, nl, pl))) : List<&2, M.Entry<K, V>>}
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, rr, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), ST.ents(~K, ~V, rr, nl, pl), ents_rest(~K, ~V, nl, pl, ui, si, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, hus, rr, hur, hsr)) : {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)), _)) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)), ST.ents(~K, ~V, rr, nl, pl))) : List<&2, M.Entry<K, V>>}
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)), ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)), ent_mv(K, V, nl, pl, ui, si, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, hus)) : {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, nl, pl), ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, rr, nl, pl))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, xa, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)), ST.ents(~K, ~V, rr, nl, pl))) : List<&2, M.Entry<K, V>>}
  {==}


# every remaining id still has a node and a value
def oks_new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +ui: Nat, +si: Nat, +c0: Bool, +a0: Nat, +b0: Nat, +q0: Nat, +ks: K, +cs0: Bool, +as0: Nat, +bs0: Nat, +qs0: Nat, +hb: {Nat.is_lt(ui, SC.length(M.Node<K>, nl)) == True{} : Bool}, +hbp: {Nat.is_lt(ui, SC.length(Maybe<&2, V>, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}))) == True{} : Bool}, +hsn: {ST.nd(K, nl, 1n+si) == M.N{cs0, as0, bs0, qs0, ks} : M.Node<K>}, +hus: {Nat.is_eq(1n+ui, 1n+si) == False{} : Bool}, +xa: List<&2, Nat>, +rr: List<&2, Nat>, +hux: {NL.memn(1n+ui, xa) == False{} : Bool}, +hsx: {NL.memn(1n+si, xa) == False{} : Bool}, +hur: {NL.memn(1n+ui, rr) == False{} : Bool}, +hsr: {NL.memn(1n+si, rr) == False{} : Bool}, +h: {EN.oks(~K, ~V, SC.append(Nat, xa, Con{1n+ui, Con{1n+si, rr}}), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, SC.append(Nat, xa, Con{1n+ui, rr}), PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))) == True{} : Bool}:
  +hx = SL.oks_split_l(~K, ~V, xa, Con{1n+ui, Con{1n+si, rr}}, nl, pl, h)
  +hsr0 = L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+ui), ST.pv(V, pl, 1n+ui))), EN.oks(~K, ~V, Con{1n+si, rr}, nl, pl), SL.oks_split_r(~K, ~V, xa, Con{1n+ui, Con{1n+si, rr}}, nl, pl, h))
  +oks = L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si))), EN.oks(~K, ~V, rr, nl, pl), hsr0)
  +okr = L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si))), EN.oks(~K, ~V, rr, nl, pl), hsr0)
  +oku = L.subst(Maybe<&2, M.Entry<K, V>>, z => {S.is_some(M.Entry<K, V>, z) == True{} : Bool}, ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)), ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)), Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui)), ST.ent(K, V, ST.nd(K, nl, 1n+si), ST.pv(V, pl, 1n+si)), ent_mv(K, V, nl, pl, ui, si, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, hus)), oks)
  EN.oks_app(~K, ~V, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), xa, Con{1n+ui, rr}, Equal.trans(Bool, EN.oks(~K, ~V, xa, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), EN.oks(~K, ~V, xa, nl, pl), True{}, oks_rest(~K, ~V, ~cmp, ~o, nl, pl, ui, si, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, hus, xa, hux, hsx), hx), L.and_intro(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), 1n+ui), ST.pv(V, PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si)), 1n+ui))), EN.oks(~K, ~V, rr, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), oku, Equal.trans(Bool, EN.oks(~K, ~V, rr, PR.wr_nl(K, nl, 1n+ui, M.N{c0, a0, b0, q0, ks}), PR.ex_pl(V, PR.ex_pl(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si, None{}), 1n+ui, ST.pv(V, PR.ex_pl(V, pl, 1n+ui, None{}), 1n+si))), EN.oks(~K, ~V, rr, nl, pl), True{}, oks_rest(~K, ~V, ~cmp, ~o, nl, pl, ui, si, c0, a0, b0, q0, ks, cs0, as0, bs0, qs0, hb, hbp, hsn, hus, rr, hur, hsr), okr)))

# ---- the right subtree is no bigger than the tree ----


def sublen(+c: List<&2, P.Fr>, +ui: Nat, +ta: ST.Tr, +tb: ST.Tr) -> {Nat.is_le(SC.length(Nat, ST.ids(tb)), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))))) == True{} : Bool}:
  +s2 = L.subst(Nat, z => {Nat.is_le(SC.length(Nat, Con{1n+ui, ST.ids(tb)}), z) == True{} : Bool}, Nat.add(SC.length(Nat, ST.ids(ta)), SC.length(Nat, Con{1n+ui, ST.ids(tb)})), SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), Equal.sym(Nat, SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), Nat.add(SC.length(Nat, ST.ids(ta)), SC.length(Nat, Con{1n+ui, ST.ids(tb)})), LL.length_append(Nat, ST.ids(ta), Con{1n+ui, ST.ids(tb)})), TR.le_add_l(SC.length(Nat, ST.ids(ta)), SC.length(Nat, Con{1n+ui, ST.ids(tb)})))
  +s3 = L.subst(Nat, z => {Nat.is_le(SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), z) == True{} : Bool}, Nat.add(SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), SC.length(Nat, P.after(c))), SC.length(Nat, SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), Nat.add(SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), SC.length(Nat, P.after(c))), LL.length_append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), N.le_add_right(SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), SC.length(Nat, P.after(c))))
  +s4 = L.subst(Nat, z => {Nat.is_le(SC.length(Nat, SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), z) == True{} : Bool}, Nat.add(SC.length(Nat, P.before(c)), SC.length(Nat, SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), Nat.add(SC.length(Nat, P.before(c)), SC.length(Nat, SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), LL.length_append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), TR.le_add_l(SC.length(Nat, P.before(c)), SC.length(Nat, SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))))
  N.le_trans(SC.length(Nat, ST.ids(tb)), SC.length(Nat, Con{1n+ui, ST.ids(tb)}), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), N.le_succ(SC.length(Nat, ST.ids(tb))), N.le_trans(SC.length(Nat, Con{1n+ui, ST.ids(tb)}), SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), s2, N.le_trans(SC.length(Nat, ST.ids(ST.TN{1n+ui, ta, tb})), SC.length(Nat, SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c))), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, ta, tb}), P.after(c)))), s3, s4)))