proofs/containers/binary_heap/down.bend checks

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

17 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
import ./up.bend as UPS

Types

type DownS source · line 31 · raw

@-A:Data -> Data

DStp

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

DMv

@-A:Data -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @i:Nat -> @cv:A -> @ci:Nat -> DownS<A>

Definitions

def double_gt source · line 89 · raw

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

def pow2_up source · line 96 · raw

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

def double_lt_pow source · line 99 · raw

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

def kidl_bridge source · line 102 · raw

@+i:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {U32.inc(U32.shl(U32.from_nat(i))) == U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) : U32}

def right_in source · line 132 · raw

@+l:Nat -> @+n:Nat -> @+e:{Nat.is_lt(l, Nat.sub(n, 1n)) == True{} : Bool} -> {Nat.is_lt(1n+l, n) == True{} : Bool}

def two_bridge source · line 153 · raw

@+l:Nat -> @+n:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hl:{Nat.is_lt(l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hln:{Nat.is_lt(l, n) == True{} : Bool} -> @+hn:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {U32.is_lt(U32.from_nat(l), U32.sub(U32.from_nat(n), 1)) == Nat.is_lt(l, Nat.sub(n, 1n)) : Bool}

def eq_of_eq source · line 262 · raw

@+a:Nat -> @+b:Nat -> @+e:{a == b : Nat} -> {Nat.is_eq(a, b) == True{} : Bool}

def or_left source · line 265 · raw

@a:Bool -> @b:Bool -> @+ea:{a == True{} : Bool} -> {Bool.or(a, b) == True{} : Bool}

def or_right source · line 269 · raw

@a:Bool -> @b:Bool -> @+eb:{b == True{} : Bool} -> {Bool.or(a, b) == True{} : Bool}

def par_not_absurd source · line 276 · raw

@+j:Nat -> @+u:Nat -> @+hkf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, u) == False{} : Bool} -> @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}) -> @+ep:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j) == u : Nat} -> Empty

def par_not_of source · line 283 · raw

@+j:Nat -> @+u:Nat -> @+hkf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, u) == False{} : Bool} -> @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}) -> @b:Bool -> @+eb:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j), u) == b : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j), u) == False{} : Bool}

def par_not source · line 290 · raw

@+j:Nat -> @+u:Nat -> @+hjpos:{Nat.is_le(1n, j) == True{} : Bool} -> @+hkf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, u) == False{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j), u) == False{} : Bool}

def eq_false_of source · line 309 · raw

@+j:Nat -> @+a:Nat -> @+b:Nat -> @+e:{a == b : Nat} -> @+h:{Nat.is_eq(j, b) == False{} : Bool} -> {Nat.is_eq(j, a) == False{} : Bool}

def side_false source · line 312 · raw

@+j:Nat -> @+u:Nat -> @+ci:Nat -> @+s:Nat -> @+hjc:{Nat.is_eq(j, ci) == False{} : Bool} -> @+hjs:{Nat.is_eq(j, s) == False{} : Bool} -> @e:Either<&2, &2, {u == ci : Nat}, {u == s : Nat}> -> {Nat.is_eq(j, u) == False{} : Bool}

def or_false source · line 319 · raw

@a:Bool -> @b:Bool -> @+ea:{a == False{} : Bool} -> @+eb:{b == False{} : Bool} -> {Bool.or(a, b) == False{} : Bool}

def kid_of_false source · line 323 · raw

@+j:Nat -> @+i:Nat -> @+ci:Nat -> @+s:Nat -> @+hjc:{Nat.is_eq(j, ci) == False{} : Bool} -> @+hjs:{Nat.is_eq(j, s) == False{} : Bool} -> @ecl:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == s : Nat}> -> @ecr:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == s : Nat}> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, i) == False{} : Bool}

def par_of_kid_go source · line 355 · raw

@+k:Nat -> @+i:Nat -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(k, i) == True{} : Bool} -> @b:Bool -> @+ebl:{Nat.is_eq(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == b : Bool} -> @c:Bool -> @+ebr:{Nat.is_eq(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k) == i : Nat}

def par_of_kid source · line 364 · raw

@+k:Nat -> @+i:Nat -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(k, i) == True{} : Bool} -> @e:Or({k == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k)) : Nat}, {k == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k)) : Nat}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k) == i : Nat}

def kid_of_grand_go source · line 367 · raw

