proofs/containers/balanced_search_tree/ord.bend
bend-collections-laws-containers@1.0.0.0 · 233 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
6import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
8
9# Order facts over entry lists for a lawful comparator (O.Order): the keys
10# of a sorted list split around each entry, and the specification's lookup
11# of a key decided by one comparison. (source: tools/generators/tm_hand/ord.src)
12
13
14# ---- strict order ----
15
16def lt_le(+c: Cmp, +h: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_le(c) == True{} : Bool}:
17 match c:
18 case LT{}:
19 {==}
20 case EQ{}:
21 Empty.absurd({Cmp.is_le(EQ{}) == True{} : Bool}, L.false_true(h))
22 case GT{}:
23 Empty.absurd({Cmp.is_le(GT{}) == True{} : Bool}, L.false_true(h))
24
25def lt_flip(+c: Cmp, +h: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_lt(O.flipc(c)) == False{} : Bool}:
26 match c:
27 case LT{}:
28 {==}
29 case EQ{}:
30 Empty.absurd({Cmp.is_lt(O.flipc(EQ{})) == False{} : Bool}, L.false_true(h))
31 case GT{}:
32 Empty.absurd({Cmp.is_lt(O.flipc(GT{})) == False{} : Bool}, L.false_true(h))
33
34def slt_c(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +c: K, +hab: {Cmp.is_lt(cmp(a, b)) == True{} : Bool}, +hbc: {Cmp.is_lt(cmp(b, c)) == True{} : Bool}, +x: Cmp, +hx: {cmp(a, c) == x : Cmp}) -> {Cmp.is_lt(x) == True{} : Bool}:
35 match x:
36 case LT{}:
37 {==}
38 case GT{}:
39 +le = O.trans(~K, ~cmp, o, a, b, c, lt_le(cmp(a, b), hab), lt_le(cmp(b, c), hbc))
40 Empty.absurd({Cmp.is_lt(GT{}) == True{} : Bool}, L.false_true(L.subst(Cmp, z => {Cmp.is_le(z) == True{} : Bool}, cmp(a, c), GT{}, hx, le)))
41 case EQ{}:
42 +e = O.antisym(~K, ~cmp, o, a, c, hx)
43 +hba = L.subst(K, z => {Cmp.is_lt(cmp(b, z)) == True{} : Bool}, c, a, Equal.sym(K, a, c, e), hbc)
44 +hf = L.subst(Cmp, z => {Cmp.is_lt(z) == True{} : Bool}, cmp(b, a), O.flipc(cmp(a, b)), O.flip(~K, ~cmp, o, a, b), hba)
45 Empty.absurd({Cmp.is_lt(EQ{}) == True{} : Bool}, L.true_not_false(Cmp.is_lt(O.flipc(cmp(a, b))), hf, lt_flip(cmp(a, b), hab)))
46
47def slt_trans(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +c: K, +hab: {Cmp.is_lt(cmp(a, b)) == True{} : Bool}, +hbc: {Cmp.is_lt(cmp(b, c)) == True{} : Bool}) -> {Cmp.is_lt(cmp(a, c)) == True{} : Bool}:
48 slt_c(~K, ~cmp, ~o, a, b, c, hab, hbc, cmp(a, c), {==})
49
50# a > b as b < a
51def gt_lt(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +h: {cmp(a, b) == GT{} : Cmp}) -> {Cmp.is_lt(cmp(b, a)) == True{} : Bool}:
52 %Equal.sym(Cmp, cmp(b, a), O.flipc(cmp(a, b)), O.flip(~K, ~cmp, o, a, b)) : {Cmp.is_lt(_) == True{} : Bool}
53 %Equal.sym(Cmp, cmp(a, b), GT{}, h) : {Cmp.is_lt(O.flipc(_)) == True{} : Bool}
54 {==}
55
56# a < b gives cmp(b, a) = GT
57def lt_gt(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +h: {Cmp.is_lt(cmp(a, b)) == True{} : Bool}) -> {cmp(b, a) == GT{} : Cmp}:
58 %Equal.sym(Cmp, cmp(b, a), O.flipc(cmp(a, b)), O.flip(~K, ~cmp, o, a, b)) : {_ == GT{} : Cmp}
59 %Equal.sym(Cmp, cmp(a, b), LT{}, O.lt_is(cmp(a, b), h)) : {O.flipc(_) == GT{} : Cmp}
60 {==}
61
62# ---- all keys above / below a key ----
63
64# k below every key
65def gtall(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> Bool:
66 match es:
67 case Nil{}:
68 True{}
69 case Con{+e, t}:
70 Bool.and(Cmp.is_lt(cmp(k, S.key(K, V, e))), gtall(~K, ~V, ~cmp, k, t))
71
72# k above every key
73def ltall(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> Bool:
74 match es:
75 case Nil{}:
76 True{}
77 case Con{+e, t}:
78 Bool.and(Cmp.is_lt(cmp(S.key(K, V, e), k)), ltall(~K, ~V, ~cmp, k, t))
79
80
81def gtall_mono(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +hab: {Cmp.is_lt(cmp(a, b)) == True{} : Bool}, +es: List<&2, M.Entry<K, V>>, +h: {gtall(~K, ~V, ~cmp, b, es) == True{} : Bool}) -> {gtall(~K, ~V, ~cmp, a, es) == True{} : Bool}:
82 match es:
83 case Nil{}:
84 {==}
85 case Con{+e, +t}:
86 +h1 = L.and_left(Cmp.is_lt(cmp(b, S.key(K, V, e))), gtall(~K, ~V, ~cmp, b, t), h)
87 +h2 = L.and_right(Cmp.is_lt(cmp(b, S.key(K, V, e))), gtall(~K, ~V, ~cmp, b, t), h)
88 L.and_intro(Cmp.is_lt(cmp(a, S.key(K, V, e))), gtall(~K, ~V, ~cmp, a, t), slt_trans(~K, ~cmp, ~o, a, b, S.key(K, V, e), hab, h1), gtall_mono(~K, ~V, ~cmp, ~o, a, b, hab, t, h2))
89
90def ltall_mono(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +a: K, +b: K, +hab: {Cmp.is_lt(cmp(a, b)) == True{} : Bool}, +es: List<&2, M.Entry<K, V>>, +h: {ltall(~K, ~V, ~cmp, a, es) == True{} : Bool}) -> {ltall(~K, ~V, ~cmp, b, es) == True{} : Bool}:
91 match es:
92 case Nil{}:
93 {==}
94 case Con{+e, +t}:
95 +h1 = L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), a)), ltall(~K, ~V, ~cmp, a, t), h)
96 +h2 = L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), a)), ltall(~K, ~V, ~cmp, a, t), h)
97 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), b)), ltall(~K, ~V, ~cmp, b, t), slt_trans(~K, ~cmp, ~o, S.key(K, V, e), a, b, h1, hab), ltall_mono(~K, ~V, ~cmp, ~o, a, b, hab, t, h2))
98
99def gtall_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +h: {gtall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}) -> {gtall(~K, ~V, ~cmp, k, ys) == True{} : Bool}:
100 match xs:
101 case Nil{}:
102 h
103 case Con{+e, +t}:
104 gtall_r(~K, ~V, ~cmp, k, t, ys, L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, e))), gtall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), h))
105
106def ltall_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +h: {ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}) -> {ltall(~K, ~V, ~cmp, k, ys) == True{} : Bool}:
107 match xs:
108 case Nil{}:
109 h
110 case Con{+e, +t}:
111 ltall_r(~K, ~V, ~cmp, k, t, ys, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), h))
112
113def gtall_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +h: {gtall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}) -> {gtall(~K, ~V, ~cmp, k, xs) == True{} : Bool}:
114 match xs:
115 case Nil{}:
116 {==}
117 case Con{+e, +t}:
118 L.and_intro(Cmp.is_lt(cmp(k, S.key(K, V, e))), gtall(~K, ~V, ~cmp, k, t), L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), gtall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), h), gtall_l(~K, ~V, ~cmp, k, t, ys, L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, e))), gtall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), h)))
119
120def ltall_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +h: {ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}) -> {ltall(~K, ~V, ~cmp, k, xs) == True{} : Bool}:
121 match xs:
122 case Nil{}:
123 {==}
124 case Con{+e, +t}:
125 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), k)), ltall(~K, ~V, ~cmp, k, t), L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), h), ltall_l(~K, ~V, ~cmp, k, t, ys, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), h)))
126
127# ---- sorted lists ----
128
129def ord_tail(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, t) == True{} : Bool}:
130 match t:
131 case Nil{}:
132 {==}
133 case Con{+e2, +u}:
134 L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, u}), h)
135
136def ord_gt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +t: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +h: {ST.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}) -> {gtall(~K, ~V, ~cmp, S.key(K, V, e), t) == True{} : Bool}:
137 match t:
138 case Nil{}:
139 {==}
140 case Con{+e2, +u}:
141 +h1 = L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, u}), h)
142 +h2 = L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, u}), h)
143 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), gtall(~K, ~V, ~cmp, S.key(K, V, e), u), h1, gtall_mono(~K, ~V, ~cmp, ~o, S.key(K, V, e), S.key(K, V, e2), h1, u, ord_gt(~K, ~V, ~cmp, ~o, u, e2, h2)))
144
145def ord_app_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, ys) == True{} : Bool}:
146 match xs:
147 case Nil{}:
148 h
149 case Con{+e, +t}:
150 ord_app_r(~K, ~V, ~cmp, t, ys, ord_tail(~K, ~V, ~cmp, e, SC.append(M.Entry<K, V>, t, ys), h))
151
152# the entries before e are below it
153def ord_mid_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}) -> {ltall(~K, ~V, ~cmp, S.key(K, V, e), xs) == True{} : Bool}:
154 match xs:
155 case Nil{}:
156 {==}
157 case Con{+a, +t}:
158 +g = gtall_r(~K, ~V, ~cmp, S.key(K, V, a), t, Con{e, ys}, ord_gt(~K, ~V, ~cmp, ~o, SC.append(M.Entry<K, V>, t, Con{e, ys}), a, h))
159 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))), ltall(~K, ~V, ~cmp, S.key(K, V, e), t), L.and_left(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))), gtall(~K, ~V, ~cmp, S.key(K, V, a), ys), g), ord_mid_l(~K, ~V, ~cmp, ~o, t, e, ys, ord_tail(~K, ~V, ~cmp, a, SC.append(M.Entry<K, V>, t, Con{e, ys}), h)))
160
161# the entries after e are above it
162def ord_mid_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}) -> {gtall(~K, ~V, ~cmp, S.key(K, V, e), ys) == True{} : Bool}:
163 ord_gt(~K, ~V, ~cmp, ~o, ys, e, ord_app_r(~K, ~V, ~cmp, xs, Con{e, ys}, h))
164
165# ---- lookup ----
166
167def orm(-X: Data, m: Maybe<&2, X>, n: Maybe<&2, X>) -> Maybe<&2, X>:
168 match m:
169 case None{}:
170 n
171 case Some{x}:
172 Some{x}
173
174def orm_none(-X: Data, +m: Maybe<&2, X>) -> {orm(X, m, None{}) == m : Maybe<&2, X>}:
175 match m:
176 case None{}:
177 {==}
178 case Some{x}:
179 {==}
180
181def find_app_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +b: Bool, +hb: {S.is_eq(cmp(k, S.key(K, V, e))) == b : Bool}, +ih: {S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)) == orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, t), S.find_e(~K, ~V, ~cmp, k, ys)) : Maybe<&2, M.Entry<K, V>>}) -> {S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, Con{e, t}, ys)) == orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, Con{e, t}), S.find_e(~K, ~V, ~cmp, k, ys)) : Maybe<&2, M.Entry<K, V>>}:
182 match b:
183 case True{}:
184 %Equal.sym(Bool, S.is_eq(cmp(k, S.key(K, V, e))), True{}, hb) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys))) == orm(M.Entry<K, V>, S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.find_e(~K, ~V, ~cmp, k, t)), S.find_e(~K, ~V, ~cmp, k, ys)) : Maybe<&2, M.Entry<K, V>>}
185 {==}
186 case False{}:
187 %Equal.sym(Bool, S.is_eq(cmp(k, S.key(K, V, e))), False{}, hb) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys))) == orm(M.Entry<K, V>, S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.find_e(~K, ~V, ~cmp, k, t)), S.find_e(~K, ~V, ~cmp, k, ys)) : Maybe<&2, M.Entry<K, V>>}
188 ih
189
190def find_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>) -> {S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.find_e(~K, ~V, ~cmp, k, ys)) : Maybe<&2, M.Entry<K, V>>}:
191 match xs:
192 case Nil{}:
193 {==}
194 case Con{+e, +t}:
195 find_app_c(~K, ~V, ~cmp, k, e, t, ys, S.is_eq(cmp(k, S.key(K, V, e))), {==}, find_app(~K, ~V, ~cmp, k, t, ys))
196
197def gt_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +es: List<&2, M.Entry<K, V>>, +h: {gtall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}:
198 match es:
199 case Nil{}:
200 {==}
201 case Con{+e, +t}:
202 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, O.lt_is(cmp(k, S.key(K, V, e)), L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), gtall(~K, ~V, ~cmp, k, t), h))) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry<K, V>>}
203 gt_none(~K, ~V, ~cmp, k, t, L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, e))), gtall(~K, ~V, ~cmp, k, t), h))
204
205def lt_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +es: List<&2, M.Entry<K, V>>, +h: {ltall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}:
206 match es:
207 case Nil{}:
208 {==}
209 case Con{+e, +t}:
210 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, lt_gt(~K, ~cmp, ~o, S.key(K, V, e), k, L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), ltall(~K, ~V, ~cmp, k, t), h))) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry<K, V>>}
211 lt_none(~K, ~V, ~cmp, ~o, k, t, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), ltall(~K, ~V, ~cmp, k, t), h))
212
213# the lookup of k around an entry e of a sorted list, by cmp(k, e.key)
214def find_mid_lt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}, +hc: {cmp(k, S.key(K, V, e)) == LT{} : Cmp}) -> {S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == S.find_e(~K, ~V, ~cmp, k, xs) : Maybe<&2, M.Entry<K, V>>}:
215 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, Con{e, ys})), orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.find_e(~K, ~V, ~cmp, k, Con{e, ys})), find_app(~K, ~V, ~cmp, k, xs, Con{e, ys})) : {_ == S.find_e(~K, ~V, ~cmp, k, xs) : Maybe<&2, M.Entry<K, V>>}
216 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, hc) : {orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, ys))) == S.find_e(~K, ~V, ~cmp, k, xs) : Maybe<&2, M.Entry<K, V>>}
217 +hlt = L.subst(Cmp, z => {Cmp.is_lt(z) == True{} : Bool}, LT{}, cmp(k, S.key(K, V, e)), Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, hc), {==})
218 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, ys), None{}, gt_none(~K, ~V, ~cmp, k, ys, gtall_mono(~K, ~V, ~cmp, ~o, k, S.key(K, V, e), hlt, ys, ord_mid_r(~K, ~V, ~cmp, ~o, xs, e, ys, h)))) : {orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), _) == S.find_e(~K, ~V, ~cmp, k, xs) : Maybe<&2, M.Entry<K, V>>}
219 orm_none(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs))
220
221def find_mid_gt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}, +hc: {cmp(k, S.key(K, V, e)) == GT{} : Cmp}) -> {S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == S.find_e(~K, ~V, ~cmp, k, ys) : Maybe<&2, M.Entry<K, V>>}:
222 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, Con{e, ys})), orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.find_e(~K, ~V, ~cmp, k, Con{e, ys})), find_app(~K, ~V, ~cmp, k, xs, Con{e, ys})) : {_ == S.find_e(~K, ~V, ~cmp, k, ys) : Maybe<&2, M.Entry<K, V>>}
223 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, hc) : {orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, ys))) == S.find_e(~K, ~V, ~cmp, k, ys) : Maybe<&2, M.Entry<K, V>>}
224 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, xs), None{}, lt_none(~K, ~V, ~cmp, ~o, k, xs, ltall_mono(~K, ~V, ~cmp, ~o, S.key(K, V, e), k, gt_lt(~K, ~cmp, ~o, k, S.key(K, V, e), hc), xs, ord_mid_l(~K, ~V, ~cmp, ~o, xs, e, ys, h)))) : {orm(M.Entry<K, V>, _, S.find_e(~K, ~V, ~cmp, k, ys)) == S.find_e(~K, ~V, ~cmp, k, ys) : Maybe<&2, M.Entry<K, V>>}
225 {==}
226
227def find_mid_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +xs: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +ys: List<&2, M.Entry<K, V>>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == True{} : Bool}, +hc: {cmp(k, S.key(K, V, e)) == EQ{} : Cmp}) -> {S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, Con{e, ys})) == Some{e} : Maybe<&2, M.Entry<K, V>>}:
228 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, Con{e, ys})), orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.find_e(~K, ~V, ~cmp, k, Con{e, ys})), find_app(~K, ~V, ~cmp, k, xs, Con{e, ys})) : {_ == Some{e} : Maybe<&2, M.Entry<K, V>>}
229 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), EQ{}, hc) : {orm(M.Entry<K, V>, S.find_e(~K, ~V, ~cmp, k, xs), S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, ys))) == Some{e} : Maybe<&2, M.Entry<K, V>>}
230 +ek = O.antisym(~K, ~cmp, o, k, S.key(K, V, e), hc)
231 +hl = L.subst(K, z => {ltall(~K, ~V, ~cmp, z, xs) == True{} : Bool}, S.key(K, V, e), k, Equal.sym(K, k, S.key(K, V, e), ek), ord_mid_l(~K, ~V, ~cmp, ~o, xs, e, ys, h))
232 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, xs), None{}, lt_none(~K, ~V, ~cmp, ~o, k, xs, hl)) : {orm(M.Entry<K, V>, _, Some{e}) == Some{e} : Maybe<&2, M.Entry<K, V>>}
233 {==}