proofs/containers/balanced_search_tree/rmp.bend source

proofs/containers/balanced_search_tree/rmp.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/list.bend as LLimport ../../lib/order.bend as Oimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/balanced_search_tree/main.bend as Simport ../../../src/containers/balanced_search_tree.bend as Mimport ./state.bend as STimport ./mirror.bend as MIimport ./ok.bend as OKimport ./find.bend as FIimport ./ends.bend as ENimport ./path.bend as Pimport ./plug.bend as PGimport ./ord.bend as ORimport ./slot.bend as SLimport ./prim.bend as PRimport ./tree.bend as TRimport ../../lib/nat.bend as Nimport ./succ.bend as SUimport ./rmv.bend as RVimport ./mokx.bend as MXimport ./dord.bend as DO# The polls: the first (last) id of the header is the leftmost (rightmost)# node, reached from the root by a path of left (right) turns; it is removed# as remove removes it, with its own key, and its entry is the answer: the# specification's poll. (source: tools/generators/tm_hand/rmp.src)# ---- poll_first ----# the entries: the node's firstdef pf_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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +cs: List<&2, P.Fr>, +ui: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, ST.TE{}, sb}) == tg : ST.Tr}, +hlb: {P.before(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hy: {ST.nd(K, nl, 1n+ui) == M.N{c0, x1, x2, x3, kU} : M.Node<K>}, +hmi: {ST.pv(V, pl, 1n+ui) == Some{vU} : Maybe<&2, V>}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl)} : List<&2, M.Entry<K, V>>}:  +e2 = L.subst(Maybe<&2, V>, z => {ST.ents(~K, ~V, Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}, nl, pl) == ST.cons_m(M.Entry<K, V>, ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, z), ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl)) : List<&2, M.Entry<K, V>>}, ST.pv(V, pl, 1n+ui), Some{vU}, hmi, L.subst(M.Node<K>, z => {ST.ents(~K, ~V, Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}, nl, pl) == ST.cons_m(M.Entry<K, V>, ST.ent(K, V, z, ST.pv(V, pl, 1n+ui)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl)) : List<&2, M.Entry<K, V>>}, ST.nd(K, nl, 1n+ui), M.N{c0, x1, x2, x3, kU}, hy, {==}))  Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}, nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), 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<K, V>>}, ST.ids(tg), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}, L.subst(List<&2, Nat>, z => {ST.ids(tg) == SC.append(Nat, z, Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}) : List<&2, Nat>}, P.before(cs), Nil{}, hlb, Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))), 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(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), hlw))), {==}), e2)# the specification's poll: the first entry, the restdef pf_sp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +cs: List<&2, P.Fr>, +ui: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, ST.TE{}, sb}) == tg : ST.Tr}, +hlb: {P.before(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hy: {ST.nd(K, nl, 1n+ui) == M.N{c0, x1, x2, x3, kU} : M.Node<K>}, +hmi: {ST.pv(V, pl, 1n+ui) == Some{vU} : Maybe<&2, V>}) -> {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{M.Entry{kU, vU}}) == S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}:  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl)}, pf_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, cs, ui, sb, hlw, hlp, hlb, hlr, hlc, c0, x1, x2, x3, kU, vU, hy, hmi)) : {(S.TM{l, S.del(~K, ~V, ~cmp, kU, _)}, Some{M.Entry{kU, vU}}) == S.poll_first_entry(K, V, S.TM{l, _}) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}  %Equal.sym(Cmp, cmp(kU, kU), EQ{}, O.refl(~K, ~cmp, ~o, kU)) : {(S.TM{l, S.pick(List<&2, M.Entry<K, V>>, S.is_eq(_), ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl), Con{M.Entry{kU, vU}, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl))})}, Some{M.Entry{kU, vU}}) == (S.TM{l, ST.ents(~K, ~V, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl)}, Some{M.Entry{kU, vU}}) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}  {==}def pf_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<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}, +cs: List<&2, P.Fr>, +ui: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, ST.TE{}, sb}) == tg : ST.Tr}, +hlb: {P.before(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +hy: {ST.nd(K, nl, 1n+ui) == M.N{c0, x1, x2, x3, kU} : M.Node<K>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+ui) == m : Maybe<&2, V>}, +hs: {S.is_some(M.Entry<K, V>, ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, m)) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, M.N{c0, x1, x2, x3, kU}), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), m))):  match m:    case None{}:      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, M.N{c0, x1, x2, x3, kU}), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), None{}))), L.false_true(hs))    case Some{+vU}:      +hbc = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))), 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(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), hlw))      +hplug = Equal.sym(ST.Tr, PG.plug(cs, ST.TN{1n+ui, ST.TE{}, sb}), tg, hlp)      L.subst(S.Model<K, V> & Maybe<&2, M.Entry<K, V>>, z => OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, z, MI.entry_value(~K, ~V, ~cmp, Some{kU}, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), Some{vU}))), (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{M.Entry{kU, vU}}), S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), pf_sp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, cs, ui, sb, hlw, hlp, hlb, hlr, hlc, c0, x1, x2, x3, kU, vU, hy, hmi), MX.ev_mok(~K, ~V, ~cmp, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), kU, vU, L.subst(Maybe<&2, V>, z => 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))}, z), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), z)), ST.pv(V, pl, 1n+ui), Some{vU}, hmi, RV.rm_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, kU, cs, ui, ST.TE{}, sb, hbc, hplug, hlr, hlc, L.subst(M.Node<K>, z => {S.is_eq(TR.kc(~K, ~cmp, kU, z)) == True{} : Bool}, M.N{c0, x1, x2, x3, kU}, ST.nd(K, nl, 1n+ui), Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+ui), M.N{c0, x1, x2, x3, kU}, hy), 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)), {==})), M.N{c0, x1, x2, x3, kU}, hy))))def pf_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<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}, +cs: List<&2, P.Fr>, +ui: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, ST.TE{}, sb}) == tg : ST.Tr}, +hlb: {P.before(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +y: M.Node<K>, +hy: {ST.nd(K, nl, 1n+ui) == y : M.Node<K>}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, y), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, y))), ST.pv(V, pl, 1n+ui)))):  match y:    case M.Free{f}:      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, M.Free{f}), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.Free{f}))), ST.pv(V, pl, 1n+ui)))), L.false_true(L.subst(M.Node<K>, z => {ST.is_node(K, z, 0n, ST.rid(sb), P.top(cs)) == True{} : Bool}, ST.nd(K, nl, 1n+ui), M.Free{f}, hy, TR.rep_node(~K, 1n+ui, ST.TE{}, sb, P.top(cs), nl, hlr))))    case M.N{+c0, +x1, +x2, +x3, +kU}:      +hk = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}, L.subst(List<&2, Nat>, z => {ST.ids(tg) == SC.append(Nat, z, Con{1n+ui, SC.append(Nat, ST.ids(sb), P.after(cs))}) : List<&2, Nat>}, P.before(cs), Nil{}, hlb, Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))), 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(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, ST.TE{}, sb}), P.after(cs))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), hlw))), 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)))      +hs0 = L.and_left(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, SC.append(Nat, ST.ids(sb), P.after(cs)), nl, pl), hk)      pf_r(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, ui, sb, hlw, hlp, hlb, hlr, hlc, c0, x1, x2, x3, kU, hy, ST.pv(V, pl, 1n+ui), {==}, L.subst(M.Node<K>, z => {S.is_some(M.Entry<K, V>, ST.ent(K, V, z, ST.pv(V, pl, 1n+ui))) == True{} : Bool}, ST.nd(K, nl, 1n+ui), M.N{c0, x1, x2, x3, kU}, hy, hs0))def pf_o(~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}, +cs: List<&2, P.Fr>, +s: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hs0: {s == ST.fst0(ST.ids(tg)) : Nat}, +hlp: {PG.plug(cs, ST.TN{s, ST.TE{}, sb}) == tg : ST.Tr}, +hlb: {P.before(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{s, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, s, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.fst0(ST.ids(tg)))):  match s:    case 0n:      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.fst0(ST.ids(tg)))), L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), 0n, ST.rid(sb), P.top(cs)), Bool.and(True{}, ST.rep(~K, sb, 0n, nl))), hlr)))    case 1n+ui:      %Equal.sym(Nat, ST.fst0(ST.ids(tg)), 1n+ui, Equal.sym(Nat, 1n+ui, ST.fst0(ST.ids(tg)), hs0)) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))      pf_q(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, ui, sb, hlw, hlp, hlb, hlr, hlc, ST.nd(K, nl, 1n+ui), {==})def pf_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<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}, +cs: List<&2, P.Fr>, +s: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hs0: {s == ST.fst0(ST.ids(tg)) : Nat}, +hlp: {PG.plug(cs, ST.TN{s, ST.TE{}, sb}) == tg : ST.Tr}, +hlb: {P.before(cs) == Nil{} : List<&2, Nat>}, r2: {ST.rep(~K, ST.TN{s, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool} & {P.ctxok(~K, cs, s, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.fst0(ST.ids(tg)))):  match r2:    case Tuple{hlr, hlc}:      pf_o(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, s, sb, hlw, hs0, hlp, hlb, hlr, hlc)def pf_mm(~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}, +cs: List<&2, P.Fr>, +s: Nat, +sb: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, ST.TE{}, sb}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hs0: {s == ST.fst0(ST.ids(tg)) : Nat}, rest: {PG.plug(cs, ST.TN{s, ST.TE{}, sb}) == tg : ST.Tr} & ({P.before(cs) == Nil{} : List<&2, Nat>} & ({ST.rep(~K, ST.TN{s, ST.TE{}, sb}, P.top(cs), nl) == True{} : Bool} & {P.ctxok(~K, cs, s, nl) == True{} : Bool}))) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.fst0(ST.ids(tg)))):  match rest:    case Tuple{hlp, Tuple{hlb, r2}}:      pf_n(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, s, sb, hlw, hs0, hlp, hlb, r2)def pf_l(~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}, lm: Sigma<&1, &1, List<&2, P.Fr>, lc_ => Sigma<&1, &1, Nat, ls_ => Sigma<&1, &1, ST.Tr, lb_ => {SC.append(Nat, P.before(lc_), SC.append(Nat, ST.ids(ST.TN{ls_, ST.TE{}, lb_}), P.after(lc_))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>} & ({ls_ == ST.fst0(ST.ids(tg)) : Nat} & ({PG.plug(lc_, ST.TN{ls_, ST.TE{}, lb_}) == tg : ST.Tr} & ({P.before(lc_) == Nil{} : List<&2, Nat>} & ({ST.rep(~K, ST.TN{ls_, ST.TE{}, lb_}, P.top(lc_), nl) == True{} : Bool} & {P.ctxok(~K, lc_, ls_, nl) == True{} : Bool}))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.fst0(ST.ids(tg)))):  match lm:    case Tuple{+cs, Tuple{+s, Tuple{+sb, Tuple{hlw, Tuple{hs0, rest}}}}}:      pf_mm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, s, sb, hlw, hs0, rest)def pf_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.fst0(ST.ids(tg)))):  match tg:    case ST.TE{}:      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, ST.TE{}, fl}, (None{}, ({==}, ({==}, hg))))    case ST.TN{+j, +a, +b}:      pf_l(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, ST.TN{j, a, b}, fl, hg, SU.lmost(~K, ~cmp, ~o, a, nl, Nil{}, j, b, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, ST.TN{j, a, b}, fl, hg), {==}))def pf_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.poll_first_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})):  %Equal.sym(Nat, lo, ST.fst0(ST.ids(tg)), N.eq_from_is_eq(lo, ST.fst0(ST.ids(tg)), ST.g_clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))  pf_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)# ---- poll_last ----def pl_eid(~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>, +cs: List<&2, P.Fr>, +ui: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, sa, ST.TE{}}) == tg : ST.Tr}, +hla: {P.after(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}) -> {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}) : List<&2, Nat>}:  +ea = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), z)) : List<&2, Nat>}, P.after(cs), Nil{}, hla, {==})  +eb = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), Nil{})) == SC.append(Nat, P.before(cs), z) : List<&2, Nat>}, SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), Nil{}), ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), LL.append_nil(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}})), {==})  +ec = Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), SC.append(Nat, P.before(cs), ST.ids(ST.TN{1n+ui, sa, ST.TE{}})), LL.append_assoc(Nat, P.before(cs), ST.ids(sa), Con{1n+ui, Nil{}}))  Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))), SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))), 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(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), hlw)), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), Nil{})), SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), ea, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), Nil{})), SC.append(Nat, P.before(cs), ST.ids(ST.TN{1n+ui, sa, ST.TE{}})), SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), eb, ec)))# the entries: the node's lastdef pl_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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +cs: List<&2, P.Fr>, +ui: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, sa, ST.TE{}}) == tg : ST.Tr}, +hla: {P.after(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hy: {ST.nd(K, nl, 1n+ui) == M.N{c0, x1, x2, x3, kU} : M.Node<K>}, +hmi: {ST.pv(V, pl, 1n+ui) == Some{vU} : Maybe<&2, V>}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}) : List<&2, M.Entry<K, V>>}:  +e2 = L.subst(Maybe<&2, V>, z => {ST.ents(~K, ~V, Con{1n+ui, Nil{}}, nl, pl) == ST.cons_m(M.Entry<K, V>, ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, z), Nil{}) : List<&2, M.Entry<K, V>>}, ST.pv(V, pl, 1n+ui), Some{vU}, hmi, L.subst(M.Node<K>, z => {ST.ents(~K, ~V, Con{1n+ui, Nil{}}, nl, pl) == ST.cons_m(M.Entry<K, V>, ST.ent(K, V, z, ST.pv(V, pl, 1n+ui)), Nil{}) : List<&2, M.Entry<K, V>>}, ST.nd(K, nl, 1n+ui), M.N{c0, x1, x2, x3, kU}, hy, {==}))  +e1 = 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<K, V>>}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), pl_eid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, cs, ui, sa, hlw, hlp, hla, hlr, hlc), {==})  +e3 = FI.ents_app(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}, nl, pl)  +e4 = L.subst(List<&2, M.Entry<K, V>>, z => {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), ST.ents(~K, ~V, Con{1n+ui, Nil{}}, nl, pl)) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), z) : List<&2, M.Entry<K, V>>}, ST.ents(~K, ~V, Con{1n+ui, Nil{}}, nl, pl), Con{M.Entry{kU, vU}, Nil{}}, e2, {==})  Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}), e1, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), ST.ents(~K, ~V, Con{1n+ui, Nil{}}, nl, pl)), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}), e3, e4))# the specification's poll: the last entry, the ones beforedef pl_sp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +cs: List<&2, P.Fr>, +ui: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, sa, ST.TE{}}) == tg : ST.Tr}, +hla: {P.after(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hy: {ST.nd(K, nl, 1n+ui) == M.N{c0, x1, x2, x3, kU} : M.Node<K>}, +hmi: {ST.pv(V, pl, 1n+ui) == Some{vU} : Maybe<&2, V>}) -> {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{M.Entry{kU, vU}}) == S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}:  +eE = pl_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, cs, ui, sa, hlw, hlp, hla, hlr, hlc, c0, x1, x2, x3, kU, vU, hy, hmi)  +hord = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}), eE, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))  +eL = Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, kU, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}})), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Nil{}), ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), DO.del_mid(~K, ~V, ~cmp, ~o, kU, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}, Nil{}, OR.ord_mid_l(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}, Nil{}, hord), O.refl(~K, ~cmp, ~o, kU)), LL.append_nil(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl)))  +eI = L.subst(List<&2, M.Entry<K, V>>, z => {SC.init(M.Entry<K, V>, z) == ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl) : List<&2, M.Entry<K, V>>}, SC.snoc(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}), LL.snoc_append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}), LL.init_snoc(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}))  +eLa = L.subst(List<&2, M.Entry<K, V>>, z => {SC.last(M.Entry<K, V>, z) == Some{M.Entry{kU, vU}} : Maybe<&2, M.Entry<K, V>>}, SC.snoc(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}), LL.snoc_append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}), LL.last_snoc(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), M.Entry{kU, vU}))  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}), eE) : {(S.TM{l, S.del(~K, ~V, ~cmp, kU, _)}, Some{M.Entry{kU, vU}}) == S.poll_last_entry(K, V, S.TM{l, _}) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}  %Equal.sym(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, kU, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}})), ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), eL) : {(S.TM{l, _}, Some{M.Entry{kU, vU}}) == (S.TM{l, SC.init(M.Entry<K, V>, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}))}, S.last(M.Entry<K, V>, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}))) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}  %Equal.sym(List<&2, M.Entry<K, V>>, SC.init(M.Entry<K, V>, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}})), ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), eI) : {(S.TM{l, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl)}, Some{M.Entry{kU, vU}}) == (S.TM{l, _}, S.last(M.Entry<K, V>, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}}))) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last(M.Entry<K, V>, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl), Con{M.Entry{kU, vU}, Nil{}})), Some{M.Entry{kU, vU}}, eLa) : {(S.TM{l, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl)}, Some{M.Entry{kU, vU}}) == (S.TM{l, ST.ents(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), nl, pl)}, _) : S.Model<K, V> & Maybe<&2, M.Entry<K, V>>}  {==}def pl_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<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}, +cs: List<&2, P.Fr>, +ui: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, sa, ST.TE{}}) == tg : ST.Tr}, +hla: {P.after(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +hy: {ST.nd(K, nl, 1n+ui) == M.N{c0, x1, x2, x3, kU} : M.Node<K>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+ui) == m : Maybe<&2, V>}, +hs: {S.is_some(M.Entry<K, V>, ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, m)) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, M.N{c0, x1, x2, x3, kU}), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), m))):  match m:    case None{}:      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, M.N{c0, x1, x2, x3, kU}), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), None{}))), L.false_true(hs))    case Some{+vU}:      +hbc = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))), 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(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), hlw))      +hplug = Equal.sym(ST.Tr, PG.plug(cs, ST.TN{1n+ui, sa, ST.TE{}}), tg, hlp)      L.subst(S.Model<K, V> & Maybe<&2, M.Entry<K, V>>, z => OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, z, MI.entry_value(~K, ~V, ~cmp, Some{kU}, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), Some{vU}))), (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{M.Entry{kU, vU}}), S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), pl_sp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, ui, sa, hlw, hlp, hla, hlr, hlc, c0, x1, x2, x3, kU, vU, hy, hmi), MX.ev_mok(~K, ~V, ~cmp, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), kU, vU, L.subst(Maybe<&2, V>, z => 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))}, z), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.N{c0, x1, x2, x3, kU}))), z)), ST.pv(V, pl, 1n+ui), Some{vU}, hmi, RV.rm_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, kU, cs, ui, sa, ST.TE{}, hbc, hplug, hlr, hlc, L.subst(M.Node<K>, z => {S.is_eq(TR.kc(~K, ~cmp, kU, z)) == True{} : Bool}, M.N{c0, x1, x2, x3, kU}, ST.nd(K, nl, 1n+ui), Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+ui), M.N{c0, x1, x2, x3, kU}, hy), 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)), {==})), M.N{c0, x1, x2, x3, kU}, hy))))def pl_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<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}, +cs: List<&2, P.Fr>, +ui: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{1n+ui, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hlp: {PG.plug(cs, ST.TN{1n+ui, sa, ST.TE{}}) == tg : ST.Tr}, +hla: {P.after(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{1n+ui, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, 1n+ui, nl) == True{} : Bool}, +y: M.Node<K>, +hy: {ST.nd(K, nl, 1n+ui) == y : M.Node<K>}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, y), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, y))), ST.pv(V, pl, 1n+ui)))):  match y:    case M.Free{f}:      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, M.Free{f}), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+ui, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+ui, None{}), tg, fl}, M.Free{f}))), ST.pv(V, pl, 1n+ui)))), L.false_true(L.subst(M.Node<K>, z => {ST.is_node(K, z, ST.rid(sa), 0n, P.top(cs)) == True{} : Bool}, ST.nd(K, nl, 1n+ui), M.Free{f}, hy, TR.rep_node(~K, 1n+ui, sa, ST.TE{}, P.top(cs), nl, hlr))))    case M.N{+c0, +x1, +x2, +x3, +kU}:      +hk = 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(cs), ST.ids(sa)), Con{1n+ui, Nil{}}), pl_eid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, cs, ui, sa, hlw, hlp, hla, hlr, hlc), 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)))      +hs0 = L.and_left(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, Nil{}, nl, pl), SL.oks_split_r(~K, ~V, SC.append(Nat, P.before(cs), ST.ids(sa)), Con{1n+ui, Nil{}}, nl, pl, hk))      pl_r(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, ui, sa, hlw, hlp, hla, hlr, hlc, c0, x1, x2, x3, kU, hy, ST.pv(V, pl, 1n+ui), {==}, L.subst(M.Node<K>, z => {S.is_some(M.Entry<K, V>, ST.ent(K, V, z, ST.pv(V, pl, 1n+ui))) == True{} : Bool}, ST.nd(K, nl, 1n+ui), M.N{c0, x1, x2, x3, kU}, hy, hs0))def pl_o(~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}, +cs: List<&2, P.Fr>, +s: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hs0: {s == ST.last0(ST.ids(tg)) : Nat}, +hlp: {PG.plug(cs, ST.TN{s, sa, ST.TE{}}) == tg : ST.Tr}, +hla: {P.after(cs) == Nil{} : List<&2, Nat>}, +hlr: {ST.rep(~K, ST.TN{s, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool}, +hlc: {P.ctxok(~K, cs, s, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.last0(ST.ids(tg)))):  match s:    case 0n:      Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.last0(ST.ids(tg)))), L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.rid(sa), 0n, P.top(cs)), Bool.and(ST.rep(~K, sa, 0n, nl), True{})), hlr)))    case 1n+ui:      %Equal.sym(Nat, ST.last0(ST.ids(tg)), 1n+ui, Equal.sym(Nat, 1n+ui, ST.last0(ST.ids(tg)), hs0)) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))      pl_q(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, ui, sa, hlw, hlp, hla, hlr, hlc, ST.nd(K, nl, 1n+ui), {==})def pl_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<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}, +cs: List<&2, P.Fr>, +s: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hs0: {s == ST.last0(ST.ids(tg)) : Nat}, +hlp: {PG.plug(cs, ST.TN{s, sa, ST.TE{}}) == tg : ST.Tr}, +hla: {P.after(cs) == Nil{} : List<&2, Nat>}, r2: {ST.rep(~K, ST.TN{s, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool} & {P.ctxok(~K, cs, s, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.last0(ST.ids(tg)))):  match r2:    case Tuple{hlr, hlc}:      pl_o(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, s, sa, hlw, hs0, hlp, hla, hlr, hlc)def pl_mm(~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}, +cs: List<&2, P.Fr>, +s: Nat, +sa: ST.Tr, +hlw: {SC.append(Nat, P.before(cs), SC.append(Nat, ST.ids(ST.TN{s, sa, ST.TE{}}), P.after(cs))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +hs0: {s == ST.last0(ST.ids(tg)) : Nat}, rest: {PG.plug(cs, ST.TN{s, sa, ST.TE{}}) == tg : ST.Tr} & ({P.after(cs) == Nil{} : List<&2, Nat>} & ({ST.rep(~K, ST.TN{s, sa, ST.TE{}}, P.top(cs), nl) == True{} : Bool} & {P.ctxok(~K, cs, s, nl) == True{} : Bool}))) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.last0(ST.ids(tg)))):  match rest:    case Tuple{hlp, Tuple{hla, r2}}:      pl_n(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, s, sa, hlw, hs0, hlp, hla, r2)def pl_l(~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}, lm: Sigma<&1, &1, List<&2, P.Fr>, rc_ => Sigma<&1, &1, Nat, rs_ => Sigma<&1, &1, ST.Tr, ra_ => {SC.append(Nat, P.before(rc_), SC.append(Nat, ST.ids(ST.TN{rs_, ra_, ST.TE{}}), P.after(rc_))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>} & ({rs_ == ST.last0(ST.ids(tg)) : Nat} & ({PG.plug(rc_, ST.TN{rs_, ra_, ST.TE{}}) == tg : ST.Tr} & ({P.after(rc_) == Nil{} : List<&2, Nat>} & ({ST.rep(~K, ST.TN{rs_, ra_, ST.TE{}}, P.top(rc_), nl) == True{} : Bool} & {P.ctxok(~K, rc_, rs_, nl) == True{} : Bool}))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.last0(ST.ids(tg)))):  match lm:    case Tuple{+cs, Tuple{+s, Tuple{+sa, Tuple{hlw, Tuple{hs0, rest}}}}}:      pl_mm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, cs, s, sa, hlw, hs0, rest)def pl_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.last0(ST.ids(tg)))):  match tg:    case ST.TE{}:      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, ST.TE{}, fl}, (None{}, ({==}, ({==}, hg))))    case ST.TN{+j, +a, +b}:      pl_l(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, ST.TN{j, a, b}, fl, hg, SU.rmost(~K, ~cmp, ~o, b, nl, Nil{}, j, a, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, ST.TN{j, a, b}, fl, hg), {==}))def pl_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.poll_last_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})):  %Equal.sym(Nat, hi, ST.last0(ST.ids(tg)), N.eq_from_is_eq(hi, ST.last0(ST.ids(tg)), ST.g_chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.remove_entry_id(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))  pl_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)