@+k:Nat -> @+i:Nat -> @+ci:Nat -> @+epk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k) == ci : Nat} -> @+hne:{Nat.is_eq(ci, i) == False{} : Bool} -> @b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(k, i) == b : Bool} -> @+hkpos:{Nat.is_le(1n, k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(k, i) == False{} : Bool}

def kid_of_grand source · line 375 · raw

@+k:Nat -> @+i:Nat -> @+ci:Nat -> @+epk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k) == ci : Nat} -> @+hkpos:{Nat.is_le(1n, k) == True{} : Bool} -> @+hne:{Nat.is_eq(ci, i) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(k, i) == False{} : Bool}

def k_gt_i source · line 378 · raw

@+k:Nat -> @+i:Nat -> @+ci:Nat -> @+epk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k) == ci : Nat} -> @+hkpos:{Nat.is_le(1n, k) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> {Nat.is_lt(i, k) == True{} : Bool}

def kidr_out source · line 508 · raw

@+i:Nat -> @+n:Nat -> @+e:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == False{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i), n) == False{} : Bool}

kidl i >= n implies kidr i >= n

def kidr_out2 source · line 512 · raw

@+i:Nat -> @+n:Nat -> @+e:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), Nat.sub(n, 1n)) == False{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i), n) == False{} : Bool}

the right child is out of range exactly when the two test fails

def kidr_in2 source · line 515 · raw

@+i:Nat -> @+n:Nat -> @+e:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), Nat.sub(n, 1n)) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i), n) == True{} : Bool}

def kidl_ne_kidr source · line 518 · raw

@+i:Nat -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == False{} : Bool}

def fuel_out source · line 687 · raw

@+i:Nat -> @+n:Nat -> @+ehasl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == True{} : Bool} -> @+hfuel:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.scale(0n, 1n+i)) == True{} : Bool} -> Empty

with no fuel left the hole has no children: n <= 1 + i and kidl i < n force 2i + 1 < 1 + i

Templates

template dreal source · line 35 · raw

@-A:Data -> @s:DownS<A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>

template ddec source · line 44 · raw

@-A:Data -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @cv:A -> @ci:Nat -> @ok:Bool -> DownS<A>

template dcmp source · line 51 · raw

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

template dtwo source · line 54 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @x:A -> @l:Nat -> @+lv:A -> @r:Nat -> @+rv:A -> @left:Bool -> DownS<A>

template drmb source · line 61 · raw

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

template dlmb source · line 68 · raw

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

template dhas source · line 77 · raw

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

template dprobe source · line 84 · raw

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

template ddec_ok source · line 106 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+cv:A -> @+ci:Nat -> @b:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_dec(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(i), cv, U32.from_nat(ci), b) == dreal(A, ddec(A, t, i, cv, ci, b)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>}

template dcmp_ok source · line 113 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_dec(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(i), cv, U32.from_nat(ci), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv)) == dreal(A, dcmp(A, cmp, t, i, x, cv, ci)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>}

template dtwo_ok source · line 116 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+l:Nat -> @+lv:A -> @+r:Nat -> @+rv:A -> @b:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_two(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(i), x, U32.from_nat(l), lv, U32.from_nat(r), rv, b) == dreal(A, dtwo(A, cmp, t, i, x, l, lv, r, rv, b)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>}

template drmb_ok source · line 123 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+l:Nat -> @+lv:A -> @+r:Nat -> @m:Maybe<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_rmb(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(i), x, U32.from_nat(l), lv, U32.from_nat(r), m) == dreal(A, drmb(A, cmp, t, i, x, l, lv, r, m)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>}

template dlmb_ok source · line 138 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+l:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hn:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @two:Bool -> @m:Maybe<&2, A> -> @+etwo:{Nat.is_lt(l, Nat.sub(n, 1n)) == two : Bool} -> @+hl:{l == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_lmb(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(i), x, U32.from_nat(l), two, m) == dreal(A, dlmb(A, cmp, t, i, x, l, two, m)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>}

template dhas_ok source · line 159 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hn:{Nat.is_le(n, 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_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_has(A, cmp, U32.from_nat(n), U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)), b) == dreal(A, dhas(A, cmp, n, i, x, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), b)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>}

