~/bend-docscommunity

proofs/containers/binary_heap/up.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/up.bend as Up

16 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/order.bend as O
import ../../lib/array.bend as AR
import ../../lib/u32.bend as U
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/binary_heap.bend as S
import ../../../src/containers/binary_heap.bend as H
import ./idx.bend as IX
import ./u32idx.bend as UX
import ./slots.bend as SL
import ./vals.bend as V
import ./bag.bend as BG
import ./multiset.bend as M

Types

type UpS source · line 21 · raw

@-A:Data -> Data

Definitions

def double_pos source · line 70 · raw

@+v:Nat -> @+h:{Nat.is_lt(0n, v) == True{} : Bool} -> {Nat.is_lt(0n, Nat.double(v)) == True{} : Bool}

def pow2_pos source · line 77 · raw

@+d:Nat -> {Nat.is_lt(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

def pos_of source · line 84 · raw

@+i:Nat -> @+eb:{Nat.is_eq(i, 0n) == False{} : Bool} -> {Nat.is_le(i, 0n) == False{} : Bool}

def par_ne source · line 204 · raw

@+i:Nat -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == False{} : Bool}

def par_lt_d source · line 207 · raw

@+d:Nat -> @+i:Nat -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

def pos_of_ne source · line 253 · raw

@+j:Nat -> @+h:{Nat.is_eq(j, 0n) == False{} : Bool} -> {Nat.is_le(1n, j) == True{} : Bool}

j >= 1 whenever j is not 0

def kid_at source · line 279 · raw

@+i:Nat -> @+j:Nat -> @+epj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j) == i : Nat} -> @e:Or({j == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) : Nat}, {j == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) : Nat}) -> Or({j == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) : Nat}, {j == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) : Nat})

def par_lt_kid source · line 306 · raw

@+i:Nat -> @+j:Nat -> @+epj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j) == i : Nat} -> @+hjpos:{Nat.is_le(1n, j) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == True{} : Bool}

Templates

template ureal source · line 25 · raw

@-A:Data -> @s:UpS<A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Up<A>

template udec source · line 34 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @pv:A -> @p:Nat -> @ok:Bool -> UpS<A>

template umb source · line 41 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @p:Nat -> @m:Maybe<&2, A> -> UpS<A>

template uroot source · line 48 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @root:Bool -> UpS<A>

template uprobe source · line 55 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> UpS<A>

template get_slot source · line 61 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+j:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {Array.get(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(j)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j)) : Pair(Array<Maybe<&2, A>>, Maybe<&2, A>)}

the slot the implementation reads, as an Array.get result

template udec_ok source · line 91 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+pv:A -> @+p:Nat -> @b:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_dec(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Up<A>}

template umb_ok source · line 98 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+p:Nat -> @m:Maybe<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_mb(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Up<A>}

template uroot_false source · line 107 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_root(A, cmp, U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), False{}) == ureal(A, uroot(A, cmp, t, i, x, False{})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Up<A>}

i > 0: the implementation reads the parent slot and the mirror reads the same slot of the shadow's slot list.

template uroot_ok source · line 113 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(i, 0n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_root(A, cmp, U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), b) == ureal(A, uroot(A, cmp, t, i, x, b)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Up<A>}

template uprobe_ok source · line 121 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_probe(A, cmp, U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)) == ureal(A, uprobe(A, cmp, t, i, x)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Up<A>}

is_eq(i, 0) = False gives 1 <= i

template ulog source · line 131 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> List<&2, Maybe<&2, A>>

template mval source · line 134 · raw

@-A:Data -> @m:Maybe<&2, A> -> @d:A -> A

template in_range source · line 142 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t))) == True{} : Bool}

slot bookkeeping for a tree whose slot list has 2^d entries

template ulog_at source · line 145 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), i) == Some{x} : Maybe<&2, A>}

template ulog_off source · line 148 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+j:Nat -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}

template UpOK source · line 153 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @d:Nat -> @n:Nat -> @tgt:List<&2, A> -> @fuel:Nat -> @x:A -> @s:UpS<A> -> Type

template set_tree source · line 158 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>>

the block after the last write, and the fact that its slot list is the logical array the invariant is about

template set_slots source · line 161 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, set_tree(A, d, t, i, x)) == ulog(A, t, i, x) : List<&2, Maybe<&2, A>>}

template set_eq source · line 164 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {Array.set(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(i), Some{x}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, set_tree(A, d, t, i, x)) : Array<Maybe<&2, A>>}

template up_stop_mk source · line 175 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @+fuel:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+eq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, fuel, x, ureal(A, Stp{t, i})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, set_tree(A, d, t, i, x)) : Array<Maybe<&2, A>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpair:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ulog(A, t, i, x), i) == True{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ulog(A, t, i, x), n) == True{} : Bool} -> @+hms:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> UpOK(A, cmp, d, n, tgt, fuel, x, Stp{t, i})

