~/bend-docscommunity

proofs/containers/binary_heap/up.bend source

proofs/containers/binary_heap/up.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/list.bend as LLimport ../../lib/order.bend as Oimport ../../lib/array.bend as ARimport ../../lib/u32.bend as Uimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/binary_heap.bend as Simport ../../../src/containers/binary_heap.bend as Himport ./idx.bend as IXimport ./u32idx.bend as UXimport ./slots.bend as SLimport ./vals.bend as Vimport ./bag.bend as BGimport ./multiset.bend as M# The sift-up loop, mirrored on the shadow tree, and the bridge that says the# executable loop state is the mirror of the shadow one.type UpS<-A: Data> is Data:  Stp{t: AR.Tree<Maybe<&2, A>>, i: Nat}  Mv{t: AR.Tree<Maybe<&2, A>>, i: Nat, pv: A, p: Nat}def ureal(~A: Data, s: UpS<A>) -> H.Up<A>:  match s:    case Stp{t, i}:      H.UStop{AR.thaw(Maybe<&2, A>, t), U32.from_nat(i)}    case Mv{t, i, pv, p}:      H.UMove{AR.thaw(Maybe<&2, A>, t), U32.from_nat(i), pv, U32.from_nat(p)}# ---- the mirror of `H.up_probe` ----def udec(~A: Data, ~cmp: A -> A -> Cmp, t: AR.Tree<Maybe<&2, A>>, +i: Nat, pv: A, p: Nat, ok: Bool) -> UpS<A>:  match ok:    case True{}:      Stp{t, i}    case False{}:      Mv{t, i, pv, p}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>:  match m:    case None{}:      Stp{t, i}    case Some{+pv}:      udec(~A, ~cmp, t, i, pv, p, S.le(~A, ~cmp, pv, x))def uroot(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, root: Bool) -> UpS<A>:  match root:    case True{}:      Stp{t, i}    case False{}:      umb(~A, ~cmp, t, i, x, IX.par(i), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)))def uprobe(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A) -> UpS<A>:  uroot(~A, ~cmp, t, i, x, Nat.is_eq(i, 0n))# ---- the bridge ----# the slot the implementation reads, as an `Array.get` resultdef 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>}:  +ss = AR.slots(Maybe<&2, A>, t)  +ej = UX.nat_round(j, d, N.lt_le(d, 32n, hd), hj)  AR.get(Maybe<&2, A>, d, t, U32.from_nat(j), SL.slot(~A, ss, j), hd,    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),    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),      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))),    pf)def double_pos(+v: Nat, +h: {Nat.is_lt(0n, v) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.double(v)) == True{} : Bool}:  match v:    case 0n:      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_not_false(Nat.is_lt(0n, 0n), h, N.lt_irrefl(0n)))    case 1n+k:      {==}def pow2_pos(+d: Nat) -> {Nat.is_lt(0n, SC.pow2(d)) == True{} : Bool}:  match d:    case 0n:      {==}    case 1n+p:      double_pos(SC.pow2(p), pow2_pos(p))def pos_of(+i: Nat, +eb: {Nat.is_eq(i, 0n) == False{} : Bool}) -> {Nat.is_le(i, 0n) == False{} : Bool}:  match i:    case 0n:      Empty.absurd({Nat.is_le(0n, 0n) == False{} : Bool}, L.true_not_false(Nat.is_eq(0n, 0n), {==}, eb))    case 1n+k:      {==}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>}:  match b:    case True{}:      {==}    case False{}:      {==}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>}:  match m:    case None{}:      {==}    case Some{+pv}:      udec_ok(~A, ~cmp, t, i, pv, p, S.le(~A, ~cmp, pv, x))# i > 0: the implementation reads the parent slot and the mirror reads the# same slot of the shadow's slot list.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>}:  +hp = N.lt_trans(IX.par(i), i, SC.pow2(d), IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), hi)  %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>}  %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>}  umb_ok(~A, ~cmp, t, i, x, IX.par(i), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(i)))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>}:  match b:    case True{}:      {==}    case False{}:      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)# is_eq(i, 0) = False gives 1 <= idef 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>}:  %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>}  uroot_ok(~A, ~cmp, d, t, i, x, hd, hi, pf, Nat.is_eq(i, 0n), {==})# ---- the logical slot list of a loop state ----## While the loop runs, slot i of the block holds a value that is about to be# overwritten; the array the invariant talks about is the block with the# sifted value x at slot i.def ulog(~A: Data, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A) -> List<&2, Maybe<&2, A>>:  SC.update(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), i, Some{x})def mval(~A: Data, m: Maybe<&2, A>, d: A) -> A:  match m:    case None{}:      d    case Some{v}:      v# slot bookkeeping for a tree whose slot list has 2^d entriesdef 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}:  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)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>}:  SL.slot_same(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, in_range(~A, d, t, i, hi, pf))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>}:  SL.slot_other(~A, AR.slots(Maybe<&2, A>, t), i, j, Some{x}, ne)# ---- what the loop delivers ----def UpOK(~A: Data, ~cmp: A -> A -> Cmp, d: Nat, n: Nat, tgt: List<&2, A>, fuel: Nat, x: A, s: UpS<A>) -> Type:  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>})))># the block after the last write, and the fact that its slot list is the# logical array the invariant is aboutdef set_tree(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A) -> AR.Tree<Maybe<&2, A>>:  AR.upd(Maybe<&2, A>, d, t, i, Some{x})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>>}:  AR.upd_slots(Maybe<&2, A>, d, t, i, Some{x}, hi, pf)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>>}:  +ss = AR.slots(Maybe<&2, A>, t)  +ei = UX.nat_round(i, d, N.lt_le(d, 32n, hd), hi)  %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>>}  AR.set(Maybe<&2, A>, d, t, U32.from_nat(i), Some{x}, SL.slot(~A, ss, i), hd,    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),    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))),    pf)# ---- the loop stops: the sifted value is written where the hole is ----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}):  +es = set_slots(~A, d, t, i, x, hi, pf)  (set_tree(~A, d, t, i, x),   (eq,    (AR.upd_perfect(Maybe<&2, A>, d, t, i, Some{x}, pf),     (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),        SL.ho_of_exc(~A, ~cmp, ulog(~A, t, i, x), n, i, hexc, hpair)),      (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),       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))))))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}):  match fuel:    case 0n:      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)    case 1n+f:      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)# ---- one step of the loop: the parent value moves down into the hole ----## `t2` is the block after that write and the hole is now at par(i); `u2` is# the logical array of the new state. The three lemmas below say what each of# its slots holds.def t2_of(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +pv: A) -> AR.Tree<Maybe<&2, A>>:  set_tree(~A, d, t, i, pv)def u2_of(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +pv: A) -> List<&2, Maybe<&2, A>>:  ulog(~A, t2_of(~A, d, t, i, pv), IX.par(i), x)def par_ne(+i: Nat, +hpos: {Nat.is_le(1n, i) == True{} : Bool}) -> {Nat.is_eq(IX.par(i), i) == False{} : Bool}:  N.is_eq_lt(IX.par(i), i, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)))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}:  N.lt_trans(IX.par(i), i, SC.pow2(d), IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), hi)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}:  AR.upd_perfect(Maybe<&2, A>, d, t, i, Some{pv}, pf)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>}:  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))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>}:  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},    ulog_off(~A, t2_of(~A, d, t, i, pv), IX.par(i), x, i, par_ne(i, hpos)),    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},      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)),      ulog_at(~A, d, t, i, pv, hi, pf)))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>}:  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),    ulog_off(~A, t2_of(~A, d, t, i, pv), IX.par(i), x, j, hjp),    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),      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)),      ulog_off(~A, t, i, pv, j, hji)))# the same three for the CURRENT logical arraydef 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>}:  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},    ulog_off(~A, t, i, x, IX.par(i), SL.ne_sym(i, IX.par(i), par_ne(i, hpos))),    hpv)# ---- the pair condition at an index that has a parent ----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}:  match i:    case 0n:      Empty.absurd({SL.pair_ok(~A, ~cmp, ss, 0n) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), hpos, {==}))    case 1n+k:      hdef 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}:  match i:    case 0n:      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, {==}))    case 1n+k:      h# j >= 1 whenever j is not 0def pos_of_ne(+j: Nat, +h: {Nat.is_eq(j, 0n) == False{} : Bool}) -> {Nat.is_le(1n, j) == True{} : Bool}:  match j:    case 0n:      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.true_not_false(Nat.is_eq(0n, 0n), {==}, h))    case 1n+k:      N.zero_le(k)# ---- the heap order of the next state, one index at a time ----##   case i     the hole's old index now holds the parent value pv, and the#              new hole above it holds x, with x <= pv because the sift moved#   case kid   a child of the old hole: pv is not larger than it, which is#              exactly the invariant H2 the state carries#   case sib   a child of the new hole other than the old one: x <= pv and pv#              was not larger than it#   case far   an index none of whose two slots changeddef 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}:  %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}  %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}  O.total(~A, ~cmp, ~o, pv, x, hnle)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}:  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)),    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)))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}:  match e:    case Inl{ej}:      Inl{L.subst(Nat, z => {j == IX.kidl(z) : Nat}, IX.par(j), i, epj, ej)}    case Inr{ej}:      Inr{L.subst(Nat, z => {j == IX.kidr(z) : Nat}, IX.par(j), i, epj, ej)}# rewrite H2 from the logical array to the blockdef 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}:  %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}  %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}  h# pv is not larger than a child of the old hole (this is H2)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}:  match e:    case Inl{+ej}:      h1n_kid_fix(~A, ~cmp, t, i, x, pv, j, hjne, hpos, hpv,        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),          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),            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))))    case Inr{+ej}:      h1n_kid_fix(~A, ~cmp, t, i, x, pv, j, hjne, hpos, hpv,        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),          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),            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))))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}:  N.lt_trans(IX.par(i), i, j, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)),    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))))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}:  %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}  %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}  %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}  hdef 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}:  +hij = SL.ne_sym(i, j, hjne)  +hpij = N.is_eq_lt(IX.par(i), j, par_lt_kid(i, j, epj, hjpos, hpos))  pair_ok_pos(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j, hjpos,    h1n_kid_goal(~A, ~cmp, d, t, i, x, pv, n, j, epj, hij, hpij, hjn, hi, hpos, pf, hpv,      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))))))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}:  +hm = pair_ok_val(~A, ~cmp, ulog(~A, t, i, x), j, hjpos, h)  %ulog_off(~A, t, i, x, j, hij) : {SL.mle(~A, ~cmp, Some{pv}, _) == True{} : Bool}  %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}  %epj : {SL.mle(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), _), SL.slot(~A, ulog(~A, t, i, x), j)) == True{} : Bool}  hmdef 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}:  %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}  %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}  %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}  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)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}:  pair_ok_pos(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j, hjpos,    h1n_sib_goal(~A, ~cmp, ~o, d, t, i, x, pv, j, hij, hpij, epj, hi, hpos, pf, hnle,      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)))))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}:  %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}  %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}  %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}  %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}  hdef 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}:  +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)))  pair_ok_pos(~A, ~cmp, u2_of(~A, d, t, i, x, pv), j, hjpos,    h1n_far_goal(~A, ~cmp, d, t, i, x, pv, j, hij, hpij, hipj, hppj, hi, pf, hm))# ---- the four cases, dispatched on the index ----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}:  match b3:    case True{}:      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)    case False{}:      h1n_far(~A, ~cmp, d, t, i, x, pv, n, j, hij, hpij, hipj, eb3, hjpos, hjn, hi, pf, hexc)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}:  match b2:    case True{}:      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)    case False{}:      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)), {==})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}:  match b1:    case True{}:      h1n_i(~A, ~cmp, ~o, d, t, i, x, pv, j, eb1, hi, hpos, pf, hnle)    case False{}:      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), {==})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}:  match j:    case 0n:      {==}    case 1n+ +m:      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), {==})# ---- H2 for the next state: the new hole's parent is not larger than the# new hole's children ----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}:  +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))  %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}  %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}  O.total(~A, ~cmp, ~o, pv, x, hnle)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}:  +ppos = pos_of_ne(IX.par(i), e)  +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)))  +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)))  %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}  %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}  %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}  hmdef 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}:  match b:    case True{}:      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)    case False{}:      h2_key_deep(~A, ~cmp, d, t, i, x, pv, n, eb, hi, hin, hpos, pf, hpv, hexc)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}:  %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}  %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}  keydef 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}:  +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))))  +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))  %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}  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)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}:  match b:    case True{}:      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), {==}))    case False{}:      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), {==}))# H2 for the next state: both children of the new holedef 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}:  match b:    case False{}:      SL.kid_le_out(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), c, eb)    case True{}:      SL.kid_le_in(~A, ~cmp, u2_of(~A, d, t, i, x, pv), n, IX.par(IX.par(i)), c, eb,        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), {==}))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}:  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))),    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), {==}),    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), {==}))# ---- the three remaining invariants of the next state ----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}:  match b:    case True{}:      SL.skip_eq(~A, ~cmp, u2_of(~A, d, t, i, x, pv), m, IX.par(i), eb)    case False{}:      SL.skip_ne(~A, ~cmp, u2_of(~A, d, t, i, x, pv), m, IX.par(i), eb,        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))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}:  match k:    case 0n:      {==}    case 1n+ +m:      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)),        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)), {==}),        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))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}:  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), {==})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}:  match b c:    case True{} _:      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)),        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)))    case False{} True{}:      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)),        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)))    case False{} False{}:      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),        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),          ulog_off(~A, t, i, x, m, SL.ne_sym(i, m, ec)),          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))),        SL.lay_at(~A, ulog(~A, t, i, x), n, m, hlay, hmn))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}:  match k:    case 0n:      {==}    case 1n+ +m:      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),        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), {==}),        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))# ---- the multiset of the next state ----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>>}:  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}),    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}),      set_slots(~A, d, t, i, pv, hi, pf),      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}))))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>}:  %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>}  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,    BG.vals_swap(~A, ~cmp, ~o, ulog(~A, t, i, x), n, i, IX.par(i), x, pv, hin,      N.lt_trans(IX.par(i), i, n, IX.par_lt(i, N.succ_le_lt(0n, i, hpos)), hin),      SL.ne_sym(i, IX.par(i), par_ne(i, hpos)),      ulog_at(~A, d, t, i, x, hi, pf),      u1_at_p(~A, t, i, x, pv, hpos, hpv)),    hms)# ---- the loop ----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}:  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)), {==})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}:  pair_ok_pos(~A, ~cmp, ulog(~A, t, i, x), i, hpos,    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)),      Equal.sym(Maybe<&2, A>, SL.slot(~A, ulog(~A, t, i, x), IX.par(i)), None{},        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)),      SL.mle_none_l(~A, ~cmp, SL.slot(~A, ulog(~A, t, i, x), i))))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}:  %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}  %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}  hledef 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}:  pair_ok_pos(~A, ~cmp, ulog(~A, t, i, x), i, hpos,    pair_stop_mle(~A, ~cmp, d, t, i, x, pv, hi, hpos, pf, hpv, hle))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)}):  (e1, more) = rest  (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))# The recursive result is about the next state; its first component has to be# rewritten through the step the loop took.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)}):  (t3, rest) = rec  up_carry_go(~A, ~cmp, d, n, tgt, f, t, i, x, pv, t3, eq, rest)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>>}:  %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>>}  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)),    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)))# The sift-up loop. `hfuel` is what says the loop has enough steps left: the# hole index is below 2^fuel, which halves with the fuel, so the loop can only# run out of fuel at the root -- where it stops anyway.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)):  match fuel bz m ble:    case _ True{} _ _:      %Equal.sym(Bool, Nat.is_eq(i, 0n), True{}, ebz) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, uroot(~A, ~cmp, t, i, x, _))      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)    case _ False{} None{} _:      %Equal.sym(Bool, Nat.is_eq(i, 0n), False{}, ebz) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, uroot(~A, ~cmp, t, i, x, _))      %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), _))      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)    case _ False{} Some{+pv} True{}:      %Equal.sym(Bool, Nat.is_eq(i, 0n), False{}, ebz) : UpOK(~A, ~cmp, d, n, tgt, fuel, x, uroot(~A, ~cmp, t, i, x, _))      %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), _))      %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), _))      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)    case 0n False{} Some{pv} False{}:      Empty.absurd(UpOK(~A, ~cmp, d, n, tgt, 0n, x, uprobe(~A, ~cmp, t, i, x)),        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))    case 1n+ +f False{} Some{+pv} False{}:      %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, _))      %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), _))      %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), _))      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),        up_loop(~A, ~cmp, ~o, f, d, n, tgt, t2_of(~A, d, t, i, pv), IX.par(i), x, hd,          par_lt_d(d, i, hi, pos_of_ne(i, ebz)),          N.lt_trans(IX.par(i), i, n, IX.par_lt(i, N.succ_le_lt(0n, i, pos_of_ne(i, ebz))), hin),          IX.par_bound(i, f, hfuel),          t2_perfect(~A, d, t, i, pv, pf),          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),          kids_next(~A, ~cmp, ~o, d, t, i, x, pv, n, hi, hin, pos_of_ne(i, ebz), pf, em, eble, hexc),          lay_next(~A, ~cmp, d, t, i, x, pv, n, n, N.le_refl(n), hi, pos_of_ne(i, ebz), pf, hlay),          ms_next(~A, ~cmp, ~o, d, t, i, x, pv, n, tgt, hi, hin, pos_of_ne(i, ebz), pf, em, hms),          Nat.is_eq(IX.par(i), 0n), {==},          SL.slot(~A, AR.slots(Maybe<&2, A>, t2_of(~A, d, t, i, pv)), IX.par(IX.par(i))), {==},          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), {==}))# ---- the entry point ----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:  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>})))>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):  (e1, more) = rest  (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))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):  (t2, rest) = r  sift_from_go(~A, ~cmp, d, n, tgt, fuel, t, i, x, t2, eq, rest)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):  sift_from_loop(~A, ~cmp, d, n, tgt, fuel, t, i, x,    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)),    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), {==}))