template dprobe_ok source · line 169 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n: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} -> @+hn:{Nat.is_le(n, 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.down_probe(A, cmp, U32.from_nat(n), U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)) == dreal(A, dprobe(A, cmp, n, i, x, t)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Down<A>}

template t2_of source · line 180 · raw

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

template d2_of source · line 183 · raw

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

template d2_at_c source · line 186 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+hc:{Nat.is_lt(ci, 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, d2_of(A, d, t, i, x, cv, ci), ci) == Some{x} : Maybe<&2, A>}

template d2_at_i source · line 189 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+hne:{Nat.is_eq(ci, i) == 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, d2_of(A, d, t, i, x, cv, ci), i) == Some{cv} : Maybe<&2, A>}

template d2_off source · line 196 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+j:Nat -> @+hji:{Nat.is_eq(i, j) == False{} : Bool} -> @+hjc:{Nat.is_eq(ci, 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, d2_of(A, d, t, i, x, cv, ci), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}

template d1_at_i source · line 205 · 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), i) == Some{x} : Maybe<&2, A>}

template kid_pick_of source · line 208 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+i:Nat -> @+ci:Nat -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ss, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @e:Or({ci == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) : Nat}, {ci == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) : Nat}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, ss, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), ci) == True{} : Bool}

template kid_pick source · line 215 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+i:Nat -> @+ci:Nat -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, ss, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, ss, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), ci) == True{} : Bool}

template d1n_i_mle source · line 218 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+hcn:{Nat.is_lt(ci, n) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, i) == 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} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, d2_of(A, d, t, i, x, cv, ci), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, d2_of(A, d, t, i, x, cv, ci), i)) == True{} : Bool}

template d1n_i source · line 225 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+j:Nat -> @+ej:{Nat.is_eq(j, i) == True{} : Bool} -> @+hcn:{Nat.is_lt(ci, n) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == 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} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(i, 0n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template d1n_c_mle source · line 236 · 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 -> @+cv:A -> @+ci:Nat -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == 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} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, d2_of(A, d, t, i, x, cv, ci), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, d2_of(A, d, t, i, x, cv, ci), ci)) == True{} : Bool}

template d1n_c source · line 243 · 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 -> @+cv:A -> @+ci:Nat -> @+j:Nat -> @+ej:{Nat.is_eq(j, ci) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == 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} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template d1n_s_mle source · line 248 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @+hsn:{Nat.is_lt(s, n) == True{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, d2_of(A, d, t, i, x, cv, ci), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, d2_of(A, d, t, i, x, cv, ci), s)) == True{} : Bool}

template d1n_s source · line 257 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @+j:Nat -> @+ej:{Nat.is_eq(j, s) == True{} : Bool} -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template d1n_far_mle source · line 293 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+j:Nat -> @+hji:{Nat.is_eq(j, i) == False{} : Bool} -> @+hjc:{Nat.is_eq(j, ci) == False{} : Bool} -> @+hpi:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j), i) == False{} : Bool} -> @+hpc:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j), ci) == 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} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.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, d2_of(A, d, t, i, x, cv, ci), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, d2_of(A, d, t, i, x, cv, ci), j)) == True{} : Bool}

template d1n_far source · line 300 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+j:Nat -> @+hji:{Nat.is_eq(j, i) == False{} : Bool} -> @+hjc:{Nat.is_eq(j, ci) == False{} : Bool} -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hkf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, i) == False{} : Bool} -> @+hkf2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, ci) == False{} : Bool} -> @+hjpos:{Nat.is_le(1n, j) == 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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template d1_next_s source · line 326 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @+j:Nat -> @+hji:{Nat.is_eq(j, i) == False{} : Bool} -> @+hjc:{Nat.is_eq(j, ci) == False{} : Bool} -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hjpos:{Nat.is_le(1n, j) == True{} : Bool} -> @+hkf2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, ci) == False{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+ecl:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == s : Nat}> -> @+ecr:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == s : Nat}> -> @+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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @b:Bool -> @+eb:{Nat.is_eq(j, s) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template d1_next_c source · line 333 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @+j:Nat -> @+hji:{Nat.is_eq(j, i) == False{} : Bool} -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hjpos:{Nat.is_le(1n, j) == True{} : Bool} -> @+hkf2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, ci) == False{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ecl:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == s : Nat}> -> @+ecr:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == s : Nat}> -> @+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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == False{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(j, ci) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template d1_next_pos source · line 340 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @+j:Nat -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hjpos:{Nat.is_le(1n, j) == True{} : Bool} -> @+hkf2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, ci) == False{} : Bool} -> @+hcn:{Nat.is_lt(ci, n) == True{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ecl:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == s : Nat}> -> @+ecr:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == s : Nat}> -> @+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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == False{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(j, i) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template d1_next_at source · line 347 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @j:Nat -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hkf2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, ci) == False{} : Bool} -> @+hcn:{Nat.is_lt(ci, n) == True{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ecl:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == s : Nat}> -> @+ecr:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == s : Nat}> -> @+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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, d2_of(A, d, t, i, x, cv, ci), j) == True{} : Bool}

