1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../lib/order.bend as O
6	import ../../../spec/lib/common.bend as SC
7	import ../../../spec/containers/binary_heap.bend as S
8	import ./idx.bend as IX
9	
10	# The slot list of an array heap, and heap order on it.
11	#
12	# Heap order is stated over CHILD indices -- "every j in [1, n) is not smaller
13	# than the value at par(j)" -- so the predicate never divides an index it does
14	# not have to, and every fact about it is pointwise: `ho_get` reads one pair
15	# out of the conjunction and `ho_put` builds the conjunction from a function
16	# that proves one pair at a time. Everything the sift proofs do is then a case
17	# analysis on a single index, never an induction over a range.
18	
19	def unwrap(~A: Data, m: Maybe<&2, Maybe<&2, A>>) -> Maybe<&2, A>:
20	  match m:
21	    case None{}:
22	      None{}
23	    case Some{s}:
24	      s
25	
26	def slot(~A: Data, ss: List<&2, Maybe<&2, A>>, +j: Nat) -> Maybe<&2, A>:
27	  unwrap(~A, SC.nth(Maybe<&2, A>, ss, j))
28	
29	# Order between two slots; vacuously true when a slot is empty (the layout
30	# invariant is what says the slots of interest are occupied).
31	def mle(~A: Data, ~cmp: A -> A -> Cmp, a: Maybe<&2, A>, b: Maybe<&2, A>) -> Bool:
32	  match a b:
33	    case Some{x} Some{y}:
34	      S.le(~A, ~cmp, x, y)
35	    case _ _:
36	      True{}
37	
38	def pair_ok(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, j: Nat) -> Bool:
39	  match j:
40	    case 0n:
41	      True{}
42	    case 1n+ +m:
43	      mle(~A, ~cmp, slot(~A, ss, IX.par(1n+m)), slot(~A, ss, 1n+m))
44	
45	# Heap order over the children 0 .. k-1 (index 0 has no parent condition).
46	def ho_upto(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat) -> Bool:
47	  match k:
48	    case 0n:
49	      True{}
50	    case 1n+ +m:
51	      Bool.and(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m))
52	
53	# Every slot of [0, k) is occupied.
54	def lay(~A: Data, +ss: List<&2, Maybe<&2, A>>, k: Nat) -> Bool:
55	  match k:
56	    case 0n:
57	      True{}
58	    case 1n+ +m:
59	      Bool.and(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m))
60	
61	# ---- reading one pair out of the conjunction ----
62	
63	def ho_get_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +j: Nat, +e: {Nat.is_eq(j, m) == True{} : Bool}, +hp: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
64	  L.subst(Nat, z => {pair_ok(~A, ~cmp, ss, z) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, e)), hp)
65	
66	def ho_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +j: Nat, +h: {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
67	  match k b:
68	    case 0n _:
69	      Empty.absurd({pair_ok(~A, ~cmp, ss, j) == True{} : Bool}, N.lt_zero_absurd(j, hj))
70	    case 1n+ +m True{}:
71	      ho_get_eq(~A, ~cmp, ss, m, j, eb, L.and_left(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m), h))
72	    case 1n+ +m False{}:
73	      ho_get(~A, ~cmp, ss, m, j, L.and_right(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
74	
75	def ho_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +j: Nat, +h: {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
76	  ho_get(~A, ~cmp, ss, k, j, h, hj, Nat.is_eq(j, N.pred(k)), {==})
77	
78	# ---- updating one slot ----
79	
80	def slot_same(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +v: Maybe<&2, A>, +hi: {Nat.is_lt(i, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {slot(~A, SC.update(Maybe<&2, A>, ss, i, v), i) == v : Maybe<&2, A>}:
81	  %Equal.sym(Maybe<&2, Maybe<&2, A>>, SC.nth(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, v), i), Some{v}, LL.nth_update_same(Maybe<&2, A>, ss, i, v, hi)) : {unwrap(~A, _) == v : Maybe<&2, A>}
82	  {==}
83	
84	def slot_other(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +j: Nat, +v: Maybe<&2, A>, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {slot(~A, SC.update(Maybe<&2, A>, ss, i, v), j) == slot(~A, ss, j) : Maybe<&2, A>}:
85	  Equal.cong(Maybe<&2, Maybe<&2, A>>, Maybe<&2, A>, m => unwrap(~A, m), SC.nth(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, v), j), SC.nth(Maybe<&2, A>, ss, j), LL.nth_update_other(Maybe<&2, A>, ss, i, j, v, ne))
86	
87	def flip_eq(c: Cmp, +h: {Cmp.is_eq(c) == False{} : Bool}) -> {Cmp.is_eq(O.flipc(c)) == False{} : Bool}:
88	  match c:
89	    case LT{}:
90	      {==}
91	    case EQ{}:
92	      Empty.absurd({Cmp.is_eq(O.flipc(EQ{})) == False{} : Bool}, L.true_false(h))
93	    case GT{}:
94	      {==}
95	
96	def ne_sym(+a: Nat, +b: Nat, +h: {Nat.is_eq(b, a) == False{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
97	  %Equal.sym(Cmp, Nat.cmp(a, b), O.flipc(Nat.cmp(b, a)), O.nat_flip(b, a)) : {Cmp.is_eq(_) == False{} : Bool}
98	  flip_eq(Nat.cmp(b, a), h)
99	
100	# ---- mle ----
101	
102	def mle_some(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +y: A, +h: {mle(~A, ~cmp, Some{x}, Some{y}) == True{} : Bool}) -> {S.le(~A, ~cmp, x, y) == True{} : Bool}:
103	  h
104	
105	def mle_mk(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +y: A, +h: {S.le(~A, ~cmp, x, y) == True{} : Bool}) -> {mle(~A, ~cmp, Some{x}, Some{y}) == True{} : Bool}:
106	  h
107	
108	def mle_none_l(~A: Data, ~cmp: A -> A -> Cmp, +b: Maybe<&2, A>) -> {mle(~A, ~cmp, None{}, b) == True{} : Bool}:
109	  match b:
110	    case None{}:
111	      {==}
112	    case Some{y}:
113	      {==}
114	
115	def mle_none_r(~A: Data, ~cmp: A -> A -> Cmp, +a: Maybe<&2, A>) -> {mle(~A, ~cmp, a, None{}) == True{} : Bool}:
116	  match a:
117	    case None{}:
118	      {==}
119	    case Some{x}:
120	      {==}
121	
122	# transitivity through an OCCUPIED middle slot (with an empty middle there is
123	# nothing to conclude: `mle` is vacuous there)
124	def mle_trans(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), a: Maybe<&2, A>, +y: A, c: Maybe<&2, A>, +hab: {mle(~A, ~cmp, a, Some{y}) == True{} : Bool}, +hbc: {mle(~A, ~cmp, Some{y}, c) == True{} : Bool}) -> {mle(~A, ~cmp, a, c) == True{} : Bool}:
125	  match a c:
126	    case Some{+x} Some{+z}:
127	      O.trans(~A, ~cmp, o, x, y, z, hab, hbc)
128	    case Some{x} None{}:
129	      {==}
130	    case None{} Some{z}:
131	      {==}
132	    case None{} None{}:
133	      {==}
134	
135	
136	# ---- the layout, pointwise ----
137	
138	def lay_get_eq(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +j: Nat, +e: {Nat.is_eq(j, m) == True{} : Bool}, +hp: {Maybe.is_some(&2, A, slot(~A, ss, m)) == True{} : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:
139	  L.subst(Nat, z => {Maybe.is_some(&2, A, slot(~A, ss, z)) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, e)), hp)
140	
141	def lay_get(~A: Data, +ss: List<&2, Maybe<&2, A>>, k: Nat, +j: Nat, +h: {lay(~A, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:
142	  match k b:
143	    case 0n _:
144	      Empty.absurd({Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}, N.lt_zero_absurd(j, hj))
145	    case 1n+ +m True{}:
146	      lay_get_eq(~A, ss, m, j, eb, L.and_left(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m), h))
147	    case 1n+ +m False{}:
148	      lay_get(~A, ss, m, j, L.and_right(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
149	
150	def lay_at(~A: Data, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +j: Nat, +h: {lay(~A, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:
151	  lay_get(~A, ss, k, j, h, hj, Nat.is_eq(j, N.pred(k)), {==})
152	
153	# An occupied slot, as a value.
154	def slot_some(~A: Data, m: Maybe<&2, A>, +h: {Maybe.is_some(&2, A, m) == True{} : Bool}) -> Sigma<&1, &1, A, v => {m == Some{v} : Maybe<&2, A>}>:
155	  match m:
156	    case None{}:
157	      Empty.absurd(Sigma<&1, &1, A, v => {None{} == Some{v} : Maybe<&2, A>}>, L.false_true(h))
158	    case Some{+v}:
159	      (v, {==})
160	
161	# ---- nth of a slot inside the list ----
162	
163	def nth_slot(~A: Data, +ss: List<&2, Maybe<&2, A>>, +j: Nat, +hj: {Nat.is_lt(j, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {SC.nth(Maybe<&2, A>, ss, j) == Some{slot(~A, ss, j)} : Maybe<&2, Maybe<&2, A>>}:
164	  match ss j:
165	    case Nil{} _:
166	      Empty.absurd({None{} == Some{slot(~A, Nil{}, j)} : Maybe<&2, Maybe<&2, A>>}, N.lt_zero_absurd(j, hj))
167	    case Con{x, r} 0n:
168	      {==}
169	    case Con{x, +r} 1n+k:
170	      nth_slot(~A, r, k, hj)
171	
172	# ---- heap order with one index excluded ----
173	#
174	# `ho_exc(ss, k, i)` is "every pair below k except the one into i holds". It
175	# is a Bool, not a function over indices: a proof term of function type could
176	# not be used twice, and a step needs its invariant more than once.
177	
178	def pair_skip(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat) -> Bool:
179	  Bool.pick(Bool, Nat.is_eq(m, i), True{}, pair_ok(~A, ~cmp, ss, m))
180	
181	def ho_exc(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat) -> Bool:
182	  match k:
183	    case 0n:
184	      True{}
185	    case 1n+ +m:
186	      Bool.and(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i))
187	
188	def skip_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hne: {Nat.is_eq(m, i) == False{} : Bool}, +h: {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:
189	  L.subst(Bool, b => {Bool.pick(Bool, b, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}, Nat.is_eq(m, i), False{}, hne, h)
190	
191	def skip_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {Nat.is_eq(m, i) == True{} : Bool}) -> {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}:
192	  %Equal.sym(Bool, Nat.is_eq(m, i), True{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
193	  {==}
194	
195	def skip_ne(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {Nat.is_eq(m, i) == False{} : Bool}, +h: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}:
196	  %Equal.sym(Bool, Nat.is_eq(m, i), False{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
197	  h
198	
199	def exc_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +j: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_skip(~A, ~cmp, ss, j, i) == True{} : Bool}:
200	  match k b:
201	    case 0n _:
202	      Empty.absurd({pair_skip(~A, ~cmp, ss, j, i) == True{} : Bool}, N.lt_zero_absurd(j, hj))
203	    case 1n+ +m True{}:
204	      L.subst(Nat, z => {pair_skip(~A, ~cmp, ss, z, i) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, eb)), L.and_left(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h))
205	    case 1n+ +m False{}:
206	      exc_get(~A, ~cmp, ss, m, i, j, L.and_right(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
207	
208	# one pair out of `ho_exc`
209	def exc_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +i: Nat, +j: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, +hne: {Nat.is_eq(j, i) == False{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
210	  skip_at(~A, ~cmp, ss, j, i, hne, exc_get(~A, ~cmp, ss, k, i, j, h, hj, Nat.is_eq(j, N.pred(k)), {==}))
211	
212	def pair_of_skip(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hi: {pair_ok(~A, ~cmp, ss, i) == True{} : Bool}, +h: {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, i) == b : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:
213	  match b:
214	    case True{}:
215	      ho_get_eq(~A, ~cmp, ss, i, m, eb, hi)
216	    case False{}:
217	      skip_at(~A, ~cmp, ss, m, i, eb, h)
218	
219	# `ho_upto` follows from `ho_exc` plus the excluded pair
220	def ho_of_exc(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hi: {pair_ok(~A, ~cmp, ss, i) == True{} : Bool}) -> {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}:
221	  match k:
222	    case 0n:
223	      {==}
224	    case 1n+ +m:
225	      L.and_intro(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m),
226	        pair_of_skip(~A, ~cmp, ss, m, i, hi, L.and_left(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), Nat.is_eq(m, i), {==}),
227	        ho_of_exc(~A, ~cmp, ss, m, i, L.and_right(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), hi))
228	
229	# ---- the children of one index ----
230	
231	def kid_le(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat) -> Bool:
232	  Bool.pick(Bool, Nat.is_lt(c, n), mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{})
233	
234	def kids_le(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +i: Nat) -> Bool:
235	  Bool.and(kid_le(~A, ~cmp, ss, n, u, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, u, IX.kidr(i)))
236	
237	def kid_le_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +hc: {Nat.is_lt(c, n) == True{} : Bool}, +h: {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}) -> {mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)) == True{} : Bool}:
238	  L.subst(Bool, b => {Bool.pick(Bool, b, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}, Nat.is_lt(c, n), True{}, hc, h)
239	
240	def kid_le_in(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +eb: {Nat.is_lt(c, n) == True{} : Bool}, +h: {mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)) == True{} : Bool}) -> {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}:
241	  %Equal.sym(Bool, Nat.is_lt(c, n), True{}, eb) : {Bool.pick(Bool, _, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}
242	  h
243	
244	def kid_le_out(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +eb: {Nat.is_lt(c, n) == False{} : Bool}) -> {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}:
245	  %Equal.sym(Bool, Nat.is_lt(c, n), False{}, eb) : {Bool.pick(Bool, _, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}
246	  {==}
247	
248	# ---- heap order with the two pairs below one index excluded ----
249	#
250	# This is what a sift-DOWN carries: the hole may be larger than its children,
251	# so the two pairs whose parent is the hole are the ones left out.
252	
253	def kid_of(+m: Nat, +i: Nat) -> Bool:
254	  Bool.or(Nat.is_eq(m, IX.kidl(i)), Nat.is_eq(m, IX.kidr(i)))
255	
256	def pair_skip2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat) -> Bool:
257	  Bool.pick(Bool, kid_of(m, i), True{}, pair_ok(~A, ~cmp, ss, m))
258	
259	def ho_exc2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat) -> Bool:
260	  match k:
261	    case 0n:
262	      True{}
263	    case 1n+ +m:
264	      Bool.and(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i))
265	
266	def skip2_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {kid_of(m, i) == True{} : Bool}) -> {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}:
267	  %Equal.sym(Bool, kid_of(m, i), True{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
268	  {==}
269	
270	def skip2_ne(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {kid_of(m, i) == False{} : Bool}, +h: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}:
271	  %Equal.sym(Bool, kid_of(m, i), False{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}
272	  h
273	
274	def skip2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hne: {kid_of(m, i) == False{} : Bool}, +h: {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:
275	  L.subst(Bool, b => {Bool.pick(Bool, b, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}, kid_of(m, i), False{}, hne, h)
276	
277	def exc2_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +j: Nat, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_skip2(~A, ~cmp, ss, j, i) == True{} : Bool}:
278	  match k b:
279	    case 0n _:
280	      Empty.absurd({pair_skip2(~A, ~cmp, ss, j, i) == True{} : Bool}, N.lt_zero_absurd(j, hj))
281	    case 1n+ +m True{}:
282	      L.subst(Nat, z => {pair_skip2(~A, ~cmp, ss, z, i) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, eb)), L.and_left(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h))
283	    case 1n+ +m False{}:
284	      exc2_get(~A, ~cmp, ss, m, i, j, L.and_right(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})
285	
286	def exc2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +i: Nat, +j: Nat, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, +hne: {kid_of(j, i) == False{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
287	  skip2_at(~A, ~cmp, ss, j, i, hne, exc2_get(~A, ~cmp, ss, k, i, j, h, hj, Nat.is_eq(j, N.pred(k)), {==}))
288	
289	def pair_of_kid(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, c: Nat, +epc: {IX.par(c) == i : Nat}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}, +h: {mle(~A, ~cmp, slot(~A, ss, i), slot(~A, ss, c)) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, c) == True{} : Bool}:
290	  match c:
291	    case 0n:
292	      Empty.absurd({pair_ok(~A, ~cmp, ss, 0n) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), hcpos, {==}))
293	    case 1n+k:
294	      %Equal.sym(Nat, IX.par(1n+k), i, epc) : {mle(~A, ~cmp, slot(~A, ss, _), slot(~A, ss, 1n+k)) == True{} : Bool}
295	      h
296	
297	# one excluded pair, from "the hole is not larger than that child"
298	def pair_kid_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, +j: Nat, +c: Nat, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +ej: {Nat.is_eq(j, c) == True{} : Bool}, +epc: {IX.par(c) == i : Nat}, +hc: {kid_le(~A, ~cmp, ss, n, i, c) == True{} : Bool}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
299	  L.subst(Nat, z => {pair_ok(~A, ~cmp, ss, z) == True{} : Bool}, c, j, Equal.sym(Nat, j, c, N.eq_from_is_eq(j, c, ej)),
300	    pair_of_kid(~A, ~cmp, ss, n, i, c, epc, hcpos, kid_le_at(~A, ~cmp, ss, n, i, c, L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, j, c, N.eq_from_is_eq(j, c, ej), hjn), hc)))
301	
302	def or_false(a: Bool, b: Bool, +ea: {a == False{} : Bool}, +eb: {b == False{} : Bool}) -> {Bool.or(a, b) == False{} : Bool}:
303	  %Equal.sym(Bool, a, False{}, ea) : {Bool.or(_, b) == False{} : Bool}
304	  eb
305	
306	# `ho_upto` from `ho_exc2` plus "the hole is not larger than its children"
307	def ho_of_exc2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +k: Nat, +i: Nat, +j: Nat, +hjk: {Nat.is_lt(j, k) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hkids: {kids_le(~A, ~cmp, ss, n, i, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, IX.kidl(i)) == b : Bool}, c: Bool, +ec: {Nat.is_eq(j, IX.kidr(i)) == c : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:
308	  match b c:
309	    case True{} _:
310	      pair_kid_at(~A, ~cmp, ss, n, i, j, IX.kidl(i), hjn, eb, IX.par_kidl(i), L.and_left(kid_le(~A, ~cmp, ss, n, i, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, i, IX.kidr(i)), hkids), IX.kidl_pos1(i))
311	    case False{} True{}:
312	      pair_kid_at(~A, ~cmp, ss, n, i, j, IX.kidr(i), hjn, ec, IX.par_kidr(i), L.and_right(kid_le(~A, ~cmp, ss, n, i, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, i, IX.kidr(i)), hkids), IX.kidr_pos1(i))
313	    case False{} False{}:
314	      exc2_at(~A, ~cmp, ss, k, i, j, h, hjk, or_false(Nat.is_eq(j, IX.kidl(i)), Nat.is_eq(j, IX.kidr(i)), eb, ec))
315	
316	def ho_of_exc2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, k: Nat, +i: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hkids: {kids_le(~A, ~cmp, ss, n, i, i) == True{} : Bool}) -> {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}:
317	  match k:
318	    case 0n:
319	      {==}
320	    case 1n+ +m:
321	      L.and_intro(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m),
322	        ho_of_exc2_at(~A, ~cmp, ss, n, 1n+m, i, m, N.lt_succ(m), N.lt_le_trans(m, 1n+m, n, N.lt_succ(m), hk), h, hkids, Nat.is_eq(m, IX.kidl(i)), {==}, Nat.is_eq(m, IX.kidr(i)), {==}),
323	        ho_of_exc2(~A, ~cmp, ss, n, m, i, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), L.and_right(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h), hkids))