1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/order.bend as O
4	import ../../../spec/lib/common.bend as SC
5	import ../../../spec/containers/balanced_search_tree/main.bend as S
6	import ../../../src/containers/balanced_search_tree.bend as M
7	import ./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	
16	def 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	
25	def 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	
34	def 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	
47	def 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
51	def 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
57	def 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
65	def 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
73	def 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	
81	def 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	
90	def 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	
99	def 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	
106	def 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	
113	def 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	
120	def 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	
129	def 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	
136	def 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	
145	def 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
153	def 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
162	def 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	
167	def 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	
174	def 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	
181	def 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	
190	def 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	
197	def 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	
205	def 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)
214	def 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	
221	def 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	
227	def 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	  {==}