~/bend-docscommunity

proofs/containers/balanced_search_tree/cnx.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/list.bend as LLimport ../../lib/order.bend as Oimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/balanced_search_tree/main.bend as Simport ../../../src/containers/balanced_search_tree.bend as Mimport ./state.bend as STimport ./mirror.bend as MIimport ./ends.bend as ENimport ./path.bend as Pimport ./plug.bend as PGimport ./dj.bend as DJimport ./ord.bend as ORimport ./navl.bend as NVimport ./cur.bend as CUimport ./nbr.bend as NBimport ./find.bend as FIimport ./slot.bend as SLimport ../../lib/nat_list.bend as NL# A cursor's step: the path to any id of the tree, and in sorted entries# the entries strictly past (before) an entry's key are the ones after# (before) it. (source: tools/generators/tm_hand/cnx.src)# ---- strictly past the middle entry ----def fw_mid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}) -> {S.first_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == S.head(M.Entry<K, V>, ys) : Maybe<&2, M.Entry<K, V>>}:  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, SC.append(M.Entry<K, V>, xs, Con{e, ys})), OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, xs), S.first_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, Con{e, ys})), NV.fw_app(~K, ~V, ~cmp, S.key(K, V, e), False{}, xs, Con{e, ys})) : {_ == S.head(M.Entry<K, V>, ys) : Maybe<&2, M.Entry<K, V>>}  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, xs), None{}, NV.fw_none(~K, ~V, ~cmp, ~o, S.key(K, V, e), False{}, xs, OR.ord_mid_l(~K, ~V, ~cmp, ~o, xs, e, ys, h))) : {OR.orm(M.Entry<K, V>, _, S.first_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, Con{e, ys})) == S.head(M.Entry<K, V>, ys) : Maybe<&2, M.Entry<K, V>>}  %Equal.sym(Cmp, cmp(S.key(K, V, e), S.key(K, V, e)), EQ{}, O.refl(~K, ~cmp, ~o, S.key(K, V, e))) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, False{}), Some{e}, S.first_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, ys)) == S.head(M.Entry<K, V>, ys) : Maybe<&2, M.Entry<K, V>>}  NV.fw_head(~K, ~V, ~cmp, S.key(K, V, e), False{}, ys, OR.ord_mid_r(~K, ~V, ~cmp, ~o, xs, e, ys, h))def lw_mid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, SC.append(M.Entry<K, V>, xs, Con{e, ys}), None{}) == S.last(M.Entry<K, V>, xs) : Maybe<&2, M.Entry<K, V>>}:  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, SC.append(M.Entry<K, V>, xs, Con{e, ys}), None{}), S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, Con{e, ys}, S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, xs, None{})), NV.lw_app(~K, ~V, ~cmp, S.key(K, V, e), False{}, xs, Con{e, ys}, None{})) : {_ == S.last(M.Entry<K, V>, xs) : Maybe<&2, M.Entry<K, V>>}  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, xs, None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xs), None{}), NV.lw_all(~K, ~V, ~cmp, S.key(K, V, e), False{}, xs, None{}, OR.ord_mid_l(~K, ~V, ~cmp, ~o, xs, e, ys, h))) : {S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, Con{e, ys}, _) == S.last(M.Entry<K, V>, xs) : 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>, xs), None{}), S.last(M.Entry<K, V>, xs), OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, xs))) : {S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, Con{e, ys}, _) == S.last(M.Entry<K, V>, xs) : Maybe<&2, M.Entry<K, V>>}  %Equal.sym(Cmp, cmp(S.key(K, V, e), S.key(K, V, e)), EQ{}, O.refl(~K, ~cmp, ~o, S.key(K, V, e))) : {S.last_where(~K, ~V, ~cmp, S.key(K, V, e), False{}, ys, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, False{}), Some{e}, S.last(M.Entry<K, V>, xs))) == S.last(M.Entry<K, V>, xs) : Maybe<&2, M.Entry<K, V>>}  NV.lw_none(~K, ~V, ~cmp, ~o, S.key(K, V, e), False{}, ys, S.last(M.Entry<K, V>, xs), OR.ord_mid_r(~K, ~V, ~cmp, ~o, xs, e, ys, h))# ---- the path to an id of the tree ----def pt_upl(-K: Data, +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +j: Nat, r: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Con{P.FR{i, True{}, tr}, c}), SC.append(Nat, ST.ids(tl), P.after(Con{P.FR{i, True{}, tr}, c}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(Con{P.FR{i, True{}, tr}, c}, tl) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(c, ST.TN{i, tl, tr}) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>:  match r:    case Tuple{+pc, Tuple{+pa, Tuple{+pb, Tuple{h1, rest}}}}:      (pc, (pa, (pb, (Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(Con{P.FR{i, True{}, tr}, c}), SC.append(Nat, ST.ids(tl), P.after(Con{P.FR{i, True{}, tr}, c}))), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))), h1, Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, True{}, tr}, c}), SC.append(Nat, ST.ids(tl), P.after(Con{P.FR{i, True{}, tr}, c}))), P.ids_l(c, i, tl, tr))), rest))))def pt_upr(-K: Data, +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +j: Nat, r: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Con{P.FR{i, False{}, tl}, c}), SC.append(Nat, ST.ids(tr), P.after(Con{P.FR{i, False{}, tl}, c}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(Con{P.FR{i, False{}, tl}, c}, tr) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(c, ST.TN{i, tl, tr}) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>:  match r:    case Tuple{+pc, Tuple{+pa, Tuple{+pb, Tuple{h1, rest}}}}:      (pc, (pa, (pb, (Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(Con{P.FR{i, False{}, tl}, c}), SC.append(Nat, ST.ids(tr), P.after(Con{P.FR{i, False{}, tl}, c}))), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))), h1, Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, False{}, tl}, c}), SC.append(Nat, ST.ids(tr), P.after(Con{P.FR{i, False{}, tl}, c}))), P.ids_r(c, i, tl, tr))), rest))))# j on the right when neither the node nor on the leftdef pt_rc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +j: Nat, +hr: {ST.rep(~K, ST.TN{i, tl, tr}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, i, nl) == True{} : Bool}, +hm: {NL.memn(j, ST.ids(ST.TN{i, tl, tr})) == True{} : Bool}, +he: {Nat.is_eq(i, j) == False{} : Bool}, +bl: Bool, +hbl: {NL.memn(j, ST.ids(tl)) == bl : Bool}, kl: @+hrl: {ST.rep(~K, tl, i, nl) == True{} : Bool} -> @+hol: {P.ctxok(~K, Con{P.FR{i, True{}, tr}, c}, ST.rid(tl), nl) == True{} : Bool} -> @+hml: {NL.memn(j, ST.ids(tl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Con{P.FR{i, True{}, tr}, c}), SC.append(Nat, ST.ids(tl), P.after(Con{P.FR{i, True{}, tr}, c}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(Con{P.FR{i, True{}, tr}, c}, tl) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>, kr: @+hrr: {ST.rep(~K, tr, i, nl) == True{} : Bool} -> @+hor: {P.ctxok(~K, Con{P.FR{i, False{}, tl}, c}, ST.rid(tr), nl) == True{} : Bool} -> @+hmr: {NL.memn(j, ST.ids(tr)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Con{P.FR{i, False{}, tl}, c}), SC.append(Nat, ST.ids(tr), P.after(Con{P.FR{i, False{}, tl}, c}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(Con{P.FR{i, False{}, tl}, c}, tr) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(c, ST.TN{i, tl, tr}) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>:  match bl:    case True{}:      pt_upl(K, nl, c, i, tl, tr, j, kl(Pair.snd({P.ctxok(~K, Con{P.FR{i, True{}, tr}, c}, ST.rid(tl), nl) == True{} : Bool}, {ST.rep(~K, tl, i, nl) == True{} : Bool}, P.ok_l(~K, nl, c, i, tl, tr, hr, hok)), Pair.fst({P.ctxok(~K, Con{P.FR{i, True{}, tr}, c}, ST.rid(tl), nl) == True{} : Bool}, {ST.rep(~K, tl, i, nl) == True{} : Bool}, P.ok_l(~K, nl, c, i, tl, tr, hr, hok)), hbl))    case False{}:      +e1 = Equal.trans(Bool, Bool.or(NL.memn(j, ST.ids(tl)), NL.memn(j, Con{i, ST.ids(tr)})), NL.memn(j, ST.ids(ST.TN{i, tl, tr})), True{}, Equal.sym(Bool, NL.memn(j, ST.ids(ST.TN{i, tl, tr})), Bool.or(NL.memn(j, ST.ids(tl)), NL.memn(j, Con{i, ST.ids(tr)})), NL.memn_app(j, ST.ids(tl), Con{i, ST.ids(tr)})), hm)      +e2 = L.subst(Bool, z => {Bool.or(z, NL.memn(j, Con{i, ST.ids(tr)})) == True{} : Bool}, NL.memn(j, ST.ids(tl)), False{}, hbl, e1)      +e3 = L.subst(Bool, z => {Bool.or(z, NL.memn(j, ST.ids(tr))) == True{} : Bool}, Nat.is_eq(i, j), False{}, he, e2)      pt_upr(K, nl, c, i, tl, tr, j, kr(Pair.snd({P.ctxok(~K, Con{P.FR{i, False{}, tl}, c}, ST.rid(tr), nl) == True{} : Bool}, {ST.rep(~K, tr, i, nl) == True{} : Bool}, P.ok_r(~K, nl, c, i, tl, tr, hr, hok)), Pair.fst({P.ctxok(~K, Con{P.FR{i, False{}, tl}, c}, ST.rid(tr), nl) == True{} : Bool}, {ST.rep(~K, tr, i, nl) == True{} : Bool}, P.ok_r(~K, nl, c, i, tl, tr, hr, hok)), e3))# the node itself, or below itdef pt_c(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +j: Nat, +hr: {ST.rep(~K, ST.TN{i, tl, tr}, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, i, nl) == True{} : Bool}, +hm: {NL.memn(j, ST.ids(ST.TN{i, tl, tr})) == True{} : Bool}, +e: Bool, +he: {Nat.is_eq(i, j) == e : Bool}, kl: @+hrl: {ST.rep(~K, tl, i, nl) == True{} : Bool} -> @+hol: {P.ctxok(~K, Con{P.FR{i, True{}, tr}, c}, ST.rid(tl), nl) == True{} : Bool} -> @+hml: {NL.memn(j, ST.ids(tl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Con{P.FR{i, True{}, tr}, c}), SC.append(Nat, ST.ids(tl), P.after(Con{P.FR{i, True{}, tr}, c}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(Con{P.FR{i, True{}, tr}, c}, tl) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>, kr: @+hrr: {ST.rep(~K, tr, i, nl) == True{} : Bool} -> @+hor: {P.ctxok(~K, Con{P.FR{i, False{}, tl}, c}, ST.rid(tr), nl) == True{} : Bool} -> @+hmr: {NL.memn(j, ST.ids(tr)) == True{} : Bool} -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Con{P.FR{i, False{}, tl}, c}), SC.append(Nat, ST.ids(tr), P.after(Con{P.FR{i, False{}, tl}, c}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(Con{P.FR{i, False{}, tl}, c}, tr) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(c, ST.TN{i, tl, tr}) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>:  match e:    case True{}:      L.subst(Nat, z => Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{z, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, tl, tr}), P.after(c))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{z, pa_, pb_}) == PG.plug(c, ST.TN{i, tl, tr}) : ST.Tr} & ({ST.rep(~K, ST.TN{z, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, z, nl) == True{} : Bool}))>>>, i, j, N.eq_from_is_eq(i, j, he), (c, (tl, (tr, ({==}, ({==}, (hr, hok)))))))    case False{}:      pt_rc(~K, ~cmp, ~o, nl, c, i, tl, tr, j, hr, hok, hm, he, NL.memn(j, ST.ids(tl)), {==}, kl, kr)def path_to(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +t: ST.Tr, +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +j: Nat, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hm: {NL.memn(j, ST.ids(t)) == True{} : Bool}) -> Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>:  match t:    case ST.TE{}:      Empty.absurd(Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TE{}), P.after(c))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{j, pa_, pb_}) == PG.plug(c, ST.TE{}) : ST.Tr} & ({ST.rep(~K, ST.TN{j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, j, nl) == True{} : Bool}))>>>, L.false_true(hm))    case ST.TN{+i, +tl, +tr}:      pt_c(~K, ~cmp, ~o, nl, c, i, tl, tr, j, hr, hok, hm, Nat.is_eq(i, j), {==}, hrl => hol => hml => path_to(~K, ~cmp, ~o, tl, nl, Con{P.FR{i, True{}, tr}, c}, j, hrl, hol, hml), hrr => hor => hmr => path_to(~K, ~cmp, ~o, tr, nl, Con{P.FR{i, False{}, tl}, c}, j, hrr, hor, hmr))# ---- ids around a node ----def idok_sc(+a: List<&2, Nat>, +b: List<&2, Nat>, +j: Nat, +h: {CU.idok(b, j) == True{} : Bool}, +e: Bool, +he: {Nat.is_eq(j, 0n) == e : Bool}) -> {CU.idok(SC.append(Nat, a, b), j) == True{} : Bool}:  match e:    case True{}:      %Equal.sym(Bool, Nat.is_eq(j, 0n), True{}, he) : {Bool.or(_, NL.memn(j, SC.append(Nat, a, b))) == True{} : Bool}      {==}    case False{}:      %Equal.sym(Bool, Nat.is_eq(j, 0n), False{}, he) : {Bool.or(_, NL.memn(j, SC.append(Nat, a, b))) == True{} : Bool}      DJ.mem_r(j, a, b, L.subst(Bool, z => {Bool.or(z, NL.memn(j, b)) == True{} : Bool}, Nat.is_eq(j, 0n), False{}, he, h))def idok_suf(+a: List<&2, Nat>, +b: List<&2, Nat>, +j: Nat, +h: {CU.idok(b, j) == True{} : Bool}) -> {CU.idok(SC.append(Nat, a, b), j) == True{} : Bool}:  idok_sc(a, b, j, h, Nat.is_eq(j, 0n), {==})def idok_pc(+a: List<&2, Nat>, +b: List<&2, Nat>, +j: Nat, +h: {CU.idok(a, j) == True{} : Bool}, +e: Bool, +he: {Nat.is_eq(j, 0n) == e : Bool}) -> {CU.idok(SC.append(Nat, a, b), j) == True{} : Bool}:  match e:    case True{}:      %Equal.sym(Bool, Nat.is_eq(j, 0n), True{}, he) : {Bool.or(_, NL.memn(j, SC.append(Nat, a, b))) == True{} : Bool}      {==}    case False{}:      %Equal.sym(Bool, Nat.is_eq(j, 0n), False{}, he) : {Bool.or(_, NL.memn(j, SC.append(Nat, a, b))) == True{} : Bool}      DJ.mem_l(j, a, b, L.subst(Bool, z => {Bool.or(z, NL.memn(j, a)) == True{} : Bool}, Nat.is_eq(j, 0n), False{}, he, h))def idok_pre(+a: List<&2, Nat>, +b: List<&2, Nat>, +j: Nat, +h: {CU.idok(a, j) == True{} : Bool}) -> {CU.idok(SC.append(Nat, a, b), j) == True{} : Bool}:  idok_pc(a, b, j, h, Nat.is_eq(j, 0n), {==})# an id ok in a list without x is 0 or not xdef sep_c(+x: Nat, +xs: List<&2, Nat>, +j: Nat, +hn: {NL.memn(x, xs) == False{} : Bool}, +h: {CU.idok(xs, j) == True{} : Bool}, +e: Bool, +he: {Nat.is_eq(j, 0n) == e : Bool}) -> {Bool.or(Nat.is_eq(j, 0n), Bool.not(Nat.is_eq(j, x))) == True{} : Bool}:  match e:    case True{}:      %Equal.sym(Bool, Nat.is_eq(j, 0n), True{}, he) : {Bool.or(_, Bool.not(Nat.is_eq(j, x))) == True{} : Bool}      {==}    case False{}:      +hm = L.subst(Bool, z => {Bool.or(z, NL.memn(j, xs)) == True{} : Bool}, Nat.is_eq(j, 0n), False{}, he, h)      %Equal.sym(Bool, Nat.is_eq(j, x), False{}, N.is_eq_sym_false(x, j, DJ.ne_nm(x, j, xs, hn, hm))) : {Bool.or(Nat.is_eq(j, 0n), Bool.not(_)) == True{} : Bool}      CU.or_r(Nat.is_eq(j, 0n), True{}, {==})def sep_mem(+x: Nat, +xs: List<&2, Nat>, +j: Nat, +hn: {NL.memn(x, xs) == False{} : Bool}, +h: {CU.idok(xs, j) == True{} : Bool}) -> {Bool.or(Nat.is_eq(j, 0n), Bool.not(Nat.is_eq(j, x))) == True{} : Bool}:  sep_c(x, xs, j, hn, h, Nat.is_eq(j, 0n), {==})# ---- iterator_next ----# the entries around the nodedef nx_est(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +v: V, +hx: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, k} : M.Node<K>}, +hm: {ST.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}) : List<&2, M.Entry<K, V>>}:  +e0 = L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry<K, V>>}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, {==})  +e1 = FI.ents_app(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl)  +eent = L.subst(Maybe<&2, V>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, M.N{c0, x1, x2, x3, k}, z) : Maybe<&2, M.Entry<K, V>>}, ST.pv(V, pl, 1n+j), Some{v}, hm, L.subst(M.Node<K>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, z, ST.pv(V, pl, 1n+j)) : Maybe<&2, M.Entry<K, V>>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx, {==}))  +e2 = L.subst(Maybe<&2, M.Entry<K, V>>, z => {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) : List<&2, M.Entry<K, V>>}, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), Some{M.Entry{k, v}}, eent, {==})  Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), e0, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), e1, e2))def nx_sf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +v: V, +hx: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, k} : M.Node<K>}, +hm: {ST.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})) == True{} : Bool}) -> {S.succ(~K, ~V, ~cmp, k, fw, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})) == CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))) : Maybe<&2, K>}:  match fw:    case True{}:      %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(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})), S.head(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), fw_mid(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), hord)) : {S.key_m(K, V, _) == CU.ck(~K, nl, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc)))) : Maybe<&2, K>}      EN.first_key_eq(~K, ~V, nl, pl, SC.append(Nat, ST.ids(pb), P.after(pc)), L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j))), EN.oks(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), SL.oks_split_r(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, 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))))))    case False{}:      %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(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), None{}), S.last(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl)), lw_mid(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), hord)) : {S.key_m(K, V, _) == CU.ck(~K, nl, ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa)))) : Maybe<&2, K>}      EN.last_key_eq(~K, ~V, nl, pl, SC.append(Nat, P.before(pc), ST.ids(pa)), SL.oks_split_l(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, 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)))))# the key after the node is the neighbour'sdef nx_succ(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +v: V, +hx: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, k} : M.Node<K>}, +hm: {ST.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>}) -> {S.succ(~K, ~V, ~cmp, k, fw, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))) : Maybe<&2, K>}:  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), nx_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm)) : {S.succ(~K, ~V, ~cmp, k, fw, _) == CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))) : Maybe<&2, K>}  nx_sf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), nx_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))# the cursor moved on: its next the neighbour, its current the nodedef nx_cg(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}) -> {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa)))), 1n+j, lo2, hi2, fw}) == True{} : Bool}:  match fw:    case True{}:      +iY = CU.fst0_ok(SC.append(Nat, ST.ids(pb), P.after(pc)))      +iW = L.subst(List<&2, Nat>, z => {CU.idok(z, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc)))) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), ST.ids(tg), Equal.sym(List<&2, Nat>, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw), idok_suf(SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), CU.idok_cons(1n+j, SC.append(Nat, ST.ids(pb), P.after(pc)), ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), iY)))      +sp = sep_mem(1n+j, SC.append(Nat, ST.ids(pb), P.after(pc)), ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), DJ.nd_head(1n+j, SC.append(Nat, ST.ids(pb), P.after(pc)), DJ.ndr(SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, DJ.ndl(ST.ids(tg), fl, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))))), iY)      L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc)))), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), 0n), Bool.not(Nat.is_eq(ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), 1n+j))))), L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc), L.and_intro(CU.idok(ST.ids(tg), ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc)))), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), 0n), Bool.not(Nat.is_eq(ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), 1n+j)))), iW, L.and_intro(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), 0n), Bool.not(Nat.is_eq(ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), 1n+j))), L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc)), sp)))    case False{}:      +iX = CU.last0_ok(SC.append(Nat, P.before(pc), ST.ids(pa)))      +iW = L.subst(List<&2, Nat>, z => {CU.idok(z, ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa)))) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), ST.ids(tg), Equal.sym(List<&2, Nat>, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw), idok_pre(SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), iX))      +sp = sep_mem(1n+j, SC.append(Nat, P.before(pc), ST.ids(pa)), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), DJ.dj_l(SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, DJ.ndl(ST.ids(tg), fl, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), 1n+j, DJ.mem_hd(1n+j, SC.append(Nat, ST.ids(pb), P.after(pc)))), iX)      L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa)))), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), 0n), Bool.not(Nat.is_eq(ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), 1n+j))))), L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc), L.and_intro(CU.idok(ST.ids(tg), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa)))), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), 0n), Bool.not(Nat.is_eq(ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), 1n+j)))), iW, L.and_intro(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), 0n), Bool.not(Nat.is_eq(ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))), 1n+j))), L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc)), sp)))# in range: the entry, and the neighbour nextdef nx_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +v: V, +hx: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, k} : M.Node<K>}, +hm: {ST.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>}, +b: Bool) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, b, (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.succ(~K, ~V, ~cmp, k, fw, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{k}, lo2, hi2, fw}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, fw}, None{})), MI.iterator_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw, M.N{c0, x1, x2, x3, k}, M.Entry{k, v}, b), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  match b:    case False{}:      (0n, (cu, (None{}, ({==}, ({==}, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu))))), L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc), L.and_intro(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu)))), {==}, L.and_intro(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu))), L.and_left(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))), L.and_right(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc))), {==}))))))))    case True{}:      +hnd = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), hid, DJ.ndl(ST.ids(tg), fl, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))      %Equal.cong(M.Node<K>, ST.Sh<K, V> & Nat, z => MI.neighbor_node(~K, ~V, ~cmp, 1n+j, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, z)), ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx) : CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.succ(~K, ~V, ~cmp, k, fw, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{k}, lo2, hi2, fw}, Some{M.Entry{k, v}}), MI.iterator_yield(~K, ~V, ~cmp, 1n+j, lo2, hi2, fw, M.Entry{k, v}, _), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)      %Equal.sym(ST.Sh<K, V> & Nat, MI.neighbor(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, fw), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))), NB.neighbor_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, pc, 1n+j, pa, pb, h3, h4, hnd, hid, N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), fw)) : CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.succ(~K, ~V, ~cmp, k, fw, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{k}, lo2, hi2, fw}, Some{M.Entry{k, v}}), MI.iterator_yield(~K, ~V, ~cmp, 1n+j, lo2, hi2, fw, M.Entry{k, v}, _), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)      +es = nx_succ(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm)      +ej = L.subst(M.Node<K>, z => {CU.ck(~K, nl, 1n+j) == M.node_key(~K, z) : Maybe<&2, K>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx, {==})      +esp = L.subst(Maybe<&2, K>, z => {(S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, z, Some{k}, lo2, hi2, fw}, Some{M.Entry{k, v}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))), CU.ck(~K, nl, 1n+j), lo2, hi2, fw}, Some{M.Entry{k, v}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))), S.succ(~K, ~V, ~cmp, k, fw, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.sym(Maybe<&2, K>, S.succ(~K, ~V, ~cmp, k, fw, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))), es), L.subst(Maybe<&2, K>, z => {(S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))), z, lo2, hi2, fw}, Some{M.Entry{k, v}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa))))), CU.ck(~K, nl, 1n+j), lo2, hi2, fw}, Some{M.Entry{k, v}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, 1n+j), Some{k}, ej, {==}))      (ST.pk(Nat, fw, ST.fst0(SC.append(Nat, ST.ids(pb), P.after(pc))), ST.last0(SC.append(Nat, P.before(pc), ST.ids(pa)))), (1n+j, (Some{M.Entry{k, v}}, ({==}, (esp, nx_cg(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4))))))# the node and its value: found, then checked against the rangedef nx_u(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +v: V, +hx: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, k} : M.Node<K>}, +hm: {ST.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>}) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, fw}), MI.iterator_read(~K, ~V, ~cmp, 1n+j, cu, lo2, hi2, fw, M.N{c0, x1, x2, x3, k}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Some{M.Entry{k, v}})), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  +efind = Equal.trans(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})), Some{M.Entry{k, v}}, L.subst(List<&2, M.Entry<K, V>>, z => {S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.find_e(~K, ~V, ~cmp, k, z) : Maybe<&2, M.Entry<K, V>>}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), nx_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm), {==}), OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), nx_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), O.refl(~K, ~cmp, ~o, k)))  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{M.Entry{k, v}}, efind) : CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.next_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), CU.ck(~K, nl, cu), lo2, hi2, fw, _), MI.iterator_read(~K, ~V, ~cmp, 1n+j, cu, lo2, hi2, fw, M.N{c0, x1, x2, x3, k}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Some{M.Entry{k, v}})), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)  %Equal.sym(Bool, M.in_range(~K, ~V, ~cmp, k, lo2, hi2), S.in_range(~K, ~cmp, k, lo2, hi2), CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2)) : CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.next_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), CU.ck(~K, nl, cu), lo2, hi2, fw, Some{M.Entry{k, v}}), MI.iterator_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw, M.N{c0, x1, x2, x3, k}, M.Entry{k, v}, _), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)  nx_b(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm, S.in_range(~K, ~cmp, k, lo2, hi2))def nx_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +x: M.Node<K>, +hx: {ST.nd(K, nl, 1n+j) == x : M.Node<K>}, +m: Maybe<&2, V>, +hm: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, M.node_key(~K, x), CU.ck(~K, nl, cu), lo2, hi2, fw}), MI.iterator_read(~K, ~V, ~cmp, 1n+j, cu, lo2, hi2, fw, x, MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, x), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, m))), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  match x m:    case M.Free{f} None{}:      (0n, (cu, (None{}, ({==}, ({==}, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu))))), L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc), L.and_intro(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu)))), {==}, L.and_intro(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu))), L.and_left(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))), L.and_right(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc))), {==}))))))))    case M.Free{f} Some{w}:      (0n, (cu, (None{}, ({==}, ({==}, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu))))), L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc), L.and_intro(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu)))), {==}, L.and_intro(CU.idok(ST.ids(tg), cu), Bool.or(True{}, Bool.not(Nat.is_eq(0n, cu))), L.and_left(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))), L.and_right(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc))), {==}))))))))    case M.N{c0, x1, x2, x3, k} None{}:      +hs = L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j))), EN.oks(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), SL.oks_split_r(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, 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)))))      Empty.absurd(CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, M.node_key(~K, M.N{c0, x1, x2, x3, k}), CU.ck(~K, nl, cu), lo2, hi2, fw}), MI.iterator_read(~K, ~V, ~cmp, 1n+j, cu, lo2, hi2, fw, M.N{c0, x1, x2, x3, k}, MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, M.N{c0, x1, x2, x3, k}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, None{}))), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw), L.false_true(L.subst(Maybe<&2, V>, z => {S.is_some(M.Entry<K, V>, ST.ent(K, V, M.N{c0, x1, x2, x3, k}, z)) == True{} : Bool}, ST.pv(V, pl, 1n+j), None{}, hm, L.subst(M.Node<K>, z => {S.is_some(M.Entry<K, V>, ST.ent(K, V, z, ST.pv(V, pl, 1n+j))) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx, hs))))    case M.N{+c0, +x1, +x2, +x3, +k} Some{+v}:      nx_u(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, v, hx, hm)def nx_s(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  nx_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, hw, h3, h4, ST.nd(K, nl, 1n+j), {==}, ST.pv(V, pl, 1n+j), {==})def nx_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, r3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  match r3:    case Tuple{h3, h4}:      +hid = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), h1))      +e1 = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(pc), z) : List<&2, Nat>}, SC.append(Nat, SC.append(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}), P.after(pc)), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), LL.append_assoc(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}, P.after(pc)), {==})      +e2 = Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), LL.append_assoc(Nat, P.before(pc), ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}))      nx_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, hid, Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hid, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), e1, e2)), h3, h4)def nx_q(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, rest: {PG.plug(pc, ST.TN{1n+j, pa, pb}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool})) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  match rest:    case Tuple{h2, r3}:      nx_r(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, h1, r3)def nx_p(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +j: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool}, pt: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{1n+j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{1n+j, pa_, pb_}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, 1n+j, nl) == True{} : Bool}))>>>) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  match pt:    case Tuple{+pc, Tuple{+pa, Tuple{+pb, Tuple{h1, rest}}}}:      nx_q(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, pc, pa, pb, h1, rest)# a good cursor steps as the specification'sdef next_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +nx: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == True{} : Bool}) -> CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw):  match nx:    case 0n:      (0n, (cu, (None{}, ({==}, ({==}, hc)))))    case 1n+j:      +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc)      nx_p(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, cu, lo2, hi2, fw, hc, path_to(~K, ~cmp, ~o, tg, nl, Nil{}, 1n+j, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), {==}, L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(1n+j, 0n), Bool.not(Nat.is_eq(1n+j, cu))))), hc))))# ---- next_key, next_value: the answer's key or value ----def ikr_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +a: MI.MCursor<K, V>, +b: Maybe<&2, M.Entry<K, V>>) -> {MI.iterator_key_result(~K, ~V, ~cmp, (a, b)) == (a, S.key_m(K, V, b)) : MI.MCursor<K, V> & Maybe<&2, K>}:  match b:    case None{}:      {==}    case Some{M.Entry{+k, +v}}:      {==}def ivr_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +a: MI.MCursor<K, V>, +b: Maybe<&2, M.Entry<K, V>>) -> {MI.iterator_value_result(~K, ~V, ~cmp, (a, b)) == (a, S.val_m(K, V, b)) : MI.MCursor<K, V> & Maybe<&2, V>}:  match b:    case None{}:      {==}    case Some{M.Entry{+k, +v}}:      {==}def ckr(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -spr: S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, +a: MI.MCursor<K, V>, +b: Maybe<&2, M.Entry<K, V>>, +c2: MI.MCursor<K, V>, +o: Maybe<&2, M.Entry<K, V>>, +h1: {(MI.rc(~K, ~V, ~cmp, a), b) == (MI.rc(~K, ~V, ~cmp, c2), o) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {spr == (CU.cmod(~K, ~V, ~cmp, c2), o) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, K>, S.key_result(K, V, spr), (a, S.key_m(K, V, b))):  match r:    case Tuple{h2, hg}:      +ea = L.pair_fst(M.Cursor<K, V, cmp>, Maybe<&2, M.Entry<K, V>>, MI.rc(~K, ~V, ~cmp, a), b, MI.rc(~K, ~V, ~cmp, c2), o, h1)      +eb = L.pair_snd(M.Cursor<K, V, cmp>, Maybe<&2, M.Entry<K, V>>, MI.rc(~K, ~V, ~cmp, a), b, MI.rc(~K, ~V, ~cmp, c2), o, h1)      (c2, (S.key_m(K, V, o), (L.pair_eq(M.Cursor<K, V, cmp>, Maybe<&2, K>, MI.rc(~K, ~V, ~cmp, a), S.key_m(K, V, b), MI.rc(~K, ~V, ~cmp, c2), S.key_m(K, V, o), ea, L.subst(Maybe<&2, M.Entry<K, V>>, z => {S.key_m(K, V, b) == S.key_m(K, V, z) : Maybe<&2, K>}, b, o, eb, {==})), (L.subst(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => {S.key_result(K, V, spr) == S.key_result(K, V, z) : S.Cursor<K, V> & Maybe<&2, K>}, spr, (CU.cmod(~K, ~V, ~cmp, c2), o), h2, {==}), hg))))def cvr(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -spr: S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, +a: MI.MCursor<K, V>, +b: Maybe<&2, M.Entry<K, V>>, +c2: MI.MCursor<K, V>, +o: Maybe<&2, M.Entry<K, V>>, +h1: {(MI.rc(~K, ~V, ~cmp, a), b) == (MI.rc(~K, ~V, ~cmp, c2), o) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {spr == (CU.cmod(~K, ~V, ~cmp, c2), o) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.value_result(K, V, spr), (a, S.val_m(K, V, b))):  match r:    case Tuple{h2, hg}:      +ea = L.pair_fst(M.Cursor<K, V, cmp>, Maybe<&2, M.Entry<K, V>>, MI.rc(~K, ~V, ~cmp, a), b, MI.rc(~K, ~V, ~cmp, c2), o, h1)      +eb = L.pair_snd(M.Cursor<K, V, cmp>, Maybe<&2, M.Entry<K, V>>, MI.rc(~K, ~V, ~cmp, a), b, MI.rc(~K, ~V, ~cmp, c2), o, h1)      (c2, (S.val_m(K, V, o), (L.pair_eq(M.Cursor<K, V, cmp>, Maybe<&2, V>, MI.rc(~K, ~V, ~cmp, a), S.val_m(K, V, b), MI.rc(~K, ~V, ~cmp, c2), S.val_m(K, V, o), ea, L.subst(Maybe<&2, M.Entry<K, V>>, z => {S.val_m(K, V, b) == S.val_m(K, V, z) : Maybe<&2, V>}, b, o, eb, {==})), (L.subst(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => {S.value_result(K, V, spr) == S.value_result(K, V, z) : S.Cursor<K, V> & Maybe<&2, V>}, spr, (CU.cmod(~K, ~V, ~cmp, c2), o), h2, {==}), hg))))# a step refined: its key, its valuedef cok_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -spr: S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, +a: MI.MCursor<K, V>, +b: Maybe<&2, M.Entry<K, V>>, p: CU.COK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, spr, (a, b))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, K>, S.key_result(K, V, spr), MI.iterator_key_result(~K, ~V, ~cmp, (a, b))):  match p:    case Tuple{+c2, Tuple{+o, Tuple{+h1, r}}}:      %Equal.sym(MI.MCursor<K, V> & Maybe<&2, K>, MI.iterator_key_result(~K, ~V, ~cmp, (a, b)), (a, S.key_m(K, V, b)), ikr_eq(~K, ~V, ~cmp, a, b)) : CU.COK(~K, ~V, ~cmp, Maybe<&2, K>, S.key_result(K, V, spr), _)      ckr(~K, ~V, ~cmp, spr, a, b, c2, o, h1, r)def cok_val(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -spr: S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, +a: MI.MCursor<K, V>, +b: Maybe<&2, M.Entry<K, V>>, p: CU.COK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, spr, (a, b))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.value_result(K, V, spr), MI.iterator_value_result(~K, ~V, ~cmp, (a, b))):  match p:    case Tuple{+c2, Tuple{+o, Tuple{+h1, r}}}:      %Equal.sym(MI.MCursor<K, V> & Maybe<&2, V>, MI.iterator_value_result(~K, ~V, ~cmp, (a, b)), (a, S.val_m(K, V, b)), ivr_eq(~K, ~V, ~cmp, a, b)) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.value_result(K, V, spr), _)      cvr(~K, ~V, ~cmp, spr, a, b, c2, o, h1, r)def next_key_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +nx: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, K>, S.iterator_next_key(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next_key(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})):  L.subst(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => CU.COK(~K, ~V, ~cmp, Maybe<&2, K>, S.key_result(K, V, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), MI.iterator_key_result(~K, ~V, ~cmp, z)), (Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), (Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), L.pair_eta(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), cok_key(~K, ~V, ~cmp, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), L.subst(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => CU.COK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), z), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), (Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), L.pair_eta(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), CU.cstep_cok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw, next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc)))))def next_value_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +nx: Nat, +cu: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_next_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})):  L.subst(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.value_result(K, V, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), MI.iterator_value_result(~K, ~V, ~cmp, z)), (Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), (Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), L.pair_eta(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), cok_val(~K, ~V, ~cmp, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), L.subst(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => CU.COK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), z), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), (Pair.fst(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), Pair.snd(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))), L.pair_eta(MI.MCursor<K, V>, Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), CU.cstep_cok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw, next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc)))))