proofs/containers/balanced_search_tree/vsz.bend

bend-collections-laws-containers@1.0.0.0 · 250 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
8import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as OR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/reads.bend as RD
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cur.bend as CU
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cnx.bend as CX
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsp.bend as VS
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vit.bend as VI
17
18# A view's size: the mirror counts the steps of the view's cursor, forward
19# from the first entry above the lower bound (backward from the last below
20# the upper), until an entry is out of range; the count is the number of
21# entries within. (source: tools/generators/tm_hand/vsz.src)
22
23
24# ---- a step whose specification is known ----
25
26def cnext(-K: Data, -V: Data, c: S.Cursor<K, V>) -> Maybe<&2, K>:
27  match c:
28    case S.CR{m, nx, cu, lo, hi, fw}:
29      nx
30
31def stp3(~K: Data, ~V: Data, ~cmp: K -> 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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {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})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +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, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, 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, lo2, hi2, fw})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}), 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, lo2, hi2, fw}) == True{} : Bool}) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
32  +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)}, a, bb, lo2, hi2, fw}, o0), 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})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe), Equal.sym(S.Cursor<K, V> & 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})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0), hsp), hs)
33  +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)}, a, bb, lo2, hi2, fw}, o0, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe, heq)
34  +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)}, a, bb, lo2, hi2, fw}, o0, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe, heq)
35  +hk2 = Equal.sym(Maybe<&2, K>, a, CU.ck(~K, nl, y2), L.subst(S.Cursor<K, V>, q => {a == cnext(K, V, q) : Maybe<&2, K>}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, ec, {==}))
36  +hm2 = L.subst(Maybe<&2, M.Entry<K, V>>, q => {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.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, q) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, oe, o0, Equal.sym(Maybe<&2, M.Entry<K, V>>, o0, oe, eo), hm)
37  (y2, (z2, (hm2, (hk2, hc2))))
38
39def stp2(~K: Data, ~V: Data, ~cmp: K -> 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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {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})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +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, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, 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, lo2, hi2, fw})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}), 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, lo2, hi2, fw}) == True{} : Bool}) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
40  match r:
41    case Tuple{hs, hc2}:
42      stp3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, cu, a, bb, o0, hsp, y2, z2, oe, hm, hs, hc2)
43
44def stp(~K: Data, ~V: Data, ~cmp: K -> 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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {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})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, 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, 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)) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
45  match st:
46    case Tuple{+y2, Tuple{+z2, Tuple{+oe, Tuple{+hm, r}}}}:
47      stp2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, cu, a, bb, o0, hsp, y2, z2, oe, hm, r)
48
49# ---- the specification's step at an entry, either way ----
50
51
52def find_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +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}) -> {S.find_e(~K, ~V, ~cmp, k, es) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
53  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, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, xa, M.Entry{k, v}, t, 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), O.refl(~K, ~cmp, ~o, k)))
54
55def sp_f(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>) -> {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, es}, Some{k}, cc, lo2, hi2, True{}}) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}:
56  +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, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), CX.fw_mid(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, 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)))
57  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{M.Entry{k, v}}, find_at(~K, ~V, ~cmp, ~o, es, xa, k, v, t, hab, hord)) : {S.next_at(~K, ~V, ~cmp, l, es, cc, lo2, hi2, True{}, _) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
58  %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.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, _), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
59  {==}
60
61def sp_b(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>) -> {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, es}, Some{k}, cc, lo2, hi2, False{}}) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}:
62  +elw = L.subst(List<&2, M.Entry<K, V>>, z => {S.last_where(~K, ~V, ~cmp, k, False{}, z, None{}) == S.last(M.Entry<K, V>, xa) : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), CX.lw_mid(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, 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)))
63  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{M.Entry{k, v}}, find_at(~K, ~V, ~cmp, ~o, es, xa, k, v, t, hab, hord)) : {S.next_at(~K, ~V, ~cmp, l, es, cc, lo2, hi2, False{}, _) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
64  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, False{}, es, None{}), S.last(M.Entry<K, V>, xa), elw) : {S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, _), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
65  {==}
66
67# ---- forward ----
68
69
70def szn2(~K: Data, ~V: Data, ~cmp: K -> 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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, +y2: Nat, +z2: Nat, +hm: {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, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}:
71  %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, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}
72  {==}
73
74def szn(~K: Data, ~V: Data, ~cmp: K -> 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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}:
75  match r:
76    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
77      szn2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, y2, z2, hm)
78
79def szt2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +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>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +y2: Nat, +z2: Nat, +hm: {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, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {CU.ck(~K, nl, y2) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, 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, lo2, hi2, 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.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
80  match r:
81    case Tuple{hk2, hc2}:
82      %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, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}
83      +e2 = VS.cong(List<&2, M.Entry<K, V>>, Nat, q => Nat.add(SC.length(M.Entry<K, V>, q), c), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Con{M.Entry{k, v}, S.within(~K, ~V, ~cmp, lo2, hi2, t)}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, t, hb))
84      +e3 = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c), 1n+Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), N.add_succ(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), Equal.sym(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), 1n+Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), e2))
85      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)), kont(y2, z2, hc2, hk2), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), e3))
86
87def szt(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +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>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, 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, lo2, hi2, 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.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
88  match r:
89    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
90      szt2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, y2, z2, hm, r2, kont)
91
92def szs2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +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>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +y2: Nat, +z2: Nat, +hm: {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, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
93  %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, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}
94  +hbu = VS.bu_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal), hb)
95  +ho = OR.ord_app_r(~K, ~V, ~cmp, xa, Con{M.Entry{k, v}, t}, 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>, xa, Con{M.Entry{k, v}, t}), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
96  +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), S.within(~K, ~V, ~cmp, lo2, hi2, t), Nil{}, VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, t, hb), VS.wnil(~K, ~V, ~cmp, ~o, lo2, hi2, k, t, hbu, OR.ord_gt(~K, ~V, ~cmp, ~o, t, M.Entry{k, v}, ho)))
97  Equal.sym(MI.MView<K, V> & Nat, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, c), VS.cong(List<&2, M.Entry<K, V>>, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, q), c)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Nil{}, hw))
98
99def szs(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +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>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
100  match r:
101    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
102      szs2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, y2, z2, hm)
103
104def szc(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +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>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +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, True{}}) == True{} : Bool}, +hk: {CU.ck(~K, nl, nx) == Some{k} : Maybe<&2, K>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : 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, lo2, hi2, 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.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
105  match b:
106    case True{}:
107      +e2 = Equal.trans(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), lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (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}, lo2, hi2, True{}}, 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, True{}}, None{})), (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}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), sp_f(~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), lo2, hi2), VS.pk_t(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (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}, lo2, hi2, True{}}, 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, True{}}, None{}), hb))
108      szt(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, Some{M.Entry{k, v}}, Equal.trans(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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}), 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, 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}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), 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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}) == 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), lo2, hi2, True{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, hk, {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)), kont)
109    case False{}:
110      +e2 = Equal.trans(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), lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (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}, lo2, hi2, True{}}, 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, True{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), sp_f(~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), lo2, hi2), VS.pk_f(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (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}, lo2, hi2, True{}}, 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, True{}}, None{}), hb))
111      szs(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, Equal.trans(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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}), 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, True{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), 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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}) == 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), lo2, hi2, True{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, hk, {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)))
112
113
114# the count forward: the entries within from the cursor on
115def szf(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +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, lo2, hi2, 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>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, bs) == True{} : Bool}, +c: Nat) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, bs), x), c, 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, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, bs)), c)) : MI.MView<K, V> & Nat}:
116  match bs:
117    case Nil{}:
118      szn(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, 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), lo2, hi2, True{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, None{}, CU.ck(~K, nl, nx), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, nx), None{}, hk), {==}), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)))
119    case Con{M.Entry{+k, +v}, +t}:
120      szc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hc, hk, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, ky => kz => kc => kk => szf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, t, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), 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, L.and_right(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal), 1n+c))
121
122# ---- backward: the entries before the cursor, reversed ----
123
124
125def sbn2(~K: Data, ~V: Data, ~cmp: K -> 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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, +y2: Nat, +z2: Nat, +hm: {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, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}:
126  %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, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}
127  {==}
128
129def sbn(~K: Data, ~V: Data, ~cmp: K -> 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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}:
130  match r:
131    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
132      sbn2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, y2, z2, hm)
133
134# the entries within the reversal of e before t: those of t's, then e's
135def wl_snoc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +t: List<&2, M.Entry<K, V>>, +k: K, +v: V) -> {S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})) == SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})) : List<&2, M.Entry<K, V>>}:
136  Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}), LL.snoc_append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), VS.within_app(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}))
137
138def sbt2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +y2: Nat, +z2: Nat, +hm: {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, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {CU.ck(~K, nl, y2) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == 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, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
139  match r:
140    case Tuple{hk2, hc2}:
141      %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, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}
142      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}), wl_snoc(~K, ~V, ~cmp, lo2, hi2, t, k, v), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), q), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}}), Con{M.Entry{k, v}, Nil{}}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)))
143      +el = Equal.trans(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}})), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}), ew), LL.length_append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}))
144      +e3 = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), Nat.add(Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c), Equal.sym(Nat, Nat.add(Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), N.add_assoc(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n, c)), VS.cong(Nat, Nat, q => Nat.add(q, c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), el)))
145      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c)), kont(y2, z2, hc2, hk2), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c), e3))
146
147def sbt(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == 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, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
148  match r:
149    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
150      sbt2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, y2, z2, hm, r2, kont)
151
152def sbs2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +y2: Nat, +z2: Nat, +hm: {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, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
153  %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, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}
154  +hal = VS.al_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu), hb)
155  +ho = 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>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
156  +hw1 = VS.wnil_lt(~K, ~V, ~cmp, ~o, lo2, hi2, k, SC.reverse(M.Entry<K, V>, t), hal, OR.ord_mid_l(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, ho))
157  +hw2 = VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)
158  +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), Nil{}, wl_snoc(~K, ~V, ~cmp, lo2, hi2, t, k, v), L.subst(List<&2, M.Entry<K, V>>, q => {SC.append(M.Entry<K, V>, q, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})) == Nil{} : List<&2, M.Entry<K, V>>}, Nil{}, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Nil{}, hw1), hw2))
159  Equal.sym(MI.MView<K, V> & Nat, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, c), VS.cong(List<&2, M.Entry<K, V>>, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, q), c)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Nil{}, hw))
160
161def sbs(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {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, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
162  match r:
163    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
164      sbs2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, y2, z2, hm)
165
166
167def sbc(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +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, False{}}) == True{} : Bool}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))) : Maybe<&2, K>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : 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, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
168  match b:
169    case True{}:
170      +e2 = Equal.trans(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), lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, 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, False{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), sp_b(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.reverse(M.Entry<K, V>, t), k, v, bs, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_t(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, 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, False{}}, None{}), hb))
171      sbt(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, Some{M.Entry{k, v}}, Equal.trans(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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}), 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, False{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), 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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}) == 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), lo2, hi2, False{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, nx), S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Some{k}, hk, VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Some{M.Entry{k, v}}, LL.last_snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)), kont)
172    case False{}:
173      +e2 = Equal.trans(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), lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, 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, False{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), sp_b(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.reverse(M.Entry<K, V>, t), k, v, bs, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_f(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, 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, False{}}, None{}), hb))
174      sbs(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, Equal.trans(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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}), 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, False{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), 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)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}) == 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), lo2, hi2, False{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, nx), S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Some{k}, hk, VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Some{M.Entry{k, v}}, LL.last_snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)))
175
176
177# the count backward: the entries within before the cursor
178def szb(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +rr: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +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, lo2, hi2, False{}}) == True{} : Bool}, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr), bs) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr))) : Maybe<&2, K>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, rr) == True{} : Bool}, +c: Nat) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, rr), x), c, 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, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, rr))), c)) : MI.MView<K, V> & Nat}:
179  match rr:
180    case Nil{}:
181      sbn(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, 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), lo2, hi2, False{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, None{}, CU.ck(~K, nl, nx), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, nx), None{}, hk), {==}), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)))
182    case Con{M.Entry{+k, +v}, +t}:
183      sbc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), hbu, c, hc, hk, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, ky => kz => kc => kk => szb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, t, Con{M.Entry{k, v}, bs}, 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>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), kk, L.and_right(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu), 1n+c))
184
185# ---- the view's size ----
186
187
188def vsf2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>})) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
189  match r:
190    case Tuple{hal, Tuple{hwa, hfb}}:
191      %Equal.sym(ST.Sh<K, V> & Nat, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, True{}, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
192      +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), LL.length_append(M.Entry<K, V>, xa, xb), N.add_comm(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)))
193      %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+_, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
194      +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), h2, Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), VS.start_fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.head(M.Entry<K, V>, xb), hfb)))
195      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), VS.within_app(~K, ~V, ~cmp, lo2, hi2, xa, xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, q, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xa), Nil{}, hwa)))
196      +ec = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), N.add_zero(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), ew)))
197      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))), szf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, SC.length(M.Entry<K, V>, xa), xb, xa, j, 0n, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, True{}), hab, hk, hal, 0n), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), ec))
198
199def vsf1(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
200  match sp:
201    case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}:
202      vsf2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)
203
204def vsb2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>})) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
205  match r:
206    case Tuple{hbu, Tuple{hwb, hlb}}:
207      %Equal.sym(ST.Sh<K, V> & Nat, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, False{}, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
208      +err = LL.spec_rev_rev(M.Entry<K, V>, xa)
209      +hab2 = L.subst(List<&2, M.Entry<K, V>>, q => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, q, xb) : List<&2, M.Entry<K, V>>}, xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err), hab)
210      +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), LL.length_append(M.Entry<K, V>, xa, xb), VS.cong(Nat, Nat, q => Nat.add(q, SC.length(M.Entry<K, V>, xb)), SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(Nat, SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xa), LL.length_rev(M.Entry<K, V>, xa))))
211      %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+_, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
212      +hk0 = Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), VS.start_lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last(M.Entry<K, V>, xa), Equal.trans(Maybe<&2, M.Entry<K, V>>, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}), S.last(M.Entry<K, V>, xa), hlb, OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, xa)))))
213      +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), h2, hk0), VS.cong(List<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, S.last(M.Entry<K, V>, q)), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err)))
214      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), VS.within_app(~K, ~V, ~cmp, lo2, hi2, xa, xb), Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), Nil{}), S.within(~K, ~V, ~cmp, lo2, hi2, xa), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), q), S.within(~K, ~V, ~cmp, lo2, hi2, xb), Nil{}, hwb), LL.append_nil(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa))), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err)))))
215      +ec = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), N.add_zero(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), ew)))
216      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))), szb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, SC.length(M.Entry<K, V>, xb), SC.reverse(M.Entry<K, V>, xa), xb, j, 0n, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, False{}), hab2, hk, VS.allbu_rev(~K, ~V, ~cmp, hi2, xa, hbu), 0n), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), ec))
217
218def vsb1(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>}))>>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
219  match sp:
220    case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}:
221      vsb2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)
222
223
224def vrf2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
225  match r:
226    case Tuple{h2, h3}:
227      vsf1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_fal(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
228
229def vrf(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
230  match r:
231    case Tuple{+j, Tuple{+h1, r2}}:
232      vrf2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)
233
234def vrb2(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
235  match r:
236    case Tuple{h2, h3}:
237      vsb1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_lbu(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
238
239def vrb(~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.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
240  match r:
241    case Tuple{+j, Tuple{+h1, r2}}:
242      vrb2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)
243
244# the mirror's size of a view: the number of entries within
245def view_size_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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
246  match d2:
247    case True{}:
248      vrb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, hi2, False{}))
249    case False{}:
250      vrf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, True{}))