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 ../../lib/array.bend as AR
7	import ../../lib/u32.bend as U
8	import ../../../spec/lib/common.bend as SC
9	import ../../../spec/containers/binary_heap.bend as S
10	import ../../../src/containers/binary_heap.bend as H
11	import ./idx.bend as IX
12	import ./u32idx.bend as UX
13	import ./slots.bend as SL
14	import ./vals.bend as V
15	import ./bag.bend as BG
16	import ./multiset.bend as M
17	import ./up.bend as UPS
18	
19	# The sift-down loop, mirrored on the shadow tree.
20	#
21	# The invariant is the mirror image of the sift-up one. With the hole at i and
22	# the sifted value x (the logical array is `UPS.ulog(t, i, x)`):
23	#   D1  every pair holds except the two whose parent is the hole
24	#   D2  the pair INTO the hole holds (its parent is not larger than x)
25	#   D3  the value physically at the hole's parent is not larger than the
26	#       hole's children -- stated on the block, so that it also says the right
27	#       thing at the root, where the hole's "parent" is the stale slot 0
28	# and the loop moves the hole to the smaller child while that child is
29	# smaller than x.
30	
31	type DownS<-A: Data> is Data:
32	  DStp{t: AR.Tree<Maybe<&2, A>>, i: Nat}
33	  DMv{t: AR.Tree<Maybe<&2, A>>, i: Nat, cv: A, ci: Nat}
34	
35	def dreal(~A: Data, s: DownS<A>) -> H.Down<A>:
36	  match s:
37	    case DStp{t, i}:
38	      H.DStop{AR.thaw(Maybe<&2, A>, t), U32.from_nat(i)}
39	    case DMv{t, i, cv, ci}:
40	      H.DMove{AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), cv, U32.from_nat(ci)}
41	
42	# ---- the mirror of `H.down_probe` ----
43	
44	def ddec(~A: Data, t: AR.Tree<Maybe<&2, A>>, +i: Nat, cv: A, ci: Nat, ok: Bool) -> DownS<A>:
45	  match ok:
46	    case True{}:
47	      DStp{t, i}
48	    case False{}:
49	      DMv{t, i, cv, ci}
50	
51	def dcmp(~A: Data, ~cmp: A -> A -> Cmp, t: AR.Tree<Maybe<&2, A>>, +i: Nat, x: A, +cv: A, ci: Nat) -> DownS<A>:
52	  ddec(~A, t, i, cv, ci, S.le(~A, ~cmp, x, cv))
53	
54	def dtwo(~A: Data, ~cmp: A -> A -> Cmp, t: AR.Tree<Maybe<&2, A>>, +i: Nat, x: A, l: Nat, +lv: A, r: Nat, +rv: A, left: Bool) -> DownS<A>:
55	  match left:
56	    case True{}:
57	      dcmp(~A, ~cmp, t, i, x, lv, l)
58	    case False{}:
59	      dcmp(~A, ~cmp, t, i, x, rv, r)
60	
61	def drmb(~A: Data, ~cmp: A -> A -> Cmp, t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, l: Nat, +lv: A, r: Nat, m: Maybe<&2, A>) -> DownS<A>:
62	  match m:
63	    case None{}:
64	      dcmp(~A, ~cmp, t, i, x, lv, l)
65	    case Some{+rv}:
66	      dtwo(~A, ~cmp, t, i, x, l, lv, r, rv, S.le(~A, ~cmp, lv, rv))
67	
68	def dlmb(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +l: Nat, two: Bool, m: Maybe<&2, A>) -> DownS<A>:
69	  match two m:
70	    case _ None{}:
71	      DStp{t, i}
72	    case True{} Some{+lv}:
73	      drmb(~A, ~cmp, t, i, x, l, lv, 1n+l, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+l))
74	    case False{} Some{+lv}:
75	      dcmp(~A, ~cmp, t, i, x, lv, l)
76	
77	def dhas(~A: Data, ~cmp: A -> A -> Cmp, +n: Nat, +i: Nat, +x: A, +t: AR.Tree<Maybe<&2, A>>, +l: Nat, has_left: Bool) -> DownS<A>:
78	  match has_left:
79	    case True{}:
80	      dlmb(~A, ~cmp, t, i, x, l, Nat.is_lt(l, Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), l))
81	    case False{}:
82	      DStp{t, i}
83	
84	def dprobe(~A: Data, ~cmp: A -> A -> Cmp, +n: Nat, +i: Nat, +x: A, +t: AR.Tree<Maybe<&2, A>>) -> DownS<A>:
85	  dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), Nat.is_lt(IX.kidl(i), n))
86	
87	# ---- the bridge ----
88	
89	def double_gt(+v: Nat, +h: {Nat.is_lt(0n, v) == True{} : Bool}) -> {Nat.is_lt(v, Nat.double(v)) == True{} : Bool}:
90	  match v:
91	    case 0n:
92	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_not_false(Nat.is_lt(0n, 0n), h, N.lt_irrefl(0n)))
93	    case 1n+k:
94	      N.le_lt_succ(1n+k, 1n+Nat.double(k), N.lt_succ_le_succ(k, 1n+Nat.double(k), N.le_lt_trans(k, Nat.double(k), 1n+Nat.double(k), IX.double_le(k), N.lt_succ(Nat.double(k)))))
95	
96	def pow2_up(+d: Nat) -> {Nat.is_lt(SC.pow2(d), SC.pow2(1n+d)) == True{} : Bool}:
97	  double_gt(SC.pow2(d), UPS.pow2_pos(d))
98	
99	def double_lt_pow(+i: Nat, +d: Nat, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(Nat.double(i), SC.pow2(1n+d)) == True{} : Bool}:
100	  IX.double_lt(i, SC.pow2(d), hi)
101	
102	def kidl_bridge(+i: Nat, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}) -> {U32.inc(U32.shl(U32.from_nat(i))) == U32.from_nat(IX.kidl(i)) : U32}:
103	  Equal.cong(U32, U32, y => U32.inc(y), U32.shl(U32.from_nat(i)), U32.from_nat(Nat.double(i)),
104	    UX.shl_bridge(i, 1n+d, N.lt_succ_le_succ(d, 32n, hd), N.lt_trans(i, SC.pow2(d), SC.pow2(1n+d), hi, pow2_up(d)), double_lt_pow(i, d, hi)))
105	
106	def ddec_ok(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +cv: A, +ci: Nat, b: Bool) -> {H.down_dec(~A, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), cv, U32.from_nat(ci), b) == dreal(~A, ddec(~A, t, i, cv, ci, b)) : H.Down<A>}:
107	  match b:
108	    case True{}:
109	      {==}
110	    case False{}:
111	      {==}
112	
113	def dcmp_ok(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat) -> {H.down_dec(~A, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), cv, U32.from_nat(ci), S.le(~A, ~cmp, x, cv)) == dreal(~A, dcmp(~A, ~cmp, t, i, x, cv, ci)) : H.Down<A>}:
114	  ddec_ok(~A, t, i, cv, ci, S.le(~A, ~cmp, x, cv))
115	
116	def dtwo_ok(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +l: Nat, +lv: A, +r: Nat, +rv: A, b: Bool) -> {H.down_two(~A, ~cmp, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), x, U32.from_nat(l), lv, U32.from_nat(r), rv, b) == dreal(~A, dtwo(~A, ~cmp, t, i, x, l, lv, r, rv, b)) : H.Down<A>}:
117	  match b:
118	    case True{}:
119	      dcmp_ok(~A, ~cmp, t, i, x, lv, l)
120	    case False{}:
121	      dcmp_ok(~A, ~cmp, t, i, x, rv, r)
122	
123	def drmb_ok(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +l: Nat, +lv: A, +r: Nat, m: Maybe<&2, A>) -> {H.down_rmb(~A, ~cmp, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), x, U32.from_nat(l), lv, U32.from_nat(r), m) == dreal(~A, drmb(~A, ~cmp, t, i, x, l, lv, r, m)) : H.Down<A>}:
124	  match m:
125	    case None{}:
126	      dcmp_ok(~A, ~cmp, t, i, x, lv, l)
127	    case Some{+rv}:
128	      dtwo_ok(~A, ~cmp, t, i, x, l, lv, r, rv, S.le(~A, ~cmp, lv, rv))
129	
130	# l < n - 1 gives l + 1 < n
131	
132	def right_in(+l: Nat, +n: Nat, +e: {Nat.is_lt(l, Nat.sub(n, 1n)) == True{} : Bool}) -> {Nat.is_lt(1n+l, n) == True{} : Bool}:
133	  L.subst(Bool, b => {b == True{} : Bool}, Nat.is_lt(l, Nat.sub(n, 1n)), Nat.is_lt(1n+l, n), Equal.sym(Bool, Nat.is_lt(1n+l, n), Nat.is_lt(l, Nat.sub(n, 1n)), IX.succ_lt_sub(l, n)), e)
134	
135	# the right child is read only when it is inside the heap, so its index is
136	# below the block
137	
138	def dlmb_ok(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +l: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, two: Bool, m: Maybe<&2, A>, +etwo: {Nat.is_lt(l, Nat.sub(n, 1n)) == two : Bool}, +hl: {l == IX.kidl(i) : Nat}) -> {H.down_lmb(~A, ~cmp, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), x, U32.from_nat(l), two, m) == dreal(~A, dlmb(~A, ~cmp, t, i, x, l, two, m)) : H.Down<A>}:
139	  match two m:
140	    case True{} None{}:
141	      {==}
142	    case False{} None{}:
143	      {==}
144	    case False{} Some{lv}:
145	      dcmp_ok(~A, ~cmp, t, i, x, lv, l)
146	    case True{} Some{+lv}:
147	      +hr = right_in(l, n, etwo)
148	      %Equal.sym(Array<Maybe<&2, A>> & Maybe<&2, A>, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(1n+l)), (AR.thaw(Maybe<&2, A>, t), SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+l)), UPS.get_slot(~A, d, t, 1n+l, hd, N.lt_le_trans(1n+l, n, SC.pow2(d), hr, hn), pf)) : {H.down_rslot(~A, ~cmp, U32.from_nat(i), x, U32.from_nat(l), lv, U32.inc(U32.from_nat(l)), _) == dreal(~A, dlmb(~A, ~cmp, t, i, x, l, True{}, Some{lv})) : H.Down<A>}
149	      drmb_ok(~A, ~cmp, t, i, x, l, lv, 1n+l, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+l))
150	
151	# the "there is a right child" test, in Nat
152	
153	def two_bridge(+l: Nat, +n: Nat, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hl: {Nat.is_lt(l, SC.pow2(d)) == True{} : Bool}, +hln: {Nat.is_lt(l, n) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(l), U32.sub(U32.from_nat(n), 1)) == Nat.is_lt(l, Nat.sub(n, 1n)) : Bool}:
154	  +hnd = N.le_lt_trans(n, SC.pow2(d), SC.pow2(1n+d), hn, pow2_up(d))
155	  +hpos = N.lt_succ_le_succ(0n, n, N.le_lt_trans(0n, l, n, N.zero_le(l), hln))
156	  %Equal.sym(U32, U32.sub(U32.from_nat(n), 1), U32.from_nat(Nat.sub(n, 1n)), UX.sub_one(n, 1n+d, N.lt_succ_le_succ(d, 32n, hd), hnd, hpos)) : {U32.is_lt(U32.from_nat(l), _) == Nat.is_lt(l, Nat.sub(n, 1n)) : Bool}
157	  UX.lt_bridge(l, Nat.sub(n, 1n), 1n+d, N.lt_succ_le_succ(d, 32n, hd), N.lt_trans(l, SC.pow2(d), SC.pow2(1n+d), hl, pow2_up(d)), N.le_lt_trans(Nat.sub(n, 1n), n, SC.pow2(1n+d), UX.sub_le(n), hnd))
158	
159	def dhas_ok(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, b: Bool, +eb: {Nat.is_lt(IX.kidl(i), n) == b : Bool}) -> {H.down_has(~A, ~cmp, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t), U32.from_nat(IX.kidl(i)), b) == dreal(~A, dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), b)) : H.Down<A>}:
160	  match b:
161	    case False{}:
162	      {==}
163	    case True{}:
164	      +hl = N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), eb, hn)
165	      %Equal.sym(Bool, U32.is_lt(U32.from_nat(IX.kidl(i)), U32.sub(U32.from_nat(n), 1)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), two_bridge(IX.kidl(i), n, d, hd, hl, eb, hn)) : {H.down_lslot(~A, ~cmp, U32.from_nat(i), x, U32.from_nat(IX.kidl(i)), _, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(IX.kidl(i)))) == dreal(~A, dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), True{})) : H.Down<A>}
166	      %Equal.sym(Array<Maybe<&2, A>> & Maybe<&2, A>, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(IX.kidl(i))), (AR.thaw(Maybe<&2, A>, t), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))), UPS.get_slot(~A, d, t, IX.kidl(i), hd, hl, pf)) : {H.down_lslot(~A, ~cmp, U32.from_nat(i), x, U32.from_nat(IX.kidl(i)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), _) == dreal(~A, dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), True{})) : H.Down<A>}
167	      dlmb_ok(~A, ~cmp, d, n, t, i, x, IX.kidl(i), hd, hn, pf, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), {==}, {==})
168	
169	def dprobe_ok(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {H.down_probe(~A, ~cmp, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)) == dreal(~A, dprobe(~A, ~cmp, n, i, x, t)) : H.Down<A>}:
170	  %Equal.sym(U32, U32.inc(U32.shl(U32.from_nat(i))), U32.from_nat(IX.kidl(i)), kidl_bridge(i, d, hd, hi)) : {H.down_has(~A, ~cmp, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t), _, U32.is_lt(_, U32.from_nat(n))) == dreal(~A, dprobe(~A, ~cmp, n, i, x, t)) : H.Down<A>}
171	  %Equal.sym(Bool, U32.is_lt(U32.from_nat(IX.kidl(i)), U32.from_nat(n)), Nat.is_lt(IX.kidl(i), n), UX.lt_bridge(IX.kidl(i), n, 1n+d, N.lt_succ_le_succ(d, 32n, hd), IX.kidl_bound(i, d, hi), N.le_lt_trans(n, SC.pow2(d), SC.pow2(1n+d), hn, pow2_up(d)))) : {H.down_has(~A, ~cmp, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t), U32.from_nat(IX.kidl(i)), _) == dreal(~A, dprobe(~A, ~cmp, n, i, x, t)) : H.Down<A>}
172	  dhas_ok(~A, ~cmp, d, n, t, i, x, hd, hn, pf, Nat.is_lt(IX.kidl(i), n), {==})
173	
174	# ---- one step of the sift-down loop ----
175	#
176	# The hole moves from i to the child ci (whose value cv is the smaller of the
177	# children and is smaller than x). `s` is the other child. The step writes cv
178	# into slot i, so the block becomes `t2` and the logical array is `d2`.
179	
180	def t2_of(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +cv: A) -> AR.Tree<Maybe<&2, A>>:
181	  UPS.set_tree(~A, d, t, i, cv)
182	
183	def d2_of(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat) -> List<&2, Maybe<&2, A>>:
184	  UPS.ulog(~A, t2_of(~A, d, t, i, cv), ci, x)
185	
186	def d2_at_c(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), ci) == Some{x} : Maybe<&2, A>}:
187	  UPS.ulog_at(~A, d, t2_of(~A, d, t, i, cv), ci, x, hc, UPS.t2_perfect(~A, d, t, i, cv, pf))
188	
189	def d2_at_i(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +hne: {Nat.is_eq(ci, i) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i) == Some{cv} : Maybe<&2, A>}:
190	  Equal.trans(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), i), Some{cv},
191	    UPS.ulog_off(~A, t2_of(~A, d, t, i, cv), ci, x, i, hne),
192	    Equal.trans(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), i), SL.slot(~A, UPS.ulog(~A, t, i, cv), i), Some{cv},
193	      Equal.cong(List<&2, Maybe<&2, A>>, Maybe<&2, A>, ss => SL.slot(~A, ss, i), AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), UPS.ulog(~A, t, i, cv), UPS.set_slots(~A, d, t, i, cv, hi, pf)),
194	      UPS.ulog_at(~A, d, t, i, cv, hi, pf)))
195	
196	def d2_off(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +j: Nat, +hji: {Nat.is_eq(i, j) == False{} : Bool}, +hjc: {Nat.is_eq(ci, j) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), j) == SL.slot(~A, AR.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}:
197	  Equal.trans(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j),
198	    UPS.ulog_off(~A, t2_of(~A, d, t, i, cv), ci, x, j, hjc),
199	    Equal.trans(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), j), SL.slot(~A, UPS.ulog(~A, t, i, cv), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j),
200	      Equal.cong(List<&2, Maybe<&2, A>>, Maybe<&2, A>, ss => SL.slot(~A, ss, j), AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), UPS.ulog(~A, t, i, cv), UPS.set_slots(~A, d, t, i, cv, hi, pf)),
201	      UPS.ulog_off(~A, t, i, cv, j, hji)))
202	
203	# the current logical array, for reference: x sits at the hole
204	
205	def d1_at_i(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, UPS.ulog(~A, t, i, x), i) == Some{x} : Maybe<&2, A>}:
206	  UPS.ulog_at(~A, d, t, i, x, hi, pf)
207	
208	def kid_pick_of(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, +ci: Nat, +hkids: {SL.kids_le(~A, ~cmp, ss, n, IX.par(i), i) == True{} : Bool}, e: {ci == IX.kidl(i) : Nat} | {ci == IX.kidr(i) : Nat}) -> {SL.kid_le(~A, ~cmp, ss, n, IX.par(i), ci) == True{} : Bool}:
209	  match e:
210	    case Inl{ec}:
211	      L.subst(Nat, z => {SL.kid_le(~A, ~cmp, ss, n, IX.par(i), z) == True{} : Bool}, IX.kidl(i), ci, Equal.sym(Nat, ci, IX.kidl(i), ec), L.and_left(SL.kid_le(~A, ~cmp, ss, n, IX.par(i), IX.kidl(i)), SL.kid_le(~A, ~cmp, ss, n, IX.par(i), IX.kidr(i)), hkids))
212	    case Inr{ec}:
213	      L.subst(Nat, z => {SL.kid_le(~A, ~cmp, ss, n, IX.par(i), z) == True{} : Bool}, IX.kidr(i), ci, Equal.sym(Nat, ci, IX.kidr(i), ec), L.and_right(SL.kid_le(~A, ~cmp, ss, n, IX.par(i), IX.kidl(i)), SL.kid_le(~A, ~cmp, ss, n, IX.par(i), IX.kidr(i)), hkids))
214	
215	def kid_pick(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, +ci: Nat, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ss, n, IX.par(i), i) == True{} : Bool}) -> {SL.kid_le(~A, ~cmp, ss, n, IX.par(i), ci) == True{} : Bool}:
216	  kid_pick_of(~A, ~cmp, ss, n, i, ci, hkids, UPS.kid_at(i, ci, epc, IX.kid_split(ci, N.succ_le_lt(0n, ci, hcpos))))
217	
218	def d1n_i_mle(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +hcn: {Nat.is_lt(ci, n) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), IX.par(i)), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i)) == True{} : Bool}:
219	  +hgrand = SL.ne_sym(ci, IX.par(i), N.is_eq_lt(IX.par(i), ci, N.lt_trans(IX.par(i), i, ci, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), L.subst(Nat, z => {Nat.is_lt(z, ci) == True{} : Bool}, IX.par(ci), i, epc, IX.par_lt(ci, N.succ_le_lt(0n, ci, hcpos))))))
220	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), IX.par(i)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), d2_off(~A, d, t, i, x, cv, ci, IX.par(i), SL.ne_sym(i, IX.par(i), UPS.par_ne(i, hpos)), hgrand, hi, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i)) == True{} : Bool}
221	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i), Some{cv}, d2_at_i(~A, d, t, i, x, cv, ci, SL.ne_sym(ci, i, N.is_eq_lt(i, ci, L.subst(Nat, z => {Nat.is_lt(z, ci) == True{} : Bool}, IX.par(ci), i, epc, IX.par_lt(ci, N.succ_le_lt(0n, ci, hcpos))))), hi, pf)) : {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), _) == True{} : Bool}
222	  %hcv : {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), _) == True{} : Bool}
223	  SL.kid_le_at(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), ci, hcn, kid_pick(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, i, ci, epc, hcpos, hkids))
224	
225	def d1n_i(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +j: Nat, +ej: {Nat.is_eq(j, i) == True{} : Bool}, +hcn: {Nat.is_lt(ci, n) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(i, 0n) == b : Bool}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
226	  match b:
227	    case True{}:
228	      L.subst(Nat, z => {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), z) == True{} : Bool}, i, j, Equal.sym(Nat, j, i, N.eq_from_is_eq(j, i, ej)),
229	        UPS.pair_ok_zero(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), i, eb))
230	    case False{}:
231	      L.subst(Nat, z => {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), z) == True{} : Bool}, i, j, Equal.sym(Nat, j, i, N.eq_from_is_eq(j, i, ej)),
232	        UPS.pair_ok_pos(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), i, UPS.pos_of_ne(i, eb),
233	          d1n_i_mle(~A, ~cmp, d, n, t, i, x, cv, ci, hcn, hcv, epc, hcpos, UPS.pos_of_ne(i, eb), hi, pf, hkids)))
234	
235	
236	def d1n_c_mle(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hnle: {S.le(~A, ~cmp, x, cv) == False{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), IX.par(ci)), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), ci)) == True{} : Bool}:
237	  +hne = SL.ne_sym(ci, i, N.is_eq_lt(i, ci, L.subst(Nat, z => {Nat.is_lt(z, ci) == True{} : Bool}, IX.par(ci), i, epc, IX.par_lt(ci, N.succ_le_lt(0n, ci, hcpos)))))
238	  %Equal.sym(Nat, IX.par(ci), i, epc) : {SL.mle(~A, ~cmp, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), _), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), ci)) == True{} : Bool}
239	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i), Some{cv}, d2_at_i(~A, d, t, i, x, cv, ci, hne, hi, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), ci)) == True{} : Bool}
240	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), ci), Some{x}, d2_at_c(~A, d, t, i, x, cv, ci, hc, pf)) : {SL.mle(~A, ~cmp, Some{cv}, _) == True{} : Bool}
241	  O.total(~A, ~cmp, ~o, x, cv, hnle)
242	
243	def d1n_c(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +j: Nat, +ej: {Nat.is_eq(j, ci) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hnle: {S.le(~A, ~cmp, x, cv) == False{} : Bool}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
244	  L.subst(Nat, z => {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), z) == True{} : Bool}, ci, j, Equal.sym(Nat, j, ci, N.eq_from_is_eq(j, ci, ej)),
245	    UPS.pair_ok_pos(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), ci, hcpos,
246	      d1n_c_mle(~A, ~cmp, ~o, d, t, i, x, cv, ci, epc, hcpos, hc, hi, pf, hnle)))
247	
248	def d1n_s_mle(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, +hsn: {Nat.is_lt(s, n) == True{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}) -> {SL.mle(~A, ~cmp, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), IX.par(s)), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), s)) == True{} : Bool}:
249	  +hne = SL.ne_sym(ci, i, N.is_eq_lt(i, ci, L.subst(Nat, z => {Nat.is_lt(z, ci) == True{} : Bool}, IX.par(ci), i, epc, IX.par_lt(ci, N.succ_le_lt(0n, ci, hcpos)))))
250	  +hsi = N.is_eq_lt(i, s, L.subst(Nat, z => {Nat.is_lt(z, s) == True{} : Bool}, IX.par(s), i, eps, IX.par_lt(s, N.succ_le_lt(0n, s, hspos))))
251	  %Equal.sym(Nat, IX.par(s), i, eps) : {SL.mle(~A, ~cmp, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), _), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), s)) == True{} : Bool}
252	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i), Some{cv}, d2_at_i(~A, d, t, i, x, cv, ci, hne, hi, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), s)) == True{} : Bool}
253	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), s), SL.slot(~A, AR.slots(Maybe<&2, A>, t), s), d2_off(~A, d, t, i, x, cv, ci, s, hsi, hsc, hi, pf)) : {SL.mle(~A, ~cmp, Some{cv}, _) == True{} : Bool}
254	  %hcv : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), s)) == True{} : Bool}
255	  SL.kid_le_at(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s, hsn, hsib)
256	
257	def d1n_s(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, +j: Nat, +ej: {Nat.is_eq(j, s) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
258	  L.subst(Nat, z => {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), z) == True{} : Bool}, s, j, Equal.sym(Nat, j, s, N.eq_from_is_eq(j, s, ej)),
259	    UPS.pair_ok_pos(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), s, hspos,
260	      d1n_s_mle(~A, ~cmp, d, n, t, i, x, cv, ci, s, L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, j, s, N.eq_from_is_eq(j, s, ej), hjn), hsc, eps, hspos, hi, hcpos, epc, pf, hsib, hcv)))
261	
262	def eq_of_eq(+a: Nat, +b: Nat, +e: {a == b : Nat}) -> {Nat.is_eq(a, b) == True{} : Bool}:
263	  L.subst(Nat, z => {Nat.is_eq(a, z) == True{} : Bool}, a, b, e, N.is_eq_refl(a))
264	
265	def or_left(a: Bool, b: Bool, +ea: {a == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
266	  %Equal.sym(Bool, a, True{}, ea) : {Bool.or(_, b) == True{} : Bool}
267	  {==}
268	
269	def or_right(a: Bool, b: Bool, +eb: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
270	  match a:
271	    case True{}:
272	      {==}
273	    case False{}:
274	      eb
275	
276	def par_not_absurd(+j: Nat, +u: Nat, +hkf: {SL.kid_of(j, u) == False{} : Bool}, e: {j == IX.kidl(IX.par(j)) : Nat} | {j == IX.kidr(IX.par(j)) : Nat}, +ep: {IX.par(j) == u : Nat}) -> Empty:
277	  match e:
278	    case Inl{ej}:
279	      L.true_not_false(SL.kid_of(j, u), or_left(Nat.is_eq(j, IX.kidl(u)), Nat.is_eq(j, IX.kidr(u)), eq_of_eq(j, IX.kidl(u), L.subst(Nat, z => {j == IX.kidl(z) : Nat}, IX.par(j), u, ep, ej))), hkf)
280	    case Inr{ej}:
281	      L.true_not_false(SL.kid_of(j, u), or_right(Nat.is_eq(j, IX.kidl(u)), Nat.is_eq(j, IX.kidr(u)), eq_of_eq(j, IX.kidr(u), L.subst(Nat, z => {j == IX.kidr(z) : Nat}, IX.par(j), u, ep, ej))), hkf)
282	
283	def par_not_of(+j: Nat, +u: Nat, +hkf: {SL.kid_of(j, u) == False{} : Bool}, e: {j == IX.kidl(IX.par(j)) : Nat} | {j == IX.kidr(IX.par(j)) : Nat}, b: Bool, +eb: {Nat.is_eq(IX.par(j), u) == b : Bool}) -> {Nat.is_eq(IX.par(j), u) == False{} : Bool}:
284	  match b:
285	    case False{}:
286	      eb
287	    case True{}:
288	      Empty.absurd({Nat.is_eq(IX.par(j), u) == False{} : Bool}, par_not_absurd(j, u, hkf, e, N.eq_from_is_eq(IX.par(j), u, eb)))
289	
290	def par_not(+j: Nat, +u: Nat, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hkf: {SL.kid_of(j, u) == False{} : Bool}) -> {Nat.is_eq(IX.par(j), u) == False{} : Bool}:
291	  par_not_of(j, u, hkf, IX.kid_split(j, N.succ_le_lt(0n, j, hjpos)), Nat.is_eq(IX.par(j), u), {==})
292	
293	def d1n_far_mle(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +j: Nat, +hji: {Nat.is_eq(j, i) == False{} : Bool}, +hjc: {Nat.is_eq(j, ci) == False{} : Bool}, +hpi: {Nat.is_eq(IX.par(j), i) == False{} : Bool}, +hpc: {Nat.is_eq(IX.par(j), ci) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hm: {SL.mle(~A, ~cmp, SL.slot(~A, UPS.ulog(~A, t, i, x), IX.par(j)), SL.slot(~A, UPS.ulog(~A, t, i, x), j)) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), IX.par(j)), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), j)) == True{} : Bool}:
294	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), IX.par(j)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(j)), d2_off(~A, d, t, i, x, cv, ci, IX.par(j), SL.ne_sym(i, IX.par(j), hpi), SL.ne_sym(ci, IX.par(j), hpc), hi, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), j)) == True{} : Bool}
295	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j), d2_off(~A, d, t, i, x, cv, ci, j, SL.ne_sym(i, j, hji), SL.ne_sym(ci, j, hjc), hi, pf)) : {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(j)), _) == True{} : Bool}
296	  %UPS.ulog_off(~A, t, i, x, IX.par(j), SL.ne_sym(i, IX.par(j), hpi)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}
297	  %UPS.ulog_off(~A, t, i, x, j, SL.ne_sym(i, j, hji)) : {SL.mle(~A, ~cmp, SL.slot(~A, UPS.ulog(~A, t, i, x), IX.par(j)), _) == True{} : Bool}
298	  hm
299	
300	def d1n_far(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +j: Nat, +hji: {Nat.is_eq(j, i) == False{} : Bool}, +hjc: {Nat.is_eq(j, ci) == False{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hkf: {SL.kid_of(j, i) == False{} : Bool}, +hkf2: {SL.kid_of(j, ci) == False{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
301	  +hpi = par_not(j, i, hjpos, hkf)
302	  +hpc = par_not(j, ci, hjpos, hkf2)
303	  +hm = UPS.pair_ok_val(~A, ~cmp, UPS.ulog(~A, t, i, x), j, hjpos, SL.exc2_at(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, j, hexc, hjn, hkf))
304	  UPS.pair_ok_pos(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j, hjpos,
305	    d1n_far_mle(~A, ~cmp, d, t, i, x, cv, ci, j, hji, hjc, hpi, hpc, hi, pf, hm))
306	
307	# ---- the four cases, dispatched on the index ----
308	
309	def eq_false_of(+j: Nat, +a: Nat, +b: Nat, +e: {a == b : Nat}, +h: {Nat.is_eq(j, b) == False{} : Bool}) -> {Nat.is_eq(j, a) == False{} : Bool}:
310	  L.subst(Nat, z => {Nat.is_eq(j, z) == False{} : Bool}, b, a, Equal.sym(Nat, a, b, e), h)
311	
312	def side_false(+j: Nat, +u: Nat, +ci: Nat, +s: Nat, +hjc: {Nat.is_eq(j, ci) == False{} : Bool}, +hjs: {Nat.is_eq(j, s) == False{} : Bool}, e: Either<&2, &2, {u == ci : Nat}, {u == s : Nat}>) -> {Nat.is_eq(j, u) == False{} : Bool}:
313	  match e:
314	    case Inl{eu}:
315	      eq_false_of(j, u, ci, eu, hjc)
316	    case Inr{eu}:
317	      eq_false_of(j, u, s, eu, hjs)
318	
319	def or_false(a: Bool, b: Bool, +ea: {a == False{} : Bool}, +eb: {b == False{} : Bool}) -> {Bool.or(a, b) == False{} : Bool}:
320	  %Equal.sym(Bool, a, False{}, ea) : {Bool.or(_, b) == False{} : Bool}
321	  eb
322	
323	def kid_of_false(+j: Nat, +i: Nat, +ci: Nat, +s: Nat, +hjc: {Nat.is_eq(j, ci) == False{} : Bool}, +hjs: {Nat.is_eq(j, s) == False{} : Bool}, ecl: Either<&2, &2, {IX.kidl(i) == ci : Nat}, {IX.kidl(i) == s : Nat}>, ecr: Either<&2, &2, {IX.kidr(i) == ci : Nat}, {IX.kidr(i) == s : Nat}>) -> {SL.kid_of(j, i) == False{} : Bool}:
324	  or_false(Nat.is_eq(j, IX.kidl(i)), Nat.is_eq(j, IX.kidr(i)), side_false(j, IX.kidl(i), ci, s, hjc, hjs, ecl), side_false(j, IX.kidr(i), ci, s, hjc, hjs, ecr))
325	
326	def d1_next_s(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, +j: Nat, +hji: {Nat.is_eq(j, i) == False{} : Bool}, +hjc: {Nat.is_eq(j, ci) == False{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hkf2: {SL.kid_of(j, ci) == False{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +ecl: Either<&2, &2, {IX.kidl(i) == ci : Nat}, {IX.kidl(i) == s : Nat}>, +ecr: Either<&2, &2, {IX.kidr(i) == ci : Nat}, {IX.kidr(i) == s : Nat}>, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, b: Bool, +eb: {Nat.is_eq(j, s) == b : Bool}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
327	  match b:
328	    case True{}:
329	      d1n_s(~A, ~cmp, d, n, t, i, x, cv, ci, s, j, eb, hjn, hsc, eps, hspos, hi, hcpos, epc, pf, hsib, hcv)
330	    case False{}:
331	      d1n_far(~A, ~cmp, d, n, t, i, x, cv, ci, j, hji, hjc, hjn, kid_of_false(j, i, ci, s, hjc, eb, ecl, ecr), hkf2, hjpos, hi, pf, hexc)
332	
333	def d1_next_c(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, +j: Nat, +hji: {Nat.is_eq(j, i) == False{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hkf2: {SL.kid_of(j, ci) == False{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +ecl: Either<&2, &2, {IX.kidl(i) == ci : Nat}, {IX.kidl(i) == s : Nat}>, +ecr: Either<&2, &2, {IX.kidr(i) == ci : Nat}, {IX.kidr(i) == s : Nat}>, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, x, cv) == False{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, ci) == b : Bool}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
334	  match b:
335	    case True{}:
336	      d1n_c(~A, ~cmp, ~o, d, t, i, x, cv, ci, j, eb, epc, hcpos, hc, hi, pf, hnle)
337	    case False{}:
338	      d1_next_s(~A, ~cmp, ~o, d, n, t, i, x, cv, ci, s, j, hji, eb, hjn, hjpos, hkf2, hsc, eps, hspos, epc, hcpos, ecl, ecr, hi, pf, hexc, hsib, hcv, Nat.is_eq(j, s), {==})
339	
340	def d1_next_pos(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, +j: Nat, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hkf2: {SL.kid_of(j, ci) == False{} : Bool}, +hcn: {Nat.is_lt(ci, n) == True{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +ecl: Either<&2, &2, {IX.kidl(i) == ci : Nat}, {IX.kidl(i) == s : Nat}>, +ecr: Either<&2, &2, {IX.kidr(i) == ci : Nat}, {IX.kidr(i) == s : Nat}>, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, x, cv) == False{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, i) == b : Bool}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
341	  match b:
342	    case True{}:
343	      d1n_i(~A, ~cmp, d, n, t, i, x, cv, ci, j, eb, hcn, hcv, epc, hcpos, hi, pf, hkids, Nat.is_eq(i, 0n), {==})
344	    case False{}:
345	      d1_next_c(~A, ~cmp, ~o, d, n, t, i, x, cv, ci, s, j, eb, hjn, hjpos, hkf2, hsc, eps, hspos, epc, hcpos, hc, ecl, ecr, hi, pf, hexc, hsib, hcv, hnle, Nat.is_eq(j, ci), {==})
346	
347	def d1_next_at(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, j: Nat, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hkf2: {SL.kid_of(j, ci) == False{} : Bool}, +hcn: {Nat.is_lt(ci, n) == True{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +ecl: Either<&2, &2, {IX.kidl(i) == ci : Nat}, {IX.kidl(i) == s : Nat}>, +ecr: Either<&2, &2, {IX.kidr(i) == ci : Nat}, {IX.kidr(i) == s : Nat}>, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, x, cv) == False{} : Bool}) -> {SL.pair_ok(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), j) == True{} : Bool}:
348	  match j:
349	    case 0n:
350	      {==}
351	    case 1n+ +m:
352	      d1_next_pos(~A, ~cmp, ~o, d, n, t, i, x, cv, ci, s, 1n+m, hjn, N.zero_le(m), hkf2, hcn, hsc, eps, hspos, epc, hcpos, hc, ecl, ecr, hi, pf, hexc, hkids, hsib, hcv, hnle, Nat.is_eq(1n+m, i), {==})
353	
354	
355	def par_of_kid_go(+k: Nat, +i: Nat, +eb: {SL.kid_of(k, i) == True{} : Bool}, b: Bool, +ebl: {Nat.is_eq(k, IX.kidl(i)) == b : Bool}, c: Bool, +ebr: {Nat.is_eq(k, IX.kidr(i)) == c : Bool}) -> {IX.par(k) == i : Nat}:
356	  match b c:
357	    case True{} _:
358	      L.subst(Nat, z => {IX.par(z) == i : Nat}, IX.kidl(i), k, Equal.sym(Nat, k, IX.kidl(i), N.eq_from_is_eq(k, IX.kidl(i), ebl)), IX.par_kidl(i))
359	    case False{} True{}:
360	      L.subst(Nat, z => {IX.par(z) == i : Nat}, IX.kidr(i), k, Equal.sym(Nat, k, IX.kidr(i), N.eq_from_is_eq(k, IX.kidr(i), ebr)), IX.par_kidr(i))
361	    case False{} False{}:
362	      Empty.absurd({IX.par(k) == i : Nat}, L.true_not_false(SL.kid_of(k, i), eb, or_false(Nat.is_eq(k, IX.kidl(i)), Nat.is_eq(k, IX.kidr(i)), ebl, ebr)))
363	
364	def par_of_kid(+k: Nat, +i: Nat, +eb: {SL.kid_of(k, i) == True{} : Bool}, e: {k == IX.kidl(IX.par(k)) : Nat} | {k == IX.kidr(IX.par(k)) : Nat}) -> {IX.par(k) == i : Nat}:
365	  par_of_kid_go(k, i, eb, Nat.is_eq(k, IX.kidl(i)), {==}, Nat.is_eq(k, IX.kidr(i)), {==})
366	
367	def kid_of_grand_go(+k: Nat, +i: Nat, +ci: Nat, +epk: {IX.par(k) == ci : Nat}, +hne: {Nat.is_eq(ci, i) == False{} : Bool}, b: Bool, +eb: {SL.kid_of(k, i) == b : Bool}, +hkpos: {Nat.is_le(1n, k) == True{} : Bool}) -> {SL.kid_of(k, i) == False{} : Bool}:
368	  match b:
369	    case False{}:
370	      eb
371	    case True{}:
372	      Empty.absurd({SL.kid_of(k, i) == False{} : Bool},
373	        L.true_not_false(Nat.is_eq(ci, i), eq_of_eq(ci, i, Equal.trans(Nat, ci, IX.par(k), i, Equal.sym(Nat, IX.par(k), ci, epk), par_of_kid(k, i, eb, IX.kid_split(k, N.succ_le_lt(0n, k, hkpos))))), hne))
374	
375	def kid_of_grand(+k: Nat, +i: Nat, +ci: Nat, +epk: {IX.par(k) == ci : Nat}, +hkpos: {Nat.is_le(1n, k) == True{} : Bool}, +hne: {Nat.is_eq(ci, i) == False{} : Bool}) -> {SL.kid_of(k, i) == False{} : Bool}:
376	  kid_of_grand_go(k, i, ci, epk, hne, SL.kid_of(k, i), {==}, hkpos)
377	
378	def k_gt_i(+k: Nat, +i: Nat, +ci: Nat, +epk: {IX.par(k) == ci : Nat}, +hkpos: {Nat.is_le(1n, k) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}) -> {Nat.is_lt(i, k) == True{} : Bool}:
379	  N.lt_trans(i, ci, k,
380	    L.subst(Nat, z => {Nat.is_lt(z, ci) == True{} : Bool}, IX.par(ci), i, epc, IX.par_lt(ci, N.succ_le_lt(0n, ci, hcpos))),
381	    L.subst(Nat, z => {Nat.is_lt(z, k) == True{} : Bool}, IX.par(k), ci, epk, IX.par_lt(k, N.succ_le_lt(0n, k, hkpos))))
382	
383	def t2_at_i(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +cv: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), i) == Some{cv} : Maybe<&2, A>}:
384	  Equal.trans(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), i), SL.slot(~A, UPS.ulog(~A, t, i, cv), i), Some{cv},
385	    Equal.cong(List<&2, Maybe<&2, A>>, Maybe<&2, A>, ss => SL.slot(~A, ss, i), AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), UPS.ulog(~A, t, i, cv), UPS.set_slots(~A, d, t, i, cv, hi, pf)),
386	    UPS.ulog_at(~A, d, t, i, cv, hi, pf))
387	
388	def t2_off(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +cv: A, +j: Nat, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), j) == SL.slot(~A, AR.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}:
389	  Equal.trans(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), j), SL.slot(~A, UPS.ulog(~A, t, i, cv), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j),
390	    Equal.cong(List<&2, Maybe<&2, A>>, Maybe<&2, A>, ss => SL.slot(~A, ss, j), AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), UPS.ulog(~A, t, i, cv), UPS.set_slots(~A, d, t, i, cv, hi, pf)),
391	    UPS.ulog_off(~A, t, i, cv, j, hij))
392	
393	def kid_next_mle(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +k: Nat, +epk: {IX.par(k) == ci : Nat}, +hkpos: {Nat.is_le(1n, k) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hcne: {Nat.is_eq(ci, i) == False{} : Bool}, +hkn: {Nat.is_lt(k, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}) -> {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), i), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), k)) == True{} : Bool}:
394	  +hki = N.is_eq_lt(i, k, k_gt_i(k, i, ci, epk, hkpos, epc, hcpos))
395	  +hm = UPS.pair_ok_val(~A, ~cmp, UPS.ulog(~A, t, i, x), k, hkpos, SL.exc2_at(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, k, hexc, hkn, kid_of_grand(k, i, ci, epk, hkpos, hcne)))
396	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), i), Some{cv}, t2_at_i(~A, d, t, i, cv, hi, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), k)) == True{} : Bool}
397	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), k), SL.slot(~A, AR.slots(Maybe<&2, A>, t), k), t2_off(~A, d, t, i, cv, k, hki, hi, pf)) : {SL.mle(~A, ~cmp, Some{cv}, _) == True{} : Bool}
398	  %hcv : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), k)) == True{} : Bool}
399	  %UPS.ulog_off(~A, t, i, x, k, hki) : {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci), _) == True{} : Bool}
400	  %epk : {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), _), SL.slot(~A, UPS.ulog(~A, t, i, x), k)) == True{} : Bool}
401	  %UPS.ulog_off(~A, t, i, x, IX.par(k), SL.ne_sym(i, IX.par(k), par_not(k, i, hkpos, kid_of_grand(k, i, ci, epk, hkpos, hcne)))) : {SL.mle(~A, ~cmp, _, SL.slot(~A, UPS.ulog(~A, t, i, x), k)) == True{} : Bool}
402	  hm
403	
404	def kid_next_one(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +k: Nat, +epk: {IX.par(k) == ci : Nat}, +hkpos: {Nat.is_le(1n, k) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hcne: {Nat.is_eq(ci, i) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, b: Bool, +eb: {Nat.is_lt(k, n) == b : Bool}) -> {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), n, i, k) == True{} : Bool}:
405	  match b:
406	    case False{}:
407	      SL.kid_le_out(~A, ~cmp, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), n, i, k, eb)
408	    case True{}:
409	      SL.kid_le_in(~A, ~cmp, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), n, i, k, eb,
410	        kid_next_mle(~A, ~cmp, d, n, t, i, x, cv, ci, k, epk, hkpos, epc, hcpos, hcne, eb, hi, pf, hexc, hcv))
411	
412	def kids_next_d(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hcne: {Nat.is_eq(ci, i) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}) -> {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), n, IX.par(ci), ci) == True{} : Bool}:
413	  %Equal.sym(Nat, IX.par(ci), i, epc) : {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), n, _, ci) == True{} : Bool}
414	  L.and_intro(SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), n, i, IX.kidl(ci)), SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), n, i, IX.kidr(ci)),
415	    kid_next_one(~A, ~cmp, d, n, t, i, x, cv, ci, IX.kidl(ci), IX.par_kidl(ci), IX.kidl_pos1(ci), epc, hcpos, hcne, hi, pf, hexc, hcv, Nat.is_lt(IX.kidl(ci), n), {==}),
416	    kid_next_one(~A, ~cmp, d, n, t, i, x, cv, ci, IX.kidr(ci), IX.par_kidr(ci), IX.kidr_pos1(ci), epc, hcpos, hcne, hi, pf, hexc, hcv, Nat.is_lt(IX.kidr(ci), n), {==}))
417	
418	# D1 for the next state, built index by index
419	def skip2_next(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, +m: Nat, +hmn: {Nat.is_lt(m, n) == True{} : Bool}, +hcn: {Nat.is_lt(ci, n) == True{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +ecl: Either<&2, &2, {IX.kidl(i) == ci : Nat}, {IX.kidl(i) == s : Nat}>, +ecr: Either<&2, &2, {IX.kidr(i) == ci : Nat}, {IX.kidr(i) == s : Nat}>, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, x, cv) == False{} : Bool}, b: Bool, +eb: {SL.kid_of(m, ci) == b : Bool}) -> {SL.pair_skip2(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), m, ci) == True{} : Bool}:
420	  match b:
421	    case True{}:
422	      SL.skip2_eq(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), m, ci, eb)
423	    case False{}:
424	      SL.skip2_ne(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), m, ci, eb,
425	        d1_next_at(~A, ~cmp, ~o, d, n, t, i, x, cv, ci, s, m, hmn, eb, hcn, hsc, eps, hspos, epc, hcpos, hc, ecl, ecr, hi, pf, hexc, hkids, hsib, hcv, hnle))
426	
427	def exc2_next(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +s: Nat, k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hcn: {Nat.is_lt(ci, n) == True{} : Bool}, +hsc: {Nat.is_eq(ci, s) == False{} : Bool}, +eps: {IX.par(s) == i : Nat}, +hspos: {Nat.is_le(1n, s) == True{} : Bool}, +epc: {IX.par(ci) == i : Nat}, +hcpos: {Nat.is_le(1n, ci) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +ecl: Either<&2, &2, {IX.kidl(i) == ci : Nat}, {IX.kidl(i) == s : Nat}>, +ecr: Either<&2, &2, {IX.kidr(i) == ci : Nat}, {IX.kidr(i) == s : Nat}>, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}, +hsib: {SL.kid_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, x, cv) == False{} : Bool}) -> {SL.ho_exc2(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), k, ci) == True{} : Bool}:
428	  match k:
429	    case 0n:
430	      {==}
431	    case 1n+ +m:
432	      L.and_intro(SL.pair_skip2(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), m, ci), SL.ho_exc2(~A, ~cmp, d2_of(~A, d, t, i, x, cv, ci), m, ci),
433	        skip2_next(~A, ~cmp, ~o, d, n, t, i, x, cv, ci, s, m, N.lt_le_trans(m, 1n+m, n, N.lt_succ(m), hk), hcn, hsc, eps, hspos, epc, hcpos, hc, ecl, ecr, hi, pf, hexc, hkids, hsib, hcv, hnle, SL.kid_of(m, ci), {==}),
434	        exc2_next(~A, ~cmp, ~o, d, n, t, i, x, cv, ci, s, m, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), hcn, hsc, eps, hspos, epc, hcpos, hc, ecl, ecr, hi, pf, hexc, hkids, hsib, hcv, hnle))
435	
436	# the layout and the multiset of the next state
437	def some_next_d(~A: Data, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +m: Nat, +hmn: {Nat.is_lt(m, n) == True{} : Bool}, +hcne: {Nat.is_eq(ci, i) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hlay: {SL.lay(~A, UPS.ulog(~A, t, i, x), n) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, ci) == b : Bool}, c: Bool, +ec: {Nat.is_eq(m, i) == c : Bool}) -> {Maybe.is_some(&2, A, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), m)) == True{} : Bool}:
438	  match b c:
439	    case True{} _:
440	      L.subst(Nat, z => {Maybe.is_some(&2, A, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), z)) == True{} : Bool}, ci, m, Equal.sym(Nat, m, ci, N.eq_from_is_eq(m, ci, eb)),
441	        UPS.some_of_eq(~A, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), ci), x, d2_at_c(~A, d, t, i, x, cv, ci, hc, pf)))
442	    case False{} True{}:
443	      L.subst(Nat, z => {Maybe.is_some(&2, A, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), z)) == True{} : Bool}, i, m, Equal.sym(Nat, m, i, N.eq_from_is_eq(m, i, ec)),
444	        UPS.some_of_eq(~A, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), i), cv, d2_at_i(~A, d, t, i, x, cv, ci, hcne, hi, pf)))
445	    case False{} False{}:
446	      L.subst(Maybe<&2, A>, w => {Maybe.is_some(&2, A, w) == True{} : Bool}, SL.slot(~A, UPS.ulog(~A, t, i, x), m), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), m),
447	        Equal.trans(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), m), SL.slot(~A, AR.slots(Maybe<&2, A>, t), m), SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), m),
448	          UPS.ulog_off(~A, t, i, x, m, SL.ne_sym(i, m, ec)),
449	          Equal.sym(Maybe<&2, A>, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), m), SL.slot(~A, AR.slots(Maybe<&2, A>, t), m), d2_off(~A, d, t, i, x, cv, ci, m, SL.ne_sym(i, m, ec), SL.ne_sym(ci, m, eb), hi, pf))),
450	        SL.lay_at(~A, UPS.ulog(~A, t, i, x), n, m, hlay, hmn))
451	
452	def lay_next_d(~A: Data, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hcne: {Nat.is_eq(ci, i) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hlay: {SL.lay(~A, UPS.ulog(~A, t, i, x), n) == True{} : Bool}) -> {SL.lay(~A, d2_of(~A, d, t, i, x, cv, ci), k) == True{} : Bool}:
453	  match k:
454	    case 0n:
455	      {==}
456	    case 1n+ +m:
457	      L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, d2_of(~A, d, t, i, x, cv, ci), m)), SL.lay(~A, d2_of(~A, d, t, i, x, cv, ci), m),
458	        some_next_d(~A, d, n, t, i, x, cv, ci, m, N.lt_le_trans(m, 1n+m, n, N.lt_succ(m), hk), hcne, hi, hc, pf, hlay, Nat.is_eq(m, ci), {==}, Nat.is_eq(m, i), {==}),
459	        lay_next_d(~A, d, n, t, i, x, cv, ci, m, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), hcne, hi, hc, pf, hlay))
460	
461	def d2_swap_form(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {d2_of(~A, d, t, i, x, cv, ci) == SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, UPS.ulog(~A, t, i, x), i, Some{cv}), ci, Some{x}) : List<&2, Maybe<&2, A>>}:
462	  Equal.cong(List<&2, Maybe<&2, A>>, List<&2, Maybe<&2, A>>, ss => SC.update(Maybe<&2, A>, ss, ci, Some{x}), AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), SC.update(Maybe<&2, A>, UPS.ulog(~A, t, i, x), i, Some{cv}),
463	    Equal.trans(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), UPS.ulog(~A, t, i, cv), SC.update(Maybe<&2, A>, UPS.ulog(~A, t, i, x), i, Some{cv}),
464	      UPS.set_slots(~A, d, t, i, cv, hi, pf),
465	      Equal.sym(List<&2, Maybe<&2, A>>, SC.update(Maybe<&2, A>, UPS.ulog(~A, t, i, x), i, Some{cv}), UPS.ulog(~A, t, i, cv), BG.upd_upd_same(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, Some{cv}))))
466	
467	def ms_next_d(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +tgt: List<&2, A>, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hcn: {Nat.is_lt(ci, n) == True{} : Bool}, +hcne: {Nat.is_eq(ci, i) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>}, +hms: {V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> {V.msort(~A, ~cmp, V.vals(~A, d2_of(~A, d, t, i, x, cv, ci), n)) == tgt : List<&2, A>}:
468	  %Equal.sym(List<&2, Maybe<&2, A>>, d2_of(~A, d, t, i, x, cv, ci), SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, UPS.ulog(~A, t, i, x), i, Some{cv}), ci, Some{x}), d2_swap_form(~A, d, t, i, x, cv, ci, hi, pf)) : {V.msort(~A, ~cmp, V.vals(~A, _, n)) == tgt : List<&2, A>}
469	  Equal.trans(List<&2, A>, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, UPS.ulog(~A, t, i, x), i, Some{cv}), ci, Some{x}), n)), V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), n)), tgt,
470	    BG.vals_swap(~A, ~cmp, ~o, UPS.ulog(~A, t, i, x), n, i, ci, x, cv, hin, hcn, SL.ne_sym(i, ci, hcne),
471	      UPS.ulog_at(~A, d, t, i, x, hi, pf),
472	      Equal.trans(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), ci), SL.slot(~A, AR.slots(Maybe<&2, A>, t), ci), Some{cv}, UPS.ulog_off(~A, t, i, x, ci, SL.ne_sym(i, ci, hcne)), hcv)),
473	    hms)
474	
475	# ---- what the loop delivers ----
476	
477	def DownOK(~A: Data, ~cmp: A -> A -> Cmp, d: Nat, n: Nat, tgt: List<&2, A>, fuel: Nat, x: A, s: DownS<A>) -> Type:
478	  Sigma<&1, &1, AR.Tree<Maybe<&2, A>>, t2 => {H.down_go(~A, ~cmp, fuel, U32.from_nat(n), x, dreal(~A, s)) == AR.thaw(Maybe<&2, A>, t2) : Array<Maybe<&2, A>>} & ({AR.perfect(Maybe<&2, A>, d, t2) == True{} : Bool} & ({SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t2), n) == True{} : Bool} & ({SL.lay(~A, AR.slots(Maybe<&2, A>, t2), n) == True{} : Bool} & {V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t2), n)) == tgt : List<&2, A>})))>
479	
480	# the loop stops: x is written at the hole and the two pairs below it hold
481	def down_stop_mk(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +tgt: List<&2, A>, +fuel: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +eq: {H.down_go(~A, ~cmp, fuel, U32.from_nat(n), x, dreal(~A, DStp{t, i})) == AR.thaw(Maybe<&2, A>, UPS.set_tree(~A, d, t, i, x)) : Array<Maybe<&2, A>>}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, i) == True{} : Bool}, +hlay: {SL.lay(~A, UPS.ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> DownOK(~A, ~cmp, d, n, tgt, fuel, x, DStp{t, i}):
482	  +es = UPS.set_slots(~A, d, t, i, x, hi, pf)
483	  (UPS.set_tree(~A, d, t, i, x),
484	   (eq,
485	    (AR.upd_perfect(Maybe<&2, A>, d, t, i, Some{x}, pf),
486	     (L.subst(List<&2, Maybe<&2, A>>, ss => {SL.ho_upto(~A, ~cmp, ss, n) == True{} : Bool}, UPS.ulog(~A, t, i, x), AR.slots(Maybe<&2, A>, UPS.set_tree(~A, d, t, i, x)), Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, UPS.set_tree(~A, d, t, i, x)), UPS.ulog(~A, t, i, x), es),
487	        SL.ho_of_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, n, i, N.le_refl(n), hexc, hkids)),
488	      (L.subst(List<&2, Maybe<&2, A>>, ss => {SL.lay(~A, ss, n) == True{} : Bool}, UPS.ulog(~A, t, i, x), AR.slots(Maybe<&2, A>, UPS.set_tree(~A, d, t, i, x)), Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, UPS.set_tree(~A, d, t, i, x)), UPS.ulog(~A, t, i, x), es), hlay),
489	       L.subst(List<&2, Maybe<&2, A>>, ss => {V.msort(~A, ~cmp, V.vals(~A, ss, n)) == tgt : List<&2, A>}, UPS.ulog(~A, t, i, x), AR.slots(Maybe<&2, A>, UPS.set_tree(~A, d, t, i, x)), Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, UPS.set_tree(~A, d, t, i, x)), UPS.ulog(~A, t, i, x), es), hms))))))
490	
491	def down_stop_ok(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +tgt: List<&2, A>, fuel: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, i) == True{} : Bool}, +hlay: {SL.lay(~A, UPS.ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> DownOK(~A, ~cmp, d, n, tgt, fuel, x, DStp{t, i}):
492	  match fuel:
493	    case 0n:
494	      down_stop_mk(~A, ~cmp, d, n, tgt, 0n, t, i, x, UPS.set_eq(~A, d, t, i, x, hd, hi, pf), hi, hn, pf, hexc, hkids, hlay, hms)
495	    case 1n+f:
496	      down_stop_mk(~A, ~cmp, d, n, tgt, 1n+f, t, i, x, UPS.set_eq(~A, d, t, i, x, hd, hi, pf), hi, hn, pf, hexc, hkids, hlay, hms)
497	
498	# ---- the facts each shape of the probe gives ----
499	
500	# a slot inside the heap is occupied, so a probe that reads None there is
501	# impossible
502	def slot_some_at(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +n: Nat, +j: Nat, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hji: {Nat.is_eq(i, j) == False{} : Bool}, +hlay: {SL.lay(~A, UPS.ulog(~A, t, i, x), n) == True{} : Bool}, +em: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), j) == None{} : Maybe<&2, A>}) -> Empty:
503	  L.true_not_false(Maybe.is_some(&2, A, SL.slot(~A, UPS.ulog(~A, t, i, x), j)), SL.lay_at(~A, UPS.ulog(~A, t, i, x), n, j, hlay, hjn),
504	    L.subst(Maybe<&2, A>, w => {Maybe.is_some(&2, A, w) == False{} : Bool}, None{}, SL.slot(~A, UPS.ulog(~A, t, i, x), j),
505	      Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), j), None{}, Equal.trans(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j), None{}, UPS.ulog_off(~A, t, i, x, j, hji), em)), {==}))
506	
507	# kidl i >= n implies kidr i >= n
508	def kidr_out(+i: Nat, +n: Nat, +e: {Nat.is_lt(IX.kidl(i), n) == False{} : Bool}) -> {Nat.is_lt(IX.kidr(i), n) == False{} : Bool}:
509	  N.le_not_lt(IX.kidr(i), n, N.le_trans(n, IX.kidl(i), IX.kidr(i), N.not_lt_le(IX.kidl(i), n, e), N.le_succ(IX.kidl(i))))
510	
511	# the right child is out of range exactly when the `two` test fails
512	def kidr_out2(+i: Nat, +n: Nat, +e: {Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)) == False{} : Bool}) -> {Nat.is_lt(IX.kidr(i), n) == False{} : Bool}:
513	  L.subst(Bool, b => {b == False{} : Bool}, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), Nat.is_lt(IX.kidr(i), n), Equal.sym(Bool, Nat.is_lt(IX.kidr(i), n), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), IX.succ_lt_sub(IX.kidl(i), n)), e)
514	
515	def kidr_in2(+i: Nat, +n: Nat, +e: {Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)) == True{} : Bool}) -> {Nat.is_lt(IX.kidr(i), n) == True{} : Bool}:
516	  L.subst(Bool, b => {b == True{} : Bool}, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), Nat.is_lt(IX.kidr(i), n), Equal.sym(Bool, Nat.is_lt(IX.kidr(i), n), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), IX.succ_lt_sub(IX.kidl(i), n)), e)
517	
518	def kidl_ne_kidr(+i: Nat) -> {Nat.is_eq(IX.kidl(i), IX.kidr(i)) == False{} : Bool}:
519	  N.is_eq_lt(IX.kidl(i), IX.kidr(i), N.lt_succ(IX.kidl(i)))
520	
521	def kid_le_x_mle(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +c: Nat, +cv: A, +hci: {Nat.is_eq(i, c) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), c) == Some{cv} : Maybe<&2, A>}, +hle: {S.le(~A, ~cmp, x, cv) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, UPS.ulog(~A, t, i, x), i), SL.slot(~A, UPS.ulog(~A, t, i, x), c)) == True{} : Bool}:
522	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), i), Some{x}, UPS.ulog_at(~A, d, t, i, x, hi, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, UPS.ulog(~A, t, i, x), c)) == True{} : Bool}
523	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), c), SL.slot(~A, AR.slots(Maybe<&2, A>, t), c), UPS.ulog_off(~A, t, i, x, c, hci)) : {SL.mle(~A, ~cmp, Some{x}, _) == True{} : Bool}
524	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), c), Some{cv}, hcv) : {SL.mle(~A, ~cmp, Some{x}, _) == True{} : Bool}
525	  hle
526	
527	# "x is not larger than that child", as the kid_le conjunct
528	def kid_le_x(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +n: Nat, +c: Nat, +cv: A, +hcn: {Nat.is_lt(c, n) == True{} : Bool}, +hci: {Nat.is_eq(i, c) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hcv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), c) == Some{cv} : Maybe<&2, A>}, +hle: {S.le(~A, ~cmp, x, cv) == True{} : Bool}) -> {SL.kid_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, c) == True{} : Bool}:
529	  SL.kid_le_in(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, c, hcn, kid_le_x_mle(~A, ~cmp, d, t, i, x, c, cv, hci, hi, pf, hcv, hle))
530	
531	# ---- the loop ----
532	
533	# the value the probe compares x with, as a function of its three reads
534	def pick_cv2(~A: Data, +x: A, +lv: A, two: Bool, mr: Maybe<&2, A>, left: Bool) -> A:
535	  match two mr left:
536	    case False{} _ _:
537	      lv
538	    case True{} None{} _:
539	      lv
540	    case True{} Some{rv} True{}:
541	      lv
542	    case True{} Some{rv} False{}:
543	      rv
544	
545	def pick_cv(~A: Data, +x: A, ml: Maybe<&2, A>, two: Bool, mr: Maybe<&2, A>, left: Bool) -> A:
546	  match ml:
547	    case None{}:
548	      x
549	    case Some{+lv}:
550	      pick_cv2(~A, x, lv, two, mr, left)
551	
552	def down_carry_go(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +tgt: List<&2, A>, +f: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +t3: AR.Tree<Maybe<&2, A>>, +eq: {H.down_go(~A, ~cmp, 1n+f, U32.from_nat(n), x, dreal(~A, DMv{t, i, cv, ci})) == H.down_go(~A, ~cmp, f, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv)))) : Array<Maybe<&2, A>>}, rest: {H.down_go(~A, ~cmp, f, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv)))) == AR.thaw(Maybe<&2, A>, t3) : Array<Maybe<&2, A>>} & ({AR.perfect(Maybe<&2, A>, d, t3) == True{} : Bool} & ({SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t3), n) == True{} : Bool} & ({SL.lay(~A, AR.slots(Maybe<&2, A>, t3), n) == True{} : Bool} & {V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t3), n)) == tgt : List<&2, A>}))) ) -> DownOK(~A, ~cmp, d, n, tgt, 1n+f, x, DMv{t, i, cv, ci}):
553	  (e1, more) = rest
554	  (t3, (Equal.trans(Array<Maybe<&2, A>>, H.down_go(~A, ~cmp, 1n+f, U32.from_nat(n), x, dreal(~A, DMv{t, i, cv, ci})), H.down_go(~A, ~cmp, f, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv)))), AR.thaw(Maybe<&2, A>, t3), eq, e1), more))
555	
556	def down_carry(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +tgt: List<&2, A>, +f: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +eq: {H.down_go(~A, ~cmp, 1n+f, U32.from_nat(n), x, dreal(~A, DMv{t, i, cv, ci})) == H.down_go(~A, ~cmp, f, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv)))) : Array<Maybe<&2, A>>}, rec: DownOK(~A, ~cmp, d, n, tgt, f, x, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv)))) -> DownOK(~A, ~cmp, d, n, tgt, 1n+f, x, DMv{t, i, cv, ci}):
557	  (t3, rest) = rec
558	  down_carry_go(~A, ~cmp, d, n, tgt, f, t, i, x, cv, ci, t3, eq, rest)
559	
560	def down_step_eq(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +f: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +cv: A, +ci: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hc: {Nat.is_lt(ci, SC.pow2(d)) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {H.down_go(~A, ~cmp, 1n+f, U32.from_nat(n), x, dreal(~A, DMv{t, i, cv, ci})) == H.down_go(~A, ~cmp, f, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv)))) : Array<Maybe<&2, A>>}:
561	  %Equal.sym(Array<Maybe<&2, A>>, Array.set(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), Some{cv}), AR.thaw(Maybe<&2, A>, t2_of(~A, d, t, i, cv)), UPS.set_eq(~A, d, t, i, cv, hd, hi, pf)) : {H.down_go(~A, ~cmp, f, U32.from_nat(n), x, H.down_probe(~A, ~cmp, U32.from_nat(n), U32.from_nat(ci), x, _)) == H.down_go(~A, ~cmp, f, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv)))) : Array<Maybe<&2, A>>}
562	  Equal.cong(H.Down<A>, Array<Maybe<&2, A>>, s => H.down_go(~A, ~cmp, f, U32.from_nat(n), x, s), H.down_probe(~A, ~cmp, U32.from_nat(n), U32.from_nat(ci), x, AR.thaw(Maybe<&2, A>, t2_of(~A, d, t, i, cv))), dreal(~A, dprobe(~A, ~cmp, n, ci, x, t2_of(~A, d, t, i, cv))),
563	    dprobe_ok(~A, ~cmp, d, n, t2_of(~A, d, t, i, cv), ci, x, hd, hc, hn, UPS.t2_perfect(~A, d, t, i, cv, pf)))
564	
565	# the probe's result as a function of its three reads and two comparisons
566	def pick_state2(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +lv: A, two: Bool, mr: Maybe<&2, A>, left: Bool, ok: Bool) -> DownS<A>:
567	  match two mr left ok:
568	    case False{} _ _ True{}:
569	      DStp{t, i}
570	    case False{} _ _ False{}:
571	      DMv{t, i, lv, IX.kidl(i)}
572	    case True{} None{} _ True{}:
573	      DStp{t, i}
574	    case True{} None{} _ False{}:
575	      DMv{t, i, lv, IX.kidl(i)}
576	    case True{} Some{rv} True{} True{}:
577	      DStp{t, i}
578	    case True{} Some{rv} True{} False{}:
579	      DMv{t, i, lv, IX.kidl(i)}
580	    case True{} Some{rv} False{} True{}:
581	      DStp{t, i}
582	    case True{} Some{+rv} False{} False{}:
583	      DMv{t, i, rv, IX.kidr(i)}
584	
585	def pick_state(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, hasl: Bool, ml: Maybe<&2, A>, two: Bool, mr: Maybe<&2, A>, left: Bool, ok: Bool) -> DownS<A>:
586	  match hasl ml:
587	    case False{} _:
588	      DStp{t, i}
589	    case True{} None{}:
590	      DStp{t, i}
591	    case True{} Some{+lv}:
592	      pick_state2(~A, t, i, lv, two, mr, left, ok)
593	
594	def probe_shape(~A: Data, ~cmp: A -> A -> Cmp, +n: Nat, +i: Nat, +x: A, +t: AR.Tree<Maybe<&2, A>>, hasl: Bool, +ehasl: {Nat.is_lt(IX.kidl(i), n) == hasl : Bool}, ml: Maybe<&2, A>, +eml: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)) == ml : Maybe<&2, A>}, two: Bool, +etwo: {Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)) == two : Bool}, mr: Maybe<&2, A>, +emr: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)) == mr : Maybe<&2, A>}, left: Bool, +eleft: {S.le(~A, ~cmp, UPS.mval(~A, ml, x), UPS.mval(~A, mr, x)) == left : Bool}, ok: Bool, +eok: {S.le(~A, ~cmp, x, pick_cv(~A, x, ml, two, mr, left)) == ok : Bool}) -> {dprobe(~A, ~cmp, n, i, x, t) == pick_state(~A, t, i, hasl, ml, two, mr, left, ok) : DownS<A>}:
595	  match hasl ml two mr left ok:
596	    case False{} _ _ _ _ _:
597	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), False{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
598	      {==}
599	    case True{} None{} True{} _ _ _:
600	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
601	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), True{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DStp{t, i} : DownS<A>}
602	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), None{}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), True{}, _) == DStp{t, i} : DownS<A>}
603	      {==}
604	    case True{} None{} False{} _ _ _:
605	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
606	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), False{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DStp{t, i} : DownS<A>}
607	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), None{}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), False{}, _) == DStp{t, i} : DownS<A>}
608	      {==}
609	    case True{} Some{lv} False{} _ _ True{}:
610	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
611	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), False{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DStp{t, i} : DownS<A>}
612	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), False{}, _) == DStp{t, i} : DownS<A>}
613	      %Equal.sym(Bool, S.le(~A, ~cmp, x, lv), True{}, eok) : {ddec(~A, t, i, lv, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
614	      {==}
615	    case True{} Some{lv} False{} _ _ False{}:
616	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
617	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), False{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
618	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), False{}, _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
619	      %Equal.sym(Bool, S.le(~A, ~cmp, x, lv), False{}, eok) : {ddec(~A, t, i, lv, IX.kidl(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
620	      {==}
621	    case True{} Some{lv} True{} None{} _ True{}:
622	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
623	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), True{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DStp{t, i} : DownS<A>}
624	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), True{}, _) == DStp{t, i} : DownS<A>}
625	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), None{}, emr) : {drmb(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), _) == DStp{t, i} : DownS<A>}
626	      %Equal.sym(Bool, S.le(~A, ~cmp, x, lv), True{}, eok) : {ddec(~A, t, i, lv, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
627	      {==}
628	    case True{} Some{lv} True{} None{} _ False{}:
629	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
630	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), True{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
631	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), True{}, _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
632	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), None{}, emr) : {drmb(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
633	      %Equal.sym(Bool, S.le(~A, ~cmp, x, lv), False{}, eok) : {ddec(~A, t, i, lv, IX.kidl(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
634	      {==}
635	    case True{} Some{lv} True{} Some{rv} True{} True{}:
636	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
637	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), True{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DStp{t, i} : DownS<A>}
638	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), True{}, _) == DStp{t, i} : DownS<A>}
639	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), Some{rv}, emr) : {drmb(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), _) == DStp{t, i} : DownS<A>}
640	      %Equal.sym(Bool, S.le(~A, ~cmp, lv, rv), True{}, eleft) : {dtwo(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), rv, _) == DStp{t, i} : DownS<A>}
641	      %Equal.sym(Bool, S.le(~A, ~cmp, x, lv), True{}, eok) : {ddec(~A, t, i, lv, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
642	      {==}
643	    case True{} Some{lv} True{} Some{rv} True{} False{}:
644	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
645	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), True{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
646	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), True{}, _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
647	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), Some{rv}, emr) : {drmb(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
648	      %Equal.sym(Bool, S.le(~A, ~cmp, lv, rv), True{}, eleft) : {dtwo(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), rv, _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
649	      %Equal.sym(Bool, S.le(~A, ~cmp, x, lv), False{}, eok) : {ddec(~A, t, i, lv, IX.kidl(i), _) == DMv{t, i, lv, IX.kidl(i)} : DownS<A>}
650	      {==}
651	    case True{} Some{lv} True{} Some{rv} False{} True{}:
652	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DStp{t, i} : DownS<A>}
653	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), True{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DStp{t, i} : DownS<A>}
654	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), True{}, _) == DStp{t, i} : DownS<A>}
655	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), Some{rv}, emr) : {drmb(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), _) == DStp{t, i} : DownS<A>}
656	      %Equal.sym(Bool, S.le(~A, ~cmp, lv, rv), False{}, eleft) : {dtwo(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), rv, _) == DStp{t, i} : DownS<A>}
657	      %Equal.sym(Bool, S.le(~A, ~cmp, x, rv), True{}, eok) : {ddec(~A, t, i, rv, IX.kidr(i), _) == DStp{t, i} : DownS<A>}
658	      {==}
659	    case True{} Some{lv} True{} Some{rv} False{} False{}:
660	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), n), True{}, ehasl) : {dhas(~A, ~cmp, n, i, x, t, IX.kidl(i), _) == DMv{t, i, rv, IX.kidr(i)} : DownS<A>}
661	      %Equal.sym(Bool, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), True{}, etwo) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == DMv{t, i, rv, IX.kidr(i)} : DownS<A>}
662	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {dlmb(~A, ~cmp, t, i, x, IX.kidl(i), True{}, _) == DMv{t, i, rv, IX.kidr(i)} : DownS<A>}
663	      %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), Some{rv}, emr) : {drmb(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), _) == DMv{t, i, rv, IX.kidr(i)} : DownS<A>}
664	      %Equal.sym(Bool, S.le(~A, ~cmp, lv, rv), False{}, eleft) : {dtwo(~A, ~cmp, t, i, x, IX.kidl(i), lv, IX.kidr(i), rv, _) == DMv{t, i, rv, IX.kidr(i)} : DownS<A>}
665	      %Equal.sym(Bool, S.le(~A, ~cmp, x, rv), False{}, eok) : {ddec(~A, t, i, rv, IX.kidr(i), _) == DMv{t, i, rv, IX.kidr(i)} : DownS<A>}
666	      {==}
667	
668	# ---- what the stop cases have to show: x is not larger than its children ----
669	
670	def g_no_left(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +n: Nat, +e: {Nat.is_lt(IX.kidl(i), n) == False{} : Bool}) -> {SL.kids_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, i) == True{} : Bool}:
671	  L.and_intro(SL.kid_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidl(i)), SL.kid_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidr(i)),
672	    SL.kid_le_out(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidl(i), e),
673	    SL.kid_le_out(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidr(i), kidr_out(i, n, e)))
674	
675	def g_left_only(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +n: Nat, +lv: A, +ehasl: {Nat.is_lt(IX.kidl(i), n) == True{} : Bool}, +etwo: {Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)) == False{} : Bool}, +eml: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)) == Some{lv} : Maybe<&2, A>}, +eok: {S.le(~A, ~cmp, x, lv) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.kids_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, i) == True{} : Bool}:
676	  L.and_intro(SL.kid_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidl(i)), SL.kid_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidr(i)),
677	    kid_le_x(~A, ~cmp, d, t, i, x, n, IX.kidl(i), lv, ehasl, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i)), hi, pf, eml, eok),
678	    SL.kid_le_out(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidr(i), kidr_out2(i, n, etwo)))
679	
680	def g_both(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +n: Nat, +lv: A, +rv: A, +ehasl: {Nat.is_lt(IX.kidl(i), n) == True{} : Bool}, +etwo: {Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)) == True{} : Bool}, +eml: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)) == Some{lv} : Maybe<&2, A>}, +emr: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)) == Some{rv} : Maybe<&2, A>}, +hxl: {S.le(~A, ~cmp, x, lv) == True{} : Bool}, +hxr: {S.le(~A, ~cmp, x, rv) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.kids_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, i) == True{} : Bool}:
681	  L.and_intro(SL.kid_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidl(i)), SL.kid_le(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i, IX.kidr(i)),
682	    kid_le_x(~A, ~cmp, d, t, i, x, n, IX.kidl(i), lv, ehasl, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i)), hi, pf, eml, hxl),
683	    kid_le_x(~A, ~cmp, d, t, i, x, n, IX.kidr(i), rv, kidr_in2(i, n, etwo), N.is_eq_lt(i, IX.kidr(i), IX.kidr_gt(i)), hi, pf, emr, hxr))
684	
685	# with no fuel left the hole has no children: n <= 1 + i and kidl i < n force
686	# 2i + 1 < 1 + i
687	def fuel_out(+i: Nat, +n: Nat, +ehasl: {Nat.is_lt(IX.kidl(i), n) == True{} : Bool}, +hfuel: {Nat.is_le(n, IX.scale(0n, 1n+i)) == True{} : Bool}) -> Empty:
688	  L.true_not_false(Nat.is_lt(IX.kidl(i), 1n+i), N.lt_le_trans(IX.kidl(i), n, 1n+i, ehasl, hfuel), N.le_not_lt(IX.kidl(i), 1n+i, IX.double_le(i)))
689	
690	def sib_mle(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +lv: A, +rv: A, +eml: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)) == Some{lv} : Maybe<&2, A>}, +emr: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)) == Some{rv} : Maybe<&2, A>}, +hle: {S.le(~A, ~cmp, lv, rv) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i))) == True{} : Bool}:
691	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i))) == True{} : Bool}
692	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), Some{rv}, emr) : {SL.mle(~A, ~cmp, Some{lv}, _) == True{} : Bool}
693	  hle
694	
695	def sib_mle_r(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +lv: A, +rv: A, +eml: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)) == Some{lv} : Maybe<&2, A>}, +emr: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)) == Some{rv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, lv, rv) == False{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == True{} : Bool}:
696	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), Some{rv}, emr) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i))) == True{} : Bool}
697	  %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Some{lv}, eml) : {SL.mle(~A, ~cmp, Some{rv}, _) == True{} : Bool}
698	  O.total(~A, ~cmp, ~o, lv, rv, hnle)
699	
700	
701	def down_loop_go(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), fuel: Nat, +d: Nat, +n: Nat, +tgt: List<&2, A>, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +hfuel: {Nat.is_le(n, IX.scale(fuel, 1n+i)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hpair: {SL.pair_ok(~A, ~cmp, UPS.ulog(~A, t, i, x), i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}, +hlay: {SL.lay(~A, UPS.ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), n)) == tgt : List<&2, A>}, hasl: Bool, +ehasl: {Nat.is_lt(IX.kidl(i), n) == hasl : Bool}, ml: Maybe<&2, A>, +eml: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)) == ml : Maybe<&2, A>}, two: Bool, +etwo: {Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)) == two : Bool}, mr: Maybe<&2, A>, +emr: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)) == mr : Maybe<&2, A>}, left: Bool, +eleft: {S.le(~A, ~cmp, UPS.mval(~A, ml, x), UPS.mval(~A, mr, x)) == left : Bool}, ok: Bool, +eok: {S.le(~A, ~cmp, x, pick_cv(~A, x, ml, two, mr, left)) == ok : Bool}) -> DownOK(~A, ~cmp, d, n, tgt, fuel, x, pick_state(~A, t, i, hasl, ml, two, mr, left, ok)):
702	  match fuel hasl ml two mr left ok:
703	    case _ False{} _ _ _ _ _:
704	      down_stop_ok(~A, ~cmp, d, n, tgt, fuel, t, i, x, hd, hi, hn, pf, hexc, g_no_left(~A, ~cmp, t, i, x, n, ehasl), hlay, hms)
705	    case _ True{} None{} True{} _ _ _:
706	      Empty.absurd(DownOK(~A, ~cmp, d, n, tgt, fuel, x, DStp{t, i}), slot_some_at(~A, t, i, x, n, IX.kidl(i), ehasl, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i)), hlay, eml))
707	    case _ True{} None{} False{} _ _ _:
708	      Empty.absurd(DownOK(~A, ~cmp, d, n, tgt, fuel, x, DStp{t, i}), slot_some_at(~A, t, i, x, n, IX.kidl(i), ehasl, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i)), hlay, eml))
709	    case _ True{} Some{lv} False{} _ _ True{}:
710	      down_stop_ok(~A, ~cmp, d, n, tgt, fuel, t, i, x, hd, hi, hn, pf, hexc, g_left_only(~A, ~cmp, d, t, i, x, n, lv, ehasl, etwo, eml, eok, hi, pf), hlay, hms)
711	    case 0n True{} Some{lv} False{} _ _ False{}:
712	      Empty.absurd(DownOK(~A, ~cmp, d, n, tgt, 0n, x, DMv{t, i, lv, IX.kidl(i)}), fuel_out(i, n, ehasl, hfuel))
713	    case 1n+ +f True{} Some{+lv} False{} _ _ False{}:
714	      down_carry(~A, ~cmp, d, n, tgt, f, t, i, x, lv, IX.kidl(i),
715	        down_step_eq(~A, ~cmp, d, n, f, t, i, x, lv, IX.kidl(i), hd, hi, N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), hn, pf),
716	        L.subst(DownS<A>, st => DownOK(~A, ~cmp, d, n, tgt, f, x, st), pick_state(~A, t2_of(~A, d, t, i, lv), IX.kidl(i), Nat.is_lt(IX.kidl(IX.kidl(i)), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x))))), dprobe(~A, ~cmp, n, IX.kidl(i), x, t2_of(~A, d, t, i, lv)),
717	          Equal.sym(DownS<A>, dprobe(~A, ~cmp, n, IX.kidl(i), x, t2_of(~A, d, t, i, lv)), pick_state(~A, t2_of(~A, d, t, i, lv), IX.kidl(i), Nat.is_lt(IX.kidl(IX.kidl(i)), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x))))), probe_shape(~A, ~cmp, n, IX.kidl(i), x, t2_of(~A, d, t, i, lv), Nat.is_lt(IX.kidl(IX.kidl(i)), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), {==}, Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~
718	          down_loop_go(~A, ~cmp, ~o, f, d, n, tgt, t2_of(~A, d, t, i, lv), IX.kidl(i), x, hd, N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), ehasl, hn,
719	            N.le_trans(n, IX.scale(f, Nat.double(1n+i)), IX.scale(f, 1n+IX.kidl(i)), hfuel, IX.scale_mono(f, Nat.double(1n+i), 1n+IX.kidl(i), IX.kid_double(i, IX.kidl(i), IX.par_kidl(i), IX.kidl_pos1(i)))),
720	            UPS.t2_perfect(~A, d, t, i, lv, pf),
721	            exc2_next(~A, ~cmp, ~o, d, n, t, i, x, lv, IX.kidl(i), IX.kidr(i), n, N.le_refl(n), ehasl, kidl_ne_kidr(i), IX.par_kidr(i), IX.kidr_pos1(i), IX.par_kidl(i), IX.kidl_pos1(i), N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), Inl{{==}}, Inr{{==}}, hi, pf, hexc, hkids, SL.kid_le_out(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.kidl(i), IX.kidr(i), kidr_out2(i, n, etwo)), eml, eok),
722	            d1n_c(~A, ~cmp, ~o, d, t, i, x, lv, IX.kidl(i), IX.kidl(i), N.is_eq_refl(IX.kidl(i)), IX.par_kidl(i), IX.kidl_pos1(i), N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), hi, pf, eok),
723	            kids_next_d(~A, ~cmp, d, n, t, i, x, lv, IX.kidl(i), IX.par_kidl(i), IX.kidl_pos1(i), SL.ne_sym(IX.kidl(i), i, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i))), hi, pf, hexc, eml),
724	            lay_next_d(~A, d, n, t, i, x, lv, IX.kidl(i), n, N.le_refl(n), SL.ne_sym(IX.kidl(i), i, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i))), hi, N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), pf, hlay),
725	            ms_next_d(~A, ~cmp, ~o, d, n, t, i, x, lv, IX.kidl(i), tgt, hin, ehasl, SL.ne_sym(IX.kidl(i), i, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i))), hi, pf, eml, hms),
726	            Nat.is_lt(IX.kidl(IX.kidl(i)), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), {==}, Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)))), {==})))
727	    case _ True{} Some{lv} True{} None{} _ True{}:
728	      Empty.absurd(DownOK(~A, ~cmp, d, n, tgt, fuel, x, pick_state2(~A, t, i, lv, True{}, None{}, left, True{})), slot_some_at(~A, t, i, x, n, IX.kidr(i), kidr_in2(i, n, etwo), N.is_eq_lt(i, IX.kidr(i), IX.kidr_gt(i)), hlay, emr))
729	    case _ True{} Some{lv} True{} None{} _ False{}:
730	      Empty.absurd(DownOK(~A, ~cmp, d, n, tgt, fuel, x, pick_state2(~A, t, i, lv, True{}, None{}, left, False{})), slot_some_at(~A, t, i, x, n, IX.kidr(i), kidr_in2(i, n, etwo), N.is_eq_lt(i, IX.kidr(i), IX.kidr_gt(i)), hlay, emr))
731	    case _ True{} Some{+lv} True{} Some{+rv} True{} True{}:
732	      down_stop_ok(~A, ~cmp, d, n, tgt, fuel, t, i, x, hd, hi, hn, pf, hexc, g_both(~A, ~cmp, ~o, d, t, i, x, n, lv, rv, ehasl, etwo, eml, emr, eok, O.trans(~A, ~cmp, o, x, lv, rv, eok, eleft), hi, pf), hlay, hms)
733	    case 0n True{} Some{lv} True{} Some{rv} True{} False{}:
734	      Empty.absurd(DownOK(~A, ~cmp, d, n, tgt, 0n, x, DMv{t, i, lv, IX.kidl(i)}), fuel_out(i, n, ehasl, hfuel))
735	    case 1n+ +f True{} Some{+lv} True{} Some{rv} True{} False{}:
736	      down_carry(~A, ~cmp, d, n, tgt, f, t, i, x, lv, IX.kidl(i),
737	        down_step_eq(~A, ~cmp, d, n, f, t, i, x, lv, IX.kidl(i), hd, hi, N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), hn, pf),
738	        L.subst(DownS<A>, st => DownOK(~A, ~cmp, d, n, tgt, f, x, st), pick_state(~A, t2_of(~A, d, t, i, lv), IX.kidl(i), Nat.is_lt(IX.kidl(IX.kidl(i)), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x))))), dprobe(~A, ~cmp, n, IX.kidl(i), x, t2_of(~A, d, t, i, lv)),
739	          Equal.sym(DownS<A>, dprobe(~A, ~cmp, n, IX.kidl(i), x, t2_of(~A, d, t, i, lv)), pick_state(~A, t2_of(~A, d, t, i, lv), IX.kidl(i), Nat.is_lt(IX.kidl(IX.kidl(i)), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x))))), probe_shape(~A, ~cmp, n, IX.kidl(i), x, t2_of(~A, d, t, i, lv), Nat.is_lt(IX.kidl(IX.kidl(i)), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), {==}, Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~
740	          down_loop_go(~A, ~cmp, ~o, f, d, n, tgt, t2_of(~A, d, t, i, lv), IX.kidl(i), x, hd, N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), ehasl, hn,
741	            N.le_trans(n, IX.scale(f, Nat.double(1n+i)), IX.scale(f, 1n+IX.kidl(i)), hfuel, IX.scale_mono(f, Nat.double(1n+i), 1n+IX.kidl(i), IX.kid_double(i, IX.kidl(i), IX.par_kidl(i), IX.kidl_pos1(i)))),
742	            UPS.t2_perfect(~A, d, t, i, lv, pf),
743	            exc2_next(~A, ~cmp, ~o, d, n, t, i, x, lv, IX.kidl(i), IX.kidr(i), n, N.le_refl(n), ehasl, kidl_ne_kidr(i), IX.par_kidr(i), IX.kidr_pos1(i), IX.par_kidl(i), IX.kidl_pos1(i), N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), Inl{{==}}, Inr{{==}}, hi, pf, hexc, hkids, SL.kid_le_in(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.kidl(i), IX.kidr(i), kidr_in2(i, n, etwo), sib_mle(~A, ~cmp, t, i, lv, rv, eml, emr, eleft)), eml, eok),
744	            d1n_c(~A, ~cmp, ~o, d, t, i, x, lv, IX.kidl(i), IX.kidl(i), N.is_eq_refl(IX.kidl(i)), IX.par_kidl(i), IX.kidl_pos1(i), N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), hi, pf, eok),
745	            kids_next_d(~A, ~cmp, d, n, t, i, x, lv, IX.kidl(i), IX.par_kidl(i), IX.kidl_pos1(i), SL.ne_sym(IX.kidl(i), i, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i))), hi, pf, hexc, eml),
746	            lay_next_d(~A, d, n, t, i, x, lv, IX.kidl(i), n, N.le_refl(n), SL.ne_sym(IX.kidl(i), i, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i))), hi, N.lt_le_trans(IX.kidl(i), n, SC.pow2(d), ehasl, hn), pf, hlay),
747	            ms_next_d(~A, ~cmp, ~o, d, n, t, i, x, lv, IX.kidl(i), tgt, hin, ehasl, SL.ne_sym(IX.kidl(i), i, N.is_eq_lt(i, IX.kidl(i), IX.kidl_gt(i))), hi, pf, eml, hms),
748	            Nat.is_lt(IX.kidl(IX.kidl(i)), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), {==}, Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), Nat.is_lt(IX.kidl(IX.kidl(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidl(IX.kidl(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)))), {==})))
749	    case _ True{} Some{+lv} True{} Some{+rv} False{} True{}:
750	      down_stop_ok(~A, ~cmp, d, n, tgt, fuel, t, i, x, hd, hi, hn, pf, hexc, g_both(~A, ~cmp, ~o, d, t, i, x, n, lv, rv, ehasl, etwo, eml, emr, O.trans(~A, ~cmp, o, x, rv, lv, eok, O.total(~A, ~cmp, ~o, lv, rv, eleft)), eok, hi, pf), hlay, hms)
751	    case 0n True{} Some{lv} True{} Some{rv} False{} False{}:
752	      Empty.absurd(DownOK(~A, ~cmp, d, n, tgt, 0n, x, DMv{t, i, rv, IX.kidr(i)}), fuel_out(i, n, ehasl, hfuel))
753	    case 1n+ +f True{} Some{lv} True{} Some{+rv} False{} False{}:
754	      down_carry(~A, ~cmp, d, n, tgt, f, t, i, x, rv, IX.kidr(i),
755	        down_step_eq(~A, ~cmp, d, n, f, t, i, x, rv, IX.kidr(i), hd, hi, N.lt_le_trans(IX.kidr(i), n, SC.pow2(d), kidr_in2(i, n, etwo), hn), hn, pf),
756	        L.subst(DownS<A>, st => DownOK(~A, ~cmp, d, n, tgt, f, x, st), pick_state(~A, t2_of(~A, d, t, i, rv), IX.kidr(i), Nat.is_lt(IX.kidl(IX.kidr(i)), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x))))), dprobe(~A, ~cmp, n, IX.kidr(i), x, t2_of(~A, d, t, i, rv)),
757	          Equal.sym(DownS<A>, dprobe(~A, ~cmp, n, IX.kidr(i), x, t2_of(~A, d, t, i, rv)), pick_state(~A, t2_of(~A, d, t, i, rv), IX.kidr(i), Nat.is_lt(IX.kidl(IX.kidr(i)), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x))))), probe_shape(~A, ~cmp, n, IX.kidr(i), x, t2_of(~A, d, t, i, rv), Nat.is_lt(IX.kidl(IX.kidr(i)), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), {==}, Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~
758	          down_loop_go(~A, ~cmp, ~o, f, d, n, tgt, t2_of(~A, d, t, i, rv), IX.kidr(i), x, hd, N.lt_le_trans(IX.kidr(i), n, SC.pow2(d), kidr_in2(i, n, etwo), hn), kidr_in2(i, n, etwo), hn,
759	            N.le_trans(n, IX.scale(f, Nat.double(1n+i)), IX.scale(f, 1n+IX.kidr(i)), hfuel, IX.scale_mono(f, Nat.double(1n+i), 1n+IX.kidr(i), IX.kid_double(i, IX.kidr(i), IX.par_kidr(i), IX.kidr_pos1(i)))),
760	            UPS.t2_perfect(~A, d, t, i, rv, pf),
761	            exc2_next(~A, ~cmp, ~o, d, n, t, i, x, rv, IX.kidr(i), IX.kidl(i), n, N.le_refl(n), kidr_in2(i, n, etwo), SL.ne_sym(IX.kidr(i), IX.kidl(i), kidl_ne_kidr(i)), IX.par_kidl(i), IX.kidl_pos1(i), IX.par_kidr(i), IX.kidr_pos1(i), N.lt_le_trans(IX.kidr(i), n, SC.pow2(d), kidr_in2(i, n, etwo), hn), Inr{{==}}, Inl{{==}}, hi, pf, hexc, hkids, SL.kid_le_in(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.kidr(i), IX.kidl(i), ehasl, sib_mle_r(~A, ~cmp, ~o, t, i, lv, rv, eml, emr, eleft)), emr, eok),
762	            d1n_c(~A, ~cmp, ~o, d, t, i, x, rv, IX.kidr(i), IX.kidr(i), N.is_eq_refl(IX.kidr(i)), IX.par_kidr(i), IX.kidr_pos1(i), N.lt_le_trans(IX.kidr(i), n, SC.pow2(d), kidr_in2(i, n, etwo), hn), hi, pf, eok),
763	            kids_next_d(~A, ~cmp, d, n, t, i, x, rv, IX.kidr(i), IX.par_kidr(i), IX.kidr_pos1(i), SL.ne_sym(IX.kidr(i), i, N.is_eq_lt(i, IX.kidr(i), IX.kidr_gt(i))), hi, pf, hexc, emr),
764	            lay_next_d(~A, d, n, t, i, x, rv, IX.kidr(i), n, N.le_refl(n), SL.ne_sym(IX.kidr(i), i, N.is_eq_lt(i, IX.kidr(i), IX.kidr_gt(i))), hi, N.lt_le_trans(IX.kidr(i), n, SC.pow2(d), kidr_in2(i, n, etwo), hn), pf, hlay),
765	            ms_next_d(~A, ~cmp, ~o, d, n, t, i, x, rv, IX.kidr(i), tgt, hin, kidr_in2(i, n, etwo), SL.ne_sym(IX.kidr(i), i, N.is_eq_lt(i, IX.kidr(i), IX.kidr_gt(i))), hi, pf, emr, hms),
766	            Nat.is_lt(IX.kidl(IX.kidr(i)), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), {==}, Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), Nat.is_lt(IX.kidl(IX.kidr(i)), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidl(IX.kidr(i))), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x)))), {==})))
767	
768	# ---- the entry point ----
769	
770	def SiftDownOK(~A: Data, ~cmp: A -> A -> Cmp, d: Nat, n: Nat, tgt: List<&2, A>, fuel: Nat, t: AR.Tree<Maybe<&2, A>>, i: Nat, x: A) -> Type:
771	  Sigma<&1, &1, AR.Tree<Maybe<&2, A>>, t2 => {H.sift_down(~A, ~cmp, fuel, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)) == AR.thaw(Maybe<&2, A>, t2) : Array<Maybe<&2, A>>} & ({AR.perfect(Maybe<&2, A>, d, t2) == True{} : Bool} & ({SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t2), n) == True{} : Bool} & ({SL.lay(~A, AR.slots(Maybe<&2, A>, t2), n) == True{} : Bool} & {V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t2), n)) == tgt : List<&2, A>})))>
772	
773	def dsift_from_go(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +tgt: List<&2, A>, +fuel: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +t2: AR.Tree<Maybe<&2, A>>, +eq: {H.sift_down(~A, ~cmp, fuel, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)) == H.down_go(~A, ~cmp, fuel, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, i, x, t))) : Array<Maybe<&2, A>>}, rest: {H.down_go(~A, ~cmp, fuel, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, i, x, t))) == AR.thaw(Maybe<&2, A>, t2) : Array<Maybe<&2, A>>} & ({AR.perfect(Maybe<&2, A>, d, t2) == True{} : Bool} & ({SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t2), n) == True{} : Bool} & ({SL.lay(~A, AR.slots(Maybe<&2, A>, t2), n) == True{} : Bool} & {V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t2), n)) == tgt : List<&2, A>})))) -> SiftDownOK(~A, ~cmp, d, n, tgt, fuel, t, i, x):
774	  (e1, more) = rest
775	  (t2, (Equal.trans(Array<Maybe<&2, A>>, H.sift_down(~A, ~cmp, fuel, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)), H.down_go(~A, ~cmp, fuel, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, i, x, t))), AR.thaw(Maybe<&2, A>, t2), eq, e1), more))
776	
777	def dsift_from_loop(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +n: Nat, +tgt: List<&2, A>, +fuel: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +eq: {H.sift_down(~A, ~cmp, fuel, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)) == H.down_go(~A, ~cmp, fuel, U32.from_nat(n), x, dreal(~A, dprobe(~A, ~cmp, n, i, x, t))) : Array<Maybe<&2, A>>}, r: DownOK(~A, ~cmp, d, n, tgt, fuel, x, dprobe(~A, ~cmp, n, i, x, t))) -> SiftDownOK(~A, ~cmp, d, n, tgt, fuel, t, i, x):
778	  (t2, rest) = r
779	  dsift_from_go(~A, ~cmp, d, n, tgt, fuel, t, i, x, t2, eq, rest)
780	
781	# The hole at i is below the parent pair it inherits, every other pair holds,
782	# the two pairs below the hole are the only ones the loop has to fix, and the
783	# loop has enough fuel for n <= 2^fuel * (1 + i).
784	def sift_down_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +fuel: Nat, +d: Nat, +n: Nat, +tgt: List<&2, A>, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hn: {Nat.is_le(n, SC.pow2(d)) == True{} : Bool}, +hfuel: {Nat.is_le(n, IX.scale(fuel, 1n+i)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc2(~A, ~cmp, UPS.ulog(~A, t, i, x), n, i) == True{} : Bool}, +hpair: {SL.pair_ok(~A, ~cmp, UPS.ulog(~A, t, i, x), i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, AR.slots(Maybe<&2, A>, t), n, IX.par(i), i) == True{} : Bool}, +hlay: {SL.lay(~A, UPS.ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> SiftDownOK(~A, ~cmp, d, n, tgt, fuel, t, i, x):
785	  dsift_from_loop(~A, ~cmp, d, n, tgt, fuel, t, i, x,
786	    Equal.cong(H.Down<A>, Array<Maybe<&2, A>>, s => H.down_go(~A, ~cmp, fuel, U32.from_nat(n), x, s), H.down_probe(~A, ~cmp, U32.from_nat(n), U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)), dreal(~A, dprobe(~A, ~cmp, n, i, x, t)), dprobe_ok(~A, ~cmp, d, n, t, i, x, hd, hi, hn, pf)),
787	    L.subst(DownS<A>, st => DownOK(~A, ~cmp, d, n, tgt, fuel, x, st), pick_state(~A, t, i, Nat.is_lt(IX.kidl(i), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x))))), dprobe(~A, ~cmp, n, i, x, t),
788	      Equal.sym(DownS<A>, dprobe(~A, ~cmp, n, i, x, t), pick_state(~A, t, i, Nat.is_lt(IX.kidl(i), n), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x)), S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x))))),
789	        probe_shape(~A, ~cmp, n, i, x, t, Nat.is_lt(IX.kidl(i), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), {==}, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x)))), {==})),
790	      down_loop_go(~A, ~cmp, ~o, fuel, d, n, tgt, t, i, x, hd, hi, hin, hn, hfuel, pf, hexc, hpair, hkids, hlay, hms, Nat.is_lt(IX.kidl(i), n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), {==}, Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), {==}, S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x)), {==}, S.le(~A, ~cmp, x, pick_cv(~A, x, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), Nat.is_lt(IX.kidl(i), Nat.sub(n, 1n)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), S.le(~A, ~cmp, UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidl(i)), x), UPS.mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.kidr(i)), x)))), {==})))