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 ./mirror.bend as MI import ./ok.bend as OK import ./tree.bend as TR import ./ends.bend as EN import ./path.bend as P import ./plug.bend as PG import ./ord.bend as OR import ./cur.bend as CU import ./reads.bend as RD import ./find.bend as FI import ./slot.bend as SL import ./cnx.bend as CX import ./crk.bend as CK import ./dord.bend as DO import ./prim.bend as PR import ./fix.bend as FX import ../../lib/nat_list.bend as NL # iterator_remove: the current id's node removed (as remove removes it) and # the cursor re-seeking its next key, which stays present; the mirror's # search after the removal answers as the good shadow's (given as a fact about # searches: they read only the real map). (source: tools/generators/tm_hand/crm.src) # ---- facts at a member ---- def sr_p(s: M.Search) -> Nat: match s: case M.Search{i, p, lft}: p def sr_l(s: M.Search) -> Bool: match s: case M.Search{i, p, lft}: lft def sr_eta(+s: M.Search) -> {s == M.Search{FI.sfound(s), sr_p(s), sr_l(s)} : M.Search}: match s: case M.Search{+i, +p, +lft}: {==} # a node's id among ok ids is one of them def mem_c(-K: Data, +nl: List<&2, M.Node>, +xs: List<&2, Nat>, +j: Nat, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +hx: {ST.nd(K, nl, j) == M.N{c0, x1, x2, x3, k} : M.Node}, +h: {CU.idok(xs, j) == True{} : Bool}) -> {NL.memn(j, xs) == True{} : Bool}: match j: case 0n: Empty.absurd({NL.memn(0n, xs) == True{} : Bool}, L.none_some(K, k, L.subst(M.Node, z => {M.node_key(~K, z) == Some{k} : Maybe<&2, K>}, M.N{c0, x1, x2, x3, k}, ST.nd(K, nl, 0n), Equal.sym(M.Node, ST.nd(K, nl, 0n), M.N{c0, x1, x2, x3, k}, hx), {==}))) case 1n+i: h # a member's entry is some def some_at_s(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +j: Nat, +hk: {EN.oks(~K, ~V, xs, nl, pl) == True{} : Bool}, r: Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {xs == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>) -> {S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))) == True{} : Bool}: match r: case Tuple{+sa, Tuple{+sb, h}}: L.and_left(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, sb, nl, pl), SL.oks_split_r(~K, ~V, sa, Con{j, sb}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, xs, SC.append(Nat, sa, Con{j, sb}), h, hk))) # ---- no current id: nothing removed, the cursor re-seeks its next key ---- def rmz_n(~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>, +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}, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +hx: {ST.nd(K, nl, nx) == M.N{c0, x1, x2, x3, k} : M.Node}, +hmem: {NL.memn(nx, ST.ids(tg)) == True{} : Bool}, +m: Maybe<&2, V>, +hm: {ST.pv(V, pl, nx) == m : Maybe<&2, V>}, +hs: {S.is_some(M.Entry, ST.ent(K, V, M.N{c0, x1, x2, x3, k}, m)) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_p(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_l(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))}))): match m: case None{}: Empty.absurd(CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_p(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_l(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))}))), L.false_true(hs)) case Some{+v}: +hfe = CK.find_in(~K, ~V, ~cmp, ~o, nl, pl, ST.ids(tg), nx, hmem, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), c0, x1, x2, x3, k, hx, v, hm) +hfind = L.subst(Maybe<&2, M.Entry>, z => {S.val_m(K, V, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == S.val_m(K, V, z) : Maybe<&2, V>}, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{M.Entry{k, v}}, hfe, {==}) +esp = L.subst(Maybe<&2, K>, z => {(S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}, None{}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, z, None{}, lo2, hi2, fw}, None{}) : S.Cursor & Maybe<&2, V>}, Some{k}, CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Some{k}, Pair.fst({CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == Some{k} : Maybe<&2, K>}, {CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hfind))), {==}) (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n, lo2, hi2, fw}, (None{}, ({==}, (esp, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n))))), hg, L.and_intro(CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Bool.and(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n)))), Pair.snd({CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == Some{k} : Maybe<&2, K>}, {CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hfind)), L.and_intro(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n))), {==}, CU.or_not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n))))))))) def rmz_x(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +x: M.Node, +hx: {ST.nd(K, nl, nx) == x : M.Node}, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, M.node_key(~K, x), None{}, lo2, hi2, fw}), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, x), lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, None{}))): match x: case M.Free{f}: (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 0n, 0n, lo2, hi2, fw}, (None{}, ({==}, ({==}, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(0n, 0n), Bool.not(Nat.is_eq(0n, 0n))))), hg, {==}))))) case M.N{+c0, +x1, +x2, +x3, +k}: %Equal.sym(ST.Sh & 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)) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, _)) %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_p(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_l(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))}, sr_eta(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))) +hmem = mem_c(K, nl, ST.ids(tg), nx, c0, x1, x2, x3, k, hx, L.and_left(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n))))), hc))) +hs0 = some_at_s(~K, ~V, nl, pl, ST.ids(tg), nx, 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)), CK.split_mem(ST.ids(tg), nx, hmem)) rmz_n(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, fw, nx, c0, x1, x2, x3, k, hx, hmem, ST.pv(V, pl, nx), {==}, L.subst(M.Node, z => {S.is_some(M.Entry, ST.ent(K, V, z, ST.pv(V, pl, nx))) == True{} : Bool}, ST.nd(K, nl, nx), M.N{c0, x1, x2, x3, k}, hx, hs0)) def rmz(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})): rmz_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n))))), hc), lo2, hi2, fw, nx, ST.nd(K, nl, nx), {==}, hc) # ---- a current node: removed, then the next key re-sought ---- # no next node: the cursor at nothing, over the shadow after the removal def rmn3(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +erp: {(M.Cursor{ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j)) == (M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), 0n, 0n, lo2, hi2, fw}, oa) : M.Cursor & Maybe<&2, V>}, +esp: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>}, +hg2: {ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): +em = L.pair_fst(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp) +eo = Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), oa, hfu, L.pair_snd(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp)) (MI.MC{ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, 0n, 0n, lo2, hi2, fw}, (oa, (erp, (L.pair_eq(S.Cursor, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.CR{ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), None{}, None{}, lo2, hi2, fw}, oa, L.subst(S.Model, z => {S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw} == S.CR{z, None{}, None{}, lo2, hi2, fw} : S.Cursor}, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), em, {==}), eo), L.and_intro(ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2), Bool.and(True{}, Bool.and(True{}, True{})), hg2, {==}))))) def rmn_m3(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : M.TreeMap & Maybe<&2, V>}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): match r: case Tuple{esp, hg2}: +ea = L.pair_fst(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0) +eb = L.pair_snd(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0) rmn3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, L.pair_eq(M.Cursor, Maybe<&2, V>, M.Cursor{ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j), M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), 0n, 0n, lo2, hi2, fw}, oa, L.subst(M.TreeMap, z => {M.Cursor{ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), 0n, 0n, lo2, hi2, fw} == M.Cursor{z, 0n, 0n, lo2, hi2, fw} : M.Cursor}, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), ea, {==}), eb), esp, hg2) def rmn_m2(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +sh2: ST.Sh, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, sh2), oa) : M.TreeMap & Maybe<&2, V>}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, sh2), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): match sh2: case ST.SH{+n2, +r2, +lo3, +hi3, +fr2, +l2, +d2, +nl2, +pl2, +t2, +fl2}: rmn_m3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, erp0, r) def rmn_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, rmr: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): match rmr: case Tuple{+sh2, Tuple{+oa, Tuple{+erp0, r}}}: rmn_m2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, sh2, oa, erp0, r) # ---- a next key: re-sought after the removal ---- def tm_es(-K: Data, -V: Data, m: S.Model) -> List<&2, M.Entry>: match m: case S.TM{+l, +es}: es def rmk3(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +ea: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}) : M.TreeMap}, +eb: {ST.pv(V, pl, 1n+j) == oa : Maybe<&2, V>}, +esp: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>}, +hg2: {ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2) == True{} : Bool}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, ST.pv(V, pl, 1n+j), MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))): +eps = Equal.trans(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), M.Search{FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_p(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_l(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)))}), L.pair_eta(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), L.subst(M.Search, z => {(Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))) == (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), z) : ST.Sh & M.Search}, Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), M.Search{FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_p(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_l(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)))}, sr_eta(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), {==})) +hrp0 = Equal.trans(M.TreeMap & M.Search, MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, k2)), (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), hst(k2, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, ea, OK.dg_good(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, hg2)), L.subst(ST.Sh & M.Search, z => {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, k2)) == MI.rp(~K, ~V, ~cmp, M.Search, z) : M.TreeMap & M.Search}, MI.search(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, k2), (ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), RD.search_m(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, k2, hg2), {==})) +hrp = L.subst(ST.Sh & M.Search, z => {MI.rp(~K, ~V, ~cmp, M.Search, z) == (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})) : M.TreeMap & M.Search}, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), L.pair_eta(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), hrp0) +e1 = L.pair_fst(M.TreeMap, M.Search, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}), hrp) +e3 = L.subst(M.Search, z => {FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))) == FI.sfound(z) : Nat}, Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}), L.pair_snd(M.TreeMap, M.Search, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}), hrp), {==}) %Equal.sym(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), M.Search{FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_p(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_l(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)))}), eps) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, ST.pv(V, pl, 1n+j), _)) +em = L.pair_fst(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp) +eo = Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), oa, hfu, L.pair_snd(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp)) +ees = L.subst(S.Model, z => {S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == tm_es(K, V, z) : List<&2, M.Entry>}, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), em, {==}) +hfk = L.subst(List<&2, M.Entry>, z => {S.find(~K, ~V, ~cmp, k2, z) == Some{w2} : Maybe<&2, V>}, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, ST.ids(t2), nl2, pl2), ees, hfd2) +ecur = L.subst(Nat, z => {M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw} == M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), z, 0n, lo2, hi2, fw} : M.Cursor}, FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), e3, L.subst(M.TreeMap, z => {M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw} == M.Cursor{z, FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw} : M.Cursor}, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), e1, {==})) +esc = L.subst(Maybe<&2, K>, z => {S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw} == S.CR{ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), z, None{}, lo2, hi2, fw} : S.Cursor}, Some{k2}, CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Some{k2}, Pair.fst({CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == Some{k2} : Maybe<&2, K>}, {CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, hg2, k2, w2, hfk))), L.subst(S.Model, z => {S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw} == S.CR{z, Some{k2}, None{}, lo2, hi2, fw} : S.Cursor}, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), em, {==})) +cg = L.and_intro(ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2), Bool.and(CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Bool.and(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n))))), hg2, L.and_intro(CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Bool.and(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n)))), Pair.snd({CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == Some{k2} : Maybe<&2, K>}, {CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, hg2, k2, w2, hfk)), L.and_intro(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n))), {==}, CU.or_not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n))))) (MI.MC{ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n, lo2, hi2, fw}, (oa, (L.pair_eq(M.Cursor, Maybe<&2, V>, M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j), M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n, lo2, hi2, fw}, oa, ecur, eb), (L.pair_eq(S.Cursor, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.CR{ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), None{}, lo2, hi2, fw}, oa, esc, eo), cg)))) def rmk_m3(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : M.TreeMap & Maybe<&2, V>}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, ST.pv(V, pl, 1n+j), MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))): match r: case Tuple{esp, hg2}: rmk3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, L.pair_fst(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0), L.pair_snd(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0), esp, hg2, k2, w2, hfd2, hst) def rmk_m2(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +sh2: ST.Sh, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, sh2), oa) : M.TreeMap & Maybe<&2, V>}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, sh2), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, ST.pv(V, pl, 1n+j), MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))): match sh2: case ST.SH{+n2, +r2, +lo3, +hi3, +fr2, +l2, +d2, +nl2, +pl2, +t2, +fl2}: rmk_m3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, erp0, k2, w2, hfd2, hst, r) def rmk_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, rmr: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, ST.pv(V, pl, 1n+j), MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))): match rmr: case Tuple{+sh2, Tuple{+oa, Tuple{+erp0, r}}}: rmk_m2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, sh2, oa, erp0, k2, w2, hfd2, hst, r) # ---- the current node's facts, and the next node's ---- # the entries: those before and after the current node, with its own between def ru_est(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +j: Nat, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}) : List<&2, M.Entry>}: +eent = L.subst(Maybe<&2, V>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, z) : Maybe<&2, M.Entry>}, ST.pv(V, pl, 1n+j), Some{vU}, hmu, L.subst(M.Node, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, z, ST.pv(V, pl, 1n+j)) : Maybe<&2, M.Entry>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hxu, {==})) Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry>}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, {==}), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), FI.ents_app(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl), L.subst(Maybe<&2, M.Entry>, z => {SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) : List<&2, M.Entry>}, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), Some{M.Entry{kU, vU}}, eent, {==}))) # after the removal, the entries before and after: the next key found there def ru_fd(~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>, +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}, +j: Nat, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +nx: Nat, +hmxy: {NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))) == True{} : Bool}, +d0: Bool, +y1: Nat, +y2: Nat, +y3: Nat, +k2: K, +hy: {ST.nd(K, nl, nx) == M.N{d0, y1, y2, y3, k2} : M.Node}, +w2: V, +hm2: {ST.pv(V, pl, nx) == Some{w2} : Maybe<&2, V>}) -> {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}: +edel = Equal.trans(List<&2, M.Entry>, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.del(~K, ~V, ~cmp, kU, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), L.subst(List<&2, M.Entry>, z => {S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.del(~K, ~V, ~cmp, kU, z) : List<&2, M.Entry>}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), ru_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu), {==}), Equal.trans(List<&2, M.Entry>, S.del(~K, ~V, ~cmp, kU, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), DO.del_mid(~K, ~V, ~cmp, ~o, kU, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), OR.ord_mid_l(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), ru_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), O.refl(~K, ~cmp, ~o, kU)), Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), FI.ents_app(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)))) +hordxy = L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), FI.ents_app(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), DO.ord_drop(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), ru_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))) +hfe = CK.find_in(~K, ~V, ~cmp, ~o, nl, pl, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nx, hmxy, hordxy, d0, y1, y2, y3, k2, hy, w2, hm2) L.subst(List<&2, M.Entry>, z => {S.val_m(K, V, S.find_e(~K, ~V, ~cmp, k2, z)) == Some{w2} : Maybe<&2, V>}, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.sym(List<&2, M.Entry>, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), edel), L.subst(Maybe<&2, M.Entry>, z => {S.val_m(K, V, z) == Some{w2} : Maybe<&2, V>}, Some{M.Entry{k2, w2}}, S.find_e(~K, ~V, ~cmp, k2, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl)), Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k2, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl)), Some{M.Entry{k2, w2}}, hfe), {==})) def ne0y(-K: Data, +nl: List<&2, M.Node>, +nx: Nat, +d0: Bool, +y1: Nat, +y2: Nat, +y3: Nat, +k2: K, +hy: {ST.nd(K, nl, nx) == M.N{d0, y1, y2, y3, k2} : M.Node}) -> {Nat.is_eq(nx, 0n) == False{} : Bool}: match nx: case 0n: Empty.absurd({True{} == False{} : Bool}, L.none_some(K, k2, L.subst(M.Node, z => {M.node_key(~K, z) == Some{k2} : Maybe<&2, K>}, M.N{d0, y1, y2, y3, k2}, ST.nd(K, nl, 0n), Equal.sym(M.Node, ST.nd(K, nl, 0n), M.N{d0, y1, y2, y3, k2}, hy), {==}))) case 1n+i: {==} def ru_w(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +d0: Bool, +y1: Nat, +y2: Nat, +y3: Nat, +k2: K, +hy: {ST.nd(K, nl, nx) == M.N{d0, y1, y2, y3, k2} : M.Node}, +hmxy: {NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))) == True{} : Bool}, +m2: Maybe<&2, V>, +hm2: {ST.pv(V, pl, nx) == m2 : Maybe<&2, V>}, +hs: {S.is_some(M.Entry, ST.ent(K, V, M.N{d0, y1, y2, y3, k2}, m2)) == True{} : Bool}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, rmr: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, M.node_key(~K, M.N{d0, y1, y2, y3, k2}), None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, M.N{d0, y1, y2, y3, k2}), lo2, hi2, fw, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))): match m2: case None{}: Empty.absurd(CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, M.node_key(~K, M.N{d0, y1, y2, y3, k2}), None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, M.N{d0, y1, y2, y3, k2}), lo2, hi2, fw, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))), L.false_true(hs)) case Some{+w2}: rmk_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, k2, w2, ru_fd(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc), j, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu, nx, hmxy, d0, y1, y2, y3, k2, hy, w2, hm2), hst, rmr) def ru_y(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +y: M.Node, +hy: {ST.nd(K, nl, nx) == y : M.Node}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, rmr: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, M.node_key(~K, y), None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, y), lo2, hi2, fw, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))): match y: case M.Free{f}: rmn_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, rmr) case M.N{+d0, +y1, +y2, +y3, +k2}: +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) +hmx = mem_c(K, nl, ST.ids(tg), nx, d0, y1, y2, y3, k2, hy, L.and_left(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))) +h0 = ne0y(K, nl, nx, d0, y1, y2, y3, k2, hy) +hnu = L.not_true(Nat.is_eq(nx, 1n+j), L.subst(Bool, z => {Bool.or(z, Bool.not(Nat.is_eq(nx, 1n+j))) == True{} : Bool}, Nat.is_eq(nx, 0n), False{}, h0, L.and_right(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))), L.and_right(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))))) +hm1 = L.subst(List<&2, Nat>, z => {NL.memn(nx, z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, hmx) +hor = Equal.trans(Bool, Bool.or(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), Nat.is_eq(1n+j, nx)), NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), True{}, Equal.sym(Bool, NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), Bool.or(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), Nat.is_eq(1n+j, nx)), NL.memn_mid(nx, SC.append(Nat, P.before(pc), ST.ids(pa)), 1n+j, SC.append(Nat, ST.ids(pb), P.after(pc)))), hm1) +hmxy = FX.or_f(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), L.subst(Bool, z => {Bool.or(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), z) == True{} : Bool}, Nat.is_eq(1n+j, nx), False{}, N.is_eq_sym_false(nx, 1n+j, hnu), hor)) +hs0 = some_at_s(~K, ~V, nl, pl, ST.ids(tg), nx, 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)), CK.split_mem(ST.ids(tg), nx, hmx)) ru_w(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu, hfu, d0, y1, y2, y3, k2, hy, hmxy, ST.pv(V, pl, nx), {==}, L.subst(M.Node, z => {S.is_some(M.Entry, ST.ent(K, V, z, ST.pv(V, pl, nx))) == True{} : Bool}, ST.nd(K, nl, nx), M.N{d0, y1, y2, y3, k2}, hy, hs0), hst, rmr) # the current node: its key's removal, then the next node def ru_u(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})): +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) +hfe = CK.find_in(~K, ~V, ~cmp, ~o, nl, pl, ST.ids(tg), 1n+j, L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))), L.and_right(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), c0, x1, x2, x3, kU, hxu, vU, hmu) +hfu = Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vU}, ST.pv(V, pl, 1n+j), L.subst(Maybe<&2, M.Entry>, z => {S.val_m(K, V, S.find_e(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == S.val_m(K, V, z) : Maybe<&2, V>}, S.find_e(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{M.Entry{kU, vU}}, hfe, {==}), Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), Some{vU}, hmu)) %Equal.sym(M.Node, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hxu) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), M.node_key(~K, _), lo2, hi2, fw}), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, ST.nd(K, nl, nx)), lo2, hi2, fw, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) ru_y(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu, hfu, ST.nd(K, nl, nx), {==}, hst, frm(kU, pc, pa, pb, hid, hplug, h3, h4, L.subst(M.Node, z => {S.is_eq(TR.kc(~K, ~cmp, kU, z)) == True{} : Bool}, M.N{c0, x1, x2, x3, kU}, ST.nd(K, nl, 1n+j), Equal.sym(M.Node, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hxu), L.subst(Cmp, w => {S.is_eq(w) == True{} : Bool}, EQ{}, cmp(kU, kU), Equal.sym(Cmp, cmp(kU, kU), EQ{}, O.refl(~K, ~cmp, ~o, kU)), {==})))) def ru_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, +x: M.Node, +hx: {ST.nd(K, nl, 1n+j) == x : M.Node}, +m: Maybe<&2, V>, +hm: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})): match x m: case M.Free{f} +m: Empty.absurd(CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), L.false_true(L.subst(M.Node, z => {ST.is_node(K, z, ST.rid(pa), ST.rid(pb), P.top(pc)) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.Free{f}, hx, TR.rep_node(~K, 1n+j, pa, pb, P.top(pc), nl, h3)))) case M.N{c0, x1, x2, x3, kU} None{}: +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) Empty.absurd(CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), L.false_true(L.subst(Maybe<&2, V>, z => {S.is_some(M.Entry, ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, z)) == True{} : Bool}, ST.pv(V, pl, 1n+j), None{}, hm, L.subst(M.Node, z => {S.is_some(M.Entry, ST.ent(K, V, z, ST.pv(V, pl, 1n+j))) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hx, L.and_left(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j))), EN.oks(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), SL.oks_split_r(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, 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))))))))) case M.N{+c0, +x1, +x2, +x3, +kU} Some{+vU}: ru_u(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hx, hm, hid, hplug, h3, h4, frm, hst) def ru_r(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +h2: {PG.plug(pc, ST.TN{1n+j, pa, pb}) == PG.plug(Nil{}, tg) : ST.Tr}, r3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})): match r3: case Tuple{h3, h4}: +hid = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), h1)) +e1 = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(pc), z) : List<&2, Nat>}, SC.append(Nat, SC.append(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}), P.after(pc)), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), LL.append_assoc(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}, P.after(pc)), {==}) +e2 = Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), LL.append_assoc(Nat, P.before(pc), ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})) +hw = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hid, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), e1, e2)) ru_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, hid, Equal.sym(ST.Tr, PG.plug(pc, ST.TN{1n+j, pa, pb}), tg, h2), h3, h4, frm, hst, ST.nd(K, nl, 1n+j), {==}, ST.pv(V, pl, 1n+j), {==}) def ru_q(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, rest: {PG.plug(pc, ST.TN{1n+j, pa, pb}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool})) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})): match rest: case Tuple{h2, r3}: ru_r(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, frm, hst, pc, pa, pb, h1, h2, r3) def ru_p(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, pt: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{1n+j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{1n+j, pa_, pb_}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, 1n+j, nl) == True{} : Bool}))>>>) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})): match pt: case Tuple{+pc, Tuple{+pa, Tuple{+pb, Tuple{h1, rest}}}}: ru_q(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, frm, hst, pc, pa, pb, h1, rest) # a current node: removed as remove removes it, the next key re-sought; # frm is the removal's refinement (RV.rm_x at the node's path), hst the # searches' agreement over the real map (the simulation's search) def rmu(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})): +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) ru_p(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, frm, hst, CX.path_to(~K, ~cmp, ~o, tg, nl, Nil{}, 1n+j, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), {==}, L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))), L.and_right(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)))))