proofs/containers/binary_heap/slots.bend source

proofs/containers/binary_heap/slots.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 ../../../spec/lib/common.bend as SCimport ../../../spec/containers/binary_heap.bend as Simport ./idx.bend as IX# The slot list of an array heap, and heap order on it.## Heap order is stated over CHILD indices -- "every j in [1, n) is not smaller# than the value at par(j)" -- so the predicate never divides an index it does# not have to, and every fact about it is pointwise: `ho_get` reads one pair# out of the conjunction and `ho_put` builds the conjunction from a function# that proves one pair at a time. Everything the sift proofs do is then a case# analysis on a single index, never an induction over a range.def unwrap(~A: Data, m: Maybe<&2, Maybe<&2, A>>) -> Maybe<&2, A>:  match m:    case None{}:      None{}    case Some{s}:      sdef slot(~A: Data, ss: List<&2, Maybe<&2, A>>, +j: Nat) -> Maybe<&2, A>:  unwrap(~A, SC.nth(Maybe<&2, A>, ss, j))# Order between two slots; vacuously true when a slot is empty (the layout# invariant is what says the slots of interest are occupied).def mle(~A: Data, ~cmp: A -> A -> Cmp, a: Maybe<&2, A>, b: Maybe<&2, A>) -> Bool:  match a b:    case Some{x} Some{y}:      S.le(~A, ~cmp, x, y)    case _ _:      True{}def pair_ok(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, j: Nat) -> Bool:  match j:    case 0n:      True{}    case 1n+ +m:      mle(~A, ~cmp, slot(~A, ss, IX.par(1n+m)), slot(~A, ss, 1n+m))# Heap order over the children 0 .. k-1 (index 0 has no parent condition).def ho_upto(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat) -> Bool:  match k:    case 0n:      True{}    case 1n+ +m:      Bool.and(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m))# Every slot of [0, k) is occupied.def lay(~A: Data, +ss: List<&2, Maybe<&2, A>>, k: Nat) -> Bool:  match k:    case 0n:      True{}    case 1n+ +m:      Bool.and(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m))# ---- reading one pair out of the conjunction ----def ho_get_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +j: Nat, +e: {Nat.is_eq(j, m) == True{} : Bool}, +hp: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:  L.subst(Nat, z => {pair_ok(~A, ~cmp, ss, z) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, e)), hp)def ho_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +j: Nat, +h: {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:  match k b:    case 0n _:      Empty.absurd({pair_ok(~A, ~cmp, ss, j) == True{} : Bool}, N.lt_zero_absurd(j, hj))    case 1n+ +m True{}:      ho_get_eq(~A, ~cmp, ss, m, j, eb, L.and_left(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m), h))    case 1n+ +m False{}:      ho_get(~A, ~cmp, ss, m, j, L.and_right(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})def ho_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +j: Nat, +h: {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:  ho_get(~A, ~cmp, ss, k, j, h, hj, Nat.is_eq(j, N.pred(k)), {==})# ---- updating one slot ----def slot_same(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +v: Maybe<&2, A>, +hi: {Nat.is_lt(i, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {slot(~A, SC.update(Maybe<&2, A>, ss, i, v), i) == v : Maybe<&2, A>}:  %Equal.sym(Maybe<&2, Maybe<&2, A>>, SC.nth(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, v), i), Some{v}, LL.nth_update_same(Maybe<&2, A>, ss, i, v, hi)) : {unwrap(~A, _) == v : Maybe<&2, A>}  {==}def slot_other(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +j: Nat, +v: Maybe<&2, A>, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {slot(~A, SC.update(Maybe<&2, A>, ss, i, v), j) == slot(~A, ss, j) : Maybe<&2, A>}:  Equal.cong(Maybe<&2, Maybe<&2, A>>, Maybe<&2, A>, m => unwrap(~A, m), SC.nth(Maybe<&2, A>, SC.update(Maybe<&2, A>, ss, i, v), j), SC.nth(Maybe<&2, A>, ss, j), LL.nth_update_other(Maybe<&2, A>, ss, i, j, v, ne))def flip_eq(c: Cmp, +h: {Cmp.is_eq(c) == False{} : Bool}) -> {Cmp.is_eq(O.flipc(c)) == False{} : Bool}:  match c:    case LT{}:      {==}    case EQ{}:      Empty.absurd({Cmp.is_eq(O.flipc(EQ{})) == False{} : Bool}, L.true_false(h))    case GT{}:      {==}def ne_sym(+a: Nat, +b: Nat, +h: {Nat.is_eq(b, a) == False{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:  %Equal.sym(Cmp, Nat.cmp(a, b), O.flipc(Nat.cmp(b, a)), O.nat_flip(b, a)) : {Cmp.is_eq(_) == False{} : Bool}  flip_eq(Nat.cmp(b, a), h)# ---- mle ----def mle_some(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +y: A, +h: {mle(~A, ~cmp, Some{x}, Some{y}) == True{} : Bool}) -> {S.le(~A, ~cmp, x, y) == True{} : Bool}:  hdef mle_mk(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +y: A, +h: {S.le(~A, ~cmp, x, y) == True{} : Bool}) -> {mle(~A, ~cmp, Some{x}, Some{y}) == True{} : Bool}:  hdef mle_none_l(~A: Data, ~cmp: A -> A -> Cmp, +b: Maybe<&2, A>) -> {mle(~A, ~cmp, None{}, b) == True{} : Bool}:  match b:    case None{}:      {==}    case Some{y}:      {==}def mle_none_r(~A: Data, ~cmp: A -> A -> Cmp, +a: Maybe<&2, A>) -> {mle(~A, ~cmp, a, None{}) == True{} : Bool}:  match a:    case None{}:      {==}    case Some{x}:      {==}# transitivity through an OCCUPIED middle slot (with an empty middle there is# nothing to conclude: `mle` is vacuous there)def mle_trans(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), a: Maybe<&2, A>, +y: A, c: Maybe<&2, A>, +hab: {mle(~A, ~cmp, a, Some{y}) == True{} : Bool}, +hbc: {mle(~A, ~cmp, Some{y}, c) == True{} : Bool}) -> {mle(~A, ~cmp, a, c) == True{} : Bool}:  match a c:    case Some{+x} Some{+z}:      O.trans(~A, ~cmp, o, x, y, z, hab, hbc)    case Some{x} None{}:      {==}    case None{} Some{z}:      {==}    case None{} None{}:      {==}# ---- the layout, pointwise ----def lay_get_eq(~A: Data, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +j: Nat, +e: {Nat.is_eq(j, m) == True{} : Bool}, +hp: {Maybe.is_some(&2, A, slot(~A, ss, m)) == True{} : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:  L.subst(Nat, z => {Maybe.is_some(&2, A, slot(~A, ss, z)) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, e)), hp)def lay_get(~A: Data, +ss: List<&2, Maybe<&2, A>>, k: Nat, +j: Nat, +h: {lay(~A, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:  match k b:    case 0n _:      Empty.absurd({Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}, N.lt_zero_absurd(j, hj))    case 1n+ +m True{}:      lay_get_eq(~A, ss, m, j, eb, L.and_left(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m), h))    case 1n+ +m False{}:      lay_get(~A, ss, m, j, L.and_right(Maybe.is_some(&2, A, slot(~A, ss, m)), lay(~A, ss, m), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})def lay_at(~A: Data, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +j: Nat, +h: {lay(~A, ss, k) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}) -> {Maybe.is_some(&2, A, slot(~A, ss, j)) == True{} : Bool}:  lay_get(~A, ss, k, j, h, hj, Nat.is_eq(j, N.pred(k)), {==})# An occupied slot, as a value.def slot_some(~A: Data, m: Maybe<&2, A>, +h: {Maybe.is_some(&2, A, m) == True{} : Bool}) -> Sigma<&1, &1, A, v => {m == Some{v} : Maybe<&2, A>}>:  match m:    case None{}:      Empty.absurd(Sigma<&1, &1, A, v => {None{} == Some{v} : Maybe<&2, A>}>, L.false_true(h))    case Some{+v}:      (v, {==})# ---- nth of a slot inside the list ----def nth_slot(~A: Data, +ss: List<&2, Maybe<&2, A>>, +j: Nat, +hj: {Nat.is_lt(j, SC.length(Maybe<&2, A>, ss)) == True{} : Bool}) -> {SC.nth(Maybe<&2, A>, ss, j) == Some{slot(~A, ss, j)} : Maybe<&2, Maybe<&2, A>>}:  match ss j:    case Nil{} _:      Empty.absurd({None{} == Some{slot(~A, Nil{}, j)} : Maybe<&2, Maybe<&2, A>>}, N.lt_zero_absurd(j, hj))    case Con{x, r} 0n:      {==}    case Con{x, +r} 1n+k:      nth_slot(~A, r, k, hj)# ---- heap order with one index excluded ----## `ho_exc(ss, k, i)` is "every pair below k except the one into i holds". It# is a Bool, not a function over indices: a proof term of function type could# not be used twice, and a step needs its invariant more than once.def pair_skip(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat) -> Bool:  Bool.pick(Bool, Nat.is_eq(m, i), True{}, pair_ok(~A, ~cmp, ss, m))def ho_exc(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat) -> Bool:  match k:    case 0n:      True{}    case 1n+ +m:      Bool.and(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i))def skip_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hne: {Nat.is_eq(m, i) == False{} : Bool}, +h: {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:  L.subst(Bool, b => {Bool.pick(Bool, b, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}, Nat.is_eq(m, i), False{}, hne, h)def skip_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {Nat.is_eq(m, i) == True{} : Bool}) -> {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}:  %Equal.sym(Bool, Nat.is_eq(m, i), True{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}  {==}def skip_ne(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {Nat.is_eq(m, i) == False{} : Bool}, +h: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}:  %Equal.sym(Bool, Nat.is_eq(m, i), False{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}  hdef exc_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +j: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_skip(~A, ~cmp, ss, j, i) == True{} : Bool}:  match k b:    case 0n _:      Empty.absurd({pair_skip(~A, ~cmp, ss, j, i) == True{} : Bool}, N.lt_zero_absurd(j, hj))    case 1n+ +m True{}:      L.subst(Nat, z => {pair_skip(~A, ~cmp, ss, z, i) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, eb)), L.and_left(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h))    case 1n+ +m False{}:      exc_get(~A, ~cmp, ss, m, i, j, L.and_right(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})# one pair out of `ho_exc`def exc_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +i: Nat, +j: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, +hne: {Nat.is_eq(j, i) == False{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:  skip_at(~A, ~cmp, ss, j, i, hne, exc_get(~A, ~cmp, ss, k, i, j, h, hj, Nat.is_eq(j, N.pred(k)), {==}))def pair_of_skip(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hi: {pair_ok(~A, ~cmp, ss, i) == True{} : Bool}, +h: {pair_skip(~A, ~cmp, ss, m, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, i) == b : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:  match b:    case True{}:      ho_get_eq(~A, ~cmp, ss, i, m, eb, hi)    case False{}:      skip_at(~A, ~cmp, ss, m, i, eb, h)# `ho_upto` follows from `ho_exc` plus the excluded pairdef ho_of_exc(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +h: {ho_exc(~A, ~cmp, ss, k, i) == True{} : Bool}, +hi: {pair_ok(~A, ~cmp, ss, i) == True{} : Bool}) -> {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}:  match k:    case 0n:      {==}    case 1n+ +m:      L.and_intro(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m),        pair_of_skip(~A, ~cmp, ss, m, i, hi, L.and_left(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), Nat.is_eq(m, i), {==}),        ho_of_exc(~A, ~cmp, ss, m, i, L.and_right(pair_skip(~A, ~cmp, ss, m, i), ho_exc(~A, ~cmp, ss, m, i), h), hi))# ---- the children of one index ----def kid_le(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat) -> Bool:  Bool.pick(Bool, Nat.is_lt(c, n), mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{})def kids_le(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +i: Nat) -> Bool:  Bool.and(kid_le(~A, ~cmp, ss, n, u, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, u, IX.kidr(i)))def kid_le_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +hc: {Nat.is_lt(c, n) == True{} : Bool}, +h: {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}) -> {mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)) == True{} : Bool}:  L.subst(Bool, b => {Bool.pick(Bool, b, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}, Nat.is_lt(c, n), True{}, hc, h)def kid_le_in(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +eb: {Nat.is_lt(c, n) == True{} : Bool}, +h: {mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)) == True{} : Bool}) -> {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}:  %Equal.sym(Bool, Nat.is_lt(c, n), True{}, eb) : {Bool.pick(Bool, _, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}  hdef kid_le_out(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +u: Nat, +c: Nat, +eb: {Nat.is_lt(c, n) == False{} : Bool}) -> {kid_le(~A, ~cmp, ss, n, u, c) == True{} : Bool}:  %Equal.sym(Bool, Nat.is_lt(c, n), False{}, eb) : {Bool.pick(Bool, _, mle(~A, ~cmp, slot(~A, ss, u), slot(~A, ss, c)), True{}) == True{} : Bool}  {==}# ---- heap order with the two pairs below one index excluded ----## This is what a sift-DOWN carries: the hole may be larger than its children,# so the two pairs whose parent is the hole are the ones left out.def kid_of(+m: Nat, +i: Nat) -> Bool:  Bool.or(Nat.is_eq(m, IX.kidl(i)), Nat.is_eq(m, IX.kidr(i)))def pair_skip2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat) -> Bool:  Bool.pick(Bool, kid_of(m, i), True{}, pair_ok(~A, ~cmp, ss, m))def ho_exc2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat) -> Bool:  match k:    case 0n:      True{}    case 1n+ +m:      Bool.and(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i))def skip2_eq(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {kid_of(m, i) == True{} : Bool}) -> {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}:  %Equal.sym(Bool, kid_of(m, i), True{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}  {==}def skip2_ne(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +eb: {kid_of(m, i) == False{} : Bool}, +h: {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}) -> {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}:  %Equal.sym(Bool, kid_of(m, i), False{}, eb) : {Bool.pick(Bool, _, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}  hdef skip2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +m: Nat, +i: Nat, +hne: {kid_of(m, i) == False{} : Bool}, +h: {pair_skip2(~A, ~cmp, ss, m, i) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, m) == True{} : Bool}:  L.subst(Bool, b => {Bool.pick(Bool, b, True{}, pair_ok(~A, ~cmp, ss, m)) == True{} : Bool}, kid_of(m, i), False{}, hne, h)def exc2_get(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, k: Nat, +i: Nat, +j: Nat, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, N.pred(k)) == b : Bool}) -> {pair_skip2(~A, ~cmp, ss, j, i) == True{} : Bool}:  match k b:    case 0n _:      Empty.absurd({pair_skip2(~A, ~cmp, ss, j, i) == True{} : Bool}, N.lt_zero_absurd(j, hj))    case 1n+ +m True{}:      L.subst(Nat, z => {pair_skip2(~A, ~cmp, ss, z, i) == True{} : Bool}, m, j, Equal.sym(Nat, j, m, N.eq_from_is_eq(j, m, eb)), L.and_left(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h))    case 1n+ +m False{}:      exc2_get(~A, ~cmp, ss, m, i, j, L.and_right(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h), N.lt_or_eq(j, m, N.lt_succ_le(j, m, hj), eb), Nat.is_eq(j, N.pred(m)), {==})def exc2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +k: Nat, +i: Nat, +j: Nat, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hj: {Nat.is_lt(j, k) == True{} : Bool}, +hne: {kid_of(j, i) == False{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:  skip2_at(~A, ~cmp, ss, j, i, hne, exc2_get(~A, ~cmp, ss, k, i, j, h, hj, Nat.is_eq(j, N.pred(k)), {==}))def pair_of_kid(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, c: Nat, +epc: {IX.par(c) == i : Nat}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}, +h: {mle(~A, ~cmp, slot(~A, ss, i), slot(~A, ss, c)) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, c) == True{} : Bool}:  match c:    case 0n:      Empty.absurd({pair_ok(~A, ~cmp, ss, 0n) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), hcpos, {==}))    case 1n+k:      %Equal.sym(Nat, IX.par(1n+k), i, epc) : {mle(~A, ~cmp, slot(~A, ss, _), slot(~A, ss, 1n+k)) == True{} : Bool}      h# one excluded pair, from "the hole is not larger than that child"def pair_kid_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +i: Nat, +j: Nat, +c: Nat, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +ej: {Nat.is_eq(j, c) == True{} : Bool}, +epc: {IX.par(c) == i : Nat}, +hc: {kid_le(~A, ~cmp, ss, n, i, c) == True{} : Bool}, +hcpos: {Nat.is_le(1n, c) == True{} : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:  L.subst(Nat, z => {pair_ok(~A, ~cmp, ss, z) == True{} : Bool}, c, j, Equal.sym(Nat, j, c, N.eq_from_is_eq(j, c, ej)),    pair_of_kid(~A, ~cmp, ss, n, i, c, epc, hcpos, kid_le_at(~A, ~cmp, ss, n, i, c, L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, j, c, N.eq_from_is_eq(j, c, ej), hjn), hc)))def or_false(a: Bool, b: Bool, +ea: {a == False{} : Bool}, +eb: {b == False{} : Bool}) -> {Bool.or(a, b) == False{} : Bool}:  %Equal.sym(Bool, a, False{}, ea) : {Bool.or(_, b) == False{} : Bool}  eb# `ho_upto` from `ho_exc2` plus "the hole is not larger than its children"def ho_of_exc2_at(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, +k: Nat, +i: Nat, +j: Nat, +hjk: {Nat.is_lt(j, k) == True{} : Bool}, +hjn: {Nat.is_lt(j, n) == True{} : Bool}, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hkids: {kids_le(~A, ~cmp, ss, n, i, i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(j, IX.kidl(i)) == b : Bool}, c: Bool, +ec: {Nat.is_eq(j, IX.kidr(i)) == c : Bool}) -> {pair_ok(~A, ~cmp, ss, j) == True{} : Bool}:  match b c:    case True{} _:      pair_kid_at(~A, ~cmp, ss, n, i, j, IX.kidl(i), hjn, eb, IX.par_kidl(i), L.and_left(kid_le(~A, ~cmp, ss, n, i, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, i, IX.kidr(i)), hkids), IX.kidl_pos1(i))    case False{} True{}:      pair_kid_at(~A, ~cmp, ss, n, i, j, IX.kidr(i), hjn, ec, IX.par_kidr(i), L.and_right(kid_le(~A, ~cmp, ss, n, i, IX.kidl(i)), kid_le(~A, ~cmp, ss, n, i, IX.kidr(i)), hkids), IX.kidr_pos1(i))    case False{} False{}:      exc2_at(~A, ~cmp, ss, k, i, j, h, hjk, or_false(Nat.is_eq(j, IX.kidl(i)), Nat.is_eq(j, IX.kidr(i)), eb, ec))def ho_of_exc2(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +n: Nat, k: Nat, +i: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +h: {ho_exc2(~A, ~cmp, ss, k, i) == True{} : Bool}, +hkids: {kids_le(~A, ~cmp, ss, n, i, i) == True{} : Bool}) -> {ho_upto(~A, ~cmp, ss, k) == True{} : Bool}:  match k:    case 0n:      {==}    case 1n+ +m:      L.and_intro(pair_ok(~A, ~cmp, ss, m), ho_upto(~A, ~cmp, ss, m),        ho_of_exc2_at(~A, ~cmp, ss, n, 1n+m, i, m, N.lt_succ(m), N.lt_le_trans(m, 1n+m, n, N.lt_succ(m), hk), h, hkids, Nat.is_eq(m, IX.kidl(i)), {==}, Nat.is_eq(m, IX.kidr(i)), {==}),        ho_of_exc2(~A, ~cmp, ss, n, m, i, N.le_trans(m, 1n+m, n, N.le_succ(m), hk), L.and_right(pair_skip2(~A, ~cmp, ss, m, i), ho_exc2(~A, ~cmp, ss, m, i), h), hkids))