proofs/containers/balanced_search_tree/ccv.bend source

proofs/containers/balanced_search_tree/ccv.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 ./ord.bend as ORimport ./cur.bend as CUimport ./reads.bend as RDimport ./cnx.bend as CX# contains_value: the mirror's walk from the first entry steps through the# entries in order, each step the specification's, until a value equals the# wanted one; its answer is the specification's any_value.# (source: tools/generators/tm_hand/ccv.src)# the specification cursor's next keydef cnext(-K: Data, -V: Data, c: S.Cursor<K, V>) -> Maybe<&2, K>:  match c:    case S.CR{m, nx, cu, lo, hi, fw}:      nx# ---- the specification's step at an entry of sorted entries ----def sp_con(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +hab: {es == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +cc: Maybe<&2, K>) -> {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, es}, Some{k}, cc, M.Unbounded{}, M.Unbounded{}, True{}}) == (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}:  +ho2 = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, hord)  +hba = Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab)  +efind = L.subst(List<&2, M.Entry<K, V>>, z => {S.find_e(~K, ~V, ~cmp, k, z) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, hba, OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, xa, M.Entry{k, v}, t, ho2, O.refl(~K, ~cmp, ~o, k)))  +efw = L.subst(List<&2, M.Entry<K, V>>, z => {S.first_where(~K, ~V, ~cmp, k, False{}, z) == S.head(M.Entry<K, V>, t) : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, hba, CX.fw_mid(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, ho2))  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{M.Entry{k, v}}, efind) : {S.next_at(~K, ~V, ~cmp, l, es, cc, M.Unbounded{}, M.Unbounded{}, True{}, _) == (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, False{}, es), S.head(M.Entry<K, V>, t), efw) : {(S.CR{S.TM{l, es}, S.key_m(K, V, _), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}) == (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}  {==}# ---- found: the walk stops with True ----def cvt4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +w: V, +g: Nat, +y: Nat, +z: Nat, +oe: Maybe<&2, M.Entry<K, V>>) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, g, w, True{}, (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y, z, M.Unbounded{}, M.Unbounded{}, True{}}, oe)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, True{}) : ST.Sh<K, V> & Bool}:  match g oe:    case 0n None{}:      {==}    case 0n Some{e}:      {==}    case 1n+h None{}:      {==}    case 1n+h Some{e}:      {==}def cvt3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +w: V, +g: Nat, +y: Nat, +z: Nat, st: 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}, y, z, M.Unbounded{}, M.Unbounded{}, True{}})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y, z, M.Unbounded{}, M.Unbounded{}, True{}}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Unbounded{}, M.Unbounded{}, True{})) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, g, w, True{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y, z, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, True{}) : ST.Sh<K, V> & Bool}:  match st:    case Tuple{+y2, Tuple{+z2, Tuple{+oe, Tuple{+hm, r}}}}:      %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}, y, z, M.Unbounded{}, M.Unbounded{}, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe), hm) : {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, g, w, True{}, _) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, True{}) : ST.Sh<K, V> & Bool}      cvt4(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, g, y2, z2, oe)# ---- no entry left: the walk stops with False ----def cvn3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +w: V, +x: Nat, +nx: Nat, +cu: Nat, +hk: {CU.ck(~K, nl, nx) == None{} : Maybe<&2, K>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hs: {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, M.Unbounded{}, M.Unbounded{}, True{}})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Nil{}))) : ST.Sh<K, V> & Bool}:  +hs2 = L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), M.Unbounded{}, M.Unbounded{}, True{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), None{}, hk, hs)  +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), M.Unbounded{}, M.Unbounded{}, True{}}, None{}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, oe, hs2)  %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, M.Unbounded{}, M.Unbounded{}, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe), hm) : {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), w, False{}, _) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Nil{}))) : ST.Sh<K, V> & Bool}  %eo : {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), w, False{}, (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, _)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Nil{}))) : ST.Sh<K, V> & Bool}  {==}def cvn2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +w: V, +x: Nat, +nx: Nat, +cu: Nat, +hk: {CU.ck(~K, nl, nx) == None{} : Maybe<&2, K>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {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, M.Unbounded{}, M.Unbounded{}, True{}})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool}) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Nil{}))) : ST.Sh<K, V> & Bool}:  match r:    case Tuple{hs, hc2}:      cvn3(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, x, nx, cu, hk, y2, z2, oe, hm, hs)def cvn(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +w: V, +x: Nat, +nx: Nat, +cu: Nat, +hk: {CU.ck(~K, nl, nx) == None{} : Maybe<&2, K>}, st: 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, M.Unbounded{}, M.Unbounded{}, True{}})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Unbounded{}, M.Unbounded{}, True{})) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Nil{}))) : ST.Sh<K, V> & Bool}:  match st:    case Tuple{+y2, Tuple{+z2, Tuple{+oe, Tuple{+hm, r}}}}:      cvn2(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, x, nx, cu, hk, y2, z2, oe, hm, r)# ---- an entry: its value compared, the walk goes on past it ----def cvc4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +w: V, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +x: Nat, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == Some{k} : Maybe<&2, K>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hc2: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool}, +heq: {(S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), w, eq(v, w), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(eq(v, w), S.any_value(~K, ~V, ~eq, w, t))) : ST.Sh<K, V> & Bool}) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Con{M.Entry{k, v}, t}))) : ST.Sh<K, V> & Bool}:  +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, oe, heq)  +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, oe, heq)  +hk2 = Equal.sym(Maybe<&2, K>, S.key_m(K, V, S.head(M.Entry<K, V>, t)), CU.ck(~K, nl, y2), L.subst(S.Cursor<K, V>, q => {S.key_m(K, V, S.head(M.Entry<K, V>, t)) == cnext(K, V, q) : Maybe<&2, K>}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, ec, {==}))  %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, M.Unbounded{}, M.Unbounded{}, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe), hm) : {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), w, False{}, _) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Con{M.Entry{k, v}, t}))) : ST.Sh<K, V> & Bool}  %eo : {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), w, False{}, (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, _)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Con{M.Entry{k, v}, t}))) : ST.Sh<K, V> & Bool}  kont(y2, z2, hc2, hk2)def cvc3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +w: V, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +x: Nat, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == Some{k} : Maybe<&2, K>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hs: {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, M.Unbounded{}, M.Unbounded{}, True{}})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hc2: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), w, eq(v, w), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(eq(v, w), S.any_value(~K, ~V, ~eq, w, t))) : ST.Sh<K, V> & Bool}) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Con{M.Entry{k, v}, t}))) : ST.Sh<K, V> & Bool}:  +hs2 = L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), M.Unbounded{}, M.Unbounded{}, True{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, hk, hs)  +spc = sp_con(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), xa, k, v, t, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu))  +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{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), M.Unbounded{}, M.Unbounded{}, True{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), M.Unbounded{}, M.Unbounded{}, True{}}, oe), Equal.sym(S.Cursor<K, V> & 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), M.Unbounded{}, M.Unbounded{}, True{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, M.Unbounded{}, M.Unbounded{}, True{}}, Some{M.Entry{k, v}}), spc), hs2)  cvc4(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w, xa, k, v, t, x, nx, cu, hab, hk, y2, z2, oe, hm, hc2, heq, kont)def cvc2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +w: V, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +x: Nat, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == Some{k} : Maybe<&2, K>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {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, M.Unbounded{}, M.Unbounded{}, True{}})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), w, eq(v, w), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(eq(v, w), S.any_value(~K, ~V, ~eq, w, t))) : ST.Sh<K, V> & Bool}) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Con{M.Entry{k, v}, t}))) : ST.Sh<K, V> & Bool}:  match r:    case Tuple{hs, hc2}:      cvc3(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w, xa, k, v, t, x, nx, cu, hab, hk, y2, z2, oe, hm, hs, hc2, kont)def cvc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +w: V, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +x: Nat, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == Some{k} : Maybe<&2, K>}, st: 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, M.Unbounded{}, M.Unbounded{}, True{}})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Unbounded{}, M.Unbounded{}, True{}), kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), w, eq(v, w), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(eq(v, w), S.any_value(~K, ~V, ~eq, w, t))) : ST.Sh<K, V> & Bool}) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(False{}, S.any_value(~K, ~V, ~eq, w, Con{M.Entry{k, v}, t}))) : ST.Sh<K, V> & Bool}:  match st:    case Tuple{+y2, Tuple{+z2, Tuple{+oe, Tuple{+hm, r}}}}:      cvc2(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w, xa, k, v, t, x, nx, cu, hab, hk, y2, z2, oe, hm, r, kont)# ---- the walk: the entries before the cursor visited, the rest ahead ----def cvl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +w: V, +bs: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +x: Nat, +nx: Nat, +cu: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}}) == True{} : Bool}, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, bs) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.head(M.Entry<K, V>, bs)) : Maybe<&2, K>}, +f: Bool) -> {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, bs), x), w, f, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Bool.or(f, S.any_value(~K, ~V, ~eq, w, bs))) : ST.Sh<K, V> & Bool}:  match bs f:    case Nil{} True{}:      cvt3(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), nx, cu, CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}, hc))    case Con{+e, +t} True{}:      cvt3(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{e, t}), x), nx, cu, CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}, hc))    case Nil{} False{}:      cvn(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, x, nx, cu, hk, CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}, hc))    case Con{M.Entry{+k, +v}, +t} False{}:      cvc(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w, xa, k, v, t, x, nx, cu, hab, hk, CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, M.Unbounded{}, M.Unbounded{}, True{}, hc), ky => kz => kc => kk => cvl(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w, t, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), x, ky, kz, kc, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), SC.append(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), t), hab, Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), t), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), LL.append_assoc(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}, t))), kk, eq(v, w)))# contains_value: the walk from the first entry with enough fueldef contains_value_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +w: V) -> {MI.contains_value(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.any_value(~K, ~V, ~eq, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Bool}:  +hn = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), 0n), SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), n, N.add_zero(SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), Equal.sym(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))  %hn : {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+_, w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo, 0n, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.any_value(~K, ~V, ~eq, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Bool}  %Equal.sym(Nat, lo, ST.fst0(ST.ids(tg)), N.eq_from_is_eq(lo, ST.fst0(ST.ids(tg)), ST.g_clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))) : {MI.contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+Nat.add(SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), 0n), w, False{}, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _, 0n, M.Unbounded{}, M.Unbounded{}, True{}})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.any_value(~K, ~V, ~eq, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Bool}  cvl(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl), Nil{}, 0n, ST.fst0(ST.ids(tg)), 0n, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, ST.fst0(ST.ids(tg)), CU.fst0_ok(ST.ids(tg)), True{}), {==}, Equal.sym(Maybe<&2, K>, S.key_m(K, V, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), CU.ck(~K, nl, ST.fst0(ST.ids(tg))), EN.first_key_eq(~K, ~V, nl, pl, ST.ids(tg), 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)))), False{})