template up_stop_ok source · line 185 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @fuel:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpair:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ulog(A, t, i, x), i) == True{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ulog(A, t, i, x), n) == True{} : Bool} -> @+hms:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> UpOK(A, cmp, d, n, tgt, fuel, x, Stp{t, i})

template t2_of source · line 198 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+pv:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>>

template u2_of source · line 201 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> List<&2, Maybe<&2, A>>

template t2_perfect source · line 210 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+pv:A -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t2_of(A, d, t, i, pv)) == True{} : Bool}

template u2_at_p source · line 213 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{x} : Maybe<&2, A>}

template u2_at_i source · line 216 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), i) == Some{pv} : Maybe<&2, A>}

template u2_off source · line 223 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+j:Nat -> @+hji:{Nat.is_eq(i, j) == False{} : Bool} -> @+hjp:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}

template u1_at_p source · line 231 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>}

the same three for the CURRENT logical array

template pair_ok_pos source · line 238 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @i:Nat -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ss, i) == True{} : Bool}

template pair_ok_val source · line 245 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @i:Nat -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ss, i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i)) == True{} : Bool}

template h1n_i_mle source · line 270 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), i)) == True{} : Bool}

template h1n_i source · line 275 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h1n_kid_fix source · line 287 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), j)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{pv}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j)) == True{} : Bool}

rewrite H2 from the logical array to the block

template h1n_kid_mle source · line 293 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @e:Or({j == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) : Nat}, {j == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) : Nat}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{pv}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j)) == True{} : Bool}

pv is not larger than a child of the old hole (this is H2)

template h1n_kid_goal source · line 309 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+j:Nat -> @+epj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j) == i : Nat} -> @+hij:{Nat.is_eq(i, j) == False{} : Bool} -> @+hpij:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{pv}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), j)) == True{} : Bool}

template h1n_kid source · line 314 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+j:Nat -> @+hjne:{Nat.is_eq(j, i) == False{} : Bool} -> @+epj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h1n_old source · line 321 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+j:Nat -> @+hij:{Nat.is_eq(i, j) == False{} : Bool} -> @+epj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i) : Nat} -> @+hjpos:{Nat.is_le(1n, j) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ulog(A, t, i, x), j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{pv}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j)) == True{} : Bool}

template h1n_sib_goal source · line 327 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+j:Nat -> @+hij:{Nat.is_eq(i, j) == False{} : Bool} -> @+hpij:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+epj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i) : Nat} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{pv}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), j)) == True{} : Bool}

template h1n_sib source · line 332 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+epj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i) : Nat} -> @+hjpos:{Nat.is_le(1n, j) == True{} : Bool} -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h1n_far_goal source · line 336 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+j:Nat -> @+hij:{Nat.is_eq(i, j) == False{} : Bool} -> @+hpij:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+hipj:{Nat.is_eq(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) == False{} : Bool} -> @+hppj:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) == False{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), j)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), j)) == True{} : Bool}

template h1n_far source · line 342 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+hipj:{Nat.is_eq(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) == False{} : Bool} -> @+hppj:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h1_next_s source · line 349 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+hipj:{Nat.is_eq(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @b3:Bool -> @+eb3:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) == b3 : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h1_next_p source · line 356 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @b2:Bool -> @+eb2:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j), i) == b2 : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h1_next_pos source · line 363 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+j:Nat -> @+hpij:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @b1:Bool -> @+eb1:{Nat.is_eq(j, i) == b1 : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h1_next_at source · line 370 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), j) == False{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, u2_of(A, d, t, i, x, pv), j) == True{} : Bool}

template h2_key_root source · line 380 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i) == 0n : Nat} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), Some{pv}) == True{} : Bool}

template h2_key_deep source · line 386 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+e:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), 0n) == False{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), Some{pv}) == True{} : Bool}

template h2_key source · line 396 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), 0n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), Some{pv}) == True{} : Bool}

template kid_mle_same source · line 403 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+key:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), Some{pv}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), c)) == True{} : Bool}

template kid_mle_other source · line 407 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+c:Nat -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+key:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), Some{pv}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), c)) == True{} : Bool}

template kid_mle source · line 412 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+c:Nat -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i) : Nat} -> @+hcpos:{Nat.is_le(1n, c) == True{} : Bool} -> @+hcn:{Nat.is_lt(c, n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(c, i) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), c)) == True{} : Bool}

template kid_next source · line 420 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+c:Nat -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i) : Nat} -> @+hcpos:{Nat.is_le(1n, c) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_lt(c, n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, u2_of(A, d, t, i, x, pv), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), c) == True{} : Bool}

H2 for the next state: both children of the new hole

template kids_next source · line 428 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, u2_of(A, d, t, i, x, pv), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == True{} : Bool}

