proofs/containers/balanced_search_tree/vclr.bend

bend-collections-laws-containers@1.0.0.0 · 260 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/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as OR
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dord.bend as DO
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cur.bend as CU
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsp.bend as VS
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsz.bend as VZ
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vdef.bend as VD
16
17# A view's clear: the implementation walks the view's cursor, removing each
18# entry in range, until one is out of range; each step is the specification
19# cursor's, so what is left is the entries outside the view.
20# (source: tools/generators/tm_hand/vclr.src)
21
22
23# ---- the cursor's view ----
24
25def vw_of(-K: Data, -V: Data, c: S.Cursor<K, V>) -> S.View<K, V>:
26  match c:
27    case S.CR{m, nx, cu, lo, hi, fw}:
28      S.VW{m, lo, hi, Bool.not(fw)}
29
30def iv_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c2: MI.MCursor<K, V>, +hc2: {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, vw_of(K, V, CU.cmod(~K, ~V, ~cmp, c2)), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))):
31  match c2:
32    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +a, +b, +lo3, +hi3, +fw3}:
33      (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo3, hi3, Bool.not(fw3)}, ({==}, ({==}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), a), Bool.and(CU.idok(ST.ids(tg), b), Bool.or(Nat.is_eq(a, 0n), Bool.not(Nat.is_eq(a, b))))), hc2))))
34
35def is_nil(-A: Data, xs: List<&2, A>) -> Bool:
36  match xs:
37    case Nil{}:
38      True{}
39    case Con{h, t}:
40      False{}
41
42def con_nil(-A: Data, +x: A, +t: List<&2, A>, +h: {Con{x, t} == Nil{} : List<&2, A>}) -> Empty:
43  L.false_true(VS.cong(List<&2, A>, Bool, z => is_nil(A, z), Con{x, t}, Nil{}, h))
44
45# nothing within: nothing to clear
46def oid_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}) == Nil{} : List<&2, M.Entry<K, V>>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2) == b : Bool}, kf: @+ht: {S.within(~K, ~V, ~cmp, lo2, hi2, t) == Nil{} : List<&2, M.Entry<K, V>>} -> {S.outside(~K, ~V, ~cmp, lo2, hi2, t) == t : List<&2, M.Entry<K, V>>}) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}) == Con{e, t} : List<&2, M.Entry<K, V>>}:
47  match b:
48    case True{}:
49      Empty.absurd({S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}) == Con{e, t} : List<&2, M.Entry<K, V>>}, con_nil(M.Entry<K, V>, e, S.within(~K, ~V, ~cmp, lo2, hi2, t), Equal.trans(List<&2, M.Entry<K, V>>, Con{e, S.within(~K, ~V, ~cmp, lo2, hi2, t)}, S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Nil{}, Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lo2, hi2, t)}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, e, t, hb)), h)))
50    case False{}:
51      +ht = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, t), S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Nil{}, Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.within(~K, ~V, ~cmp, lo2, hi2, t), VS.w_out(~K, ~V, ~cmp, lo2, hi2, e, t, hb)), h)
52      Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, Con{e, t}, VS.pk_f(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, S.outside(~K, ~V, ~cmp, lo2, hi2, t), t, kf(ht)))
53
54def out_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +xs: List<&2, M.Entry<K, V>>, +h: {S.within(~K, ~V, ~cmp, lo2, hi2, xs) == Nil{} : List<&2, M.Entry<K, V>>}) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, xs) == xs : List<&2, M.Entry<K, V>>}:
55  match xs:
56    case Nil{}:
57      {==}
58    case Con{+e, +t}:
59      oid_c(~K, ~V, ~cmp, lo2, hi2, e, t, h, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), {==}, ht => out_id(~K, ~V, ~cmp, lo2, hi2, t, ht))
60
61def oapp_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +ih: {S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)) == SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)) : List<&2, M.Entry<K, V>>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2) == b : Bool}) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)) == SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)) : List<&2, M.Entry<K, V>>}:
62  match b:
63    case True{}:
64      +l1 = VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys))}, hb)
65      +r1 = VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, z, S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, t), VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb))
66      Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), l1, ih), Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), r1))
67    case False{}:
68      +l1 = VS.pk_f(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys))}, hb)
69      +r1 = VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, z, S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, VS.pk_f(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb))
70      Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), Con{e, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys))}, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys))}, Con{e, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys))}, l1, VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), ih)), Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), Con{e, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys))}, r1))
71
72def out_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xs, ys)) == SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xs), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)) : List<&2, M.Entry<K, V>>}:
73  match xs:
74    case Nil{}:
75      {==}
76    case Con{+e, +t}:
77      oapp_c(~K, ~V, ~cmp, lo2, hi2, e, t, ys, out_app(~K, ~V, ~cmp, lo2, hi2, t, ys), S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), {==})
78
79# ---- forward ----
80
81
82# a cursor at the end of the run: its view
83def cf_end(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +cc: Maybe<&2, K>, -sp: S.View<K, V>, -r: M.View<K, V, cmp>, +c2: MI.MCursor<K, V>, +hc2: {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, +ec: {S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +hs: {S.VW{S.TM{l, es}, lo2, hi2, False{}} == sp : S.View<K, V>}, +hr: {M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == r : M.View<K, V, cmp>}) -> VD.VOK(~K, ~V, ~cmp, sp, r):
84  L.subst(M.View<K, V, cmp>, z => VD.VOK(~K, ~V, ~cmp, sp, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), r, hr, L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), S.VW{S.TM{l, es}, lo2, hi2, False{}}, sp, hs, L.subst(S.Cursor<K, V>, z => VD.VOK(~K, ~V, ~cmp, vw_of(K, V, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, CU.cmod(~K, ~V, ~cmp, c2), ec), iv_ok(~K, ~V, ~cmp, c2, hc2))))
85
86
87def cfn2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
88  match r:
89    case Tuple{h2, h3}:
90      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, hsp)), h2)
91      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
92      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
93      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), _))
94      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
95      cf_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, xa, Nil{}), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, {==}, {==})
96
97def cfn(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
98  match p:
99    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
100      cfn2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, c, cc, hsp, c2, ov, h1, r)
101
102def cfs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
103  match r:
104    case Tuple{h2, h3}:
105      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}}, hsp), VZ.sp_f(~K, ~V, ~cmp, ~o, l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), xa, k, v, t, {==}, hord, cc, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), hb))
106      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), hsv), h2)
107      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
108      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
109      +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)
110      +ho = OR.ord_app_r(~K, ~V, ~cmp, xa, Con{M.Entry{k, v}, t}, hord)
111      +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)))
112      +hs = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, z)}, lo2, hi2, False{}}, Con{M.Entry{k, v}, t}, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Con{M.Entry{k, v}, t}, out_id(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}, hw)))
113      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
114      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
115      cf_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, hs, {==})
116
117def cfs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
118  match p:
119    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
120      cfs2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ov, h1, r)
121
122def cft4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +c3: MI.MCursor<K, V>, +o3: Maybe<&2, V>, +g1: {M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == (MI.rc(~K, ~V, ~cmp, c3), o3) : M.Cursor<K, V, cmp> & Maybe<&2, V>}, r: {S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)) == (CU.cmod(~K, ~V, ~cmp, c3), o3) : S.Cursor<K, V> & Maybe<&2, V>} & {CU.cgood(~K, ~V, ~cmp, c3) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
123  match r:
124    case Tuple{g2, g3}:
125      +f1 = VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, V>, z => S.iterator_remove(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, CU.cmod(~K, ~V, ~cmp, c2), ec))
126      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}), S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), (CU.cmod(~K, ~V, ~cmp, c3), o3), Equal.sym(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}), f1), g2)
127      +ec3 = L.pair_fst(S.Cursor<K, V>, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}))}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, S.find(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})), CU.cmod(~K, ~V, ~cmp, c3), o3, heq)
128      +hdel = DO.del_mid(~K, ~V, ~cmp, ~o, k, xa, M.Entry{k, v}, t, OR.ord_mid_l(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, hord), O.refl(~K, ~cmp, ~o, k))
129      +hsp3 = Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, c3), S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}))}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}))}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, CU.cmod(~K, ~V, ~cmp, c3), ec3), VS.cong(List<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})), SC.append(M.Entry<K, V>, xa, t), hdel))
130      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, V>, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), (MI.rc(~K, ~V, ~cmp, c3), o3), g1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, _)))
131      +eo = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, z)}, lo2, hi2, False{}}, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, t), VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{M.Entry{k, v}, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb)))
132      L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c3)))), S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, eo, kont(c3, g3, hsp3))
133
134def cft3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, q: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
135  match q:
136    case Tuple{+c3, Tuple{+o3, Tuple{+g1, r}}}:
137      cft4(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ec, c3, o3, g1, r, kont)
138
139def cft2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
140  match r:
141    case Tuple{h2, h3}:
142      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}}, hsp), VZ.sp_f(~K, ~V, ~cmp, ~o, l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), xa, k, v, t, {==}, hord, cc, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, 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, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), hb))
143      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), hsv), h2)
144      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
145      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
146      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
147      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
148      cft3(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ec, rok(c2, h3), kont)
149
150def cft(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
151  match p:
152    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
153      cft2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ov, h1, r, kont)
154
155def cfc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
156  match b:
157    case True{}:
158      cft(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, p, kont)
159    case False{}:
160      cfs(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, p)
161
162# the clear forward: every entry of the run from the cursor on removed
163def clf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, bs)}, S.key_m(K, V, S.head(M.Entry<K, V>, bs)), cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, bs)) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, bs) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, bs))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, bs), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
164  match bs:
165    case Nil{}:
166      cfn(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, c, cc, hsp, nok(c, hc))
167    case Con{M.Entry{+k, +v}, +t}:
168      cfc(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, nok(c, hc), kc3 => kh3 => ks3 => clf(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, t, kc3, None{}, kh3, ks3, DO.ord_drop(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, hord), L.and_right(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal)))
169
170# ---- backward: the entries before the cursor, reversed, then the rest ----
171
172
173def cb_end(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +cc: Maybe<&2, K>, -sp: S.View<K, V>, -r: M.View<K, V, cmp>, +c2: MI.MCursor<K, V>, +hc2: {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, +ec: {S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +hs: {S.VW{S.TM{l, es}, lo2, hi2, True{}} == sp : S.View<K, V>}, +hr: {M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == r : M.View<K, V, cmp>}) -> VD.VOK(~K, ~V, ~cmp, sp, r):
174  L.subst(M.View<K, V, cmp>, z => VD.VOK(~K, ~V, ~cmp, sp, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), r, hr, L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), S.VW{S.TM{l, es}, lo2, hi2, True{}}, sp, hs, L.subst(S.Cursor<K, V>, z => VD.VOK(~K, ~V, ~cmp, vw_of(K, V, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, CU.cmod(~K, ~V, ~cmp, c2), ec), iv_ok(~K, ~V, ~cmp, c2, hc2))))
175
176def cbn2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
177  match r:
178    case Tuple{h2, h3}:
179      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, hsp)), h2)
180      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
181      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
182      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), _))
183      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
184      cb_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, {==}, {==})
185
186def cbn(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
187  match p:
188    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
189      cbn2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, c, cc, hsp, c2, ov, h1, r)
190
191def cbs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
192  match r:
193    case Tuple{h2, h3}:
194      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}, hsp), VZ.sp_b(~K, ~V, ~cmp, ~o, l, 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.reverse(M.Entry<K, V>, t), k, v, bs, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord, cc, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), hb))
195      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), hsv), h2)
196      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
197      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
198      +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)
199      +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, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, 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}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord)))
200      +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{}, VZ.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), VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)))
201      +hs = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, z, bs)}, lo2, hi2, True{}}, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), out_id(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), hw)))
202      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
203      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
204      cb_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, hs, {==})
205
206def cbs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
207  match p:
208    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
209      cbs2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ov, h1, r)
210
211def cbt4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +c3: MI.MCursor<K, V>, +o3: Maybe<&2, V>, +g1: {M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == (MI.rc(~K, ~V, ~cmp, c3), o3) : M.Cursor<K, V, cmp> & Maybe<&2, V>}, r: {S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)) == (CU.cmod(~K, ~V, ~cmp, c3), o3) : S.Cursor<K, V> & Maybe<&2, V>} & {CU.cgood(~K, ~V, ~cmp, c3) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
212  match r:
213    case Tuple{g2, g3}:
214      +f1 = VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, V>, z => S.iterator_remove(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, CU.cmod(~K, ~V, ~cmp, c2), ec))
215      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}), S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), (CU.cmod(~K, ~V, ~cmp, c3), o3), Equal.sym(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}), f1), g2)
216      +ec3 = L.pair_fst(S.Cursor<K, V>, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs))}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, S.find(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)), CU.cmod(~K, ~V, ~cmp, c3), o3, heq)
217      +hdel = Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)), S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs})), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => S.del(~K, ~V, ~cmp, k, z), 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}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), DO.del_mid(~K, ~V, ~cmp, ~o, k, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, OR.ord_mid_l(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, 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}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord)), O.refl(~K, ~cmp, ~o, k)))
218      +hsp3 = Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, c3), S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs))}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs))}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, CU.cmod(~K, ~V, ~cmp, c3), ec3), VS.cong(List<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, S.del(~K, ~V, ~cmp, k, 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), bs), hdel))
219      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, V>, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), (MI.rc(~K, ~V, ~cmp, c3), o3), g1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, _)))
220      +eo1 = Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), S.outside(~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.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~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>>, z => S.outside(~K, ~V, ~cmp, lo2, hi2, z), 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})), out_app(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}))
221      +eo2 = Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Nil{}), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), z), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}}), Nil{}, VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), Nil{}, Con{M.Entry{k, v}, Nil{}}, hb)), LL.append_nil(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))))
222      +eo = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, z, bs)}, lo2, hi2, True{}}, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~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.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), eo1, eo2)))
223      L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c3)))), S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, eo, kont(c3, g3, hsp3))
224
225def cbt3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, q: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
226  match q:
227    case Tuple{+c3, Tuple{+o3, Tuple{+g1, r}}}:
228      cbt4(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ec, c3, o3, g1, r, kont)
229
230def cbt2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
231  match r:
232    case Tuple{h2, h3}:
233      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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}}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}, hsp), VZ.sp_b(~K, ~V, ~cmp, ~o, l, 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.reverse(M.Entry<K, V>, t), k, v, bs, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord, cc, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), hb))
234      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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}}), hsv), h2)
235      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
236      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
237      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
238      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
239      cbt3(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ec, rok(c2, h3), kont)
240
241def cbt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
242  match p:
243    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
244      cbt2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ov, h1, r, kont)
245
246def cbc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
247  match b:
248    case True{}:
249      cbt(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, p, kont)
250    case False{}:
251      cbs(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, p)
252
253
254# the clear backward: every entry of the run before the cursor removed
255def clb(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +rr: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr))), cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, rr) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, rr)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, rr), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
256  match rr:
257    case Nil{}:
258      cbn(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, c, cc, hsp, nok(c, hc))
259    case Con{M.Entry{+k, +v}, +t}:
260      cbc(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, 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}))), cc, lo2, hi2, False{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}, hsp, VS.cong(Maybe<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, z), cc, lo2, hi2, False{}}, 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}))), hord, hbu, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, nok(c, hc), kc3 => kh3 => ks3 => clb(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, t, kc3, None{}, kh3, ks3, DO.ord_drop(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, 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}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord)), L.and_right(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu)))