proofs/containers/balanced_search_tree/vsp.bend

bend-collections-laws-containers@1.0.0.0 · 700 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/order.bend as O
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
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/ord.bend as OR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/navl.bend as NV
11
12# A view's entries in sorted entries, for a lawful comparator: the bounds are
13# monotone, so the entries within them are a run; its first (last) is the
14# first entry above the lower bound (the last below the upper), when in
15# range, and a strict search from a key inside the view is the search in the
16# whole map, checked against the range. (source: tools/generators/tm_hand/vsp.src)
17
18
19# ---- generic ----
20
21def pk_t(-T: Type, +b: Bool, -x: T, -y: T, +h: {b == True{} : Bool}) -> {S.pick(T, b, x, y) == x : T}:
22  %Equal.sym(Bool, b, True{}, h) : {S.pick(T, _, x, y) == x : T}
23  {==}
24
25def pk_f(-T: Type, +b: Bool, -x: T, -y: T, +h: {b == False{} : Bool}) -> {S.pick(T, b, x, y) == y : T}:
26  %Equal.sym(Bool, b, False{}, h) : {S.pick(T, _, x, y) == y : T}
27  {==}
28
29def cong(-A: Type, -B: Type, -f: A -> B, -a: A, -b: A, e: {a == b : A}) -> {f(a) == f(b) : B}:
30  L.subst(A, z => {f(a) == f(z) : B}, a, b, e, {==})
31
32def and_f(+a: Bool) -> {Bool.and(a, False{}) == False{} : Bool}:
33  match a:
34    case True{}:
35      {==}
36    case False{}:
37      {==}
38
39def lt_tr(+c: Cmp, +h: {c == LT{} : Cmp}) -> {Cmp.is_lt(c) == True{} : Bool}:
40  L.subst(Cmp, z => {Cmp.is_lt(z) == True{} : Bool}, LT{}, c, Equal.sym(Cmp, c, LT{}, h), {==})
41
42def lt_okf(+c: Cmp, +h: {Cmp.is_lt(c) == True{} : Bool}) -> {S.ordering_ok(c, False{}) == True{} : Bool}:
43  L.subst(Cmp, z => {S.ordering_ok(z, False{}) == True{} : Bool}, LT{}, c, Equal.sym(Cmp, c, LT{}, O.lt_is(c, h)), {==})
44
45# ---- comparisons ----
46
47def okw_l(+c: Cmp, +i: Bool, +j: Bool, +h: {S.ordering_ok(c, Bool.and(i, j)) == True{} : Bool}) -> {S.ordering_ok(c, i) == True{} : Bool}:
48  match c i:
49    case LT{} True{}:
50      {==}
51    case LT{} False{}:
52      {==}
53    case EQ{} True{}:
54      {==}
55    case EQ{} False{}:
56      Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
57    case GT{} True{}:
58      Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
59    case GT{} False{}:
60      Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
61
62def okw_r(+c: Cmp, +i: Bool, +j: Bool, +h: {S.ordering_ok(c, Bool.and(i, j)) == True{} : Bool}) -> {S.ordering_ok(c, j) == True{} : Bool}:
63  match c i:
64    case LT{} True{}:
65      {==}
66    case LT{} False{}:
67      {==}
68    case EQ{} True{}:
69      h
70    case EQ{} False{}:
71      Empty.absurd({j == True{} : Bool}, L.false_true(h))
72    case GT{} True{}:
73      Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
74    case GT{} False{}:
75      Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
76
77def okflip(+c: Cmp, +i: Bool, +h: {S.ordering_ok(c, i) == False{} : Bool}) -> {S.ordering_ok(O.flipc(c), Bool.not(i)) == True{} : Bool}:
78  match c i:
79    case LT{} True{}:
80      Empty.absurd({False{} == True{} : Bool}, L.true_false(h))
81    case LT{} False{}:
82      Empty.absurd({False{} == True{} : Bool}, L.true_false(h))
83    case EQ{} True{}:
84      Empty.absurd({False{} == True{} : Bool}, L.true_false(h))
85    case EQ{} False{}:
86      {==}
87    case GT{} True{}:
88      {==}
89    case GT{} False{}:
90      {==}
91
92def okf0(+c: Cmp, +h: {S.ordering_ok(c, False{}) == True{} : Bool}) -> {c == LT{} : Cmp}:
93  match c:
94    case LT{}:
95      {==}
96    case EQ{}:
97      Empty.absurd({EQ{} == LT{} : Cmp}, L.false_true(h))
98    case GT{}:
99      Empty.absurd({GT{} == LT{} : Cmp}, L.false_true(h))
100
101def ok_tl(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +c: K, +i1: Bool, +i2: Bool, +hx: {cmp(a, b) == LT{} : Cmp}, +y: Cmp, +hy: {cmp(b, c) == y : Cmp}, +h2: {S.ordering_ok(y, i2) == True{} : Bool}) -> {S.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}:
102  match y:
103    case LT{}:
104      +lab = lt_tr(cmp(a, b), hx)
105      +lbc = lt_tr(cmp(b, c), hy)
106      %Equal.sym(Cmp, cmp(a, c), LT{}, O.lt_is(cmp(a, c), OR.slt_trans(~K, ~cmp, ~o, a, b, c, lab, lbc))) : {S.ordering_ok(_, Bool.and(i1, i2)) == True{} : Bool}
107      {==}
108    case EQ{}:
109      +ebc = O.antisym(~K, ~cmp, o, b, c, hy)
110      L.subst(K, z => {S.ordering_ok(cmp(a, z), Bool.and(i1, i2)) == True{} : Bool}, b, c, ebc, L.subst(Cmp, z => {S.ordering_ok(z, Bool.and(i1, i2)) == True{} : Bool}, LT{}, cmp(a, b), Equal.sym(Cmp, cmp(a, b), LT{}, hx), {==}))
111    case GT{}:
112      Empty.absurd({S.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}, L.false_true(h2))
113
114def ok_te(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +c: K, +i1: Bool, +i2: Bool, +hx: {cmp(a, b) == EQ{} : Cmp}, +h1: {i1 == True{} : Bool}, +h2: {S.ordering_ok(cmp(b, c), i2) == True{} : Bool}) -> {S.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}:
115  +eab = O.antisym(~K, ~cmp, o, a, b, hx)
116  %Equal.sym(Bool, i1, True{}, h1) : {S.ordering_ok(cmp(a, c), Bool.and(_, i2)) == True{} : Bool}
117  L.subst(K, z => {S.ordering_ok(cmp(z, c), i2) == True{} : Bool}, b, a, Equal.sym(K, a, b, eab), h2)
118
119def ok_tc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +c: K, +i1: Bool, +i2: Bool, +x: Cmp, +hx: {cmp(a, b) == x : Cmp}, +h1: {S.ordering_ok(x, i1) == True{} : Bool}, +h2: {S.ordering_ok(cmp(b, c), i2) == True{} : Bool}) -> {S.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}:
120  match x:
121    case LT{}:
122      ok_tl(~K, ~cmp, ~o, a, b, c, i1, i2, hx, cmp(b, c), {==}, h2)
123    case EQ{}:
124      ok_te(~K, ~cmp, ~o, a, b, c, i1, i2, hx, h1, h2)
125    case GT{}:
126      Empty.absurd({S.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}, L.false_true(h1))
127
128# a <= b <= c (each strict or not): a <= c, strict when either is
129def ok_trans(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +c: K, +i1: Bool, +i2: Bool, +h1: {S.ordering_ok(cmp(a, b), i1) == True{} : Bool}, +h2: {S.ordering_ok(cmp(b, c), i2) == True{} : Bool}) -> {S.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}:
130  ok_tc(~K, ~cmp, ~o, a, b, c, i1, i2, cmp(a, b), {==}, h1, h2)
131
132def fl_ok(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +x: K, +k: K, +i: Bool, +h: {S.ordering_ok(cmp(x, k), i) == False{} : Bool}) -> {S.ordering_ok(cmp(k, x), Bool.not(i)) == True{} : Bool}:
133  L.subst(Cmp, z => {S.ordering_ok(z, Bool.not(i)) == True{} : Bool}, O.flipc(cmp(x, k)), cmp(k, x), Equal.sym(Cmp, cmp(k, x), O.flipc(cmp(x, k)), O.flip(~K, ~cmp, o, x, k)), okflip(cmp(x, k), i, h))
134
135def lt_both(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +h1: {cmp(a, b) == LT{} : Cmp}, +h2: {cmp(b, a) == LT{} : Cmp}) -> Empty:
136  +e1 = L.subst(Cmp, z => {cmp(b, a) == O.flipc(z) : Cmp}, cmp(a, b), LT{}, h1, O.flip(~K, ~cmp, o, a, b))
137  L.cmp_lt_gt(Equal.trans(Cmp, LT{}, cmp(b, a), GT{}, Equal.sym(Cmp, cmp(b, a), LT{}, h2), e1))
138
139# ---- the bounds are monotone ----
140
141def al_mono(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +a: K, +e: K, +i: Bool, +ha: {S.above_lower(~K, ~cmp, a, lw) == True{} : Bool}, +hp: {S.ordering_ok(cmp(a, e), i) == True{} : Bool}) -> {S.above_lower(~K, ~cmp, e, lw) == True{} : Bool}:
142  match lw:
143    case M.Unbounded{}:
144      {==}
145    case M.Inclusive{+x}:
146      okw_l(cmp(x, e), True{}, i, ok_trans(~K, ~cmp, ~o, x, a, e, True{}, i, ha, hp))
147    case M.Exclusive{+x}:
148      okw_l(cmp(x, e), False{}, i, ok_trans(~K, ~cmp, ~o, x, a, e, False{}, i, ha, hp))
149
150def bu_mono(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound<K>, +a: K, +e: K, +i: Bool, +ha: {S.below_upper(~K, ~cmp, a, up) == True{} : Bool}, +hq: {S.ordering_ok(cmp(e, a), i) == True{} : Bool}) -> {S.below_upper(~K, ~cmp, e, up) == True{} : Bool}:
151  match up:
152    case M.Unbounded{}:
153      {==}
154    case M.Inclusive{+y}:
155      okw_r(cmp(e, y), i, True{}, ok_trans(~K, ~cmp, ~o, e, a, y, i, True{}, hq, ha))
156    case M.Exclusive{+y}:
157      okw_r(cmp(e, y), i, False{}, ok_trans(~K, ~cmp, ~o, e, a, y, i, False{}, hq, ha))
158
159# below the lower bound, above it: strictly less
160def al_lt(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +k: K, +e: K, +hk: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}, +he: {S.above_lower(~K, ~cmp, e, lw) == True{} : Bool}) -> {cmp(k, e) == LT{} : Cmp}:
161  match lw:
162    case M.Unbounded{}:
163      Empty.absurd({cmp(k, e) == LT{} : Cmp}, L.true_false(hk))
164    case M.Inclusive{+x}:
165      okf0(cmp(k, e), ok_trans(~K, ~cmp, ~o, k, x, e, False{}, True{}, fl_ok(~K, ~cmp, ~o, x, k, True{}, hk), he))
166    case M.Exclusive{+x}:
167      okf0(cmp(k, e), ok_trans(~K, ~cmp, ~o, k, x, e, True{}, False{}, fl_ok(~K, ~cmp, ~o, x, k, False{}, hk), he))
168
169def bu_lt(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound<K>, +k: K, +e: K, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}, +he: {S.below_upper(~K, ~cmp, e, up) == True{} : Bool}) -> {cmp(e, k) == LT{} : Cmp}:
170  match up:
171    case M.Unbounded{}:
172      Empty.absurd({cmp(e, k) == LT{} : Cmp}, L.true_false(hk))
173    case M.Inclusive{+y}:
174      okf0(cmp(e, k), ok_trans(~K, ~cmp, ~o, e, y, k, True{}, False{}, he, fl_ok(~K, ~cmp, ~o, k, y, True{}, hk)))
175    case M.Exclusive{+y}:
176      okf0(cmp(e, k), ok_trans(~K, ~cmp, ~o, e, y, k, False{}, True{}, he, fl_ok(~K, ~cmp, ~o, k, y, False{}, hk)))
177
178def bu_fc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound<K>, +k: K, +f: K, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}, +hlt: {Cmp.is_lt(cmp(k, f)) == True{} : Bool}, +b: Bool, +hb: {S.below_upper(~K, ~cmp, f, up) == b : Bool}) -> {S.below_upper(~K, ~cmp, f, up) == False{} : Bool}:
179  match b:
180    case True{}:
181      Empty.absurd({S.below_upper(~K, ~cmp, f, up) == False{} : Bool}, lt_both(~K, ~cmp, ~o, f, k, bu_lt(~K, ~cmp, ~o, up, k, f, hk, hb), O.lt_is(cmp(k, f), hlt)))
182    case False{}:
183      hb
184
185# past a key above the upper bound: above it
186def bu_false(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound<K>, +k: K, +f: K, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}, +hlt: {Cmp.is_lt(cmp(k, f)) == True{} : Bool}) -> {S.below_upper(~K, ~cmp, f, up) == False{} : Bool}:
187  bu_fc(~K, ~cmp, ~o, up, k, f, hk, hlt, S.below_upper(~K, ~cmp, f, up), {==})
188
189def al_fc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +k: K, +f: K, +hk: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}, +hlt: {Cmp.is_lt(cmp(f, k)) == True{} : Bool}, +b: Bool, +hb: {S.above_lower(~K, ~cmp, f, lw) == b : Bool}) -> {S.above_lower(~K, ~cmp, f, lw) == False{} : Bool}:
190  match b:
191    case True{}:
192      Empty.absurd({S.above_lower(~K, ~cmp, f, lw) == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, S.above_lower(~K, ~cmp, k, lw), False{}, Equal.sym(Bool, S.above_lower(~K, ~cmp, k, lw), True{}, al_mono(~K, ~cmp, ~o, lw, f, k, False{}, hb, lt_okf(cmp(f, k), hlt))), hk)))
193    case False{}:
194      hb
195
196# before a key below the lower bound: below it
197def al_false(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +k: K, +f: K, +hk: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}, +hlt: {Cmp.is_lt(cmp(f, k)) == True{} : Bool}) -> {S.above_lower(~K, ~cmp, f, lw) == False{} : Bool}:
198  al_fc(~K, ~cmp, ~o, lw, k, f, hk, hlt, S.above_lower(~K, ~cmp, f, lw), {==})
199
200def ir_t(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +ha: {S.above_lower(~K, ~cmp, k, lw) == True{} : Bool}, +hb: {S.below_upper(~K, ~cmp, k, up) == True{} : Bool}) -> {S.in_range(~K, ~cmp, k, lw, up) == True{} : Bool}:
201  L.and_intro(S.above_lower(~K, ~cmp, k, lw), S.below_upper(~K, ~cmp, k, up), ha, hb)
202
203def ir_fb(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +hb: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}) -> {S.in_range(~K, ~cmp, k, lw, up) == False{} : Bool}:
204  %Equal.sym(Bool, S.below_upper(~K, ~cmp, k, up), False{}, hb) : {Bool.and(S.above_lower(~K, ~cmp, k, lw), _) == False{} : Bool}
205  and_f(S.above_lower(~K, ~cmp, k, lw))
206
207def ir_fa(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +ha: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}) -> {S.in_range(~K, ~cmp, k, lw, up) == False{} : Bool}:
208  %Equal.sym(Bool, S.above_lower(~K, ~cmp, k, lw), False{}, ha) : {Bool.and(_, S.below_upper(~K, ~cmp, k, up)) == False{} : Bool}
209  {==}
210
211# ---- the entries within ----
212
213def w_in(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == True{} : Bool}) -> {S.within(~K, ~V, ~cmp, lw, up, Con{e, t}) == Con{e, S.within(~K, ~V, ~cmp, lw, up, t)} : List<&2, M.Entry<K, V>>}:
214  pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, S.within(~K, ~V, ~cmp, lw, up, t), h)
215
216def w_out(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == False{} : Bool}) -> {S.within(~K, ~V, ~cmp, lw, up, Con{e, t}) == S.within(~K, ~V, ~cmp, lw, up, t) : List<&2, M.Entry<K, V>>}:
217  pk_f(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, S.within(~K, ~V, ~cmp, lw, up, t), h)
218
219def chk(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, m: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>:
220  match m:
221    case None{}:
222      None{}
223    case Some{+e}:
224      S.pick(Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), Some{e}, None{})
225
226def chk_in(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +h: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == True{} : Bool}) -> {chk(~K, ~V, ~cmp, lw, up, Some{e}) == Some{e} : Maybe<&2, M.Entry<K, V>>}:
227  pk_t(Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), Some{e}, None{}, h)
228
229def chk_out(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +h: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == False{} : Bool}) -> {chk(~K, ~V, ~cmp, lw, up, Some{e}) == None{} : Maybe<&2, M.Entry<K, V>>}:
230  pk_f(Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), Some{e}, None{}, h)
231
232# above a key past the upper bound, nothing is within
233def wnil(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +t: List<&2, M.Entry<K, V>>, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}, +hg: {OR.gtall(~K, ~V, ~cmp, k, t) == True{} : Bool}) -> {S.within(~K, ~V, ~cmp, lw, up, t) == Nil{} : List<&2, M.Entry<K, V>>}:
234  match t:
235    case Nil{}:
236      {==}
237    case Con{+e, +u}:
238      +h1 = L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, u), hg)
239      +h2 = L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, u), hg)
240      Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, Con{e, u}), S.within(~K, ~V, ~cmp, lw, up, u), Nil{}, w_out(~K, ~V, ~cmp, lw, up, e, u, ir_fb(~K, ~cmp, lw, up, S.key(K, V, e), bu_false(~K, ~cmp, ~o, up, k, S.key(K, V, e), hk, h1))), wnil(~K, ~V, ~cmp, ~o, lw, up, k, u, hk, h2))
241
242def gt_wc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +e: M.Entry<K, V>, +u: List<&2, M.Entry<K, V>>, +h1: {Cmp.is_lt(cmp(k, S.key(K, V, e))) == True{} : Bool}, +hu: {OR.gtall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, u)) == True{} : Bool}, +b: Bool) -> {OR.gtall(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry<K, V>>, b, Con{e, S.within(~K, ~V, ~cmp, lw, up, u)}, S.within(~K, ~V, ~cmp, lw, up, u))) == True{} : Bool}:
243  match b:
244    case True{}:
245      L.and_intro(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, u)), h1, hu)
246    case False{}:
247      hu
248
249def gt_w(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +t: List<&2, M.Entry<K, V>>, +h: {OR.gtall(~K, ~V, ~cmp, k, t) == True{} : Bool}) -> {OR.gtall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, t)) == True{} : Bool}:
250  match t:
251    case Nil{}:
252      {==}
253    case Con{+e, +u}:
254      gt_wc(~K, ~V, ~cmp, lw, up, k, e, u, L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, u), h), gt_w(~K, ~V, ~cmp, lw, up, k, u, L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, u), h)), S.in_range(~K, ~cmp, S.key(K, V, e), lw, up))
255
256def wgt_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +e: M.Entry<K, V>, +u: List<&2, M.Entry<K, V>>, +hk: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}, +hu: {OR.gtall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, u)) == True{} : Bool}, +b: Bool, +hb: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == b : Bool}) -> {OR.gtall(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry<K, V>>, b, Con{e, S.within(~K, ~V, ~cmp, lw, up, u)}, S.within(~K, ~V, ~cmp, lw, up, u))) == True{} : Bool}:
257  match b:
258    case True{}:
259      L.and_intro(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, u)), lt_tr(cmp(k, S.key(K, V, e)), al_lt(~K, ~cmp, ~o, lw, k, S.key(K, V, e), hk, L.and_left(S.above_lower(~K, ~cmp, S.key(K, V, e), lw), S.below_upper(~K, ~cmp, S.key(K, V, e), up), hb))), hu)
260    case False{}:
261      hu
262
263# a key below the lower bound is below everything within
264def wgt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +es: List<&2, M.Entry<K, V>>, +hk: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}) -> {OR.gtall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, es)) == True{} : Bool}:
265  match es:
266    case Nil{}:
267      {==}
268    case Con{+e, +u}:
269      wgt_c(~K, ~V, ~cmp, ~o, lw, up, k, e, u, hk, wgt(~K, ~V, ~cmp, ~o, lw, up, k, u, hk), S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), {==})
270
271def wlt_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +e: M.Entry<K, V>, +u: List<&2, M.Entry<K, V>>, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}, +hu: {OR.ltall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, u)) == True{} : Bool}, +b: Bool, +hb: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == b : Bool}) -> {OR.ltall(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry<K, V>>, b, Con{e, S.within(~K, ~V, ~cmp, lw, up, u)}, S.within(~K, ~V, ~cmp, lw, up, u))) == True{} : Bool}:
272  match b:
273    case True{}:
274      L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, u)), lt_tr(cmp(S.key(K, V, e), k), bu_lt(~K, ~cmp, ~o, up, k, S.key(K, V, e), hk, L.and_right(S.above_lower(~K, ~cmp, S.key(K, V, e), lw), S.below_upper(~K, ~cmp, S.key(K, V, e), up), hb))), hu)
275    case False{}:
276      hu
277
278# a key above the upper bound is above everything within
279def wlt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +es: List<&2, M.Entry<K, V>>, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}) -> {OR.ltall(~K, ~V, ~cmp, k, S.within(~K, ~V, ~cmp, lw, up, es)) == True{} : Bool}:
280  match es:
281    case Nil{}:
282      {==}
283    case Con{+e, +u}:
284      wlt_c(~K, ~V, ~cmp, ~o, lw, up, k, e, u, hk, wlt(~K, ~V, ~cmp, ~o, lw, up, k, u, hk), S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), {==})
285
286# ---- the first within: the first above the lower bound, checked ----
287
288def fal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>:
289  match es:
290    case Nil{}:
291      None{}
292    case Con{+e, +t}:
293      S.pick(Maybe<&2, M.Entry<K, V>>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t))
294
295
296def e1_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, +ih: {S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)) == chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)) : Maybe<&2, M.Entry<K, V>>}, +a: Bool, +ha: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == a : Bool}, +b: Bool, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == b : Bool}) -> {S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})) == chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})) : Maybe<&2, M.Entry<K, V>>}:
297  match a b:
298    case True{} True{}:
299      +hir = ir_t(~K, ~cmp, lw, up, S.key(K, V, e), ha, hb)
300      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.head(M.Entry<K, V>, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, w_in(~K, ~V, ~cmp, lw, up, e, t, hir))
301      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), fal(~K, ~V, ~cmp, lw, Con{e, t}), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t), ha))
302      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), Some{e}, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), l1, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), Some{e}, Equal.trans(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, Some{e}), Some{e}, r1, chk_in(~K, ~V, ~cmp, lw, up, e, hir))))
303    case True{} False{}:
304      +hir = ir_fb(~K, ~cmp, lw, up, S.key(K, V, e), hb)
305      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.head(M.Entry<K, V>, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, hir))
306      +l2 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.head(M.Entry<K, V>, z), S.within(~K, ~V, ~cmp, lw, up, t), Nil{}, wnil(~K, ~V, ~cmp, ~o, lw, up, S.key(K, V, e), t, hb, OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, h)))
307      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), fal(~K, ~V, ~cmp, lw, Con{e, t}), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t), ha))
308      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), None{}, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), None{}, l1, l2), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), None{}, Equal.trans(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, Some{e}), None{}, r1, chk_out(~K, ~V, ~cmp, lw, up, e, hir))))
309    case False{} True{}:
310      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.head(M.Entry<K, V>, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, ir_fa(~K, ~cmp, lw, up, S.key(K, V, e), ha)))
311      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), fal(~K, ~V, ~cmp, lw, Con{e, t}), fal(~K, ~V, ~cmp, lw, t), pk_f(Maybe<&2, M.Entry<K, V>>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t), ha))
312      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)), l1, ih), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)), r1))
313    case False{} False{}:
314      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.head(M.Entry<K, V>, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, ir_fa(~K, ~cmp, lw, up, S.key(K, V, e), ha)))
315      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), fal(~K, ~V, ~cmp, lw, Con{e, t}), fal(~K, ~V, ~cmp, lw, t), pk_f(Maybe<&2, M.Entry<K, V>>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t), ha))
316      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)), l1, ih), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)), r1))
317
318def first_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> {S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)) == chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, es)) : Maybe<&2, M.Entry<K, V>>}:
319  match es:
320    case Nil{}:
321      {==}
322    case Con{+e, +t}:
323      e1_c(~K, ~V, ~cmp, ~o, lw, up, e, t, h, first_within(~K, ~V, ~cmp, ~o, lw, up, t, OR.ord_tail(~K, ~V, ~cmp, e, t, h)), S.above_lower(~K, ~cmp, S.key(K, V, e), lw), {==}, S.below_upper(~K, ~cmp, S.key(K, V, e), up), {==})
324
325# ---- the last within: the last below the upper bound, checked ----
326
327def lbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound<K>, es: List<&2, M.Entry<K, V>>, +best: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>:
328  match es:
329    case Nil{}:
330      best
331    case Con{+e, t}:
332      lbu(~K, ~V, ~cmp, up, t, S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, best))
333
334# a candidate before every entry
335def bgood(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Maybe<&2, M.Entry<K, V>>, +es: List<&2, M.Entry<K, V>>) -> Bool:
336  match m:
337    case None{}:
338      True{}
339    case Some{+b}:
340      OR.gtall(~K, ~V, ~cmp, S.key(K, V, b), es)
341
342def bg_tail(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m: Maybe<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {bgood(~K, ~V, ~cmp, m, Con{e, t}) == True{} : Bool}) -> {bgood(~K, ~V, ~cmp, m, t) == True{} : Bool}:
343  match m:
344    case None{}:
345      {==}
346    case Some{+b}:
347      L.and_right(Cmp.is_lt(cmp(S.key(K, V, b), S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, S.key(K, V, b), t), h)
348
349# a candidate before an entry below the lower bound is out of range
350def chk_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +m: Maybe<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +hbg: {bgood(~K, ~V, ~cmp, m, Con{e, t}) == True{} : Bool}, +hal: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == False{} : Bool}) -> {chk(~K, ~V, ~cmp, lw, up, m) == None{} : Maybe<&2, M.Entry<K, V>>}:
351  match m:
352    case None{}:
353      {==}
354    case Some{+b}:
355      chk_out(~K, ~V, ~cmp, lw, up, b, ir_fa(~K, ~cmp, lw, up, S.key(K, V, b), al_false(~K, ~cmp, ~o, lw, S.key(K, V, e), S.key(K, V, b), hal, L.and_left(Cmp.is_lt(cmp(S.key(K, V, b), S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, S.key(K, V, b), t), hbg))))
356
357# past a key above the upper bound, no entry is a candidate
358def lbu_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound<K>, +k: K, +t: List<&2, M.Entry<K, V>>, +best: Maybe<&2, M.Entry<K, V>>, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}, +hg: {OR.gtall(~K, ~V, ~cmp, k, t) == True{} : Bool}) -> {lbu(~K, ~V, ~cmp, up, t, best) == best : Maybe<&2, M.Entry<K, V>>}:
359  match t:
360    case Nil{}:
361      {==}
362    case Con{+f, +u}:
363      +h1 = L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, f))), OR.gtall(~K, ~V, ~cmp, k, u), hg)
364      +h2 = L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, f))), OR.gtall(~K, ~V, ~cmp, k, u), hg)
365      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, f), up), Some{f}, best), best, pk_f(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, f), up), Some{f}, best, bu_false(~K, ~cmp, ~o, up, k, S.key(K, V, f), hk, h1))) : {lbu(~K, ~V, ~cmp, up, u, _) == best : Maybe<&2, M.Entry<K, V>>}
366      lbu_none(~K, ~V, ~cmp, ~o, up, k, u, best, hk, h2)
367
368
369def e2_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, +hbg: {bgood(~K, ~V, ~cmp, bst, Con{e, t}) == True{} : Bool}, +ih: {OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, Some{e})) == chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, Some{e})) : Maybe<&2, M.Entry<K, V>>}, +a: Bool, +ha: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == a : Bool}, +b: Bool, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == b : Bool}) -> {OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, bst)) == chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)) : Maybe<&2, M.Entry<K, V>>}:
370  match a b:
371    case True{} True{}:
372      +hir = ir_t(~K, ~cmp, lw, up, S.key(K, V, e), ha, hb)
373      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, z), chk(~K, ~V, ~cmp, lw, up, bst)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, w_in(~K, ~V, ~cmp, lw, up, e, t, hir))
374      +l2 = Equal.sym(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}), chk(~K, ~V, ~cmp, lw, up, bst)), NV.lw_all_c(K, V, e, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, bst)))
375      +l3 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), z), Some{e}, chk(~K, ~V, ~cmp, lw, up, Some{e}), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, Some{e}), Some{e}, chk_in(~K, ~V, ~cmp, lw, up, e, hir)))
376      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb))
377      Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l1, Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), Some{e}), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l2, Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l3, Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, Some{e})), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), ih, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, Some{e})), r1)))))
378    case True{} False{}:
379      +hir = ir_fb(~K, ~cmp, lw, up, S.key(K, V, e), hb)
380      +hgt = OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, h)
381      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, z), chk(~K, ~V, ~cmp, lw, up, bst)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Nil{}, Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), Nil{}, w_out(~K, ~V, ~cmp, lw, up, e, t, hir), wnil(~K, ~V, ~cmp, ~o, lw, up, S.key(K, V, e), t, hb, hgt)))
382      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb))
383      +r2 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), lbu(~K, ~V, ~cmp, up, t, bst), bst, lbu_none(~K, ~V, ~cmp, ~o, up, S.key(K, V, e), t, bst, hb, hgt))
384      Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, bst), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l1, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, bst), Equal.trans(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, bst)), chk(~K, ~V, ~cmp, lw, up, bst), r1, r2)))
385    case False{} True{}:
386      +hir = ir_fa(~K, ~cmp, lw, up, S.key(K, V, e), ha)
387      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, z), chk(~K, ~V, ~cmp, lw, up, bst)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, hir))
388      +l2 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), z), chk(~K, ~V, ~cmp, lw, up, bst), None{}, chk_none(~K, ~V, ~cmp, ~o, lw, up, bst, e, t, hbg, ha))
389      +l3 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), z), None{}, chk(~K, ~V, ~cmp, lw, up, Some{e}), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, Some{e}), None{}, chk_out(~K, ~V, ~cmp, lw, up, e, hir)))
390      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb))
391      Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l1, Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), None{}), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l2, Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l3, Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, Some{e})), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), ih, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, Some{e})), r1)))))
392    case False{} False{}:
393      +hir = ir_fb(~K, ~cmp, lw, up, S.key(K, V, e), hb)
394      +hgt = OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, h)
395      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, z), chk(~K, ~V, ~cmp, lw, up, bst)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Nil{}, Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), Nil{}, w_out(~K, ~V, ~cmp, lw, up, e, t, hir), wnil(~K, ~V, ~cmp, ~o, lw, up, S.key(K, V, e), t, hb, hgt)))
396      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb))
397      +r2 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), lbu(~K, ~V, ~cmp, up, t, bst), bst, lbu_none(~K, ~V, ~cmp, ~o, up, S.key(K, V, e), t, bst, hb, hgt))
398      Equal.trans(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, bst), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), l1, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, bst), Equal.trans(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, bst)), chk(~K, ~V, ~cmp, lw, up, bst), r1, r2)))
399
400def e2g(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +hbg: {bgood(~K, ~V, ~cmp, bst, es) == True{} : Bool}) -> {OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)), chk(~K, ~V, ~cmp, lw, up, bst)) == chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, es, bst)) : Maybe<&2, M.Entry<K, V>>}:
401  match es:
402    case Nil{}:
403      {==}
404    case Con{+e, +t}:
405      e2_c(~K, ~V, ~cmp, ~o, lw, up, e, t, bst, h, hbg, e2g(~K, ~V, ~cmp, ~o, lw, up, t, Some{e}, OR.ord_tail(~K, ~V, ~cmp, e, t, h), OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, h)), S.above_lower(~K, ~cmp, S.key(K, V, e), lw), {==}, S.below_upper(~K, ~cmp, S.key(K, V, e), up), {==})
406
407def last_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> {S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)) == chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, es, None{})) : Maybe<&2, M.Entry<K, V>>}:
408  Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)), None{}), chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, es, None{})), Equal.sym(Maybe<&2, M.Entry<K, V>>, OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)), None{}), S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)), OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)))), e2g(~K, ~V, ~cmp, ~o, lw, up, es, None{}, h, {==}))
409
410# ---- a search from a key inside the view: the whole map's, checked ----
411
412
413# a failing first entry skipped, within or not
414def fw_skip(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +hp: {S.ordering_ok(cmp(k, S.key(K, V, e)), incl) == False{} : Bool}, +c: Bool, +hc: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == c : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})) == S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)) : Maybe<&2, M.Entry<K, V>>}:
415  match c:
416    case True{}:
417      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.first_where(~K, ~V, ~cmp, k, incl, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}), S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)), cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.first_where(~K, ~V, ~cmp, k, incl, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, w_in(~K, ~V, ~cmp, lw, up, e, t, hc)), pk_f(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)), hp))
418    case False{}:
419      cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.first_where(~K, ~V, ~cmp, k, incl, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, hc))
420
421def n1_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, +hk: {S.above_lower(~K, ~cmp, k, lw) == True{} : Bool}, +ih: {S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)) == chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, t)) : Maybe<&2, M.Entry<K, V>>}, +pv: Bool, +hp: {S.ordering_ok(cmp(k, S.key(K, V, e)), incl) == pv : Bool}, +b: Bool, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == b : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})) == chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})) : Maybe<&2, M.Entry<K, V>>}:
422  match pv b:
423    case True{} True{}:
424      +hir = ir_t(~K, ~cmp, lw, up, S.key(K, V, e), al_mono(~K, ~cmp, ~o, lw, k, S.key(K, V, e), incl, hk, hp), hb)
425      +l1 = Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.first_where(~K, ~V, ~cmp, k, incl, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}), Some{e}, cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.first_where(~K, ~V, ~cmp, k, incl, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, w_in(~K, ~V, ~cmp, lw, up, e, t, hir)), pk_t(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)), hp))
426      +r1 = Equal.trans(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, Some{e}), Some{e}, cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t}), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t), hp)), chk_in(~K, ~V, ~cmp, lw, up, e, hir))
427      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), Some{e}, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), l1, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), Some{e}, r1))
428    case True{} False{}:
429      +hir = ir_fb(~K, ~cmp, lw, up, S.key(K, V, e), hb)
430      +l1 = Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)), None{}, cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.first_where(~K, ~V, ~cmp, k, incl, z), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, hir)), cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.first_where(~K, ~V, ~cmp, k, incl, z), S.within(~K, ~V, ~cmp, lw, up, t), Nil{}, wnil(~K, ~V, ~cmp, ~o, lw, up, S.key(K, V, e), t, hb, OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, h))))
431      +r1 = Equal.trans(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, Some{e}), None{}, cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t}), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t), hp)), chk_out(~K, ~V, ~cmp, lw, up, e, hir))
432      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), None{}, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), l1, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), None{}, r1))
433    case False{} True{}:
434      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t}), S.first_where(~K, ~V, ~cmp, k, incl, t), pk_f(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t), hp))
435      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, t)), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, t)), fw_skip(~K, ~V, ~cmp, ~o, lw, up, k, incl, e, t, hp, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), {==}), ih), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, t)), r1))
436    case False{} False{}:
437      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, z), S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t}), S.first_where(~K, ~V, ~cmp, k, incl, t), pk_f(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t), hp))
438      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, t)), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, t)), fw_skip(~K, ~V, ~cmp, ~o, lw, up, k, incl, e, t, hp, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), {==}), ih), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, t)), r1))
439
440# from a key above the lower bound, the first at or past it within is the
441# first in the map, when in range
442def fw_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +hk: {S.above_lower(~K, ~cmp, k, lw) == True{} : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es)) == chk(~K, ~V, ~cmp, lw, up, S.first_where(~K, ~V, ~cmp, k, incl, es)) : Maybe<&2, M.Entry<K, V>>}:
443  match es:
444    case Nil{}:
445      {==}
446    case Con{+e, +t}:
447      n1_c(~K, ~V, ~cmp, ~o, lw, up, k, incl, e, t, h, hk, fw_within(~K, ~V, ~cmp, ~o, lw, up, k, incl, t, OR.ord_tail(~K, ~V, ~cmp, e, t, h), hk), S.ordering_ok(cmp(k, S.key(K, V, e)), incl), {==}, S.below_upper(~K, ~cmp, S.key(K, V, e), up), {==})
448
449# from a key below the lower bound, the first within
450def fw_below(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +hk: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es)) == S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)) : Maybe<&2, M.Entry<K, V>>}:
451  NV.fw_head(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es), wgt(~K, ~V, ~cmp, ~o, lw, up, k, es, hk))
452
453def lw_skip(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +m: Maybe<&2, M.Entry<K, V>>, +hq: {S.ordering_ok(cmp(S.key(K, V, e), k), incl) == False{} : Bool}, +c: Bool, +hc: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == c : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), m) == S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), m) : Maybe<&2, M.Entry<K, V>>}:
454  match c:
455    case True{}:
456      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), m), S.last_where(~K, ~V, ~cmp, k, incl, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, m), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), m), cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.last_where(~K, ~V, ~cmp, k, incl, z, m), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, w_in(~K, ~V, ~cmp, lw, up, e, t, hc)), cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), z), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, m), m, pk_f(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, m, hq)))
457    case False{}:
458      cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.last_where(~K, ~V, ~cmp, k, incl, z, m), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, hc))
459
460
461def n3_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, +hbg: {bgood(~K, ~V, ~cmp, bst, Con{e, t}) == True{} : Bool}, +hk: {S.below_upper(~K, ~cmp, k, up) == True{} : Bool}, +ih1: {S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, Some{e})) == chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, Some{e})) : Maybe<&2, M.Entry<K, V>>}, +ih2: {S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, bst)) == chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, bst)) : Maybe<&2, M.Entry<K, V>>}, +qv: Bool, +hq: {S.ordering_ok(cmp(S.key(K, V, e), k), incl) == qv : Bool}, +a: Bool, +ha: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == a : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)) == chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)) : Maybe<&2, M.Entry<K, V>>}:
462  match qv a:
463    case True{} True{}:
464      +hir = ir_t(~K, ~cmp, lw, up, S.key(K, V, e), ha, bu_mono(~K, ~cmp, ~o, up, k, S.key(K, V, e), incl, hk, hq))
465      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.last_where(~K, ~V, ~cmp, k, incl, z, chk(~K, ~V, ~cmp, lw, up, bst)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, w_in(~K, ~V, ~cmp, lw, up, e, t, hir))
466      +l2 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), z), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, Some{e}), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, chk(~K, ~V, ~cmp, lw, up, bst)), Some{e}, chk(~K, ~V, ~cmp, lw, up, Some{e}), pk_t(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, chk(~K, ~V, ~cmp, lw, up, bst), hq), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, Some{e}), Some{e}, chk_in(~K, ~V, ~cmp, lw, up, e, hir))))
467      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq))
468      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, Some{e})), l1, l2), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, Some{e})), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), ih1, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, Some{e})), r1)))
469    case True{} False{}:
470      +hir = ir_fa(~K, ~cmp, lw, up, S.key(K, V, e), ha)
471      +l1 = cong(List<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.last_where(~K, ~V, ~cmp, k, incl, z, chk(~K, ~V, ~cmp, lw, up, bst)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, hir))
472      +l2 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), z), chk(~K, ~V, ~cmp, lw, up, bst), chk(~K, ~V, ~cmp, lw, up, Some{e}), Equal.trans(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, bst), None{}, chk(~K, ~V, ~cmp, lw, up, Some{e}), chk_none(~K, ~V, ~cmp, ~o, lw, up, bst, e, t, hbg, ha), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, Some{e}), None{}, chk_out(~K, ~V, ~cmp, lw, up, e, hir))))
473      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq))
474      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, Some{e})), l1, l2), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, Some{e})), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, Some{e})), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), ih1, Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, Some{e})), r1)))
475    case False{} True{}:
476      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq))
477      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, bst)), lw_skip(~K, ~V, ~cmp, ~o, lw, up, k, incl, e, t, chk(~K, ~V, ~cmp, lw, up, bst), hq, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), {==}), ih2), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, bst)), r1))
478    case False{} False{}:
479      +r1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq))
480      Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), chk(~K, ~V, ~cmp, lw, up, bst)), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), chk(~K, ~V, ~cmp, lw, up, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, bst)), lw_skip(~K, ~V, ~cmp, ~o, lw, up, k, incl, e, t, chk(~K, ~V, ~cmp, lw, up, bst), hq, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), {==}), ih2), Equal.sym(Maybe<&2, M.Entry<K, V>>, chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, Con{e, t}, bst)), chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, bst)), r1))
481
482def n3g(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +hbg: {bgood(~K, ~V, ~cmp, bst, es) == True{} : Bool}, +hk: {S.below_upper(~K, ~cmp, k, up) == True{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es), chk(~K, ~V, ~cmp, lw, up, bst)) == chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, es, bst)) : Maybe<&2, M.Entry<K, V>>}:
483  match es:
484    case Nil{}:
485      {==}
486    case Con{+e, +t}:
487      n3_c(~K, ~V, ~cmp, ~o, lw, up, k, incl, e, t, bst, h, hbg, hk, n3g(~K, ~V, ~cmp, ~o, lw, up, k, incl, t, Some{e}, OR.ord_tail(~K, ~V, ~cmp, e, t, h), OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, h), hk), n3g(~K, ~V, ~cmp, ~o, lw, up, k, incl, t, bst, OR.ord_tail(~K, ~V, ~cmp, e, t, h), bg_tail(~K, ~V, ~cmp, bst, e, t, hbg), hk), S.ordering_ok(cmp(S.key(K, V, e), k), incl), {==}, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), {==})
488
489# from a key below the upper bound, the last at or before it within is the
490# last in the map, when in range
491def lw_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +hk: {S.below_upper(~K, ~cmp, k, up) == True{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es), None{}) == chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, es, None{})) : Maybe<&2, M.Entry<K, V>>}:
492  n3g(~K, ~V, ~cmp, ~o, lw, up, k, incl, es, None{}, h, {==}, hk)
493
494# from a key above the upper bound, the last within
495def lw_above(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +hk: {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es), None{}) == S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)) : Maybe<&2, M.Entry<K, V>>}:
496  Equal.trans(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)), None{}), S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es)), NV.lw_all(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es), None{}, wlt(~K, ~V, ~cmp, ~o, lw, up, k, es, hk)), OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, es))))
497
498# ---- the bounds' own searches ----
499
500def fal_u(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +es: List<&2, M.Entry<K, V>>) -> {fal(~K, ~V, ~cmp, M.Unbounded{}, es) == S.head(M.Entry<K, V>, es) : Maybe<&2, M.Entry<K, V>>}:
501  match es:
502    case Nil{}:
503      {==}
504    case Con{+e, +t}:
505      {==}
506
507def fal_i(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: K, +es: List<&2, M.Entry<K, V>>) -> {fal(~K, ~V, ~cmp, M.Inclusive{x}, es) == S.first_where(~K, ~V, ~cmp, x, True{}, es) : Maybe<&2, M.Entry<K, V>>}:
508  match es:
509    case Nil{}:
510      {==}
511    case Con{+e, +t}:
512      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(x, S.key(K, V, e)), True{}), Some{e}, z), fal(~K, ~V, ~cmp, M.Inclusive{x}, t), S.first_where(~K, ~V, ~cmp, x, True{}, t), fal_i(~K, ~V, ~cmp, x, t))
513
514def fal_x(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: K, +es: List<&2, M.Entry<K, V>>) -> {fal(~K, ~V, ~cmp, M.Exclusive{x}, es) == S.first_where(~K, ~V, ~cmp, x, False{}, es) : Maybe<&2, M.Entry<K, V>>}:
515  match es:
516    case Nil{}:
517      {==}
518    case Con{+e, +t}:
519      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(x, S.key(K, V, e)), False{}), Some{e}, z), fal(~K, ~V, ~cmp, M.Exclusive{x}, t), S.first_where(~K, ~V, ~cmp, x, False{}, t), fal_x(~K, ~V, ~cmp, x, t))
520
521def lbu_u(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +es: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {lbu(~K, ~V, ~cmp, M.Unbounded{}, es, b) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, es), b) : Maybe<&2, M.Entry<K, V>>}:
522  match es:
523    case Nil{}:
524      {==}
525    case Con{+e, +t}:
526      Equal.trans(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, M.Unbounded{}, t, Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, t), Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, t}), b), lbu_u(~K, ~V, ~cmp, t, Some{e}), NV.lw_all_c(K, V, e, t, b))
527
528def lbu_i(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +y: K, +es: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {lbu(~K, ~V, ~cmp, M.Inclusive{y}, es, b) == S.last_where(~K, ~V, ~cmp, y, True{}, es, b) : Maybe<&2, M.Entry<K, V>>}:
529  match es:
530    case Nil{}:
531      {==}
532    case Con{+e, +t}:
533      lbu_i(~K, ~V, ~cmp, y, t, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), y), True{}), Some{e}, b))
534
535def lbu_x(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +y: K, +es: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {lbu(~K, ~V, ~cmp, M.Exclusive{y}, es, b) == S.last_where(~K, ~V, ~cmp, y, False{}, es, b) : Maybe<&2, M.Entry<K, V>>}:
536  match es:
537    case Nil{}:
538      {==}
539    case Con{+e, +t}:
540      lbu_x(~K, ~V, ~cmp, y, t, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), y), False{}), Some{e}, b))
541
542# ---- runs of entries ----
543
544
545def wapp_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +ih: {S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, t, ys)) == SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)) : List<&2, M.Entry<K, V>>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, S.key(K, V, e), lw, up) == b : Bool}) -> {S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, Con{e, t}, ys)) == SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)) : List<&2, M.Entry<K, V>>}:
546  match b:
547    case True{}:
548      +l1 = w_in(~K, ~V, ~cmp, lw, up, e, SC.append(M.Entry<K, V>, t, ys), hb)
549      +r1 = cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, z, S.within(~K, ~V, ~cmp, lw, up, ys)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}, w_in(~K, ~V, ~cmp, lw, up, e, t, hb))
550      Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, Con{e, t}, ys)), Con{e, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys))}, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, Con{e, t}, ys)), Con{e, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, t, ys))}, Con{e, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys))}, l1, cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, t, ys)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), ih)), Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), Con{e, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys))}, r1))
551    case False{}:
552      +l1 = w_out(~K, ~V, ~cmp, lw, up, e, SC.append(M.Entry<K, V>, t, ys), hb)
553      +r1 = cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, z, S.within(~K, ~V, ~cmp, lw, up, ys)), S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), w_out(~K, ~V, ~cmp, lw, up, e, t, hb))
554      Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, Con{e, t}, ys)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, Con{e, t}, ys)), S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, t, ys)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), l1, ih), Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), r1))
555
556def within_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>) -> {S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry<K, V>, xs, ys)) == SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lw, up, xs), S.within(~K, ~V, ~cmp, lw, up, ys)) : List<&2, M.Entry<K, V>>}:
557  match xs:
558    case Nil{}:
559      {==}
560    case Con{+e, +t}:
561      wapp_c(~K, ~V, ~cmp, lw, up, e, t, ys, within_app(~K, ~V, ~cmp, lw, up, t, ys), S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), {==})
562
563# every entry above the lower bound / below the upper bound
564def allal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, es: List<&2, M.Entry<K, V>>) -> Bool:
565  match es:
566    case Nil{}:
567      True{}
568    case Con{+e, t}:
569      Bool.and(S.above_lower(~K, ~cmp, S.key(K, V, e), lw), allal(~K, ~V, ~cmp, lw, t))
570
571def allbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound<K>, es: List<&2, M.Entry<K, V>>) -> Bool:
572  match es:
573    case Nil{}:
574      True{}
575    case Con{+e, t}:
576      Bool.and(S.below_upper(~K, ~cmp, S.key(K, V, e), up), allbu(~K, ~V, ~cmp, up, t))
577
578# sorted, the first above the lower bound: all are
579def al_all(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +t: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, +ha: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == True{} : Bool}) -> {allal(~K, ~V, ~cmp, lw, Con{e, t}) == True{} : Bool}:
580  match t:
581    case Nil{}:
582      L.and_intro(S.above_lower(~K, ~cmp, S.key(K, V, e), lw), True{}, ha, {==})
583    case Con{+f, +u}:
584      +hlt = L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, f))), ST.ordered(~K, ~V, ~cmp, Con{f, u}), h)
585      +hf = al_mono(~K, ~cmp, ~o, lw, S.key(K, V, e), S.key(K, V, f), False{}, ha, lt_okf(cmp(S.key(K, V, e), S.key(K, V, f)), hlt))
586      L.and_intro(S.above_lower(~K, ~cmp, S.key(K, V, e), lw), allal(~K, ~V, ~cmp, lw, Con{f, u}), ha, al_all(~K, ~V, ~cmp, ~o, lw, u, f, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, f))), ST.ordered(~K, ~V, ~cmp, Con{f, u}), h), hf))
587
588def allbu_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound<K>, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +hx: {allbu(~K, ~V, ~cmp, up, xs) == True{} : Bool}, +hy: {allbu(~K, ~V, ~cmp, up, ys) == True{} : Bool}) -> {allbu(~K, ~V, ~cmp, up, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}:
589  match xs:
590    case Nil{}:
591      hy
592    case Con{+e, +t}:
593      L.and_intro(S.below_upper(~K, ~cmp, S.key(K, V, e), up), allbu(~K, ~V, ~cmp, up, SC.append(M.Entry<K, V>, t, ys)), L.and_left(S.below_upper(~K, ~cmp, S.key(K, V, e), up), allbu(~K, ~V, ~cmp, up, t), hx), allbu_app(~K, ~V, ~cmp, up, t, ys, L.and_right(S.below_upper(~K, ~cmp, S.key(K, V, e), up), allbu(~K, ~V, ~cmp, up, t), hx), hy))
594
595def allbu_rev(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound<K>, +xs: List<&2, M.Entry<K, V>>, +h: {allbu(~K, ~V, ~cmp, up, xs) == True{} : Bool}) -> {allbu(~K, ~V, ~cmp, up, SC.reverse(M.Entry<K, V>, xs)) == True{} : Bool}:
596  match xs:
597    case Nil{}:
598      {==}
599    case Con{+e, +t}:
600      +h1 = allbu_app(~K, ~V, ~cmp, up, SC.reverse(M.Entry<K, V>, t), Con{e, Nil{}}, allbu_rev(~K, ~V, ~cmp, up, t, L.and_right(S.below_upper(~K, ~cmp, S.key(K, V, e), up), allbu(~K, ~V, ~cmp, up, t), h)), L.and_intro(S.below_upper(~K, ~cmp, S.key(K, V, e), up), True{}, L.and_left(S.below_upper(~K, ~cmp, S.key(K, V, e), up), allbu(~K, ~V, ~cmp, up, t), h), {==}))
601      L.subst(List<&2, M.Entry<K, V>>, z => {allbu(~K, ~V, ~cmp, up, z) == True{} : Bool}, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{e, Nil{}}), SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), e), Equal.sym(List<&2, M.Entry<K, V>>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), e), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{e, Nil{}}), LL.snoc_append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), e)), h1)
602
603# below a key under the lower bound, nothing is within
604def wnil_lt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +xs: List<&2, M.Entry<K, V>>, +hk: {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}, +hl: {OR.ltall(~K, ~V, ~cmp, k, xs) == True{} : Bool}) -> {S.within(~K, ~V, ~cmp, lw, up, xs) == Nil{} : List<&2, M.Entry<K, V>>}:
605  match xs:
606    case Nil{}:
607      {==}
608    case Con{+e, +u}:
609      +h1 = L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, u), hl)
610      +h2 = L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, u), hl)
611      Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, Con{e, u}), S.within(~K, ~V, ~cmp, lw, up, u), Nil{}, w_out(~K, ~V, ~cmp, lw, up, e, u, ir_fa(~K, ~cmp, lw, up, S.key(K, V, e), al_false(~K, ~cmp, ~o, lw, k, S.key(K, V, e), hk, h1))), wnil_lt(~K, ~V, ~cmp, ~o, lw, up, k, u, hk, h2))
612
613def bu_of(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +ha: {S.above_lower(~K, ~cmp, k, lw) == True{} : Bool}, +hir: {S.in_range(~K, ~cmp, k, lw, up) == False{} : Bool}) -> {S.below_upper(~K, ~cmp, k, up) == False{} : Bool}:
614  L.subst(Bool, z => {Bool.and(z, S.below_upper(~K, ~cmp, k, up)) == False{} : Bool}, S.above_lower(~K, ~cmp, k, lw), True{}, ha, hir)
615
616def al_oc(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +hb: {S.below_upper(~K, ~cmp, k, up) == True{} : Bool}, +hir: {S.in_range(~K, ~cmp, k, lw, up) == False{} : Bool}, +a: Bool, +ha: {S.above_lower(~K, ~cmp, k, lw) == a : Bool}) -> {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}:
617  match a:
618    case True{}:
619      Empty.absurd({S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, S.below_upper(~K, ~cmp, k, up), False{}, Equal.sym(Bool, S.below_upper(~K, ~cmp, k, up), True{}, hb), bu_of(~K, ~cmp, lw, up, k, ha, hir))))
620    case False{}:
621      ha
622
623def al_of(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +up: M.Bound<K>, +k: K, +hb: {S.below_upper(~K, ~cmp, k, up) == True{} : Bool}, +hir: {S.in_range(~K, ~cmp, k, lw, up) == False{} : Bool}) -> {S.above_lower(~K, ~cmp, k, lw) == False{} : Bool}:
624  al_oc(~K, ~cmp, lw, up, k, hb, hir, S.above_lower(~K, ~cmp, k, lw), {==})
625
626# ---- a sorted list split at a bound ----
627
628
629def spf_up2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +hf: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == False{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +h1: {t == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {fal(~K, ~V, ~cmp, lw, t) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>})) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {Con{e, t} == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {fal(~K, ~V, ~cmp, lw, Con{e, t}) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>:
630  match r:
631    case Tuple{h2, Tuple{h3, h4}}:
632      (Con{e, xa}, (xb, (cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, t, SC.append(M.Entry<K, V>, xa, xb), h1), (h2, (Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, Con{e, xa}), S.within(~K, ~V, ~cmp, lw, up, xa), Nil{}, w_out(~K, ~V, ~cmp, lw, up, e, xa, ir_fa(~K, ~cmp, lw, up, S.key(K, V, e), hf)), h3), Equal.trans(Maybe<&2, M.Entry<K, V>>, fal(~K, ~V, ~cmp, lw, Con{e, t}), fal(~K, ~V, ~cmp, lw, t), S.head(M.Entry<K, V>, xb), pk_f(Maybe<&2, M.Entry<K, V>>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t), hf), h4))))))
633
634def spf_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +hf: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == False{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {t == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {fal(~K, ~V, ~cmp, lw, t) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {Con{e, t} == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {fal(~K, ~V, ~cmp, lw, Con{e, t}) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>:
635  match r:
636    case Tuple{+xa, Tuple{+xb, Tuple{+h1, r2}}}:
637      spf_up2(~K, ~V, ~cmp, ~o, lw, up, e, t, hf, xa, xb, h1, r2)
638
639def spf_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {t == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {fal(~K, ~V, ~cmp, lw, t) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>, +a: Bool, +ha: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == a : Bool}) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {Con{e, t} == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {fal(~K, ~V, ~cmp, lw, Con{e, t}) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>:
640  match a:
641    case True{}:
642      (Nil{}, (Con{e, t}, ({==}, (al_all(~K, ~V, ~cmp, ~o, lw, t, e, h, ha), ({==}, pk_t(Maybe<&2, M.Entry<K, V>>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t), ha))))))
643    case False{}:
644      spf_up(~K, ~V, ~cmp, ~o, lw, up, e, t, ha, r)
645
646# the entries below the lower bound, then those above it
647def split_fal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {es == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {fal(~K, ~V, ~cmp, lw, es) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>:
648  match es:
649    case Nil{}:
650      (Nil{}, (Nil{}, ({==}, ({==}, ({==}, {==})))))
651    case Con{+e, +t}:
652      spf_c(~K, ~V, ~cmp, ~o, lw, up, e, t, h, split_fal(~K, ~V, ~cmp, ~o, lw, up, t, OR.ord_tail(~K, ~V, ~cmp, e, t, h)), S.above_lower(~K, ~cmp, S.key(K, V, e), lw), {==})
653
654
655def spb_up2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +h1: {t == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {lbu(~K, ~V, ~cmp, up, t, Some{e}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), Some{e}) : Maybe<&2, M.Entry<K, V>>})) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {Con{e, t} == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {lbu(~K, ~V, ~cmp, up, Con{e, t}, bst) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), bst) : Maybe<&2, M.Entry<K, V>>}))>>:
656  match r:
657    case Tuple{h2, Tuple{h3, h4}}:
658      +e1 = cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => lbu(~K, ~V, ~cmp, up, t, z), S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb))
659      (Con{e, xa}, (xb, (cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, t, SC.append(M.Entry<K, V>, xa, xb), h1), (L.and_intro(S.below_upper(~K, ~cmp, S.key(K, V, e), up), allbu(~K, ~V, ~cmp, up, xa), hb, h2), (h3, Equal.trans(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, xa}), bst), Equal.trans(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst), lbu(~K, ~V, ~cmp, up, t, Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), Some{e}), e1, h4), NV.lw_all_c(K, V, e, xa, bst)))))))
660
661def spb_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == True{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {t == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {lbu(~K, ~V, ~cmp, up, t, Some{e}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), Some{e}) : Maybe<&2, M.Entry<K, V>>}))>>) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {Con{e, t} == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {lbu(~K, ~V, ~cmp, up, Con{e, t}, bst) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), bst) : Maybe<&2, M.Entry<K, V>>}))>>:
662  match r:
663    case Tuple{+xa, Tuple{+xb, Tuple{+h1, r2}}}:
664      spb_up2(~K, ~V, ~cmp, ~o, lw, up, e, t, bst, hb, xa, xb, h1, r2)
665
666def spb_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {t == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {lbu(~K, ~V, ~cmp, up, t, Some{e}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), Some{e}) : Maybe<&2, M.Entry<K, V>>}))>>, +b: Bool, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == b : Bool}) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {Con{e, t} == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {lbu(~K, ~V, ~cmp, up, Con{e, t}, bst) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), bst) : Maybe<&2, M.Entry<K, V>>}))>>:
667  match b:
668    case True{}:
669      spb_up(~K, ~V, ~cmp, ~o, lw, up, e, t, bst, hb, r)
670    case False{}:
671      +hgt = OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, h)
672      +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, t), Nil{}, w_out(~K, ~V, ~cmp, lw, up, e, t, ir_fb(~K, ~cmp, lw, up, S.key(K, V, e), hb)), wnil(~K, ~V, ~cmp, ~o, lw, up, S.key(K, V, e), t, hb, hgt))
673      +hl = Equal.trans(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst), lbu(~K, ~V, ~cmp, up, t, bst), bst, cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => lbu(~K, ~V, ~cmp, up, t, z), S.pick(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry<K, V>>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb)), lbu_none(~K, ~V, ~cmp, ~o, up, S.key(K, V, e), t, bst, hb, hgt))
674      (Nil{}, (Con{e, t}, ({==}, ({==}, (hw, hl)))))
675
676# the entries below the upper bound, then those above it
677def split_lbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound<K>, +up: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +bst: Maybe<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {es == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {lbu(~K, ~V, ~cmp, up, es, bst) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), bst) : Maybe<&2, M.Entry<K, V>>}))>>:
678  match es:
679    case Nil{}:
680      (Nil{}, (Nil{}, ({==}, ({==}, ({==}, {==})))))
681    case Con{+e, +t}:
682      spb_c(~K, ~V, ~cmp, ~o, lw, up, e, t, bst, h, split_lbu(~K, ~V, ~cmp, ~o, lw, up, t, Some{e}, OR.ord_tail(~K, ~V, ~cmp, e, t, h)), S.below_upper(~K, ~cmp, S.key(K, V, e), up), {==})
683
684def start_fal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound<K>, +es: List<&2, M.Entry<K, V>>) -> {S.start(~K, ~V, ~cmp, lw, True{}, es) == S.key_m(K, V, fal(~K, ~V, ~cmp, lw, es)) : Maybe<&2, K>}:
685  match lw:
686    case M.Unbounded{}:
687      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, z => S.key_m(K, V, z), S.head(M.Entry<K, V>, es), fal(~K, ~V, ~cmp, M.Unbounded{}, es), Equal.sym(Maybe<&2, M.Entry<K, V>>, fal(~K, ~V, ~cmp, M.Unbounded{}, es), S.head(M.Entry<K, V>, es), fal_u(~K, ~V, ~cmp, es)))
688    case M.Inclusive{+x}:
689      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, z => S.key_m(K, V, z), S.first_where(~K, ~V, ~cmp, x, True{}, es), fal(~K, ~V, ~cmp, M.Inclusive{x}, es), Equal.sym(Maybe<&2, M.Entry<K, V>>, fal(~K, ~V, ~cmp, M.Inclusive{x}, es), S.first_where(~K, ~V, ~cmp, x, True{}, es), fal_i(~K, ~V, ~cmp, x, es)))
690    case M.Exclusive{+x}:
691      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, z => S.key_m(K, V, z), S.first_where(~K, ~V, ~cmp, x, False{}, es), fal(~K, ~V, ~cmp, M.Exclusive{x}, es), Equal.sym(Maybe<&2, M.Entry<K, V>>, fal(~K, ~V, ~cmp, M.Exclusive{x}, es), S.first_where(~K, ~V, ~cmp, x, False{}, es), fal_x(~K, ~V, ~cmp, x, es)))
692
693def start_lbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound<K>, +es: List<&2, M.Entry<K, V>>) -> {S.start(~K, ~V, ~cmp, up, False{}, es) == S.key_m(K, V, lbu(~K, ~V, ~cmp, up, es, None{})) : Maybe<&2, K>}:
694  match up:
695    case M.Unbounded{}:
696      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, z => S.key_m(K, V, z), S.last(M.Entry<K, V>, es), lbu(~K, ~V, ~cmp, M.Unbounded{}, es, None{}), Equal.sym(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, M.Unbounded{}, es, None{}), S.last(M.Entry<K, V>, es), Equal.trans(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, M.Unbounded{}, es, None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, es), None{}), S.last(M.Entry<K, V>, es), lbu_u(~K, ~V, ~cmp, es, None{}), OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, es)))))
697    case M.Inclusive{+y}:
698      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, z => S.key_m(K, V, z), S.last_where(~K, ~V, ~cmp, y, True{}, es, None{}), lbu(~K, ~V, ~cmp, M.Inclusive{y}, es, None{}), Equal.sym(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, M.Inclusive{y}, es, None{}), S.last_where(~K, ~V, ~cmp, y, True{}, es, None{}), lbu_i(~K, ~V, ~cmp, y, es, None{})))
699    case M.Exclusive{+y}:
700      cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, z => S.key_m(K, V, z), S.last_where(~K, ~V, ~cmp, y, False{}, es, None{}), lbu(~K, ~V, ~cmp, M.Exclusive{y}, es, None{}), Equal.sym(Maybe<&2, M.Entry<K, V>>, lbu(~K, ~V, ~cmp, M.Exclusive{y}, es, None{}), S.last_where(~K, ~V, ~cmp, y, False{}, es, None{}), lbu_x(~K, ~V, ~cmp, y, es, None{})))