template t2_at_i source · line 383 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+cv: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2_of(A, d, t, i, cv)), i) == Some{cv} : Maybe<&2, A>}

template t2_off source · line 388 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+cv:A -> @+j:Nat -> @+hij:{Nat.is_eq(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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2_of(A, d, t, i, cv)), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j) : Maybe<&2, A>}

template kid_next_mle source · line 393 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+k:Nat -> @+epk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k) == ci : Nat} -> @+hkpos:{Nat.is_le(1n, k) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hcne:{Nat.is_eq(ci, i) == False{} : Bool} -> @+hkn:{Nat.is_lt(k, 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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2_of(A, d, t, i, cv)), i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2_of(A, d, t, i, cv)), k)) == True{} : Bool}

template kid_next_one source · line 404 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+k:Nat -> @+epk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(k) == ci : Nat} -> @+hkpos:{Nat.is_le(1n, k) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hcne:{Nat.is_eq(ci, i) == 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} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @b:Bool -> @+eb:{Nat.is_lt(k, n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2_of(A, d, t, i, cv)), n, i, k) == True{} : Bool}

template kids_next_d source · line 412 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hcne:{Nat.is_eq(ci, i) == 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} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t2_of(A, d, t, i, cv)), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci), ci) == True{} : Bool}

template skip2_next source · line 419 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @+m:Nat -> @+hmn:{Nat.is_lt(m, n) == True{} : Bool} -> @+hcn:{Nat.is_lt(ci, n) == True{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ecl:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == s : Nat}> -> @+ecr:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == s : Nat}> -> @+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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == False{} : Bool} -> @b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(m, ci) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_skip2(A, cmp, d2_of(A, d, t, i, x, cv, ci), m, ci) == True{} : Bool}

D1 for the next state, built index by index

template exc2_next source · line 427 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+s:Nat -> @k:Nat -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+hcn:{Nat.is_lt(ci, n) == True{} : Bool} -> @+hsc:{Nat.is_eq(ci, s) == False{} : Bool} -> @+eps:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(s) == i : Nat} -> @+hspos:{Nat.is_le(1n, s) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(ci) == i : Nat} -> @+hcpos:{Nat.is_le(1n, ci) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ecl:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i) == s : Nat}> -> @+ecr:Either<&2, &2, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == ci : Nat}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i) == s : Nat}> -> @+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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hsib:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, ci, s) == True{} : Bool} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc2(A, cmp, d2_of(A, d, t, i, x, cv, ci), k, ci) == True{} : Bool}

template some_next_d source · line 437 · raw

@-A:Data -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+m:Nat -> @+hmn:{Nat.is_lt(m, n) == True{} : Bool} -> @+hcne:{Nat.is_eq(ci, i) == False{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(m, ci) == 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, d2_of(A, d, t, i, x, cv, ci), m)) == True{} : Bool}

the layout and the multiset of the next state

template lay_next_d source · line 452 · raw

@-A:Data -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @k:Nat -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+hcne:{Nat.is_eq(ci, i) == False{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, d2_of(A, d, t, i, x, cv, ci), k) == True{} : Bool}

template d2_swap_form source · line 461 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+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} -> {d2_of(A, d, t, i, x, cv, ci) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), i, Some{cv}), ci, Some{x}) : List<&2, Maybe<&2, A>>}

template ms_next_d source · line 467 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+tgt:List<&2, A> -> @+hin:{Nat.is_lt(i, n) == True{} : Bool} -> @+hcn:{Nat.is_lt(ci, n) == True{} : Bool} -> @+hcne:{Nat.is_eq(ci, i) == 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} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), ci) == Some{cv} : Maybe<&2, A>} -> @+hms:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.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, d2_of(A, d, t, i, x, cv, ci), n)) == tgt : List<&2, A>}

template DownOK source · line 477 · raw

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

