proofs/containers/balanced_search_tree/rmi.bend
bend-collections-laws-containers@1.0.0.0 · 86 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as OK
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/reads.bend as RD
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/find.bend as FI
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as EN
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as P
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/plug.bend as PG
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as OR
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/tree.bend as TR
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/spath.bend as SP
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/putm.bend as PM
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmv.bend as RV
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mokx.bend as MX
23
24# remove_if_equal: the found value compared with the expected one; equal,
25# the node is removed as remove removes it, the answer true; otherwise, or
26# absent, nothing changes. (source: tools/generators/tm_hand/rmi.src)
27
28
29# equal or not: removed, or left
30def rmi_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V, +c: List<&2, P.Fr>, +ui: Nat, +a: ST.Tr, +b: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, a, b}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, a, b}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, a, b}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, ST.TN{1n+ui, a, b}, nl) == True{} : Bool}, +vi: V, +hmi: {ST.pv(V, pl, 1n+ui) == Some{vi} : Maybe<&2, V>}, +bq: Bool) -> OK.MOK(~K, ~V, ~cmp, Bool, S.pick(S.Model<K, V> & Bool, bq, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, True{}), (S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, False{})), MI.remove_if_apply(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+ui, e, bq)):
31 match bq:
32 case False{}:
33 (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (False{}, ({==}, ({==}, hg))))
34 case True{}:
35 %Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+ui), Some{vi}, hmi) : OK.MOK(~K, ~V, ~cmp, Bool, (S.TM{l, S.del(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, True{}), MI.changed_value(~K, ~V, ~cmp, (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}, ST.nd(K, nl, 1n+ui)))), _)))
36 MX.cv_mok(~K, ~V, ~cmp, S.TM{l, S.del(~K, ~V, ~cmp, k, 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}, ST.nd(K, nl, 1n+ui)))), vi, L.subst(Maybe<&2, V>, z => OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, k, 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}, ST.nd(K, nl, 1n+ui)))), z)), ST.pv(V, pl, 1n+ui), Some{vi}, hmi, RV.rm_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, c, ui, a, b, hbc, hplug, hr, hok, hfin, ST.nd(K, nl, 1n+ui), {==})))
37
38# a node found: its value
39def rmi_h(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V, +c: List<&2, P.Fr>, +ui: Nat, +a: ST.Tr, +b: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, a, b}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{1n+ui, a, b}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{1n+ui, a, b}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, 1n+ui, nl) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, ST.TN{1n+ui, a, b}, nl) == True{} : Bool}, +hfd: {ST.pv(V, pl, 1n+ui) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+ui) == m : Maybe<&2, V>}, +hm: {ST.some2(V, m) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+ui, P.top(c), SP.dir(c)}))):
40 match m:
41 case None{}:
42 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+ui, P.top(c), SP.dir(c)}))), L.false_true(hm))
43 case Some{+vi}:
44 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vi}, Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+ui), Some{vi}, Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+ui), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd), hmi)) : OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, _), MI.remove_if_value(~K, ~V, ~cmp, ~eq, 1n+ui, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.pv(V, pl, 1n+ui))))
45 %Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+ui), Some{vi}, hmi) : OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, Some{vi}), MI.remove_if_value(~K, ~V, ~cmp, ~eq, 1n+ui, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _)))
46 rmi_b(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, c, ui, a, b, hbc, hplug, hr, hok, hfin, vi, hmi, eq(vi, e))
47
48def rmi_tn(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +hfd: {ST.pv(V, pl, i) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TN{i, a, b}) : ST.Tr}, +hr: {ST.rep(~K, ST.TN{i, a, b}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, i, nl) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, ST.TN{i, a, b}, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{i, P.top(c), SP.dir(c)}))):
49 match i:
50 case 0n:
51 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))), PM.tn_zero(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, a, b, hr))
52 case 1n+ui:
53 rmi_h(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, c, ui, a, b, PM.tn_hbc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+ui, a, b, hwh), hplug, hr, hok, hfin, hfd, ST.pv(V, pl, 1n+ui), {==}, PM.tn_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+ui, a, b, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+ui, a, b}), P.after(c))), hwh, hk0)))
54
55def rmi_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, +ha: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))):
56 match t:
57 case ST.TE{}:
58 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}, Equal.sym(Maybe<&2, V>, None{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd)) : OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, _), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, False{}))
59 (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (False{}, ({==}, ({==}, hg))))
60 case ST.TN{+i, +a, +b}:
61 rmi_tn(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, c, i, a, b, hfd, hwh, hplug, hr, hokc, hfin)
62
63def rmi_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, r2: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))):
64 match r2:
65 case Tuple{ha, hfin}:
66 rmi_t(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, c, t, hfd, hwh, hplug, hr, hokc, hb, ha, hfin)
67
68def rmi_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, r: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))):
69 match r:
70 case Tuple{hts, Tuple{hwh, Tuple{hplug, Tuple{hr, Tuple{hokc, Tuple{hb, r2}}}}}}:
71 +hts2 = hts
72 %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2) : OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _)))
73 rmi_c2(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, c, t, L.subst(M.Search, z => {ST.pv(V, pl, FI.sfound(z)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2, FI.tfind(~K, ~V, ~cmp, ~o, nl, pl, tg, 0n, False{}, k, 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), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), hwh, hplug, hr, hokc, hb, r2)
74
75def rmi_sp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, P.Fr>, c => Sigma<&1, &1, ST.Tr, t => {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))>>) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))):
76 match sp:
77 case Tuple{+c, Tuple{+t, r}}:
78 rmi_c(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, c, t, r)
79
80def rmi_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +e: V) -> OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, e)):
81 +ean = LL.append_nil(Nat, ST.ids(tg))
82 +hk1 = 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))
83 +hk0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), ean), hk1)
84 +ho0 = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), ean), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
85 %Equal.sym(ST.Sh<K, V> & 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)) : OK.MOK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_found(~K, ~V, ~cmp, ~eq, e, e, _))
86 rmi_sp(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, hk0, SP.spath(~K, ~V, ~cmp, ~o, nl, pl, tg, Nil{}, k, 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), ho0, hk0, {==}, {==}))