proofs/containers/balanced_search_tree/navs.bend source

proofs/containers/balanced_search_tree/navs.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 ./nav.bend as NVimport ./navl.bend as NL# The ghost navigation answers the specification: along a path whose ids# before the subtree have keys below k and after it above k, the entry at# gnav's id is nav's (the first entry at or above k upward, the last at or# below it downward). (source: tools/generators/tm_hand/navs.src)def oks_l(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +h: {EN.oks(~K, ~V, SC.append(Nat, xs, ys), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, xs, nl, pl) == True{} : Bool}:  match xs:    case Nil{}:      {==}    case Con{+x, +t}:      L.and_intro(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), EN.oks(~K, ~V, t, nl, pl), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), EN.oks(~K, ~V, SC.append(Nat, t, ys), nl, pl), h), oks_l(~K, ~V, nl, pl, t, ys, L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), EN.oks(~K, ~V, SC.append(Nat, t, ys), nl, pl), h)))def oks_r(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +h: {EN.oks(~K, ~V, SC.append(Nat, xs, ys), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, ys, nl, pl) == True{} : Bool}:  match xs:    case Nil{}:      h    case Con{+x, +t}:      oks_r(~K, ~V, nl, pl, t, ys, L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), EN.oks(~K, ~V, SC.append(Nat, t, ys), nl, pl), h))# ---- at the end of the path ----def nav_te(~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>, +k: K, +h: Bool, +incl: Bool, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TE{}), 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}) -> {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, ST.TE{}, c, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, ST.TE{}, c, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TE{}), P.after(c))), nl, pl)) : Maybe<&2, M.Entry<K, V>>}:  match h:    case True{}:      %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), P.after(c)), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), FI.ents_app(~K, ~V, P.before(c), P.after(c), nl, pl)) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(P.after(c))), ST.pv(V, pl, ST.fst0(P.after(c)))) == S.first_where(~K, ~V, ~cmp, k, incl, _) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl))), OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl)), S.first_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl))), NL.fw_app(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl))) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(P.after(c))), ST.pv(V, pl, ST.fst0(P.after(c)))) == _ : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl)), None{}, NL.fw_none(~K, ~V, ~cmp, ~o, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl), hb)) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(P.after(c))), ST.pv(V, pl, ST.fst0(P.after(c)))) == OR.orm(M.Entry<K, V>, _, S.first_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl))) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl)), S.head(M.Entry<K, V>, ST.ents(~K, ~V, P.after(c), nl, pl)), NL.fw_head(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl), ha)) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(P.after(c))), ST.pv(V, pl, ST.fst0(P.after(c)))) == _ : Maybe<&2, M.Entry<K, V>>}      Equal.sym(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, ST.ents(~K, ~V, P.after(c), nl, pl)), ST.ent(K, V, ST.nd(K, nl, ST.fst0(P.after(c))), ST.pv(V, pl, ST.fst0(P.after(c)))), EN.head_ents(~K, ~V, nl, pl, P.after(c), oks_r(~K, ~V, nl, pl, P.before(c), P.after(c), hk)))    case False{}:      %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), P.after(c)), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), FI.ents_app(~K, ~V, P.before(c), P.after(c), nl, pl)) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(P.before(c))), ST.pv(V, pl, ST.last0(P.before(c)))) == S.last_where(~K, ~V, ~cmp, k, incl, _, None{}) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), None{}), S.last_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl), S.last_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl), None{})), NL.lw_app(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl), None{})) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(P.before(c))), ST.pv(V, pl, ST.last0(P.before(c)))) == _ : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl)), None{}), NL.lw_all(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.before(c), nl, pl), None{}, hb)) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(P.before(c))), ST.pv(V, pl, ST.last0(P.before(c)))) == S.last_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl), _) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl)), None{}), S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl)), OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl)))) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(P.before(c))), ST.pv(V, pl, ST.last0(P.before(c)))) == S.last_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl), _) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl), S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl))), S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl)), NL.lw_none(~K, ~V, ~cmp, ~o, k, incl, ST.ents(~K, ~V, P.after(c), nl, pl), S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl)), ha)) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(P.before(c))), ST.pv(V, pl, ST.last0(P.before(c)))) == _ : Maybe<&2, M.Entry<K, V>>}      Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl)), ST.ent(K, V, ST.nd(K, nl, ST.last0(P.before(c))), ST.pv(V, pl, ST.last0(P.before(c)))), EN.last_ents_all(~K, ~V, nl, pl, P.before(c), oks_l(~K, ~V, nl, pl, P.before(c), P.after(c), hk)))# ---- at a node ----def geq(~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, +h: Bool, +incl: Bool, +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>>}, +hc: {cmp(k, key) == EQ{} : Cmp}, +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}, +hkx: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl) == True{} : Bool}, +hky: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl) == True{} : Bool}) -> {ST.ent(K, V, ST.nd(K, nl, ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))))), ST.pv(V, pl, ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))) == S.nav(~K, ~V, ~cmp, k, h, incl, 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)})) : Maybe<&2, M.Entry<K, V>>}:  match h incl:    case True{} True{}:      +ek = O.antisym(~K, ~cmp, o, k, key, hc)      +hl = L.subst(K, z => {OR.ltall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), 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))      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, True{}, 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)})), OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), S.first_where(~K, ~V, ~cmp, k, True{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)})), NL.fw_app(~K, ~V, ~cmp, k, True{}, 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)})) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == _ : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), None{}, NL.fw_none(~K, ~V, ~cmp, ~o, k, True{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), hl)) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == OR.orm(M.Entry<K, V>, _, S.first_where(~K, ~V, ~cmp, k, True{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)})) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Cmp, cmp(k, key), EQ{}, hc) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, True{}), Some{M.Entry{key, v}}, S.first_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))) : Maybe<&2, M.Entry<K, V>>}      hE    case False{} True{}:      +ek = O.antisym(~K, ~cmp, o, k, key, hc)      +hl = L.subst(K, z => {OR.ltall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), 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))      +hg = L.subst(K, z => {OR.gtall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), 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))      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, True{}, 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)}), None{}), S.last_where(~K, ~V, ~cmp, k, True{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}, S.last_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), None{})), NL.lw_app(~K, ~V, ~cmp, k, True{}, 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)}, None{})) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == _ : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), None{}), NL.lw_all(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), None{}, hl)) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == S.last_where(~K, ~V, ~cmp, k, True{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}, _) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(K, k, key, ek) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == S.last_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(key, _), True{}), Some{M.Entry{key, v}}, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), None{}))) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Cmp, cmp(key, key), EQ{}, O.refl(~K, ~cmp, ~o, key)) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == S.last_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, True{}), Some{M.Entry{key, v}}, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), None{}))) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, True{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), Some{M.Entry{key, v}}), Some{M.Entry{key, v}}, NL.lw_none(~K, ~V, ~cmp, ~o, k, True{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), Some{M.Entry{key, v}}, hg)) : {ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)) == _ : Maybe<&2, M.Entry<K, V>>}      hE    case True{} False{}:      +ek = O.antisym(~K, ~cmp, o, k, key, hc)      +hl = L.subst(K, z => {OR.ltall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), 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))      +hg = L.subst(K, z => {OR.gtall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), 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))      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, False{}, 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)})), OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), S.first_where(~K, ~V, ~cmp, k, False{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)})), NL.fw_app(~K, ~V, ~cmp, k, False{}, 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)})) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c)))), ST.pv(V, pl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))))) == _ : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), None{}, NL.fw_none(~K, ~V, ~cmp, ~o, k, False{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), hl)) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c)))), ST.pv(V, pl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))))) == OR.orm(M.Entry<K, V>, _, S.first_where(~K, ~V, ~cmp, k, False{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)})) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Cmp, cmp(k, key), EQ{}, hc) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c)))), ST.pv(V, pl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))))) == S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, False{}), Some{M.Entry{key, v}}, S.first_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl))) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)), S.head(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)), NL.fw_head(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), hg)) : {ST.ent(K, V, ST.nd(K, nl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c)))), ST.pv(V, pl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))))) == _ : Maybe<&2, M.Entry<K, V>>}      Equal.sym(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)), ST.ent(K, V, ST.nd(K, nl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c)))), ST.pv(V, pl, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))))), EN.head_ents(~K, ~V, nl, pl, SC.append(Nat, ST.ids(r), P.after(c)), hky))    case False{} False{}:      +ek = O.antisym(~K, ~cmp, o, k, key, hc)      +hl = L.subst(K, z => {OR.ltall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), 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))      +hg = L.subst(K, z => {OR.gtall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), 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))      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, False{}, 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)}), None{}), S.last_where(~K, ~V, ~cmp, k, False{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}, S.last_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), None{})), NL.lw_app(~K, ~V, ~cmp, k, False{}, 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)}, None{})) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ST.pv(V, pl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) == _ : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), None{}), NL.lw_all(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl), None{}, hl)) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ST.pv(V, pl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) == S.last_where(~K, ~V, ~cmp, k, False{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}, _) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), None{}), S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)))) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ST.pv(V, pl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) == S.last_where(~K, ~V, ~cmp, k, False{}, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}, _) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(K, k, key, ek) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ST.pv(V, pl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) == S.last_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(key, _), False{}), Some{M.Entry{key, v}}, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)))) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Cmp, cmp(key, key), EQ{}, O.refl(~K, ~cmp, ~o, key)) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ST.pv(V, pl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) == S.last_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, False{}), Some{M.Entry{key, v}}, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)))) : Maybe<&2, M.Entry<K, V>>}      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, False{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl))), S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), NL.lw_none(~K, ~V, ~cmp, ~o, k, False{}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), hg)) : {ST.ent(K, V, ST.nd(K, nl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ST.pv(V, pl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) == _ : Maybe<&2, M.Entry<K, V>>}      Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl)), ST.ent(K, V, ST.nd(K, nl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ST.pv(V, pl, ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))), EN.last_ents_all(~K, ~V, nl, pl, SC.append(Nat, P.before(c), ST.ids(l)), hkx))def gcase(~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, +h: Bool, +incl: Bool, +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>>}, +hW: {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)}) : List<&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}, +hkx: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl) == True{} : Bool}, +hky: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(r), 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} -> {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, 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}))), nl, pl)) : Maybe<&2, M.Entry<K, V>>}, 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} -> {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, 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}))), nl, pl)) : Maybe<&2, M.Entry<K, V>>}, +cc: Cmp, +hc: {cmp(k, key) == cc : Cmp}) -> {ST.ent(K, V, ST.nd(K, nl, TR.pk3(Nat, cc, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))), ST.pv(V, pl, TR.pk3(Nat, cc, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))))))) == S.nav(~K, ~V, ~cmp, k, h, incl, 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)) : Maybe<&2, M.Entry<K, V>>}:  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)      %Equal.sym(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}))), eqL) : {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, _, nl, pl)) : Maybe<&2, M.Entry<K, V>>}      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)      %Equal.sym(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}))), eqR) : {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, _, nl, pl)) : Maybe<&2, M.Entry<K, V>>}      kr(hr2)    case EQ{}:      %Equal.sym(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), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl)}), hW) : {ST.ent(K, V, ST.nd(K, nl, ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))))), ST.pv(V, pl, ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))) == S.nav(~K, ~V, ~cmp, k, h, incl, _) : Maybe<&2, M.Entry<K, V>>}      geq(~K, ~V, ~cmp, ~o, nl, pl, c, i, l, r, k, h, incl, key, v, hE, hc, ho, hkx, hky)def gnode(~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, +h: Bool, +incl: Bool, +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}, +hkx: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), ST.ids(l)), nl, pl) == True{} : Bool}, +hky: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(r), 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} -> {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, 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}))), nl, pl)) : Maybe<&2, M.Entry<K, V>>}, 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} -> {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, 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}))), nl, pl)) : Maybe<&2, M.Entry<K, V>>}) -> {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, ST.TN{i, l, r}, c, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, ST.TN{i, l, r}, c, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, 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)) : Maybe<&2, M.Entry<K, V>>}:  match x m:    case M.Free{f} +m:      Empty.absurd({ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, ST.TN{i, l, r}, c, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, ST.TN{i, l, r}, c, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, 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)) : Maybe<&2, M.Entry<K, V>>}, L.false_true(hx))    case M.N{cc, a, b, q, +key} None{}:      Empty.absurd({ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, ST.TN{i, l, r}, c, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, ST.TN{i, l, r}, c, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, 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)) : Maybe<&2, M.Entry<K, V>>}, 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)      %Equal.sym(M.Node<K>, ST.nd(K, nl, i), M.N{cc, a, b, q, key}, hxi) : {ST.ent(K, V, ST.nd(K, nl, TR.pk3(Nat, TR.kc(~K, ~cmp, k, _), NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))), ST.pv(V, pl, TR.pk3(Nat, TR.kc(~K, ~cmp, k, _), NV.gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), NV.gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))))))) == S.nav(~K, ~V, ~cmp, k, h, incl, 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)) : Maybe<&2, M.Entry<K, V>>}      gcase(~K, ~V, ~cmp, ~o, nl, pl, c, i, l, r, k, h, incl, key, v, hEg, hW, ho2, hkx, hky, eqL, eqR, kl, kr, cmp(k, key), {==})# the ids split around a node: before and its left ids, the node, its right# ids and afterdef wh_node(+c: List<&2, P.Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr) -> {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))}) : List<&2, Nat>}:  %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, SC.append(Nat, ST.ids(r), P.after(c))}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(l), Con{i, SC.append(Nat, ST.ids(r), P.after(c))})), LL.append_assoc(Nat, P.before(c), ST.ids(l), Con{i, SC.append(Nat, ST.ids(r), P.after(c))})) : {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))) == _ : List<&2, Nat>}  P.eq_l(P.before(c), P.after(c), i, ST.ids(l), ST.ids(r))# the entry at the ghost navigation's id is the specification's answerdef gspec(~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, +h: Bool, +incl: Bool, +hr: {ST.rep(~K, t, P.top(c), 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}) -> {ST.ent(K, V, ST.nd(K, nl, NV.gnav(~K, ~cmp, t, c, nl, k, h, incl)), ST.pv(V, pl, NV.gnav(~K, ~cmp, t, c, nl, k, h, incl))) == S.nav(~K, ~V, ~cmp, k, h, incl, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))), nl, pl)) : Maybe<&2, M.Entry<K, V>>}:  match t:    case ST.TE{}:      nav_te(~K, ~V, ~cmp, ~o, nl, pl, c, k, h, incl, hk, hb, ha)    case ST.TN{+i, +l, +r}:      +eqW = 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)      +hkx = oks_l(~K, ~V, nl, pl, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, SC.append(Nat, ST.ids(r), P.after(c))}, hk2)      +hky = L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i))), EN.oks(~K, ~V, SC.append(Nat, ST.ids(r), P.after(c)), nl, pl), oks_r(~K, ~V, nl, pl, SC.append(Nat, P.before(c), ST.ids(l)), Con{i, SC.append(Nat, ST.ids(r), P.after(c))}, hk2))      +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))      +eqL = P.ids_l(c, i, l, r)      +eqR = P.ids_r(c, i, l, r)      gnode(~K, ~V, ~cmp, ~o, nl, pl, c, i, l, r, k, h, incl, 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, hkx, hky, eqL, eqR, hl => gspec(~K, ~V, ~cmp, ~o, nl, pl, l, Con{P.FR{i, True{}, r}, c}, k, h, incl, TR.rep_l(~K, i, l, r, P.top(c), nl, hr), 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 => gspec(~K, ~V, ~cmp, ~o, nl, pl, r, Con{P.FR{i, False{}, l}, c}, k, h, incl, TR.rep_r(~K, i, l, r, P.top(c), nl, hr), 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))