1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../lib/order.bend as O
6	import ../../lib/array.bend as AR
7	import ../../lib/u32.bend as U
8	import ../../../spec/lib/common.bend as SC
9	import ../../../spec/containers/binary_heap.bend as S
10	import ../../../src/containers/binary_heap.bend as H
11	import ./idx.bend as IX
12	import ./u32idx.bend as UX
13	import ./slots.bend as SL
14	import ./vals.bend as V
15	import ./bag.bend as BG
16	import ./multiset.bend as M
17	
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	
21	type 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	
25	def 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	
34	def 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	
41	def 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	
48	def 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	
55	def 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
61	def 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	
70	def 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	
77	def 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	
84	def 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	
91	def 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	
98	def 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.
107	def 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	
113	def 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
121	def 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	
131	def 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	
134	def 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
142	def 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	
145	def 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	
148	def 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	
153	def 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
158	def 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	
161	def 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	
164	def 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	
175	def 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	
185	def 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	
198	def 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	
201	def 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	
204	def 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	
207	def 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	
210	def 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	
213	def 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	
216	def 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	
223	def 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
231	def 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	
238	def 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	
245	def 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
253	def 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	
270	def 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	
275	def 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	
279	def 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
287	def 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)
293	def 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	
306	def 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))))
309	def 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
314	def 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	
321	def 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
327	def 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)
332	def 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)))))
336	def 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
342	def 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	
349	def 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	
356	def 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	
363	def 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	
370	def 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	
380	def 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	
386	def 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	
396	def 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	
403	def 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
407	def 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)
412	def 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
420	def 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	
428	def 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	
435	def 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	
443	def 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	
452	def 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	
455	def 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	
470	def 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	
481	def 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	
487	def 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	
499	def 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	
502	def 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	
509	def 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	
514	def 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	
518	def 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.
524	def 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	
528	def 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.
536	def 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	
573	def 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	
576	def 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	
580	def 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	
584	def 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), {==}))