proofs/containers/balanced_search_tree/spath.bend source
proofs/containers/balanced_search_tree/spath.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/order.bend as Oimport ../../lib/list.bend as LLimport ../../../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 ./ord.bend as ORimport ./find.bend as FIimport ./ends.bend as ENimport ./tree.bend as TRimport ./path.bend as Pimport ./navl.bend as NLimport ./navs.bend as NSimport ./plug.bend as PG# The search as a path: from a subtree the path leads to, the ghost search# stops at a subtree (empty, or a node whose key equals k) along a longer# path whose ids before have keys below k and after it above k; its result# names that subtree's root, the path's parent and side.# (source: tools/generators/tm_hand/spath.src)# the side of the path's last stepdef dir(c: List<&2, P.Fr>) -> Bool: match c: case Nil{}: False{} case Con{f, t}: match f: case P.FR{p, +lft, s}: lft# where a search stops: nothing, or a node with k's keydef fin(~K: Data, ~cmp: K -> K -> Cmp, +k: K, t: ST.Tr, +nl: List<&2, M.Node<K>>) -> Bool: match t: case ST.TE{}: True{} case ST.TN{+i, l, r}: S.is_eq(TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)))# a step's result carried up: the search of the node is the child'sdef up_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +c: List<&2, P.Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +k: K, +ekc: {TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)) == LT{} : Cmp}, +eqL: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))) : List<&2, Nat>}, ih: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, l, nl, k, P.top(Con{P.FR{i, True{}, r}, c}), dir(Con{P.FR{i, True{}, r}, c})) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(Con{P.FR{i, True{}, r}, c}, l) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, ST.TN{i, l, r}, nl, k, P.top(c), dir(c)) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(c, ST.TN{i, l, r}) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>: match ih: case Tuple{+c2, Tuple{+t2, Tuple{+p1, Tuple{+p2, Tuple{+p3, rest}}}}}: +q1 = L.subst(Cmp, z => {TR.pk3(M.Search, z, TR.tsearch(~K, ~V, ~cmp, l, nl, k, i, True{}), TR.tsearch(~K, ~V, ~cmp, r, nl, k, i, False{}), M.Search{i, P.top(c), dir(c)}) == M.Search{ST.rid(t2), P.top(c2), dir(c2)} : M.Search}, LT{}, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), Equal.sym(Cmp, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), LT{}, ekc), p1) (c2, (t2, (q1, (Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))), SC.append(Nat, P.before(c2), SC.append(Nat, ST.ids(t2), P.after(c2))), eqL, p2), (p3, rest)))))def up_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +c: List<&2, P.Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +k: K, +ekc: {TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)) == GT{} : Cmp}, +eqR: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))) : List<&2, Nat>}, ih: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, r, nl, k, P.top(Con{P.FR{i, False{}, l}, c}), dir(Con{P.FR{i, False{}, l}, c})) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(Con{P.FR{i, False{}, l}, c}, r) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, ST.TN{i, l, r}, nl, k, P.top(c), dir(c)) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(c, ST.TN{i, l, r}) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>: match ih: case Tuple{+c2, Tuple{+t2, Tuple{+p1, Tuple{+p2, Tuple{+p3, rest}}}}}: +q1 = L.subst(Cmp, z => {TR.pk3(M.Search, z, TR.tsearch(~K, ~V, ~cmp, l, nl, k, i, True{}), TR.tsearch(~K, ~V, ~cmp, r, nl, k, i, False{}), M.Search{i, P.top(c), dir(c)}) == M.Search{ST.rid(t2), P.top(c2), dir(c2)} : M.Search}, GT{}, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), Equal.sym(Cmp, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), GT{}, ekc), p1) (c2, (t2, (q1, (Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))), SC.append(Nat, P.before(c2), SC.append(Nat, ST.ids(t2), P.after(c2))), eqR, p2), (p3, rest)))))def scase(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +c: List<&2, P.Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +k: K, +key: K, +v: V, +hE: {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == Some{M.Entry{key, v}} : Maybe<&2, M.Entry<K, V>>}, +ho: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)})) == True{} : Bool}, +ekey: {TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)) == cmp(k, key) : Cmp}, +hr: {ST.rep(~K, ST.TN{i, l, r}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, i, 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}, +eqL: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))) : List<&2, Nat>}, +eqR: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))) : List<&2, Nat>}, kl: @+hl: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(Con{P.FR{i, True{}, r}, c}), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, l, nl, k, P.top(Con{P.FR{i, True{}, r}, c}), dir(Con{P.FR{i, True{}, r}, c})) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(Con{P.FR{i, True{}, r}, c}, l) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>, kr: @+hr2: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(Con{P.FR{i, False{}, l}, c}), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, r, nl, k, P.top(Con{P.FR{i, False{}, l}, c}), dir(Con{P.FR{i, False{}, l}, c})) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(Con{P.FR{i, False{}, l}, c}, r) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>, +cc: Cmp, +hc: {cmp(k, key) == cc : Cmp}) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, ST.TN{i, l, r}, nl, k, P.top(c), dir(c)) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(c, ST.TN{i, l, r}) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>: match cc: case LT{}: +hkl = L.subst(Cmp, z => {Cmp.is_lt(z) == True{} : Bool}, LT{}, cmp(k, key), Equal.sym(Cmp, cmp(k, key), LT{}, hc), {==}) +hg = L.and_intro(Cmp.is_lt(cmp(k, key)), OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)), hkl, OR.gtall_mono(~K, ~V, ~cmp, ~o, k, key, hkl, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), OR.ord_mid_r(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), ho))) +hl = L.subst(Maybe<&2, M.Entry<K, V>>, z => {OR.gtall(~K, ~V, ~cmp, k, ST.cons_m(M.Entry<K, V>, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))) == True{} : Bool}, Some{M.Entry{key, v}}, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), Some{M.Entry{key, v}}, hE), hg) up_l(~K, ~V, ~cmp, nl, pl, c, i, l, r, k, Equal.trans(Cmp, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), cmp(k, key), LT{}, ekey, hc), eqL, kl(hl)) case GT{}: +hlk = OR.gt_lt(~K, ~cmp, ~o, k, key, hc) +hx = NL.ltall_app(~K, ~V, ~cmp, k, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), Con{M.Entry{key, v}, Nil{}}, OR.ltall_mono(~K, ~V, ~cmp, ~o, key, k, hlk, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), OR.ord_mid_l(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), ho)), L.and_intro(Cmp.is_lt(cmp(key, k)), True{}, hlk, {==})) +hx2 = L.subst(Maybe<&2, M.Entry<K, V>>, z => {OR.ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.cons_m(M.Entry<K, V>, z, Nil{}))) == True{} : Bool}, Some{M.Entry{key, v}}, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), Some{M.Entry{key, v}}, hE), hx) +hx3 = L.subst(List<&2, M.Entry<K, V>>, z => {OR.ltall(~K, ~V, ~cmp, k, z) == True{} : Bool}, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.ents(~K, ~V, Con{i, Nil{}}, nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, Nil{}}), nl, pl), Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, Nil{}}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.ents(~K, ~V, Con{i, Nil{}}, nl, pl)), FI.ents_app(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, Nil{}}, nl, pl)), hx2) +hr2 = L.subst(List<&2, Nat>, z => {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, Nil{}}), P.before(Con{P.FR{i, False{}, l}, c}), LL.append_assoc(Nat, P.before(c), ST.ids(l), Con{i, Nil{}}), hx3) up_r(~K, ~V, ~cmp, nl, pl, c, i, l, r, k, Equal.trans(Cmp, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), cmp(k, key), GT{}, ekey, hc), eqR, kr(hr2)) case EQ{}: +ekc = Equal.trans(Cmp, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), cmp(k, key), EQ{}, ekey, hc) +p1 = L.subst(Cmp, z => {TR.pk3(M.Search, z, TR.tsearch(~K, ~V, ~cmp, l, nl, k, i, True{}), TR.tsearch(~K, ~V, ~cmp, r, nl, k, i, False{}), M.Search{i, P.top(c), dir(c)}) == M.Search{i, P.top(c), dir(c)} : M.Search}, EQ{}, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), Equal.sym(Cmp, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), EQ{}, ekc), {==}) +pf = L.subst(Cmp, z => {S.is_eq(z) == True{} : Bool}, EQ{}, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), Equal.sym(Cmp, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), EQ{}, ekc), {==}) (c, (ST.TN{i, l, r}, (p1, ({==}, ({==}, (hr, (hok, (hb, (ha, pf)))))))))def snode(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +c: List<&2, P.Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +k: K, +x: M.Node<K>, +m: Maybe<&2, V>, +hx: {ST.is_node(K, x, ST.rid(l), ST.rid(r), P.top(c)) == True{} : Bool}, +hm: {ST.some2(V, m) == True{} : Bool}, +hxi: {ST.nd(K, nl, i) == x : M.Node<K>}, +hEg: {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}, +hW0: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), nl, pl) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))) : List<&2, M.Entry<K, V>>}, +ho: {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), nl, pl)) == True{} : Bool}, +hr: {ST.rep(~K, ST.TN{i, l, r}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, i, 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}, +eqL: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))) : List<&2, Nat>}, +eqR: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))) : List<&2, Nat>}, kl: @+hl: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(Con{P.FR{i, True{}, r}, c}), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, l, nl, k, P.top(Con{P.FR{i, True{}, r}, c}), dir(Con{P.FR{i, True{}, r}, c})) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(Con{P.FR{i, True{}, r}, c}, l) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>, kr: @+hr2: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(Con{P.FR{i, False{}, l}, c}), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, r, nl, k, P.top(Con{P.FR{i, False{}, l}, c}), dir(Con{P.FR{i, False{}, l}, c})) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(Con{P.FR{i, False{}, l}, c}, r) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, ST.TN{i, l, r}, nl, k, P.top(c), dir(c)) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(c, ST.TN{i, l, r}) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>: match x m: case M.Free{f} +m: Empty.absurd(Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, ST.TN{i, l, r}, nl, k, P.top(c), dir(c)) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(c, ST.TN{i, l, r}) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>, L.false_true(hx)) case M.N{cc, a, b, q, +key} None{}: Empty.absurd(Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, ST.TN{i, l, r}, nl, k, P.top(c), dir(c)) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(c, ST.TN{i, l, r}) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>, L.false_true(hm)) case M.N{+cc, +a, +b, +q, +key} Some{+v}: +hW = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}), hW0, L.subst(Maybe<&2, M.Entry<K, V>>, z => {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.cons_m(M.Entry<K, V>, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))) : List<&2, M.Entry<K, V>>}, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), Some{M.Entry{key, v}}, hEg, {==})) +ho2 = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}), hW, ho) +ekey = L.subst(M.Node<K>, z => {TR.kc(~K, ~cmp, k, z) == cmp(k, key) : Cmp}, M.N{cc, a, b, q, key}, ST.nd(K, nl, i), Equal.sym(M.Node<K>, ST.nd(K, nl, i), M.N{cc, a, b, q, key}, hxi), {==}) scase(~K, ~V, ~cmp, ~o, nl, pl, c, i, l, r, k, key, v, hEg, ho2, ekey, hr, hok, hb, ha, eqL, eqR, kl, kr, cmp(k, key), {==})def spath(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +c: List<&2, P.Fr>, +k: K, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hp: {ST.pay(~V, t, pl) == True{} : Bool}, +ho: {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))), nl, pl)) == True{} : Bool}, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))), nl, pl) == 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}) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pt_ => {TR.tsearch(~K, ~V, ~cmp, t, nl, k, P.top(c), dir(c)) == M.Search{ST.rid(pt_), P.top(pc_), dir(pc_)} : M.Search} & ({SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) == SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(pt_), P.after(pc_))) : List<&2, Nat>} & ({PG.plug(c, t) == PG.plug(pc_, pt_) : ST.Tr} & ({ST.rep(~K, pt_, P.top(pc_), nl) == True{} : Bool} & ({P.ctxok(~K, pc_, ST.rid(pt_), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(pc_), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(pc_), nl, pl)) == True{} : Bool} & {fin(~K, ~cmp, k, pt_, nl) == True{} : Bool}))))))>>: match t: case ST.TE{}: (c, (ST.TE{}, ({==}, ({==}, ({==}, (hr, (hok, (hb, (ha, {==}))))))))) case ST.TN{+i, +l, +r}: +eqW = NS.wh_node(c, i, l, r) +hk2 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, SC.append(Nat, ST.ids(r), P.after(c))}), eqW, hk) +hW0 = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), nl, pl), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, SC.append(Nat, ST.ids(r), P.after(c))}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))), L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry<K, V>>}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, SC.append(Nat, ST.ids(r), P.after(c))}), eqW, {==}), FI.ents_app(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, SC.append(Nat, ST.ids(r), P.after(c))}, nl, pl)) snode(~K, ~V, ~cmp, ~o, nl, pl, c, i, l, r, k, ST.nd(K, nl, i), ST.pv(V, pl, i), TR.rep_node(~K, i, l, r, P.top(c), nl, hr), FI.pay_node(~V, i, l, r, pl, hp), {==}, {==}, hW0, ho, hr, hok, hb, ha, P.ids_l(c, i, l, r), P.ids_r(c, i, l, r), hl => spath(~K, ~V, ~cmp, ~o, nl, pl, l, Con{P.FR{i, True{}, r}, c}, k, Pair.snd({P.ctxok(~K, Con{P.FR{i, True{}, r}, c}, ST.rid(l), nl) == True{} : Bool}, {ST.rep(~K, l, i, nl) == True{} : Bool}, P.ok_l(~K, nl, c, i, l, r, hr, hok)), Pair.fst({P.ctxok(~K, Con{P.FR{i, True{}, r}, c}, ST.rid(l), nl) == True{} : Bool}, {ST.rep(~K, l, i, nl) == True{} : Bool}, P.ok_l(~K, nl, c, i, l, r, hr, hok)), FI.pay_l(~V, i, l, r, pl, hp), L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))), P.ids_l(c, i, l, r), ho), L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))), P.ids_l(c, i, l, r), hk), hb, hl), hr2 => spath(~K, ~V, ~cmp, ~o, nl, pl, r, Con{P.FR{i, False{}, l}, c}, k, Pair.snd({P.ctxok(~K, Con{P.FR{i, False{}, l}, c}, ST.rid(r), nl) == True{} : Bool}, {ST.rep(~K, r, i, nl) == True{} : Bool}, P.ok_r(~K, nl, c, i, l, r, hr, hok)), Pair.fst({P.ctxok(~K, Con{P.FR{i, False{}, l}, c}, ST.rid(r), nl) == True{} : Bool}, {ST.rep(~K, r, i, nl) == True{} : Bool}, P.ok_r(~K, nl, c, i, l, r, hr, hok)), FI.pay_r(~V, i, l, r, pl, hp), L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))), P.ids_r(c, i, l, r), ho), L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))), P.ids_r(c, i, l, r), hk), hr2, ha))