proofs/containers/balanced_search_tree/rmf.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../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 ./tree.bend as TRimport ./path.bend as Pimport ./mirror.bend as MIimport ./ok.bend as OKimport ./ends.bend as ENimport ./slot.bend as SLimport ./xtr.bend as XTimport ../../lib/nat_list.bend as NL# The end of a removal: the unlinked tree's ends refreshed, the shadow with# the new tree and free chain satisfies the invariant, and its model is the# specification's removal, given the facts about the remaining ids.# (source: tools/generators/tm_hand/rmf.src)def rm_f3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +flf: List<&2, Nat>, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +k: K, +es0: List<&2, M.Entry<K, V>>, +fv: Maybe<&2, V>, +hdel: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) == S.del(~K, ~V, ~cmp, k, es0) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, es0)) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})) == True{} : Bool}, +hin: {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hln: {Nat.is_eq(SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hsz: {Nat.is_eq(Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))) == True{} : Bool}, +hcl: {Nat.is_le(l, 31n) == True{} : Bool}, +hcd: {Nat.is_le(d, l) == True{} : Bool}, +hcap: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hcpl: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +fr: Nat, +fn: List<&2, M.Node<K>>, +ft: ST.Tr, +heq: {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr, lo, hi, 1n+ui, l, d, fn, pl, tg, fl} : ST.Sh<K, V>}, +hrp: {ST.rep(~K, ft, 0n, fn) == True{} : Bool}, +hrid: {fr == ST.rid(ft) : Nat}, +hids: {ST.ids(ft) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>}, +hrb: {ST.root_black(~K, ft, fn) == True{} : Bool}, +h4: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) : List<&2, M.Entry<K, V>>}, +h5: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl) == True{} : Bool}, +h6: {ST.fll(~K, fn, Con{1n+ui, flf}) == True{} : Bool}, +h7: {SC.length(M.Node<K>, fn) == SC.length(M.Node<K>, nl) : Nat}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui)), fv)):  %Equal.sym(ST.Sh<K, V>, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui), ST.SH{Nat.sub(n, 1n), fr, lo, hi, 1n+ui, l, d, fn, pl, tg, fl}, heq) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv), (MI.refresh_ends(~K, ~V, ~cmp, _), fv))  %Equal.sym(Nat, fr, ST.rid(ft), hrid) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv), (MI.refresh_ends(~K, ~V, ~cmp, ST.SH{Nat.sub(n, 1n), _, lo, hi, 1n+ui, l, d, fn, pl, tg, fl}), fv))  +esz = N.eq_from_is_eq(Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), hsz)  +hle = L.subst(Nat, z => {Nat.is_le(TR.ht(ft), z) == True{} : Bool}, SC.length(Nat, ST.ids(ft)), Nat.sub(n, 1n), Equal.trans(Nat, SC.length(Nat, ST.ids(ft)), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), Nat.sub(n, 1n), L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(ft)) == SC.length(Nat, z) : Nat}, ST.ids(ft), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), hids, {==}), Equal.sym(Nat, Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c)))), esz)), TR.ht_le(ft))  %Equal.sym(ST.Sh<K, V>, MI.refresh_ends(~K, ~V, ~cmp, ST.SH{Nat.sub(n, 1n), ST.rid(ft), lo, hi, 1n+ui, l, d, fn, pl, tg, fl}), ST.SH{Nat.sub(n, 1n), ST.rid(ft), ST.fst0(ST.ids(ft)), ST.last0(ST.ids(ft)), 1n+ui, l, d, fn, pl, tg, fl}, XT.refresh_m(~K, ~V, ~cmp, Nat.sub(n, 1n), lo, hi, 1n+ui, l, d, fn, pl, tg, fl, ft, hrp, N.le_lt_succ(TR.ht(ft), Nat.sub(n, 1n), hle))) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv), (_, fv))  +eids = L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, ST.ids(ft), fn, pl) == ST.ents(~K, ~V, z, fn, pl) : List<&2, M.Entry<K, V>>}, ST.ids(ft), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), hids, {==})  +eD = Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, es0), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), ST.ents(~K, ~V, ST.ids(ft), fn, pl), Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), S.del(~K, ~V, ~cmp, k, es0), hdel), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl), ST.ents(~K, ~V, ST.ids(ft), fn, pl), Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl), h4), Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(ft), fn, pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl), eids)))  +esp = L.subst(List<&2, M.Entry<K, V>>, z => {(S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv) == (S.TM{l, z}, fv) : S.Model<K, V> & Maybe<&2, V>}, S.del(~K, ~V, ~cmp, k, es0), ST.ents(~K, ~V, ST.ids(ft), fn, pl), eD, {==})  +el = Equal.sym(Nat, SC.length(M.Node<K>, fn), SC.length(M.Node<K>, nl), h7)  +gcap = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, fn), el, hcap)  +gcpl = L.subst(Nat, z => {Nat.is_eq(SC.length(Maybe<&2, V>, pl), z) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, fn), el, hcpl)  +gpay = SL.pay_oks(~K, ~V, ft, fn, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, fn, pl) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ST.ids(ft), Equal.sym(List<&2, Nat>, ST.ids(ft), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), hids), h5))  +gnd = L.subst(List<&2, Nat>, z => {NL.nodupn(SC.append(Nat, z, Con{1n+ui, flf})) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ST.ids(ft), Equal.sym(List<&2, Nat>, ST.ids(ft), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), hids), hnd)  +gin = L.subst(Nat, w => {ST.allin(SC.append(Nat, ST.ids(ft), Con{1n+ui, flf}), w) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, fn), el, L.subst(List<&2, Nat>, z => {ST.allin(SC.append(Nat, z, Con{1n+ui, flf}), SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ST.ids(ft), Equal.sym(List<&2, Nat>, ST.ids(ft), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), hids), hin))  +gln = L.subst(Nat, w => {Nat.is_eq(SC.length(Nat, SC.append(Nat, ST.ids(ft), Con{1n+ui, flf})), w) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, fn), el, L.subst(List<&2, Nat>, z => {Nat.is_eq(SC.length(Nat, SC.append(Nat, z, Con{1n+ui, flf})), SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ST.ids(ft), Equal.sym(List<&2, Nat>, ST.ids(ft), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), hids), hln))  +gord = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, S.del(~K, ~V, ~cmp, k, es0), ST.ents(~K, ~V, ST.ids(ft), fn, pl), eD, hord)  +gsz = L.subst(List<&2, Nat>, z => {Nat.is_eq(Nat.sub(n, 1n), SC.length(Nat, z)) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), ST.ids(ft), Equal.sym(List<&2, Nat>, ST.ids(ft), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), hids), hsz)  +good = ST.good_intro(~K, ~V, ~cmp, Nat.sub(n, 1n), ST.rid(ft), ST.fst0(ST.ids(ft)), ST.last0(ST.ids(ft)), 1n+ui, l, d, fn, pl, ft, Con{1n+ui, flf}, hcl, hcd, gcap, gcpl, hrp, gpay, h6, gnd, gin, gln, gord, hrb, gsz, N.is_eq_refl(ST.rid(ft)), N.is_eq_refl(ST.fst0(ST.ids(ft))), N.is_eq_refl(ST.last0(ST.ids(ft))), N.is_eq_refl(1n+ui))  (ST.SH{Nat.sub(n, 1n), ST.rid(ft), ST.fst0(ST.ids(ft)), ST.last0(ST.ids(ft)), 1n+ui, l, d, fn, pl, ft, Con{1n+ui, flf}}, (fv, ({==}, (esp, good))))def rm_f2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +flf: List<&2, Nat>, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +k: K, +es0: List<&2, M.Entry<K, V>>, +fv: Maybe<&2, V>, +hdel: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) == S.del(~K, ~V, ~cmp, k, es0) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, es0)) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})) == True{} : Bool}, +hin: {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hln: {Nat.is_eq(SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hsz: {Nat.is_eq(Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))) == True{} : Bool}, +hcl: {Nat.is_le(l, 31n) == True{} : Bool}, +hcd: {Nat.is_le(d, l) == True{} : Bool}, +hcap: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hcpl: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +fr: Nat, +fn: List<&2, M.Node<K>>, +ft: ST.Tr, +heq: {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr, lo, hi, 1n+ui, l, d, fn, pl, tg, fl} : ST.Sh<K, V>}, +hrp: {ST.rep(~K, ft, 0n, fn) == True{} : Bool}, +hrid: {fr == ST.rid(ft) : Nat}, +hids: {ST.ids(ft) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>}, +hrb: {ST.root_black(~K, ft, fn) == True{} : Bool}, +h4: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) : List<&2, M.Entry<K, V>>}, +h5: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl) == True{} : Bool}, r8: {ST.fll(~K, fn, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn) == SC.length(M.Node<K>, nl) : Nat}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui)), fv)):  match r8:    case Tuple{h6, h7}:      rm_f3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, flf, c, ui, ch, k, es0, fv, hdel, hord, hnd, hin, hln, hsz, hcl, hcd, hcap, hcpl, fr, fn, ft, heq, hrp, hrid, hids, hrb, h4, h5, h6, h7)def rm_f1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +flf: List<&2, Nat>, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +k: K, +es0: List<&2, M.Entry<K, V>>, +fv: Maybe<&2, V>, +hdel: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) == S.del(~K, ~V, ~cmp, k, es0) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, es0)) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})) == True{} : Bool}, +hin: {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hln: {Nat.is_eq(SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hsz: {Nat.is_eq(Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))) == True{} : Bool}, +hcl: {Nat.is_le(l, 31n) == True{} : Bool}, +hcd: {Nat.is_le(d, l) == True{} : Bool}, +hcap: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hcpl: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +fr: Nat, +fn: List<&2, M.Node<K>>, +ft: ST.Tr, rest: {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr, lo, hi, 1n+ui, l, d, fn, pl, tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft, 0n, fn) == True{} : Bool} & ({fr == ST.rid(ft) : Nat} & ({ST.ids(ft) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft, fn) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn, pl) == True{} : Bool} & ({ST.fll(~K, fn, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn) == SC.length(M.Node<K>, nl) : Nat})))))) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui)), fv)):  match rest:    case Tuple{heq, Tuple{hrp, Tuple{hrid, Tuple{hids, Tuple{hrb, Tuple{h4, Tuple{h5, r8}}}}}}}:      rm_f2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, flf, c, ui, ch, k, es0, fv, hdel, hord, hnd, hin, hln, hsz, hcl, hcd, hcap, hcpl, fr, fn, ft, heq, hrp, hrid, hids, hrb, h4, h5, r8)def rm_fin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +flf: List<&2, Nat>, +c: List<&2, P.Fr>, +ui: Nat, +ch: ST.Tr, +k: K, +es0: List<&2, M.Entry<K, V>>, +fv: Maybe<&2, V>, +hdel: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) == S.del(~K, ~V, ~cmp, k, es0) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, S.del(~K, ~V, ~cmp, k, es0)) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})) == True{} : Bool}, +hin: {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf}), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hln: {Nat.is_eq(SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), Con{1n+ui, flf})), SC.length(M.Node<K>, nl)) == True{} : Bool}, +hsz: {Nat.is_eq(Nat.sub(n, 1n), SC.length(Nat, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))))) == True{} : Bool}, +hcl: {Nat.is_le(l, 31n) == True{} : Bool}, +hcd: {Nat.is_le(d, l) == True{} : Bool}, +hcap: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hcpl: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, r: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui) == ST.SH{Nat.sub(n, 1n), fr_, lo, hi, 1n+ui, l, d, fn_, pl, tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), nl, pl) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ch), P.after(c))), fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, Con{1n+ui, flf}) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nl) : Nat})))))>>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, es0)}, fv), (MI.refresh_ends(~K, ~V, ~cmp, MI.unlink(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui)), fv)):  match r:    case Tuple{+fr, Tuple{+fn, Tuple{+ft, rest}}}:      rm_f1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, flf, c, ui, ch, k, es0, fv, hdel, hord, hnd, hin, hln, hsz, hcl, hcd, hcap, hcpl, fr, fn, ft, rest)