proofs/containers/binary_heap/proof.bend checks

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

17 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../lib/order.bend as O
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/binary_heap.bend as S
import ../../../src/containers/binary_heap.bend as H
import ../../../src/containers/types/binary_heap.bend as E
import ./state.bend as ST
import ./steps.bend as SP
import ./trace.bend as TR
import ../../../spec/lib/order.bend as SO
import ./multiset.bend as M
import ./vals.bend as VL
import ./bag.bend as BG

Definitions

def u32_step_ok source · line 79 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<U32> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(U32, U32.cmp, sh) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(U32, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(U32, op)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(U32, U32.cmp, sh, op)

def u32_trace source · line 82 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<U32>> -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.pushes(U32, ops), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.TraceOK(U32, U32.cmp, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(U32))

def u32_new_inv source · line 85 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Inv(U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(U32))

def string_step_ok source · line 88 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<String> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<String> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(String, String.order, sh) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(String, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(String, op)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(String, String.order, sh, op)

def string_trace source · line 91 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<String>> -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.pushes(String, ops), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.TraceOK(String, String.order, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(String))

def string_new_inv source · line 94 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Inv(String, String.order, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(String))

def succ_add source · line 175 · raw

@+a:Nat -> @+b:Nat -> {Nat.add(a, 1n+b) == Nat.add(1n+a, b) : Nat}

Templates

template new_real source · line 47 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(A) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(A)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>}

template new_inv source · line 50 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(A)) == True{} : Bool}

template new_abs source · line 53 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(A)) == [] : List<&2, A>}

template step_ok source · line 58 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(A, op)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op)

template abs_real source · line 63 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.abs(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh) : List<&2, A>}

The abstraction of an actual heap is the model of its shadow: the laws above, stated on shadows, are laws about actual heaps.

template new_heap_inv source · line 66 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Inv(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(A))

template trace_from source · line 71 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh0) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.pushes(A, ops)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.TraceOK(A, cmp, ops, sh0)

template trace_new source · line 74 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A>> -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.pushes(A, ops), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.TraceOK(A, cmp, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(A))

template Impl source · line 101 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @Post:(@_:Pair(List<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>) -> Type) -> Type

ascending: each element is below all the later ones ---- the implementation ----

template impl_of source · line 104 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @-Post:(@_:Pair(List<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>) -> Type) -> @k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(A, cmp, sh, op) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.step(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh), op)) -> Impl(A, cmp, sh, op, Post)

template impl source · line 110 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<A> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, sh) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(A, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(A, op)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> @-Post:(@_:Pair(List<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Obs<A>) -> Type) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.step(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh), op)) -> Impl(A, cmp, sh, op, Post)

the heap must have room for a push (size + pushes < 2^q, q <= 31)

template ag_trans source · line 114 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+x:A -> @+h:A -> @+t:List<&2, A> -> @+hxh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, h) == True{} : Bool} -> @+hht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, h, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, x, t) == True{} : Bool}

---- ordering ----

template is_c source · line 121 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+x:A -> @+h:A -> @+t:List<&2, A> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, h <> t) == True{} : Bool} -> @+b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, h) == b : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, t)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, h <> t)) == True{} : Bool}

template ins_sorted source · line 131 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+x:A -> @+xs:List<&2, A> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, xs)) == True{} : Bool}

template msort_sorted source · line 138 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, xs)) == True{} : Bool}

template model_sorted source · line 146 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, sh)) == True{} : Bool}

every model (the multiset of a heap) is ascending

template from_list_sorted_go source · line 151 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+ys:List<&2, A> -> @+acc:List<&2, A> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, acc) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.from_list(A, cmp, ys, acc)) == True{} : Bool}

template ins_len_c source · line 159 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+x:A -> @+h:A -> @+t:List<&2, A> -> @+b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, h) == b : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, t)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, t) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, h <> t)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, h <> t) : Nat}

---- lengths ----

template ins_length source · line 168 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+x:A -> @+xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, xs)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs) : Nat}

template from_list_length_go source · line 180 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ys:List<&2, A> -> @+acc:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.from_list(A, cmp, ys, acc)) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, ys), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, acc)) : Nat}

template length_result source · line 190 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Length.length_result(A, cmp, xs)

---- Length ----

template length_frame source · line 193 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Length.length_frame(A, cmp, xs)

template new_empty source · line 197 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(A)) == [] : List<&2, A>}

---- Empty_Set ----

template push_length source · line 201 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> @+x:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Insert.push_length(A, cmp, xs, x)

---- Insert: one more element, exactly one more occurrence of it, still ordered ----

template push_bag source · line 204 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+xs:List<&2, A> -> @+x:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Insert.push_bag(A, cmp, o, xs, x)

template push_sorted source · line 207 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+xs:List<&2, A> -> @+x:A -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, xs) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Insert.push_sorted(A, cmp, o, xs, x, hs)

template peek_min source · line 211 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+h:A -> @+t:List<&2, A> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, h <> t) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.First_Element.peek_min(A, cmp, h, t, hs)

---- First_Element: the minimum; nothing changes ----

template peek_frame source · line 214 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.First_Element.peek_frame(A, cmp, xs)

template peek_empty source · line 217 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.First_Element.peek_empty(A, cmp)

template pop_length source · line 221 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+h:A -> @+t:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Delete_First.pop_length(A, cmp, h, t)

---- Delete_First: the minimum is removed once; the result is it ----

template pop_result source · line 224 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+h:A -> @+t:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Delete_First.pop_result(A, cmp, h, t)

template pop_min source · line 227 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+h:A -> @+t:List<&2, A> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, h <> t) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Delete_First.pop_min(A, cmp, h, t, hs)

template pop_bag source · line 231 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+h:A -> @+t:List<&2, A> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.sorted(A, cmp, h <> t) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Delete_First.pop_bag(A, cmp, o, h, t, hs)

the old multiset is the new one with the minimum put back

template pop_empty source · line 234 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Delete_First.pop_empty(A, cmp)

template from_list_model source · line 238 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.To_Set.from_list_model(A, cmp, xs, ys)

---- To_Set: the multiset of the list, ordered ----

template from_list_length source · line 241 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.To_Set.from_list_length(A, cmp, xs, ys)

template from_list_sorted source · line 244 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(A, cmp) -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.To_Set.from_list_sorted(A, cmp, o, xs, ys)

template to_sorted_result source · line 248 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Elements.to_sorted_result(A, cmp, xs)

---- Elements: to_sorted_list returns the ordered model ----

template to_sorted_frame source · line 251 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+xs:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.Elements.to_sorted_frame(A, cmp, xs)