template down_stop_mk source · line 481 · 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.down_go(A, cmp, fuel, U32.from_nat(n), x, dreal(A, DStp{t, i})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.set_tree(A, d, t, i, x)) : Array<Maybe<&2, A>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hn:{Nat.is_le(n, 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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i, i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> DownOK(A, cmp, d, n, tgt, fuel, x, DStp{t, i})

the loop stops: x is written at the hole and the two pairs below it hold

template down_stop_ok source · line 491 · 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} -> @+hn:{Nat.is_le(n, 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_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i, i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> DownOK(A, cmp, d, n, tgt, fuel, x, DStp{t, i})

template slot_some_at source · line 502 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+n:Nat -> @+j:Nat -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hji:{Nat.is_eq(i, j) == False{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n) == True{} : Bool} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), j) == None{} : Maybe<&2, A>} -> Empty

a slot inside the heap is occupied, so a probe that reads None there is impossible

template kid_le_x_mle source · line 521 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+c:Nat -> @+cv:A -> @+hci:{Nat.is_eq(i, c) == 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} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), c) == Some{cv} : Maybe<&2, A>} -> @+hle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), c)) == True{} : Bool}

template kid_le_x source · line 528 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+n:Nat -> @+c:Nat -> @+cv:A -> @+hcn:{Nat.is_lt(c, n) == True{} : Bool} -> @+hci:{Nat.is_eq(i, c) == 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} -> @+hcv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), c) == Some{cv} : Maybe<&2, A>} -> @+hle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, cv) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i, c) == True{} : Bool}

"x is not larger than that child", as the kid_le conjunct

template pick_cv2 source · line 534 · raw

@-A:Data -> @+x:A -> @+lv:A -> @two:Bool -> @mr:Maybe<&2, A> -> @left:Bool -> A

the value the probe compares x with, as a function of its three reads

template pick_cv source · line 545 · raw

@-A:Data -> @+x:A -> @ml:Maybe<&2, A> -> @two:Bool -> @mr:Maybe<&2, A> -> @left:Bool -> A

template down_carry_go source · line 552 · 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 -> @+cv:A -> @+ci:Nat -> @+t3:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+eq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, 1n+f, U32.from_nat(n), x, dreal(A, DMv{t, i, cv, ci})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, f, U32.from_nat(n), x, dreal(A, dprobe(A, cmp, n, ci, x, t2_of(A, d, t, i, cv)))) : Array<Maybe<&2, A>>} -> @rest:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, f, U32.from_nat(n), x, dreal(A, dprobe(A, cmp, n, ci, x, t2_of(A, d, t, i, cv)))) == 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>})))) -> DownOK(A, cmp, d, n, tgt, 1n+f, x, DMv{t, i, cv, ci})

template down_carry source · line 556 · 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 -> @+cv:A -> @+ci:Nat -> @+eq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, 1n+f, U32.from_nat(n), x, dreal(A, DMv{t, i, cv, ci})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, f, U32.from_nat(n), x, dreal(A, dprobe(A, cmp, n, ci, x, t2_of(A, d, t, i, cv)))) : Array<Maybe<&2, A>>} -> @rec:DownOK(A, cmp, d, n, tgt, f, x, dprobe(A, cmp, n, ci, x, t2_of(A, d, t, i, cv))) -> DownOK(A, cmp, d, n, tgt, 1n+f, x, DMv{t, i, cv, ci})

template down_step_eq source · line 560 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+n:Nat -> @+f:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+cv:A -> @+ci:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hc:{Nat.is_lt(ci, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hn:{Nat.is_le(n, 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.down_go(A, cmp, 1n+f, U32.from_nat(n), x, dreal(A, DMv{t, i, cv, ci})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, f, U32.from_nat(n), x, dreal(A, dprobe(A, cmp, n, ci, x, t2_of(A, d, t, i, cv)))) : Array<Maybe<&2, A>>}

template pick_state2 source · line 566 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+lv:A -> @two:Bool -> @mr:Maybe<&2, A> -> @left:Bool -> @ok:Bool -> DownS<A>

the probe's result as a function of its three reads and two comparisons

template pick_state source · line 585 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @hasl:Bool -> @ml:Maybe<&2, A> -> @two:Bool -> @mr:Maybe<&2, A> -> @left:Bool -> @ok:Bool -> DownS<A>

template probe_shape source · line 594 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+n:Nat -> @+i:Nat -> @+x:A -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @hasl:Bool -> @+ehasl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == hasl : Bool} -> @ml:Maybe<&2, A> -> @+eml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == ml : Maybe<&2, A>} -> @two:Bool -> @+etwo:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), Nat.sub(n, 1n)) == two : Bool} -> @mr:Maybe<&2, A> -> @+emr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == mr : Maybe<&2, A>} -> @left:Bool -> @+eleft:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.mval(A, ml, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.mval(A, mr, x)) == left : Bool} -> @ok:Bool -> @+eok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, pick_cv(A, x, ml, two, mr, left)) == ok : Bool} -> {dprobe(A, cmp, n, i, x, t) == pick_state(A, t, i, hasl, ml, two, mr, left, ok) : DownS<A>}

