proofs/containers/binary_heap/up.bend
bend-collections-laws-containers@1.0.0.0 · 587 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
17
18# The sift-up loop, mirrored on the shadow tree, and the bridge that says the
19# executable loop state is the mirror of the shadow one.
20
21type UpS<-A: Data> is Data:
22 Stp{t: AR.Tree<Maybe<&2, A>>, i: Nat}
23 Mv{t: AR.Tree<Maybe<&2, A>>, i: Nat, pv: A, p: Nat}
24
25def ureal(~A: Data, s: UpS<A>) -> H.Up<A>:
26 match s:
27 case Stp{t, i}:
28 H.UStop{AR.thaw(Maybe<&2, A>, t), U32.from_nat(i)}
29 case Mv{t, i, pv, p}:
30 H.UMove{AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), pv, U32.from_nat(p)}
31
32# ---- the mirror of `H.up_probe` ----
33
34def udec(~A: Data, ~cmp: A -> A -> Cmp, t: AR.Tree<Maybe<&2, A>>, +i: Nat, pv: A, p: Nat, ok: Bool) -> UpS<A>:
35 match ok:
36 case True{}:
37 Stp{t, i}
38 case False{}:
39 Mv{t, i, pv, p}
40
41def umb(~A: Data, ~cmp: A -> A -> Cmp, t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, p: Nat, m: Maybe<&2, A>) -> UpS<A>:
42 match m:
43 case None{}:
44 Stp{t, i}
45 case Some{+pv}:
46 udec(~A, ~cmp, t, i, pv, p, S.le(~A, ~cmp, pv, x))
47
48def uroot(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, root: Bool) -> UpS<A>:
49 match root:
50 case True{}:
51 Stp{t, i}
52 case False{}:
53 umb(~A, ~cmp, t, i, x, IX.par(i), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)))
54
55def uprobe(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A) -> UpS<A>:
56 uroot(~A, ~cmp, t, i, x, Nat.is_eq(i, 0n))
57
58# ---- the bridge ----
59
60# the slot the implementation reads, as an `Array.get` result
61def get_slot(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +j: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(j)) == (AR.thaw(Maybe<&2, A>, t), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) : Array<Maybe<&2, A>> & Maybe<&2, A>}:
62 +ss = AR.slots(Maybe<&2, A>, t)
63 +ej = UX.nat_round(j, d, N.lt_le(d, 32n, hd), hj)
64 AR.get(Maybe<&2, A>, d, t, U32.from_nat(j), SL.slot(~A, ss, j), hd,
65 L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, j, U32.to_nat(U32.from_nat(j)), Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, ej), hj),
66 L.subst(Nat, z => {SC.nth(Maybe<&2, A>, ss, z) == Some{SL.slot(~A, ss, j)} : Maybe<&2, Maybe<&2, A>>}, j, U32.to_nat(U32.from_nat(j)), Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, ej),
67 SL.nth_slot(~A, ss, j, L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, A>, ss), Equal.sym(Nat, SC.length(Maybe<&2, A>, ss), SC.pow2(d), AR.slots_length(Maybe<&2, A>, d, t, pf)), hj))),
68 pf)
69
70def double_pos(+v: Nat, +h: {Nat.is_lt(0n, v) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.double(v)) == True{} : Bool}:
71 match v:
72 case 0n:
73 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_not_false(Nat.is_lt(0n, 0n), h, N.lt_irrefl(0n)))
74 case 1n+k:
75 {==}
76
77def pow2_pos(+d: Nat) -> {Nat.is_lt(0n, SC.pow2(d)) == True{} : Bool}:
78 match d:
79 case 0n:
80 {==}
81 case 1n+p:
82 double_pos(SC.pow2(p), pow2_pos(p))
83
84def pos_of(+i: Nat, +eb: {Nat.is_eq(i, 0n) == False{} : Bool}) -> {Nat.is_le(i, 0n) == False{} : Bool}:
85 match i:
86 case 0n:
87 Empty.absurd({Nat.is_le(0n, 0n) == False{} : Bool}, L.true_not_false(Nat.is_eq(0n, 0n), {==}, eb))
88 case 1n+k:
89 {==}
90
91def udec_ok(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +pv: A, +p: Nat, b: Bool) -> {H.up_dec(~A, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), pv, U32.from_nat(p), b) == ureal(~A, udec(~A, ~cmp, t, i, pv, p, b)) : H.Up<A>}:
92 match b:
93 case True{}:
94 {==}
95 case False{}:
96 {==}
97
98def umb_ok(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +p: Nat, m: Maybe<&2, A>) -> {H.up_mb(~A, ~cmp, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), x, U32.from_nat(p), m) == ureal(~A, umb(~A, ~cmp, t, i, x, p, m)) : H.Up<A>}:
99 match m:
100 case None{}:
101 {==}
102 case Some{+pv}:
103 udec_ok(~A, ~cmp, t, i, pv, p, S.le(~A, ~cmp, pv, x))
104
105# i > 0: the implementation reads the parent slot and the mirror reads the
106# same slot of the shadow's slot list.
107def uroot_false(~A: Data, ~cmp: A -> A -> Cmp, +d: 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}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {H.up_root(~A, ~cmp, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t), False{}) == ureal(~A, uroot(~A, ~cmp, t, i, x, False{})) : H.Up<A>}:
108 +hp = N.lt_trans(IX.par(i), i, SC.pow2(d), IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), hi)
109 %Equal.sym(U32, U32.shr(U32.sub(U32.from_nat(i), 1)), U32.from_nat(IX.par(i)), UX.par_bridge(i, d, N.lt_le(d, 32n, hd), hi, hpos)) : {H.up_slot(~A, ~cmp, U32.from_nat(i), x, _, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), _)) == ureal(~A, uroot(~A, ~cmp, t, i, x, False{})) : H.Up<A>}
110 %Equal.sym(Array<Maybe<&2, A>> & Maybe<&2, A>, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(IX.par(i))), (AR.thaw(Maybe<&2, A>, t), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i))), get_slot(~A, d, t, IX.par(i), hd, hp, pf)) : {H.up_slot(~A, ~cmp, U32.from_nat(i), x, U32.from_nat(IX.par(i)), _) == ureal(~A, uroot(~A, ~cmp, t, i, x, False{})) : H.Up<A>}
111 umb_ok(~A, ~cmp, t, i, x, IX.par(i), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)))
112
113def uroot_ok(~A: Data, ~cmp: A -> A -> Cmp, +d: 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}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(i, 0n) == b : Bool}) -> {H.up_root(~A, ~cmp, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t), b) == ureal(~A, uroot(~A, ~cmp, t, i, x, b)) : H.Up<A>}:
114 match b:
115 case True{}:
116 {==}
117 case False{}:
118 uroot_false(~A, ~cmp, d, t, i, x, hd, hi, N.lt_succ_le_succ(0n, i, N.not_le_lt(i, 0n, pos_of(i, eb))), pf)
119
120# is_eq(i, 0) = False gives 1 <= i
121def uprobe_ok(~A: Data, ~cmp: A -> A -> Cmp, +d: 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}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {H.up_probe(~A, ~cmp, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)) == ureal(~A, uprobe(~A, ~cmp, t, i, x)) : H.Up<A>}:
122 %Equal.sym(Bool, U32.is_eq(U32.from_nat(i), U32.from_nat(0n)), Nat.is_eq(i, 0n), UX.eq_bridge(i, 0n, d, N.lt_le(d, 32n, hd), hi, pow2_pos(d))) : {H.up_root(~A, ~cmp, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t), _) == ureal(~A, uprobe(~A, ~cmp, t, i, x)) : H.Up<A>}
123 uroot_ok(~A, ~cmp, d, t, i, x, hd, hi, pf, Nat.is_eq(i, 0n), {==})
124
125# ---- the logical slot list of a loop state ----
126#
127# While the loop runs, slot i of the block holds a value that is about to be
128# overwritten; the array the invariant talks about is the block with the
129# sifted value x at slot i.
130
131def ulog(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A) -> List<&2, Maybe<&2, A>>:
132 SC.update(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), i, Some{x})
133
134def mval(~A: Data, m: Maybe<&2, A>, d: A) -> A:
135 match m:
136 case None{}:
137 d
138 case Some{v}:
139 v
140
141# slot bookkeeping for a tree whose slot list has 2^d entries
142def in_range(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +j: Nat, +hj: {Nat.is_lt(j, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {Nat.is_lt(j, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t))) == True{} : Bool}:
143 L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, SC.pow2(d), SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), Equal.sym(Nat, SC.length(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t)), SC.pow2(d), AR.slots_length(Maybe<&2, A>, d, t, pf)), hj)
144
145def ulog_at(~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, ulog(~A, t, i, x), i) == Some{x} : Maybe<&2, A>}:
146 SL.slot_same(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, in_range(~A, d, t, i, hi, pf))
147
148def ulog_off(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {SL.slot(~A, ulog(~A, t, i, x), j) == SL.slot(~A, AR.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}:
149 SL.slot_other(~A, AR.slots(Maybe<&2, A>, t), i, j, Some{x}, ne)
150
151# ---- what the loop delivers ----
152
153def UpOK(~A: Data, ~cmp: A -> A -> Cmp, d: Nat, n: Nat, tgt: List<&2, A>, fuel: Nat, x: A, s: UpS<A>) -> Type:
154 Sigma<&1, &1, AR.Tree<Maybe<&2, A>>, t2 => {H.up_go(~A, ~cmp, fuel, x, ureal(~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>})))>
155
156# the block after the last write, and the fact that its slot list is the
157# logical array the invariant is about
158def set_tree(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A) -> AR.Tree<Maybe<&2, A>>:
159 AR.upd(Maybe<&2, A>, d, t, i, Some{x})
160
161def set_slots(~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}) -> {AR.slots(Maybe<&2, A>, set_tree(~A, d, t, i, x)) == ulog(~A, t, i, x) : List<&2, Maybe<&2, A>>}:
162 AR.upd_slots(Maybe<&2, A>, d, t, i, Some{x}, hi, pf)
163
164def set_eq(~A: Data, +d: 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}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {Array.set(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), Some{x}) == AR.thaw(Maybe<&2, A>, set_tree(~A, d, t, i, x)) : Array<Maybe<&2, A>>}:
165 +ss = AR.slots(Maybe<&2, A>, t)
166 +ei = UX.nat_round(i, d, N.lt_le(d, 32n, hd), hi)
167 %ei : {Array.set(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), Some{x}) == AR.thaw(Maybe<&2, A>, AR.upd(Maybe<&2, A>, d, t, _, Some{x})) : Array<Maybe<&2, A>>}
168 AR.set(Maybe<&2, A>, d, t, U32.from_nat(i), Some{x}, SL.slot(~A, ss, i), hd,
169 L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, ei), hi),
170 L.subst(Nat, z => {SC.nth(Maybe<&2, A>, ss, z) == Some{SL.slot(~A, ss, i)} : Maybe<&2, Maybe<&2, A>>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, ei), SL.nth_slot(~A, ss, i, in_range(~A, d, t, i, hi, pf))),
171 pf)
172
173# ---- the loop stops: the sifted value is written where the hole is ----
174
175def up_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.up_go(~A, ~cmp, fuel, x, ureal(~A, Stp{t, i})) == AR.thaw(Maybe<&2, A>, set_tree(~A, d, t, i, x)) : Array<Maybe<&2, A>>}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpair: {SL.pair_ok(~A, ~cmp, ulog(~A, t, i, x), i) == True{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hlay: {SL.lay(~A, ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> UpOK(~A, ~cmp, d, n, tgt, fuel, x, Stp{t, i}):
176 +es = set_slots(~A, d, t, i, x, hi, pf)
177 (set_tree(~A, d, t, i, x),
178 (eq,
179 (AR.upd_perfect(Maybe<&2, A>, d, t, i, Some{x}, pf),
180 (L.subst(List<&2, Maybe<&2, A>>, ss => {SL.ho_upto(~A, ~cmp, ss, n) == True{} : Bool}, ulog(~A, t, i, x), AR.slots(Maybe<&2, A>, set_tree(~A, d, t, i, x)), Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, set_tree(~A, d, t, i, x)), ulog(~A, t, i, x), es),
181 SL.ho_of_exc(~A, ~cmp, ulog(~A, t, i, x), n, i, hexc, hpair)),
182 (L.subst(List<&2, Maybe<&2, A>>, ss => {SL.lay(~A, ss, n) == True{} : Bool}, ulog(~A, t, i, x), AR.slots(Maybe<&2, A>, set_tree(~A, d, t, i, x)), Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, set_tree(~A, d, t, i, x)), ulog(~A, t, i, x), es), hlay),
183 L.subst(List<&2, Maybe<&2, A>>, ss => {V.msort(~A, ~cmp, V.vals(~A, ss, n)) == tgt : List<&2, A>}, ulog(~A, t, i, x), AR.slots(Maybe<&2, A>, set_tree(~A, d, t, i, x)), Equal.sym(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, set_tree(~A, d, t, i, x)), ulog(~A, t, i, x), es), hms))))))
184
185def up_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}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpair: {SL.pair_ok(~A, ~cmp, ulog(~A, t, i, x), i) == True{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hlay: {SL.lay(~A, ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> UpOK(~A, ~cmp, d, n, tgt, fuel, x, Stp{t, i}):
186 match fuel:
187 case 0n:
188 up_stop_mk(~A, ~cmp, d, n, tgt, 0n, t, i, x, set_eq(~A, d, t, i, x, hd, hi, pf), hi, pf, hpair, hexc, hlay, hms)
189 case 1n+f:
190 up_stop_mk(~A, ~cmp, d, n, tgt, 1n+f, t, i, x, set_eq(~A, d, t, i, x, hd, hi, pf), hi, pf, hpair, hexc, hlay, hms)
191
192# ---- one step of the loop: the parent value moves down into the hole ----
193#
194# `t2` is the block after that write and the hole is now at par(i); `u2` is
195# the logical array of the new state. The three lemmas below say what each of
196# its slots holds.
197
198def t2_of(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +pv: A) -> AR.Tree<Maybe<&2, A>>:
199 set_tree(~A, d, t, i, pv)
200
201def u2_of(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A) -> List<&2, Maybe<&2, A>>:
202 ulog(~A, t2_of(~A, d, t, i, pv), IX.par(i), x)
203
204def par_ne(+i: Nat, +hpos: {Nat.is_le(1n, i) == True{} : Bool}) -> {Nat.is_eq(IX.par(i), i) == False{} : Bool}:
205 N.is_eq_lt(IX.par(i), i, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)))
206
207def par_lt_d(+d: Nat, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}) -> {Nat.is_lt(IX.par(i), SC.pow2(d)) == True{} : Bool}:
208 N.lt_trans(IX.par(i), i, SC.pow2(d), IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), hi)
209
210def t2_perfect(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +pv: A, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {AR.perfect(Maybe<&2, A>, d, t2_of(~A, d, t, i, pv)) == True{} : Bool}:
211 AR.upd_perfect(Maybe<&2, A>, d, t, i, Some{pv}, pf)
212
213def u2_at_p(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(i)) == Some{x} : Maybe<&2, A>}:
214 ulog_at(~A, d, t2_of(~A, d, t, i, pv), IX.par(i), x, par_lt_d(d, i, hi, hpos), t2_perfect(~A, d, t, i, pv, pf))
215
216def u2_at_i(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {SL.slot(~A, u2_of(~A, d, t, i, x, pv), i) == Some{pv} : Maybe<&2, A>}:
217 Equal.trans(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), i), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), i), Some{pv},
218 ulog_off(~A, t2_of(~A, d, t, i, pv), IX.par(i), x, i, par_ne(i, hpos)),
219 Equal.trans(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), i), SL.slot(~A, ulog(~A, t, i, pv), i), Some{pv},
220 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, pv)), ulog(~A, t, i, pv), set_slots(~A, d, t, i, pv, hi, pf)),
221 ulog_at(~A, d, t, i, pv, hi, pf)))
222
223def u2_off(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +j: Nat, +hji: {Nat.is_eq(i, j) == False{} : Bool}, +hjp: {Nat.is_eq(IX.par(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, u2_of(~A, d, t, i, x, pv), j) == SL.slot(~A, AR.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}:
224 Equal.trans(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j),
225 ulog_off(~A, t2_of(~A, d, t, i, pv), IX.par(i), x, j, hjp),
226 Equal.trans(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), j), SL.slot(~A, ulog(~A, t, i, pv), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j),
227 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, pv)), ulog(~A, t, i, pv), set_slots(~A, d, t, i, pv, hi, pf)),
228 ulog_off(~A, t, i, pv, j, hji)))
229
230# the same three for the CURRENT logical array
231def u1_at_p(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}) -> {SL.slot(~A, ulog(~A, t, i, x), IX.par(i)) == Some{pv} : Maybe<&2, A>}:
232 Equal.trans(Maybe<&2, A>, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), Some{pv},
233 ulog_off(~A, t, i, x, IX.par(i), SL.ne_sym(i, IX.par(i), par_ne(i, hpos))),
234 hpv)
235
236# ---- the pair condition at an index that has a parent ----
237
238def pair_ok_pos(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, i: Nat, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +h: {SL.mle(~A, ~cmp, SL.slot(~A, ss, IX.par(i)), SL.slot(~A, ss, i)) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, ss, i) == True{} : Bool}:
239 match i:
240 case 0n:
241 Empty.absurd({SL.pair_ok(~A, ~cmp, ss, 0n) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), hpos, {==}))
242 case 1n+k:
243 h
244
245def pair_ok_val(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, i: Nat, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +h: {SL.pair_ok(~A, ~cmp, ss, i) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, ss, IX.par(i)), SL.slot(~A, ss, i)) == True{} : Bool}:
246 match i:
247 case 0n:
248 Empty.absurd({SL.mle(~A, ~cmp, SL.slot(~A, ss, IX.par(0n)), SL.slot(~A, ss, 0n)) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), hpos, {==}))
249 case 1n+k:
250 h
251
252# j >= 1 whenever j is not 0
253def pos_of_ne(+j: Nat, +h: {Nat.is_eq(j, 0n) == False{} : Bool}) -> {Nat.is_le(1n, j) == True{} : Bool}:
254 match j:
255 case 0n:
256 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.true_not_false(Nat.is_eq(0n, 0n), {==}, h))
257 case 1n+k:
258 N.zero_le(k)
259
260# ---- the heap order of the next state, one index at a time ----
261#
262# case i the hole's old index now holds the parent value pv, and the
263# new hole above it holds x, with x <= pv because the sift moved
264# case kid a child of the old hole: pv is not larger than it, which is
265# exactly the invariant H2 the state carries
266# case sib a child of the new hole other than the old one: x <= pv and pv
267# was not larger than it
268# case far an index none of whose two slots changed
269
270def h1n_i_mle(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(i)), SL.slot(~A, u2_of(~A, d, t, i, x, pv), i)) == True{} : Bool}:
271 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(i)), Some{x}, u2_at_p(~A, d, t, i, x, pv, hi, hpos, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, u2_of(~A, d, t, i, x, pv), i)) == True{} : Bool}
272 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), i), Some{pv}, u2_at_i(~A, d, t, i, x, pv, hi, hpos, pf)) : {SL.mle(~A, ~cmp, Some{x}, _) == True{} : Bool}
273 O.total(~A, ~cmp, ~o, pv, x, hnle)
274
275def h1n_i(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +j: Nat, +ej: {Nat.is_eq(j, i) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
276 L.subst(Nat, z => {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), z) == True{} : Bool}, i, j, Equal.sym(Nat, j, i, N.eq_from_is_eq(j, i, ej)),
277 pair_ok_pos(~A, ~cmp, u2_of(~A, d, t, i, x, pv), i, hpos, h1n_i_mle(~A, ~cmp, ~o, d, t, i, x, pv, hi, hpos, pf, hnle)))
278
279def kid_at(+i: Nat, +j: Nat, +epj: {IX.par(j) == i : Nat}, e: {j == IX.kidl(IX.par(j)) : Nat} | {j == IX.kidr(IX.par(j)) : Nat}) -> {j == IX.kidl(i) : Nat} | {j == IX.kidr(i) : Nat}:
280 match e:
281 case Inl{ej}:
282 Inl{L.subst(Nat, z => {j == IX.kidl(z) : Nat}, IX.par(j), i, epj, ej)}
283 case Inr{ej}:
284 Inr{L.subst(Nat, z => {j == IX.kidr(z) : Nat}, IX.par(j), i, epj, ej)}
285
286# rewrite H2 from the logical array to the block
287def h1n_kid_fix(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +j: Nat, +hjne: {Nat.is_eq(i, j) == False{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +h: {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), SL.slot(~A, ulog(~A, t, i, x), j)) == True{} : Bool}) -> {SL.mle(~A, ~cmp, Some{pv}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}:
288 %u1_at_p(~A, t, i, x, pv, hpos, hpv) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}
289 %ulog_off(~A, t, i, x, j, hjne) : {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), _) == True{} : Bool}
290 h
291
292# pv is not larger than a child of the old hole (this is H2)
293def h1n_kid_mle(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +hjne: {Nat.is_eq(i, j) == False{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}, e: {j == IX.kidl(i) : Nat} | {j == IX.kidr(i) : Nat}) -> {SL.mle(~A, ~cmp, Some{pv}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}:
294 match e:
295 case Inl{+ej}:
296 h1n_kid_fix(~A, ~cmp, t, i, x, pv, j, hjne, hpos, hpv,
297 L.subst(Nat, z => {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), SL.slot(~A, ulog(~A, t, i, x), z)) == True{} : Bool}, IX.kidl(i), j, Equal.sym(Nat, j, IX.kidl(i), ej),
298 SL.kid_le_at(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), IX.kidl(i), L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, j, IX.kidl(i), ej, hjn),
299 L.and_left(SL.kid_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), IX.kidl(i)), SL.kid_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), IX.kidr(i)), hkids))))
300 case Inr{+ej}:
301 h1n_kid_fix(~A, ~cmp, t, i, x, pv, j, hjne, hpos, hpv,
302 L.subst(Nat, z => {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), SL.slot(~A, ulog(~A, t, i, x), z)) == True{} : Bool}, IX.kidr(i), j, Equal.sym(Nat, j, IX.kidr(i), ej),
303 SL.kid_le_at(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), IX.kidr(i), L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, j, IX.kidr(i), ej, hjn),
304 L.and_right(SL.kid_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), IX.kidl(i)), SL.kid_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), IX.kidr(i)), hkids))))
305
306def par_lt_kid(+i: Nat, +j: Nat, +epj: {IX.par(j) == i : Nat}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}) -> {Nat.is_lt(IX.par(i), j) == True{} : Bool}:
307 N.lt_trans(IX.par(i), i, j, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)),
308 L.subst(Nat, z => {Nat.is_lt(z, j) == True{} : Bool}, IX.par(j), i, epj, IX.par_lt(j, N.succ_le_lt(0n, j, hjpos))))
309def h1n_kid_goal(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +epj: {IX.par(j) == i : Nat}, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +h: {SL.mle(~A, ~cmp, Some{pv}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(j)), SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}:
310 %Equal.sym(Nat, IX.par(j), i, epj) : {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), _), SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}
311 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), i), Some{pv}, u2_at_i(~A, d, t, i, x, pv, hi, hpos, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}
312 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j), u2_off(~A, d, t, i, x, pv, j, hij, hpij, hi, pf)) : {SL.mle(~A, ~cmp, Some{pv}, _) == True{} : Bool}
313 h
314def h1n_kid(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +hjne: {Nat.is_eq(j, i) == False{} : Bool}, +epj: {IX.par(j) == i : Nat}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
315 +hij = SL.ne_sym(i, j, hjne)
316 +hpij = N.is_eq_lt(IX.par(i), j, par_lt_kid(i, j, epj, hjpos, hpos))
317 pair_ok_pos(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j, hjpos,
318 h1n_kid_goal(~A, ~cmp, d, t, i, x, pv, n, j, epj, hij, hpij, hjn, hi, hpos, pf, hpv,
319 h1n_kid_mle(~A, ~cmp, t, i, x, pv, n, j, hij, hjn, hpos, hpv, hkids, kid_at(i, j, epj, IX.kid_split(j, N.succ_le_lt(0n, j, hjpos))))))
320
321def h1n_old(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +j: Nat, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +epj: {IX.par(j) == IX.par(i) : Nat}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +h: {SL.pair_ok(~A, ~cmp, ulog(~A, t, i, x), j) == True{} : Bool}) -> {SL.mle(~A, ~cmp, Some{pv}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}:
322 +hm = pair_ok_val(~A, ~cmp, ulog(~A, t, i, x), j, hjpos, h)
323 %ulog_off(~A, t, i, x, j, hij) : {SL.mle(~A, ~cmp, Some{pv}, _) == True{} : Bool}
324 %u1_at_p(~A, t, i, x, pv, hpos, hpv) : {SL.mle(~A, ~cmp, _, SL.slot(~A, ulog(~A, t, i, x), j)) == True{} : Bool}
325 %epj : {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), _), SL.slot(~A, ulog(~A, t, i, x), j)) == True{} : Bool}
326 hm
327def h1n_sib_goal(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +j: Nat, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +epj: {IX.par(j) == IX.par(i) : Nat}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +h: {SL.mle(~A, ~cmp, Some{pv}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(j)), SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}:
328 %Equal.sym(Nat, IX.par(j), IX.par(i), epj) : {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), _), SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}
329 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(i)), Some{x}, u2_at_p(~A, d, t, i, x, pv, hi, hpos, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}
330 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j), u2_off(~A, d, t, i, x, pv, j, hij, hpij, hi, pf)) : {SL.mle(~A, ~cmp, Some{x}, _) == True{} : Bool}
331 SL.mle_trans(~A, ~cmp, ~o, Some{x}, pv, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j), O.total(~A, ~cmp, ~o, pv, x, hnle), h)
332def h1n_sib(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +epj: {IX.par(j) == IX.par(i) : Nat}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
333 pair_ok_pos(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j, hjpos,
334 h1n_sib_goal(~A, ~cmp, ~o, d, t, i, x, pv, j, hij, hpij, epj, hi, hpos, pf, hnle,
335 h1n_old(~A, ~cmp, t, i, x, pv, j, hij, epj, hjpos, hpos, hpv, SL.exc_at(~A, ~cmp, ulog(~A, t, i, x), n, i, j, hexc, hjn, SL.ne_sym(j, i, hij)))))
336def h1n_far_goal(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +j: Nat, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +hipj: {Nat.is_eq(i, IX.par(j)) == False{} : Bool}, +hppj: {Nat.is_eq(IX.par(i), IX.par(j)) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +h: {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(j)), SL.slot(~A, ulog(~A, t, i, x), j)) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(j)), SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}:
337 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(j)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(j)), u2_off(~A, d, t, i, x, pv, IX.par(j), hipj, hppj, hi, pf)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, u2_of(~A, d, t, i, x, pv), j)) == True{} : Bool}
338 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), j), SL.slot(~A, AR.slots(Maybe<&2, A>, t), j), u2_off(~A, d, t, i, x, pv, j, hij, hpij, hi, pf)) : {SL.mle(~A, ~cmp, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(j)), _) == True{} : Bool}
339 %ulog_off(~A, t, i, x, IX.par(j), hipj) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), j)) == True{} : Bool}
340 %ulog_off(~A, t, i, x, j, hij) : {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(j)), _) == True{} : Bool}
341 h
342def h1n_far(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +hipj: {Nat.is_eq(i, IX.par(j)) == False{} : Bool}, +hppj: {Nat.is_eq(IX.par(i), IX.par(j)) == False{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hjn: {Nat.is_lt(j, 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_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
343 +hm = pair_ok_val(~A, ~cmp, ulog(~A, t, i, x), j, hjpos, SL.exc_at(~A, ~cmp, ulog(~A, t, i, x), n, i, j, hexc, hjn, SL.ne_sym(j, i, hij)))
344 pair_ok_pos(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j, hjpos,
345 h1n_far_goal(~A, ~cmp, d, t, i, x, pv, j, hij, hpij, hipj, hppj, hi, pf, hm))
346
347# ---- the four cases, dispatched on the index ----
348
349def h1_next_s(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +hipj: {Nat.is_eq(i, IX.par(j)) == False{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, b3: Bool, +eb3: {Nat.is_eq(IX.par(i), IX.par(j)) == b3 : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
350 match b3:
351 case True{}:
352 h1n_sib(~A, ~cmp, ~o, d, t, i, x, pv, n, j, hij, hpij, Equal.sym(Nat, IX.par(i), IX.par(j), N.eq_from_is_eq(IX.par(i), IX.par(j), eb3)), hjpos, hjn, hi, hpos, pf, hpv, hnle, hexc)
353 case False{}:
354 h1n_far(~A, ~cmp, d, t, i, x, pv, n, j, hij, hpij, hipj, eb3, hjpos, hjn, hi, pf, hexc)
355
356def h1_next_p(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +hji: {Nat.is_eq(j, i) == False{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}, b2: Bool, +eb2: {Nat.is_eq(IX.par(j), i) == b2 : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
357 match b2:
358 case True{}:
359 h1n_kid(~A, ~cmp, d, t, i, x, pv, n, j, hji, N.eq_from_is_eq(IX.par(j), i, eb2), hjpos, hjn, hi, hpos, pf, hpv, hkids)
360 case False{}:
361 h1_next_s(~A, ~cmp, ~o, d, t, i, x, pv, n, j, SL.ne_sym(i, j, hji), hpij, SL.ne_sym(i, IX.par(j), eb2), hjpos, hjn, hi, hpos, pf, hpv, hnle, hexc, Nat.is_eq(IX.par(i), IX.par(j)), {==})
362
363def h1_next_pos(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +j: Nat, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +hjpos: {Nat.is_le(1n, j) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}, b1: Bool, +eb1: {Nat.is_eq(j, i) == b1 : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
364 match b1:
365 case True{}:
366 h1n_i(~A, ~cmp, ~o, d, t, i, x, pv, j, eb1, hi, hpos, pf, hnle)
367 case False{}:
368 h1_next_p(~A, ~cmp, ~o, d, t, i, x, pv, n, j, eb1, hpij, hjpos, hjn, hi, hpos, pf, hpv, hnle, hexc, hkids, Nat.is_eq(IX.par(j), i), {==})
369
370def h1_next_at(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, j: Nat, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +hpij: {Nat.is_eq(IX.par(i), j) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j) == True{} : Bool}:
371 match j:
372 case 0n:
373 {==}
374 case 1n+ +m:
375 h1_next_pos(~A, ~cmp, ~o, d, t, i, x, pv, n, 1n+m, hpij, N.zero_le(m), hjn, hi, hpos, pf, hpv, hnle, hexc, hkids, Nat.is_eq(1n+m, i), {==})
376
377# ---- H2 for the next state: the new hole's parent is not larger than the
378# new hole's children ----
379
380def h2_key_root(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +e: {IX.par(i) == 0n : Nat}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), Some{pv}) == True{} : Bool}:
381 +at0 = L.subst(Nat, z => {SL.slot(~A, u2_of(~A, d, t, i, x, pv), z) == Some{x} : Maybe<&2, A>}, IX.par(i), 0n, e, u2_at_p(~A, d, t, i, x, pv, hi, hpos, pf))
382 %Equal.sym(Nat, IX.par(i), 0n, e) : {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(_)), Some{pv}) == True{} : Bool}
383 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), 0n), Some{x}, at0) : {SL.mle(~A, ~cmp, _, Some{pv}) == True{} : Bool}
384 O.total(~A, ~cmp, ~o, pv, x, hnle)
385
386def h2_key_deep(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +e: {Nat.is_eq(IX.par(i), 0n) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), Some{pv}) == True{} : Bool}:
387 +ppos = pos_of_ne(IX.par(i), e)
388 +hppi = N.lt_trans(IX.par(IX.par(i)), IX.par(i), i, IX.par_lt(IX.par(i), N.succ_le_lt(0n, IX.par(i), ppos)), IX.par_lt(i, N.succ_le_lt(0n, i, hpos)))
389 +hm = pair_ok_val(~A, ~cmp, ulog(~A, t, i, x), IX.par(i), ppos, SL.exc_at(~A, ~cmp, ulog(~A, t, i, x), n, i, IX.par(i), hexc, N.lt_trans(IX.par(i), i, n, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), hin), par_ne(i, hpos)))
390 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(IX.par(i))), u2_off(~A, d, t, i, x, pv, IX.par(IX.par(i)), SL.ne_sym(i, IX.par(IX.par(i)), N.is_eq_lt(IX.par(IX.par(i)), i, hppi)), SL.ne_sym(IX.par(i), IX.par(IX.par(i)), N.is_eq_lt(IX.par(IX.par(i)), IX.par(i), IX.par_lt(IX.par(i), N.succ_le_lt(0n, IX.par(i), ppos)))), hi, pf)) : {SL.mle(~A, ~cmp, _, Some{pv}) == True{} : Bool}
391 %ulog_off(~A, t, i, x, IX.par(IX.par(i)), SL.ne_sym(i, IX.par(IX.par(i)), N.is_eq_lt(IX.par(IX.par(i)), i, hppi))) : {SL.mle(~A, ~cmp, _, Some{pv}) == True{} : Bool}
392 %u1_at_p(~A, t, i, x, pv, hpos, hpv) : {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(IX.par(i))), _) == True{} : Bool}
393 hm
394
395
396def h2_key(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(IX.par(i), 0n) == b : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), Some{pv}) == True{} : Bool}:
397 match b:
398 case True{}:
399 h2_key_root(~A, ~cmp, ~o, d, t, i, x, pv, N.eq_from_is_eq(IX.par(i), 0n, eb), hi, hpos, pf, hnle)
400 case False{}:
401 h2_key_deep(~A, ~cmp, d, t, i, x, pv, n, eb, hi, hin, hpos, pf, hpv, hexc)
402
403def kid_mle_same(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +c: Nat, +eb: {Nat.is_eq(c, i) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +key: {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), Some{pv}) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), SL.slot(~A, u2_of(~A, d, t, i, x, pv), c)) == True{} : Bool}:
404 %Equal.sym(Nat, c, i, N.eq_from_is_eq(c, i, eb)) : {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), SL.slot(~A, u2_of(~A, d, t, i, x, pv), _)) == True{} : Bool}
405 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), i), Some{pv}, u2_at_i(~A, d, t, i, x, pv, hi, hpos, pf)) : {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), _) == True{} : Bool}
406 key
407def kid_mle_other(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +c: Nat, +epc: {IX.par(c) == IX.par(i) : Nat}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}, +hcn: {Nat.is_lt(c, n) == True{} : Bool}, +eb: {Nat.is_eq(c, i) == False{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +key: {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), Some{pv}) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), SL.slot(~A, u2_of(~A, d, t, i, x, pv), c)) == True{} : Bool}:
408 +hpic = N.is_eq_lt(IX.par(i), c, L.subst(Nat, z => {Nat.is_lt(z, c) == True{} : Bool}, IX.par(c), IX.par(i), epc, IX.par_lt(c, N.succ_le_lt(0n, c, hcpos))))
409 +hb = h1n_old(~A, ~cmp, t, i, x, pv, c, SL.ne_sym(i, c, eb), epc, hcpos, hpos, hpv, SL.exc_at(~A, ~cmp, ulog(~A, t, i, x), n, i, c, hexc, hcn, eb))
410 %Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), c), SL.slot(~A, AR.slots(Maybe<&2, A>, t), c), u2_off(~A, d, t, i, x, pv, c, SL.ne_sym(i, c, eb), hpic, hi, pf)) : {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), _) == True{} : Bool}
411 SL.mle_trans(~A, ~cmp, ~o, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), pv, SL.slot(~A, AR.slots(Maybe<&2, A>, t), c), key, hb)
412def kid_mle(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +c: Nat, +epc: {IX.par(c) == IX.par(i) : Nat}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}, +hcn: {Nat.is_lt(c, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(c, i) == b : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(IX.par(i))), SL.slot(~A, u2_of(~A, d, t, i, x, pv), c)) == True{} : Bool}:
413 match b:
414 case True{}:
415 kid_mle_same(~A, ~cmp, d, t, i, x, pv, c, eb, hi, hpos, pf, h2_key(~A, ~cmp, ~o, d, t, i, x, pv, n, hi, hin, hpos, pf, hpv, hnle, hexc, Nat.is_eq(IX.par(i), 0n), {==}))
416 case False{}:
417 kid_mle_other(~A, ~cmp, ~o, d, t, i, x, pv, n, c, epc, hcpos, hcn, eb, hi, hpos, pf, hpv, hexc, h2_key(~A, ~cmp, ~o, d, t, i, x, pv, n, hi, hin, hpos, pf, hpv, hnle, hexc, Nat.is_eq(IX.par(i), 0n), {==}))
418
419# H2 for the next state: both children of the new hole
420def kid_next(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +c: Nat, +epc: {IX.par(c) == IX.par(i) : Nat}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_lt(c, n) == b : Bool}) -> {SL.kid_le(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), c) == True{} : Bool}:
421 match b:
422 case False{}:
423 SL.kid_le_out(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), c, eb)
424 case True{}:
425 SL.kid_le_in(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), c, eb,
426 kid_mle(~A, ~cmp, ~o, d, t, i, x, pv, n, c, epc, hcpos, eb, hi, hin, hpos, pf, hpv, hnle, hexc, Nat.is_eq(c, i), {==}))
427
428def kids_next(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}) -> {SL.kids_le(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), IX.par(i)) == True{} : Bool}:
429 L.and_intro(SL.kid_le(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), IX.kidl(IX.par(i))), SL.kid_le(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), IX.kidr(IX.par(i))),
430 kid_next(~A, ~cmp, ~o, d, t, i, x, pv, n, IX.kidl(IX.par(i)), IX.par_kidl(IX.par(i)), IX.kidl_pos1(IX.par(i)), hi, hin, hpos, pf, hpv, hnle, hexc, Nat.is_lt(IX.kidl(IX.par(i)), n), {==}),
431 kid_next(~A, ~cmp, ~o, d, t, i, x, pv, n, IX.kidr(IX.par(i)), IX.par_kidr(IX.par(i)), IX.kidr_pos1(IX.par(i)), hi, hin, hpos, pf, hpv, hnle, hexc, Nat.is_lt(IX.kidr(IX.par(i)), n), {==}))
432
433# ---- the three remaining invariants of the next state ----
434
435def skip_next(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +m: Nat, +hmn: {Nat.is_lt(m, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, IX.par(i)) == b : Bool}) -> {SL.pair_skip(~A, ~cmp, u2_of(~A, d, t, i, x, pv), m, IX.par(i)) == True{} : Bool}:
436 match b:
437 case True{}:
438 SL.skip_eq(~A, ~cmp, u2_of(~A, d, t, i, x, pv), m, IX.par(i), eb)
439 case False{}:
440 SL.skip_ne(~A, ~cmp, u2_of(~A, d, t, i, x, pv), m, IX.par(i), eb,
441 h1_next_at(~A, ~cmp, ~o, d, t, i, x, pv, n, m, hmn, SL.ne_sym(IX.par(i), m, eb), hi, hpos, pf, hpv, hnle, hexc, hkids))
442
443def exc_next(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hnle: {S.le(~A, ~cmp, pv, x) == False{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}) -> {SL.ho_exc(~A, ~cmp, u2_of(~A, d, t, i, x, pv), k, IX.par(i)) == True{} : Bool}:
444 match k:
445 case 0n:
446 {==}
447 case 1n+ +m:
448 L.and_intro(SL.pair_skip(~A, ~cmp, u2_of(~A, d, t, i, x, pv), m, IX.par(i)), SL.ho_exc(~A, ~cmp, u2_of(~A, d, t, i, x, pv), m, IX.par(i)),
449 skip_next(~A, ~cmp, ~o, d, t, i, x, pv, n, m, N.lt_le_trans(m, 1n+m, n, N.lt_succ(m), hk), hi, hpos, pf, hpv, hnle, hexc, hkids, Nat.is_eq(m, IX.par(i)), {==}),
450 exc_next(~A, ~cmp, ~o, d, t, i, x, pv, n, m, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), hi, hpos, pf, hpv, hnle, hexc, hkids))
451
452def some_of_eq(~A: Data, m: Maybe<&2, A>, +v: A, +e: {m == Some{v} : Maybe<&2, A>}) -> {Maybe.is_some(&2, A, m) == True{} : Bool}:
453 L.subst(Maybe<&2, A>, w => {Maybe.is_some(&2, A, w) == True{} : Bool}, Some{v}, m, Equal.sym(Maybe<&2, A>, m, Some{v}, e), {==})
454
455def some_next(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +m: Nat, +hmn: {Nat.is_lt(m, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hlay: {SL.lay(~A, ulog(~A, t, i, x), n) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, IX.par(i)) == b : Bool}, c: Bool, +ec: {Nat.is_eq(m, i) == c : Bool}) -> {Maybe.is_some(&2, A, SL.slot(~A, u2_of(~A, d, t, i, x, pv), m)) == True{} : Bool}:
456 match b c:
457 case True{} _:
458 L.subst(Nat, z => {Maybe.is_some(&2, A, SL.slot(~A, u2_of(~A, d, t, i, x, pv), z)) == True{} : Bool}, IX.par(i), m, Equal.sym(Nat, m, IX.par(i), N.eq_from_is_eq(m, IX.par(i), eb)),
459 some_of_eq(~A, SL.slot(~A, u2_of(~A, d, t, i, x, pv), IX.par(i)), x, u2_at_p(~A, d, t, i, x, pv, hi, hpos, pf)))
460 case False{} True{}:
461 L.subst(Nat, z => {Maybe.is_some(&2, A, SL.slot(~A, u2_of(~A, d, t, i, x, pv), z)) == True{} : Bool}, i, m, Equal.sym(Nat, m, i, N.eq_from_is_eq(m, i, ec)),
462 some_of_eq(~A, SL.slot(~A, u2_of(~A, d, t, i, x, pv), i), pv, u2_at_i(~A, d, t, i, x, pv, hi, hpos, pf)))
463 case False{} False{}:
464 L.subst(Maybe<&2, A>, w => {Maybe.is_some(&2, A, w) == True{} : Bool}, SL.slot(~A, ulog(~A, t, i, x), m), SL.slot(~A, u2_of(~A, d, t, i, x, pv), m),
465 Equal.trans(Maybe<&2, A>, SL.slot(~A, ulog(~A, t, i, x), m), SL.slot(~A, AR.slots(Maybe<&2, A>, t), m), SL.slot(~A, u2_of(~A, d, t, i, x, pv), m),
466 ulog_off(~A, t, i, x, m, SL.ne_sym(i, m, ec)),
467 Equal.sym(Maybe<&2, A>, SL.slot(~A, u2_of(~A, d, t, i, x, pv), m), SL.slot(~A, AR.slots(Maybe<&2, A>, t), m), u2_off(~A, d, t, i, x, pv, m, SL.ne_sym(i, m, ec), SL.ne_sym(IX.par(i), m, eb), hi, pf))),
468 SL.lay_at(~A, ulog(~A, t, i, x), n, m, hlay, hmn))
469
470def lay_next(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hlay: {SL.lay(~A, ulog(~A, t, i, x), n) == True{} : Bool}) -> {SL.lay(~A, u2_of(~A, d, t, i, x, pv), k) == True{} : Bool}:
471 match k:
472 case 0n:
473 {==}
474 case 1n+ +m:
475 L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, u2_of(~A, d, t, i, x, pv), m)), SL.lay(~A, u2_of(~A, d, t, i, x, pv), m),
476 some_next(~A, ~cmp, d, t, i, x, pv, n, m, N.lt_le_trans(m, 1n+m, n, N.lt_succ(m), hk), hi, hpos, pf, hlay, Nat.is_eq(m, IX.par(i)), {==}, Nat.is_eq(m, i), {==}),
477 lay_next(~A, ~cmp, d, t, i, x, pv, n, m, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), hi, hpos, pf, hlay))
478
479# ---- the multiset of the next state ----
480
481def u2_swap_form(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {u2_of(~A, d, t, i, x, pv) == SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, ulog(~A, t, i, x), i, Some{pv}), IX.par(i), Some{x}) : List<&2, Maybe<&2, A>>}:
482 Equal.cong(List<&2, Maybe<&2, A>>, List<&2, Maybe<&2, A>>, ss => SC.update(Maybe<&2, A>, ss, IX.par(i), Some{x}), AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), SC.update(Maybe<&2, A>, ulog(~A, t, i, x), i, Some{pv}),
483 Equal.trans(List<&2, Maybe<&2, A>>, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), ulog(~A, t, i, pv), SC.update(Maybe<&2, A>, ulog(~A, t, i, x), i, Some{pv}),
484 set_slots(~A, d, t, i, pv, hi, pf),
485 Equal.sym(List<&2, Maybe<&2, A>>, SC.update(Maybe<&2, A>, ulog(~A, t, i, x), i, Some{pv}), ulog(~A, t, i, pv), BG.upd_upd_same(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, Some{pv}))))
486
487def ms_next(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +n: Nat, +tgt: List<&2, A>, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hin: {Nat.is_lt(i, n) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hms: {V.msort(~A, ~cmp, V.vals(~A, ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> {V.msort(~A, ~cmp, V.vals(~A, u2_of(~A, d, t, i, x, pv), n)) == tgt : List<&2, A>}:
488 %Equal.sym(List<&2, Maybe<&2, A>>, u2_of(~A, d, t, i, x, pv), SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, ulog(~A, t, i, x), i, Some{pv}), IX.par(i), Some{x}), u2_swap_form(~A, d, t, i, x, pv, hi, pf)) : {V.msort(~A, ~cmp, V.vals(~A, _, n)) == tgt : List<&2, A>}
489 Equal.trans(List<&2, A>, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, SC.update(Maybe<&2, A>, ulog(~A, t, i, x), i, Some{pv}), IX.par(i), Some{x}), n)), V.msort(~A, ~cmp, V.vals(~A, ulog(~A, t, i, x), n)), tgt,
490 BG.vals_swap(~A, ~cmp, ~o, ulog(~A, t, i, x), n, i, IX.par(i), x, pv, hin,
491 N.lt_trans(IX.par(i), i, n, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), hin),
492 SL.ne_sym(i, IX.par(i), par_ne(i, hpos)),
493 ulog_at(~A, d, t, i, x, hi, pf),
494 u1_at_p(~A, t, i, x, pv, hpos, hpv)),
495 hms)
496
497# ---- the loop ----
498
499def pair_ok_zero(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +e: {Nat.is_eq(i, 0n) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, ss, i) == True{} : Bool}:
500 L.subst(Nat, z => {SL.pair_ok(~A, ~cmp, ss, z) == True{} : Bool}, 0n, i, Equal.sym(Nat, i, 0n, N.eq_from_is_eq(i, 0n, e)), {==})
501
502def pair_none(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +em: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == None{} : Maybe<&2, A>}) -> {SL.pair_ok(~A, ~cmp, ulog(~A, t, i, x), i) == True{} : Bool}:
503 pair_ok_pos(~A, ~cmp, ulog(~A, t, i, x), i, hpos,
504 L.subst(Maybe<&2, A>, w => {SL.mle(~A, ~cmp, w, SL.slot(~A, ulog(~A, t, i, x), i)) == True{} : Bool}, None{}, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)),
505 Equal.sym(Maybe<&2, A>, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), None{},
506 Equal.trans(Maybe<&2, A>, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), None{}, ulog_off(~A, t, i, x, IX.par(i), SL.ne_sym(i, IX.par(i), par_ne(i, hpos))), em)),
507 SL.mle_none_l(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), i))))
508
509def pair_stop_mle(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hle: {S.le(~A, ~cmp, pv, x) == True{} : Bool}) -> {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), SL.slot(~A, ulog(~A, t, i, x), i)) == True{} : Bool}:
510 %Equal.sym(Maybe<&2, A>, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), Some{pv}, u1_at_p(~A, t, i, x, pv, hpos, hpv)) : {SL.mle(~A, ~cmp, _, SL.slot(~A, ulog(~A, t, i, x), i)) == True{} : Bool}
511 %Equal.sym(Maybe<&2, A>, SL.slot(~A, ulog(~A, t, i, x), i), Some{x}, ulog_at(~A, d, t, i, x, hi, pf)) : {SL.mle(~A, ~cmp, Some{pv}, _) == True{} : Bool}
512 hle
513
514def pair_stop(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hpv: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == Some{pv} : Maybe<&2, A>}, +hle: {S.le(~A, ~cmp, pv, x) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, ulog(~A, t, i, x), i) == True{} : Bool}:
515 pair_ok_pos(~A, ~cmp, ulog(~A, t, i, x), i, hpos,
516 pair_stop_mle(~A, ~cmp, d, t, i, x, pv, hi, hpos, pf, hpv, hle))
517
518def up_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, +pv: A, +t3: AR.Tree<Maybe<&2, A>>, +eq: {H.up_go(~A, ~cmp, 1n+f, x, ureal(~A, Mv{t, i, pv, IX.par(i)})) == H.up_go(~A, ~cmp, f, x, ureal(~A, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x))) : Array<Maybe<&2, A>>}, rest: {H.up_go(~A, ~cmp, f, x, ureal(~A, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x))) == 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>}))) ) -> UpOK(~A, ~cmp, d, n, tgt, 1n+f, x, Mv{t, i, pv, IX.par(i)}):
519 (e1, more) = rest
520 (t3, (Equal.trans(Array<Maybe<&2, A>>, H.up_go(~A, ~cmp, 1n+f, x, ureal(~A, Mv{t, i, pv, IX.par(i)})), H.up_go(~A, ~cmp, f, x, ureal(~A, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x))), AR.thaw(Maybe<&2, A>, t3), eq, e1), more))
521
522# The recursive result is about the next state; its first component has to be
523# rewritten through the step the loop took.
524def up_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, +pv: A, +eq: {H.up_go(~A, ~cmp, 1n+f, x, ureal(~A, Mv{t, i, pv, IX.par(i)})) == H.up_go(~A, ~cmp, f, x, ureal(~A, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x))) : Array<Maybe<&2, A>>}, rec: UpOK(~A, ~cmp, d, n, tgt, f, x, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x))) -> UpOK(~A, ~cmp, d, n, tgt, 1n+f, x, Mv{t, i, pv, IX.par(i)}):
525 (t3, rest) = rec
526 up_carry_go(~A, ~cmp, d, n, tgt, f, t, i, x, pv, t3, eq, rest)
527
528def up_step_eq(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +f: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +hpos: {Nat.is_le(1n, i) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {H.up_go(~A, ~cmp, 1n+f, x, ureal(~A, Mv{t, i, pv, IX.par(i)})) == H.up_go(~A, ~cmp, f, x, ureal(~A, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x))) : Array<Maybe<&2, A>>}:
529 %Equal.sym(Array<Maybe<&2, A>>, Array.set(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), Some{pv}), AR.thaw(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), set_eq(~A, d, t, i, pv, hd, hi, pf)) : {H.up_go(~A, ~cmp, f, x, H.up_probe(~A, ~cmp, U32.from_nat(IX.par(i)), x, _)) == H.up_go(~A, ~cmp, f, x, ureal(~A, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x))) : Array<Maybe<&2, A>>}
530 Equal.cong(H.Up<A>, Array<Maybe<&2, A>>, s => H.up_go(~A, ~cmp, f, x, s), H.up_probe(~A, ~cmp, U32.from_nat(IX.par(i)), x, AR.thaw(Maybe<&2, A>, t2_of(~A, d, t, i, pv))), ureal(~A, uprobe(~A, ~cmp, t2_of(~A, d, t, i, pv), IX.par(i), x)),
531 uprobe_ok(~A, ~cmp, d, t2_of(~A, d, t, i, pv), IX.par(i), x, hd, par_lt_d(d, i, hi, hpos), t2_perfect(~A, d, t, i, pv, pf)))
532
533# The sift-up loop. `hfuel` is what says the loop has enough steps left: the
534# hole index is below 2^fuel, which halves with the fuel, so the loop can only
535# run out of fuel at the root -- where it stops anyway.
536def up_loop(~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}, +hfuel: {Nat.is_lt(i, SC.pow2(fuel)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}, +hlay: {SL.lay(~A, ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, ulog(~A, t, i, x), n)) == tgt : List<&2, A>}, bz: Bool, +ebz: {Nat.is_eq(i, 0n) == bz : Bool}, m: Maybe<&2, A>, +em: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)) == m : Maybe<&2, A>}, ble: Bool, +eble: {S.le(~A, ~cmp, mval(~A, m, x), x) == ble : Bool}) -> UpOK(~A, ~cmp, d, n, tgt, fuel, x, uprobe(~A, ~cmp, t, i, x)):
537 match fuel bz m ble:
538 case _ True{} _ _:
539 %Equal.sym(Bool, Nat.is_eq(i, 0n), True{}, ebz) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, uroot(~A, ~cmp, t, i, x, _))
540 up_stop_ok(~A, ~cmp, d, n, tgt, fuel, t, i, x, hd, hi, pf, pair_ok_zero(~A, ~cmp, ulog(~A, t, i, x), i, ebz), hexc, hlay, hms)
541 case _ False{} None{} _:
542 %Equal.sym(Bool, Nat.is_eq(i, 0n), False{}, ebz) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, uroot(~A, ~cmp, t, i, x, _))
543 %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), None{}, em) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, umb(~A, ~cmp, t, i, x, IX.par(i), _))
544 up_stop_ok(~A, ~cmp, d, n, tgt, fuel, t, i, x, hd, hi, pf, pair_none(~A, ~cmp, t, i, x, pos_of_ne(i, ebz), em), hexc, hlay, hms)
545 case _ False{} Some{+pv} True{}:
546 %Equal.sym(Bool, Nat.is_eq(i, 0n), False{}, ebz) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, uroot(~A, ~cmp, t, i, x, _))
547 %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), Some{pv}, em) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, umb(~A, ~cmp, t, i, x, IX.par(i), _))
548 %Equal.sym(Bool, S.le(~A, ~cmp, pv, x), True{}, eble) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, udec(~A, ~cmp, t, i, pv, IX.par(i), _))
549 up_stop_ok(~A, ~cmp, d, n, tgt, fuel, t, i, x, hd, hi, pf, pair_stop(~A, ~cmp, d, t, i, x, pv, hi, pos_of_ne(i, ebz), pf, em, eble), hexc, hlay, hms)
550 case 0n False{} Some{pv} False{}:
551 Empty.absurd(UpOK(~A, ~cmp, d, n, tgt, 0n, x, uprobe(~A, ~cmp, t, i, x)),
552 L.true_not_false(Nat.is_eq(i, 0n), L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, 0n, i, Equal.sym(Nat, i, 0n, U.lt_one_zero(i, hfuel)), {==}), ebz))
553 case 1n+ +f False{} Some{+pv} False{}:
554 %Equal.sym(Bool, Nat.is_eq(i, 0n), False{}, ebz) : UpOK(~A, ~cmp, d, n, tgt, 1n+f, x, uroot(~A, ~cmp, t, i, x, _))
555 %Equal.sym(Maybe<&2, A>, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), Some{pv}, em) : UpOK(~A, ~cmp, d, n, tgt, 1n+f, x, umb(~A, ~cmp, t, i, x, IX.par(i), _))
556 %Equal.sym(Bool, S.le(~A, ~cmp, pv, x), False{}, eble) : UpOK(~A, ~cmp, d, n, tgt, 1n+f, x, udec(~A, ~cmp, t, i, pv, IX.par(i), _))
557 up_carry(~A, ~cmp, d, n, tgt, f, t, i, x, pv, up_step_eq(~A, ~cmp, d, f, t, i, x, pv, hd, hi, pos_of_ne(i, ebz), pf),
558 up_loop(~A, ~cmp, ~o, f, d, n, tgt, t2_of(~A, d, t, i, pv), IX.par(i), x, hd,
559 par_lt_d(d, i, hi, pos_of_ne(i, ebz)),
560 N.lt_trans(IX.par(i), i, n, IX.par_lt(i, N.succ_le_lt(0n, i, pos_of_ne(i, ebz))), hin),
561 IX.par_bound(i, f, hfuel),
562 t2_perfect(~A, d, t, i, pv, pf),
563 exc_next(~A, ~cmp, ~o, d, t, i, x, pv, n, n, N.le_refl(n), hi, pos_of_ne(i, ebz), pf, em, eble, hexc, hkids),
564 kids_next(~A, ~cmp, ~o, d, t, i, x, pv, n, hi, hin, pos_of_ne(i, ebz), pf, em, eble, hexc),
565 lay_next(~A, ~cmp, d, t, i, x, pv, n, n, N.le_refl(n), hi, pos_of_ne(i, ebz), pf, hlay),
566 ms_next(~A, ~cmp, ~o, d, t, i, x, pv, n, tgt, hi, hin, pos_of_ne(i, ebz), pf, em, hms),
567 Nat.is_eq(IX.par(i), 0n), {==},
568 SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), IX.par(IX.par(i))), {==},
569 S.le(~A, ~cmp, mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), IX.par(IX.par(i))), x), x), {==}))
570
571# ---- the entry point ----
572
573def SiftOK(~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:
574 Sigma<&1, &1, AR.Tree<Maybe<&2, A>>, t2 => {H.sift_up(~A, ~cmp, fuel, 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>})))>
575
576def sift_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_up(~A, ~cmp, fuel, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)) == H.up_go(~A, ~cmp, fuel, x, ureal(~A, uprobe(~A, ~cmp, t, i, x))) : Array<Maybe<&2, A>>}, rest: {H.up_go(~A, ~cmp, fuel, x, ureal(~A, uprobe(~A, ~cmp, t, i, x))) == 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>}))) ) -> SiftOK(~A, ~cmp, d, n, tgt, fuel, t, i, x):
577 (e1, more) = rest
578 (t2, (Equal.trans(Array<Maybe<&2, A>>, H.sift_up(~A, ~cmp, fuel, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)), H.up_go(~A, ~cmp, fuel, x, ureal(~A, uprobe(~A, ~cmp, t, i, x))), AR.thaw(Maybe<&2, A>, t2), eq, e1), more))
579
580def sift_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_up(~A, ~cmp, fuel, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)) == H.up_go(~A, ~cmp, fuel, x, ureal(~A, uprobe(~A, ~cmp, t, i, x))) : Array<Maybe<&2, A>>}, r: UpOK(~A, ~cmp, d, n, tgt, fuel, x, uprobe(~A, ~cmp, t, i, x))) -> SiftOK(~A, ~cmp, d, n, tgt, fuel, t, i, x):
581 (t2, rest) = r
582 sift_from_go(~A, ~cmp, d, n, tgt, fuel, t, i, x, t2, eq, rest)
583
584def sift_up_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}, +hfuel: {Nat.is_lt(i, SC.pow2(fuel)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +hexc: {SL.ho_exc(~A, ~cmp, ulog(~A, t, i, x), n, i) == True{} : Bool}, +hkids: {SL.kids_le(~A, ~cmp, ulog(~A, t, i, x), n, IX.par(i), i) == True{} : Bool}, +hlay: {SL.lay(~A, ulog(~A, t, i, x), n) == True{} : Bool}, +hms: {V.msort(~A, ~cmp, V.vals(~A, ulog(~A, t, i, x), n)) == tgt : List<&2, A>}) -> SiftOK(~A, ~cmp, d, n, tgt, fuel, t, i, x):
585 sift_from_loop(~A, ~cmp, d, n, tgt, fuel, t, i, x,
586 Equal.cong(H.Up<A>, Array<Maybe<&2, A>>, s => H.up_go(~A, ~cmp, fuel, x, s), H.up_probe(~A, ~cmp, U32.from_nat(i), x, AR.thaw(Maybe<&2, A>, t)), ureal(~A, uprobe(~A, ~cmp, t, i, x)), uprobe_ok(~A, ~cmp, d, t, i, x, hd, hi, pf)),
587 up_loop(~A, ~cmp, ~o, fuel, d, n, tgt, t, i, x, hd, hi, hin, hfuel, pf, hexc, hkids, hlay, hms, Nat.is_eq(i, 0n), {==}, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), {==}, S.le(~A, ~cmp, mval(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)), x), x), {==}))