proofs/containers/binary_heap/down.bend
bend-collections-laws-containers@1.0.0.0 · 790 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
10import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as H
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as IX
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/u32idx.bend as UX
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/slots.bend as SL
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as V
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/bag.bend as BG
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/multiset.bend as M
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/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
31type 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
35def 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
44def 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
51def 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
54def 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
61def 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
68def 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
77def 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
84def 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
89def 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
96def 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
99def 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
102def 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
106def 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
113def 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
116def 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
123def 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
132def 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
138def 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
153def 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
159def 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
169def 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
180def 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
183def 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
186def 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
189def 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
196def 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
205def 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
208def 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
215def 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
218def 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
225def 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
236def 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
243def 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
248def 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
257def 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
262def 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
265def 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
269def 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
276def 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
283def 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
290def 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
293def 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
300def 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
309def 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
312def 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
319def 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
323def 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
326def 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
333def 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
340def 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
347def 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
355def 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
364def 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
367def 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
375def 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
378def 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
383def 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
388def 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
393def 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
404def 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
412def 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
419def 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
427def 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
437def 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
452def 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
461def 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
467def 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
477def 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
481def 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
491def 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
502def 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
508def 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
512def 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
515def 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
518def 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
521def 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
528def 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
534def 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
545def 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
552def 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
556def 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
560def 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
566def 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
585def 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
594def 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
670def 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
675def 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
680def 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
687def 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
690def 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
695def 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
701def 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(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)))), {==})),
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(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, lv)), IX.kidr(IX.kidl(i))), x)))), {==})),
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(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, rv)), IX.kidr(IX.kidr(i))), x)))), {==})),
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
770def 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
773def 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
777def 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).
784def 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)))), {==})))