template skip_next source · line 435 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_skip(A, cmp, u2_of(A, d, t, i, x, pv), m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == True{} : Bool}

template exc_next source · line 443 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == False{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, u2_of(A, d, t, i, x, pv), k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == True{} : Bool}

template some_of_eq source · line 452 · raw

@-A:Data -> @m:Maybe<&2, A> -> @+v:A -> @+e:{m == Some{v} : Maybe<&2, A>} -> {Maybe.is_some(&2, A, m) == True{} : Bool}

template some_next source · line 455 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ulog(A, t, i, x), n) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == b : Bool} -> @c:Bool -> @+ec:{Nat.is_eq(m, i) == c : Bool} -> {Maybe.is_some(&2, A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, u2_of(A, d, t, i, x, pv), m)) == True{} : Bool}

template lay_next source · line 470 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ulog(A, t, i, x), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, u2_of(A, d, t, i, x, pv), k) == True{} : Bool}

template u2_swap_form source · line 481 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {u2_of(A, d, t, i, x, pv) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ulog(A, t, i, x), i, Some{pv}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), Some{x}) : List<&2, Maybe<&2, A>>}

template ms_next source · line 487 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+n:Nat -> @+tgt:List<&2, A> -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hms:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, u2_of(A, d, t, i, x, pv), n)) == tgt : List<&2, A>}

template pair_ok_zero source · line 499 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+e:{Nat.is_eq(i, 0n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ss, i) == True{} : Bool}

template pair_none source · line 502 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == None{} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ulog(A, t, i, x), i) == True{} : Bool}

template pair_stop_mle source · line 509 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ulog(A, t, i, x), i)) == True{} : Bool}

template pair_stop source · line 514 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == Some{pv} : Maybe<&2, A>} -> @+hle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, pv, x) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ulog(A, t, i, x), i) == True{} : Bool}

template up_carry_go source · line 518 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @+f:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+t3:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+eq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, 1n+f, x, ureal(A, Mv{t, i, pv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, f, x, ureal(A, uprobe(A, cmp, t2_of(A, d, t, i, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), x))) : Array<Maybe<&2, A>>} -> @rest:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, f, x, ureal(A, uprobe(A, cmp, t2_of(A, d, t, i, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), x))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t3) : Array<Maybe<&2, A>>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t3) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t3), n) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t3), n) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t3), n)) == tgt : List<&2, A>})))) -> UpOK(A, cmp, d, n, tgt, 1n+f, x, Mv{t, i, pv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)})

template up_carry source · line 524 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @+f:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+eq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, 1n+f, x, ureal(A, Mv{t, i, pv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, f, x, ureal(A, uprobe(A, cmp, t2_of(A, d, t, i, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.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), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), x)) -> UpOK(A, cmp, d, n, tgt, 1n+f, x, Mv{t, i, pv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)})

The recursive result is about the next state; its first component has to be rewritten through the step the loop took.

template up_step_eq source · line 528 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+f:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+pv:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, 1n+f, x, ureal(A, Mv{t, i, pv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, f, x, ureal(A, uprobe(A, cmp, t2_of(A, d, t, i, pv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), x))) : Array<Maybe<&2, A>>}

template up_loop source · line 536 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @fuel:Nat -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hfuel:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(fuel)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ulog(A, t, i, x), n) == True{} : Bool} -> @+hms:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.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:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)) == m : Maybe<&2, A>} -> @ble:Bool -> @+eble:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, mval(A, m, x), x) == ble : Bool} -> UpOK(A, cmp, d, n, tgt, fuel, x, uprobe(A, cmp, t, i, x))

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.

template SiftOK source · line 573 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @d:Nat -> @n:Nat -> @tgt:List<&2, A> -> @fuel:Nat -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @i:Nat -> @x:A -> Type

template sift_from_go source · line 576 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @+fuel:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+t2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+eq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.sift_up(A, cmp, fuel, U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, fuel, x, ureal(A, uprobe(A, cmp, t, i, x))) : Array<Maybe<&2, A>>} -> @rest:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.up_go(A, cmp, fuel, x, ureal(A, uprobe(A, cmp, t, i, x))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t2) : Array<Maybe<&2, A>>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t2) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2), n) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2), n) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2), n)) == tgt : List<&2, A>})))) -> SiftOK(A, cmp, d, n, tgt, fuel, t, i, x)

template sift_from_loop source · line 580 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @+fuel:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+eq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.sift_up(A, cmp, fuel, U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.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)

template sift_up_ok source · line 584 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+fuel:Nat -> @+d:Nat -> @+n:Nat -> @+tgt:List<&2, A> -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hfuel:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(fuel)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc(A, cmp, ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ulog(A, t, i, x), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ulog(A, t, i, x), n) == True{} : Bool} -> @+hms:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> SiftOK(A, cmp, d, n, tgt, fuel, t, i, x)