~/bend-docscommunity

proofs/containers/priority_queue/proof.bend checks

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

8 imports
import Base
import ../../../src/containers/priority_queue.bend as P2
import ../../../src/containers/binary_heap.bend as K2
import ../../../src/containers/types/binary_heap.bend as E2
import ../../../spec/containers/priority_queue.bend as S
import ../../../spec/containers/binary_heap.bend as HS
import ../../../spec/lib/order.bend as SO
import ../binary_heap/proof.bend as UP

Definitions

def priority_queue_put source · line 12 · raw

@q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<U32> -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.put(U32, U32.cmp, q, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.push(U32, U32.cmp, q, v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<U32>}

def priority_queue_get source · line 15 · raw

@q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.get(U32, U32.cmp, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.pop(U32, U32.cmp, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Error, U32>)}

def priority_queue_qsize source · line 18 · raw

@q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.qsize(U32, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.length(U32, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<U32>, Nat)}

Templates

template new_is source · line 23 · raw

@-A:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.new(A) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(A) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>}

template qsize_is source · line 26 · raw

@-A:Data -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.qsize(A, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.length(A, h) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, Nat)}

template put_is source · line 29 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A> -> @x:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.put(A, cmp, h, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.push(A, cmp, h, x) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>}

template peek_is source · line 32 · raw

@-A:Data -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.peek(A, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.peek(A, h) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Error, A>)}

template get_is source · line 35 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.get(A, cmp, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.pop(A, cmp, h) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Error, A>)}

template from_list_is source · line 38 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.from_list(A, cmp, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.from_list(A, cmp, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>}

template to_sorted_list_is source · line 41 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.to_sorted_list(A, cmp, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.to_sorted_list(A, cmp, h) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, List<&2, A>)}

template length_result source · line 46 · raw

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

template length_frame source · line 49 · raw

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

template push_length source · line 52 · raw

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

template push_bag source · line 55 · raw

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

template push_sorted source · line 58 · 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/priority_queue.Insert.push_sorted(A, cmp, o, xs, x, hs)

template peek_min source · line 61 · 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/priority_queue.First_Element.peek_min(A, cmp, h, t, hs)

template peek_frame source · line 64 · raw

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

template peek_empty source · line 67 · raw

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

template pop_length source · line 70 · raw

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

template pop_result source · line 73 · raw

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

template pop_min source · line 76 · 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/priority_queue.Delete_First.pop_min(A, cmp, h, t, hs)

template pop_bag source · line 79 · 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/priority_queue.Delete_First.pop_bag(A, cmp, o, h, t, hs)

template pop_empty source · line 82 · raw

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

template from_list_model source · line 85 · raw

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

template from_list_length source · line 88 · raw

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

template from_list_sorted source · line 91 · 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/priority_queue.To_Set.from_list_sorted(A, cmp, o, xs, ys)

template to_sorted_result source · line 94 · raw

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

template to_sorted_frame source · line 97 · raw

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