template g_no_left source · line 670 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+n:Nat -> @+e:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i, i) == True{} : Bool}

template g_left_only source · line 675 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+x:A -> @+n:Nat -> @+lv:A -> @+ehasl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == True{} : Bool} -> @+etwo:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), Nat.sub(n, 1n)) == False{} : Bool} -> @+eml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == Some{lv} : Maybe<&2, A>} -> @+eok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, lv) == 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/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i, i) == True{} : Bool}

template g_both source · line 680 · 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 -> @+n:Nat -> @+lv:A -> @+rv:A -> @+ehasl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == True{} : Bool} -> @+etwo:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), Nat.sub(n, 1n)) == True{} : Bool} -> @+eml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == Some{lv} : Maybe<&2, A>} -> @+emr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == Some{rv} : Maybe<&2, A>} -> @+hxl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, lv) == True{} : Bool} -> @+hxr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, rv) == 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/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i, i) == True{} : Bool}

template sib_mle source · line 690 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+lv:A -> @+rv:A -> @+eml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == Some{lv} : Maybe<&2, A>} -> @+emr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == Some{rv} : Maybe<&2, A>} -> @+hle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, lv, rv) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i))) == True{} : Bool}

template sib_mle_r source · line 695 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+i:Nat -> @+lv:A -> @+rv:A -> @+eml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == Some{lv} : Maybe<&2, A>} -> @+emr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == Some{rv} : Maybe<&2, A>} -> @+hnle:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, lv, rv) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i))) == True{} : Bool}

template down_loop_go source · line 701 · 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} -> @+hn:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hfuel:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.scale(fuel, 1n+i)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hpair:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> @hasl:Bool -> @+ehasl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), n) == hasl : Bool} -> @ml:Maybe<&2, A> -> @+eml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == ml : Maybe<&2, A>} -> @two:Bool -> @+etwo:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i), Nat.sub(n, 1n)) == two : Bool} -> @mr:Maybe<&2, A> -> @+emr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == mr : Maybe<&2, A>} -> @left:Bool -> @+eleft:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.mval(A, ml, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.mval(A, mr, x)) == left : Bool} -> @ok:Bool -> @+eok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, pick_cv(A, x, ml, two, mr, left)) == ok : Bool} -> DownOK(A, cmp, d, n, tgt, fuel, x, pick_state(A, t, i, hasl, ml, two, mr, left, ok))

template SiftDownOK source · line 770 · 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 dsift_from_go source · line 773 · 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_down(A, cmp, fuel, U32.from_nat(n), U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, fuel, U32.from_nat(n), x, dreal(A, dprobe(A, cmp, n, i, x, t))) : Array<Maybe<&2, A>>} -> @rest:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, fuel, U32.from_nat(n), x, dreal(A, dprobe(A, cmp, n, i, x, t))) == 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>})))) -> SiftDownOK(A, cmp, d, n, tgt, fuel, t, i, x)

template dsift_from_loop source · line 777 · 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_down(A, cmp, fuel, U32.from_nat(n), U32.from_nat(i), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.down_go(A, cmp, fuel, U32.from_nat(n), x, dreal(A, dprobe(A, cmp, n, i, x, t))) : Array<Maybe<&2, A>>} -> @r:DownOK(A, cmp, d, n, tgt, fuel, x, dprobe(A, cmp, n, i, x, t)) -> SiftDownOK(A, cmp, d, n, tgt, fuel, t, i, x)

template sift_down_ok source · line 784 · 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} -> @+hn:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hfuel:{Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.scale(fuel, 1n+i)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hexc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc2(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n, i) == True{} : Bool} -> @+hpair:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), i) == True{} : Bool} -> @+hkids:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kids_le(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(i), i) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.ulog(A, t, i, x), n)) == tgt : List<&2, A>} -> SiftDownOK(A, cmp, d, n, tgt, fuel, t, i, x)

The hole at i is below the parent pair it inherits, every other pair holds, the two pairs below the hole are the only ones the loop has to fix, and the loop has enough fuel for n <= 2^fuel * (1 + i).