1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/order.bend as O 4 import ../../lib/list.bend as LL 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/balanced_search_tree/main.bend as S 7 import ../../../src/containers/balanced_search_tree.bend as M 8 import ./state.bend as ST 9 import ./ord.bend as OR 10 import ./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 21 def 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 25 def 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 29 def 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 32 def and_f(+a: Bool) -> {Bool.and(a, False{}) == False{} : Bool}: 33 match a: 34 case True{}: 35 {==} 36 case False{}: 37 {==} 38 39 def 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 42 def 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 47 def 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 62 def 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 77 def 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 92 def 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 101 def 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 114 def 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 119 def 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 129 def 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 132 def 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 135 def 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 141 def al_mono(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +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 150 def bu_mono(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound, +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 160 def al_lt(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +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 169 def bu_lt(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound, +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 178 def bu_fc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound, +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 186 def bu_false(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound, +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 189 def al_fc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +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 197 def al_false(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +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 200 def ir_t(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +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 203 def ir_fb(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +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 207 def ir_fa(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +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 213 def w_in(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +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>}: 214 pk_t(List<&2, M.Entry>, 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 216 def w_out(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +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>}: 217 pk_f(List<&2, M.Entry>, 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 219 def chk(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, m: Maybe<&2, M.Entry>) -> Maybe<&2, M.Entry>: 220 match m: 221 case None{}: 222 None{} 223 case Some{+e}: 224 S.pick(Maybe<&2, M.Entry>, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), Some{e}, None{}) 225 226 def chk_in(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +e: M.Entry, +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>}: 227 pk_t(Maybe<&2, M.Entry>, S.in_range(~K, ~cmp, S.key(K, V, e), lw, up), Some{e}, None{}, h) 228 229 def chk_out(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +e: M.Entry, +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>}: 230 pk_f(Maybe<&2, M.Entry>, 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 233 def wnil(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +t: List<&2, M.Entry>, +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>}: 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>, 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 242 def gt_wc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +k: K, +e: M.Entry, +u: List<&2, M.Entry>, +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>, 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 249 def gt_w(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +k: K, +t: List<&2, M.Entry>, +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 256 def wgt_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +e: M.Entry, +u: List<&2, M.Entry>, +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>, 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 264 def wgt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +es: List<&2, M.Entry>, +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 271 def wlt_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +e: M.Entry, +u: List<&2, M.Entry>, +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>, 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 279 def wlt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +es: List<&2, M.Entry>, +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 288 def fal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, es: List<&2, M.Entry>) -> Maybe<&2, M.Entry>: 289 match es: 290 case Nil{}: 291 None{} 292 case Con{+e, +t}: 293 S.pick(Maybe<&2, M.Entry>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t)) 294 295 296 def e1_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, +ih: {S.head(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t)) == chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, t)) : Maybe<&2, M.Entry>}, +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, 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>}: 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>, Maybe<&2, M.Entry>, z => S.head(M.Entry, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, z), fal(~K, ~V, ~cmp, lw, Con{e, t}), Some{e}, pk_t(Maybe<&2, M.Entry>, 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>, S.head(M.Entry, 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>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), Some{e}, Equal.trans(Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, z => S.head(M.Entry, 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>, Maybe<&2, M.Entry>, z => S.head(M.Entry, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, z), fal(~K, ~V, ~cmp, lw, Con{e, t}), Some{e}, pk_t(Maybe<&2, M.Entry>, 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>, S.head(M.Entry, 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>, S.head(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.head(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t)), None{}, l1, l2), Equal.sym(Maybe<&2, M.Entry>, chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, Con{e, t})), None{}, Equal.trans(Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, z => S.head(M.Entry, 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>, Maybe<&2, M.Entry>, 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>, 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>, S.head(M.Entry, 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>, S.head(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.head(M.Entry, 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>, 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>, Maybe<&2, M.Entry>, z => S.head(M.Entry, 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>, Maybe<&2, M.Entry>, 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>, 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>, S.head(M.Entry, 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>, S.head(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), S.head(M.Entry, 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>, 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 318 def first_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +es: List<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> {S.head(M.Entry, S.within(~K, ~V, ~cmp, lw, up, es)) == chk(~K, ~V, ~cmp, lw, up, fal(~K, ~V, ~cmp, lw, es)) : Maybe<&2, M.Entry>}: 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 327 def lbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound, es: List<&2, M.Entry>, +best: Maybe<&2, M.Entry>) -> Maybe<&2, M.Entry>: 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>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, best)) 333 334 # a candidate before every entry 335 def bgood(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Maybe<&2, M.Entry>, +es: List<&2, M.Entry>) -> 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 342 def bg_tail(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m: Maybe<&2, M.Entry>, +e: M.Entry, +t: List<&2, M.Entry>, +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 350 def chk_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +m: Maybe<&2, M.Entry>, +e: M.Entry, +t: List<&2, M.Entry>, +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>}: 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 358 def lbu_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +up: M.Bound, +k: K, +t: List<&2, M.Entry>, +best: Maybe<&2, M.Entry>, +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>}: 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>, S.pick(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, f), up), Some{f}, best), best, pk_f(Maybe<&2, M.Entry>, 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>} 366 lbu_none(~K, ~V, ~cmp, ~o, up, k, u, best, hk, h2) 367 368 369 def e2_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +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, S.last(M.Entry, 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>}, +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, S.last(M.Entry, 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>}: 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>, Maybe<&2, M.Entry>, z => OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t)), Some{e}), OR.orm(M.Entry, S.last(M.Entry, 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>, Maybe<&2, M.Entry>, z => OR.orm(M.Entry, S.last(M.Entry, 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>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb)) 377 Equal.trans(Maybe<&2, M.Entry>, OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, Con{e, S.within(~K, ~V, ~cmp, lw, up, t)}), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t)), Some{e}), OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, 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>, 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>, Maybe<&2, M.Entry>, z => OR.orm(M.Entry, S.last(M.Entry, 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>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb)) 383 +r2 = cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, 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>, OR.orm(M.Entry, S.last(M.Entry, 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>, 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>, 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>, Maybe<&2, M.Entry>, z => OR.orm(M.Entry, S.last(M.Entry, 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>, Maybe<&2, M.Entry>, z => OR.orm(M.Entry, S.last(M.Entry, 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>, Maybe<&2, M.Entry>, z => OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t)), z), None{}, chk(~K, ~V, ~cmp, lw, up, Some{e}), Equal.sym(Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb)) 391 Equal.trans(Maybe<&2, M.Entry>, OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t})), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t)), chk(~K, ~V, ~cmp, lw, up, bst)), OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t)), None{}), OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, 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>, 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>, Maybe<&2, M.Entry>, z => OR.orm(M.Entry, S.last(M.Entry, 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>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, lbu(~K, ~V, ~cmp, up, t, z)), S.pick(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst, hb)) 397 +r2 = cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, 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>, OR.orm(M.Entry, S.last(M.Entry, 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>, 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>, 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 400 def e2g(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +es: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +hbg: {bgood(~K, ~V, ~cmp, bst, es) == True{} : Bool}) -> {OR.orm(M.Entry, S.last(M.Entry, 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>}: 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 407 def last_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +es: List<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> {S.last(M.Entry, 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>}: 408 Equal.trans(Maybe<&2, M.Entry>, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, es)), OR.orm(M.Entry, S.last(M.Entry, 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>, OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, es)), None{}), S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, es)), OR.orm_none(M.Entry, S.last(M.Entry, 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 414 def fw_skip(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +e: M.Entry, +t: List<&2, M.Entry>, +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>}: 415 match c: 416 case True{}: 417 Equal.trans(Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, 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>, 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>, Maybe<&2, M.Entry>, 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 421 def n1_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +e: M.Entry, +t: List<&2, M.Entry>, +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>}, +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>}: 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>, 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>, Maybe<&2, M.Entry>, 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>, 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>, 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>, Maybe<&2, M.Entry>, 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>, 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>, 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>, 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>, 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>, Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, 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>, 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>, Maybe<&2, M.Entry>, 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>, 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>, 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>, 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>, Maybe<&2, M.Entry>, 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>, 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>, 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>, 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>, 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>, Maybe<&2, M.Entry>, 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>, 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>, 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>, 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>, 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 442 def fw_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +es: List<&2, M.Entry>, +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>}: 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 450 def fw_below(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +es: List<&2, M.Entry>, +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, S.within(~K, ~V, ~cmp, lw, up, es)) : Maybe<&2, M.Entry>}: 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 453 def lw_skip(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +e: M.Entry, +t: List<&2, M.Entry>, +m: Maybe<&2, M.Entry>, +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>}: 454 match c: 455 case True{}: 456 Equal.trans(Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, z => S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), z), S.pick(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, m), m, pk_f(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, m, hq))) 457 case False{}: 458 cong(List<&2, M.Entry>, Maybe<&2, M.Entry>, 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 461 def n3_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +e: M.Entry, +t: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +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>}, +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>}, +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>}: 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>, Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, z => S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, t), z), S.pick(Maybe<&2, M.Entry>, 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>, S.pick(Maybe<&2, M.Entry>, 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>, 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>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq)) 468 Equal.trans(Maybe<&2, M.Entry>, 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>, 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>, 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>, 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>, Maybe<&2, M.Entry>, 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>, Maybe<&2, M.Entry>, 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>, 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>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq)) 474 Equal.trans(Maybe<&2, M.Entry>, 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>, 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>, 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>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq)) 477 Equal.trans(Maybe<&2, M.Entry>, 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>, 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>, 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>, Maybe<&2, M.Entry>, z => chk(~K, ~V, ~cmp, lw, up, S.last_where(~K, ~V, ~cmp, k, incl, t, z)), S.pick(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, bst, hq)) 480 Equal.trans(Maybe<&2, M.Entry>, 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>, 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>, 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 482 def n3g(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +es: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +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>}: 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 491 def lw_within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +es: List<&2, M.Entry>, +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>}: 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 495 def lw_above(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +incl: Bool, +es: List<&2, M.Entry>, +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, S.within(~K, ~V, ~cmp, lw, up, es)) : Maybe<&2, M.Entry>}: 496 Equal.trans(Maybe<&2, M.Entry>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lw, up, es), None{}), OR.orm(M.Entry, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, es)), None{}), S.last(M.Entry, 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, S.last(M.Entry, S.within(~K, ~V, ~cmp, lw, up, es)))) 497 498 # ---- the bounds' own searches ---- 499 500 def fal_u(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +es: List<&2, M.Entry>) -> {fal(~K, ~V, ~cmp, M.Unbounded{}, es) == S.head(M.Entry, es) : Maybe<&2, M.Entry>}: 501 match es: 502 case Nil{}: 503 {==} 504 case Con{+e, +t}: 505 {==} 506 507 def fal_i(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: K, +es: List<&2, M.Entry>) -> {fal(~K, ~V, ~cmp, M.Inclusive{x}, es) == S.first_where(~K, ~V, ~cmp, x, True{}, es) : Maybe<&2, M.Entry>}: 508 match es: 509 case Nil{}: 510 {==} 511 case Con{+e, +t}: 512 cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, 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 514 def fal_x(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: K, +es: List<&2, M.Entry>) -> {fal(~K, ~V, ~cmp, M.Exclusive{x}, es) == S.first_where(~K, ~V, ~cmp, x, False{}, es) : Maybe<&2, M.Entry>}: 515 match es: 516 case Nil{}: 517 {==} 518 case Con{+e, +t}: 519 cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => S.pick(Maybe<&2, M.Entry>, 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 521 def lbu_u(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +es: List<&2, M.Entry>, +b: Maybe<&2, M.Entry>) -> {lbu(~K, ~V, ~cmp, M.Unbounded{}, es, b) == OR.orm(M.Entry, S.last(M.Entry, es), b) : Maybe<&2, M.Entry>}: 522 match es: 523 case Nil{}: 524 {==} 525 case Con{+e, +t}: 526 Equal.trans(Maybe<&2, M.Entry>, lbu(~K, ~V, ~cmp, M.Unbounded{}, t, Some{e}), OR.orm(M.Entry, S.last(M.Entry, t), Some{e}), OR.orm(M.Entry, S.last(M.Entry, Con{e, t}), b), lbu_u(~K, ~V, ~cmp, t, Some{e}), NV.lw_all_c(K, V, e, t, b)) 527 528 def lbu_i(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +y: K, +es: List<&2, M.Entry>, +b: Maybe<&2, M.Entry>) -> {lbu(~K, ~V, ~cmp, M.Inclusive{y}, es, b) == S.last_where(~K, ~V, ~cmp, y, True{}, es, b) : Maybe<&2, M.Entry>}: 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>, S.ordering_ok(cmp(S.key(K, V, e), y), True{}), Some{e}, b)) 534 535 def lbu_x(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +y: K, +es: List<&2, M.Entry>, +b: Maybe<&2, M.Entry>) -> {lbu(~K, ~V, ~cmp, M.Exclusive{y}, es, b) == S.last_where(~K, ~V, ~cmp, y, False{}, es, b) : Maybe<&2, M.Entry>}: 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>, S.ordering_ok(cmp(S.key(K, V, e), y), False{}), Some{e}, b)) 541 542 # ---- runs of entries ---- 543 544 545 def wapp_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +ys: List<&2, M.Entry>, +ih: {S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, t, ys)) == SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)) : List<&2, M.Entry>}, +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, Con{e, t}, ys)) == SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)) : List<&2, M.Entry>}: 546 match b: 547 case True{}: 548 +l1 = w_in(~K, ~V, ~cmp, lw, up, e, SC.append(M.Entry, t, ys), hb) 549 +r1 = cong(List<&2, M.Entry>, List<&2, M.Entry>, z => SC.append(M.Entry, 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>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, Con{e, t}, ys)), Con{e, SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys))}, SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), Equal.trans(List<&2, M.Entry>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, Con{e, t}, ys)), Con{e, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, t, ys))}, Con{e, SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys))}, l1, cong(List<&2, M.Entry>, List<&2, M.Entry>, z => Con{e, z}, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, t, ys)), SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), ih)), Equal.sym(List<&2, M.Entry>, SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), Con{e, SC.append(M.Entry, 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, t, ys), hb) 553 +r1 = cong(List<&2, M.Entry>, List<&2, M.Entry>, z => SC.append(M.Entry, 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>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, Con{e, t}, ys)), SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), Equal.trans(List<&2, M.Entry>, S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, Con{e, t}, ys)), S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, t, ys)), SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), l1, ih), Equal.sym(List<&2, M.Entry>, SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, Con{e, t}), S.within(~K, ~V, ~cmp, lw, up, ys)), SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, t), S.within(~K, ~V, ~cmp, lw, up, ys)), r1)) 555 556 def within_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +xs: List<&2, M.Entry>, +ys: List<&2, M.Entry>) -> {S.within(~K, ~V, ~cmp, lw, up, SC.append(M.Entry, xs, ys)) == SC.append(M.Entry, S.within(~K, ~V, ~cmp, lw, up, xs), S.within(~K, ~V, ~cmp, lw, up, ys)) : List<&2, M.Entry>}: 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 564 def allal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, es: List<&2, M.Entry>) -> 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 571 def allbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound, es: List<&2, M.Entry>) -> 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 579 def al_all(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +t: List<&2, M.Entry>, +e: M.Entry, +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 588 def allbu_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound, +xs: List<&2, M.Entry>, +ys: List<&2, M.Entry>, +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, 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, 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 595 def allbu_rev(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound, +xs: List<&2, M.Entry>, +h: {allbu(~K, ~V, ~cmp, up, xs) == True{} : Bool}) -> {allbu(~K, ~V, ~cmp, up, SC.reverse(M.Entry, 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, 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>, z => {allbu(~K, ~V, ~cmp, up, z) == True{} : Bool}, SC.append(M.Entry, SC.reverse(M.Entry, t), Con{e, Nil{}}), SC.snoc(M.Entry, SC.reverse(M.Entry, t), e), Equal.sym(List<&2, M.Entry>, SC.snoc(M.Entry, SC.reverse(M.Entry, t), e), SC.append(M.Entry, SC.reverse(M.Entry, t), Con{e, Nil{}}), LL.snoc_append(M.Entry, SC.reverse(M.Entry, t), e)), h1) 602 603 # below a key under the lower bound, nothing is within 604 def wnil_lt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +k: K, +xs: List<&2, M.Entry>, +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>}: 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>, 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 613 def bu_of(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +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 616 def al_oc(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +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 623 def al_of(~K: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +up: M.Bound, +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 629 def spf_up2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +hf: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == False{} : Bool}, +xa: List<&2, M.Entry>, +xb: List<&2, M.Entry>, +h1: {t == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>}, r: {allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry>} & {fal(~K, ~V, ~cmp, lw, t) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>})) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {Con{e, t} == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry>} & {fal(~K, ~V, ~cmp, lw, Con{e, t}) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>}))>>: 630 match r: 631 case Tuple{h2, Tuple{h3, h4}}: 632 (Con{e, xa}, (xb, (cong(List<&2, M.Entry>, List<&2, M.Entry>, z => Con{e, z}, t, SC.append(M.Entry, xa, xb), h1), (h2, (Equal.trans(List<&2, M.Entry>, 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>, fal(~K, ~V, ~cmp, lw, Con{e, t}), fal(~K, ~V, ~cmp, lw, t), S.head(M.Entry, xb), pk_f(Maybe<&2, M.Entry>, S.above_lower(~K, ~cmp, S.key(K, V, e), lw), Some{e}, fal(~K, ~V, ~cmp, lw, t), hf), h4)))))) 633 634 def spf_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +hf: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == False{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {t == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry>} & {fal(~K, ~V, ~cmp, lw, t) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>}))>>) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {Con{e, t} == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry>} & {fal(~K, ~V, ~cmp, lw, Con{e, t}) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>}))>>: 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 639 def spf_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {t == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry>} & {fal(~K, ~V, ~cmp, lw, t) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>}))>>, +a: Bool, +ha: {S.above_lower(~K, ~cmp, S.key(K, V, e), lw) == a : Bool}) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {Con{e, t} == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry>} & {fal(~K, ~V, ~cmp, lw, Con{e, t}) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>}))>>: 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>, 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 647 def split_fal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +es: List<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {es == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allal(~K, ~V, ~cmp, lw, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xa) == Nil{} : List<&2, M.Entry>} & {fal(~K, ~V, ~cmp, lw, es) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>}))>>: 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 655 def spb_up2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == True{} : Bool}, +xa: List<&2, M.Entry>, +xb: List<&2, M.Entry>, +h1: {t == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>}, r: {allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry>} & {lbu(~K, ~V, ~cmp, up, t, Some{e}) == OR.orm(M.Entry, S.last(M.Entry, xa), Some{e}) : Maybe<&2, M.Entry>})) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {Con{e, t} == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry>} & {lbu(~K, ~V, ~cmp, up, Con{e, t}, bst) == OR.orm(M.Entry, S.last(M.Entry, xa), bst) : Maybe<&2, M.Entry>}))>>: 656 match r: 657 case Tuple{h2, Tuple{h3, h4}}: 658 +e1 = cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => lbu(~K, ~V, ~cmp, up, t, z), S.pick(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), Some{e}, pk_t(Maybe<&2, M.Entry>, 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>, List<&2, M.Entry>, z => Con{e, z}, t, SC.append(M.Entry, 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>, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst), OR.orm(M.Entry, S.last(M.Entry, xa), Some{e}), OR.orm(M.Entry, S.last(M.Entry, Con{e, xa}), bst), Equal.trans(Maybe<&2, M.Entry>, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst), lbu(~K, ~V, ~cmp, up, t, Some{e}), OR.orm(M.Entry, S.last(M.Entry, xa), Some{e}), e1, h4), NV.lw_all_c(K, V, e, xa, bst))))))) 660 661 def spb_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == True{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {t == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry>} & {lbu(~K, ~V, ~cmp, up, t, Some{e}) == OR.orm(M.Entry, S.last(M.Entry, xa), Some{e}) : Maybe<&2, M.Entry>}))>>) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {Con{e, t} == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry>} & {lbu(~K, ~V, ~cmp, up, Con{e, t}, bst) == OR.orm(M.Entry, S.last(M.Entry, xa), bst) : Maybe<&2, M.Entry>}))>>: 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 666 def spb_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +e: M.Entry, +t: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, r: Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {t == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry>} & {lbu(~K, ~V, ~cmp, up, t, Some{e}) == OR.orm(M.Entry, S.last(M.Entry, xa), Some{e}) : Maybe<&2, M.Entry>}))>>, +b: Bool, +hb: {S.below_upper(~K, ~cmp, S.key(K, V, e), up) == b : Bool}) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {Con{e, t} == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry>} & {lbu(~K, ~V, ~cmp, up, Con{e, t}, bst) == OR.orm(M.Entry, S.last(M.Entry, xa), bst) : Maybe<&2, M.Entry>}))>>: 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>, 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>, lbu(~K, ~V, ~cmp, up, Con{e, t}, bst), lbu(~K, ~V, ~cmp, up, t, bst), bst, cong(Maybe<&2, M.Entry>, Maybe<&2, M.Entry>, z => lbu(~K, ~V, ~cmp, up, t, z), S.pick(Maybe<&2, M.Entry>, S.below_upper(~K, ~cmp, S.key(K, V, e), up), Some{e}, bst), bst, pk_f(Maybe<&2, M.Entry>, 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 677 def split_lbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +lw: M.Bound, +up: M.Bound, +es: List<&2, M.Entry>, +bst: Maybe<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> Sigma<&1, &1, List<&2, M.Entry>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {es == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({allbu(~K, ~V, ~cmp, up, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lw, up, xb) == Nil{} : List<&2, M.Entry>} & {lbu(~K, ~V, ~cmp, up, es, bst) == OR.orm(M.Entry, S.last(M.Entry, xa), bst) : Maybe<&2, M.Entry>}))>>: 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 684 def start_fal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lw: M.Bound, +es: List<&2, M.Entry>) -> {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>, Maybe<&2, K>, z => S.key_m(K, V, z), S.head(M.Entry, es), fal(~K, ~V, ~cmp, M.Unbounded{}, es), Equal.sym(Maybe<&2, M.Entry>, fal(~K, ~V, ~cmp, M.Unbounded{}, es), S.head(M.Entry, es), fal_u(~K, ~V, ~cmp, es))) 688 case M.Inclusive{+x}: 689 cong(Maybe<&2, M.Entry>, 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>, 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>, 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>, 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 693 def start_lbu(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +up: M.Bound, +es: List<&2, M.Entry>) -> {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>, Maybe<&2, K>, z => S.key_m(K, V, z), S.last(M.Entry, es), lbu(~K, ~V, ~cmp, M.Unbounded{}, es, None{}), Equal.sym(Maybe<&2, M.Entry>, lbu(~K, ~V, ~cmp, M.Unbounded{}, es, None{}), S.last(M.Entry, es), Equal.trans(Maybe<&2, M.Entry>, lbu(~K, ~V, ~cmp, M.Unbounded{}, es, None{}), OR.orm(M.Entry, S.last(M.Entry, es), None{}), S.last(M.Entry, es), lbu_u(~K, ~V, ~cmp, es, None{}), OR.orm_none(M.Entry, S.last(M.Entry, es))))) 697 case M.Inclusive{+y}: 698 cong(Maybe<&2, M.Entry>, 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>, 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>, 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>, 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{})))