~/bend-docscommunity

proofs/containers/binary_heap/multiset.bend checks

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

6 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/order.bend as O
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/binary_heap.bend as S

Definitions

def and_swap source · line 12 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}

Templates

template ins_cons source · line 23 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+x:A -> @+h:A -> @+t:List<&2, A> -> @+b:Bool -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, h) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, h <> t) == Bool.pick(List<&2, A>, b, x <> h <> t, h <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, t)) : List<&2, A>}

template all_ge_ins_c source · line 27 · raw

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

template all_ge_ins source · line 37 · raw

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

template ins_min source · line 45 · raw

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

A value not larger than every element goes first.

template comm_nil source · line 54 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+x:A -> @+y:A -> @+bxy:Bool -> @+exy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, y) == bxy : Bool} -> @+byx:Bool -> @+eyx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, y, x) == byx : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, y, [])) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, [])) : List<&2, A>}

Insertion order is irrelevant (uses totality, transitivity, antisymmetry).

template comm_cons source · line 70 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+x:A -> @+y:A -> @+h:A -> @+t:List<&2, A> -> @+bxy:Bool -> @+exy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, y) == bxy : Bool} -> @+byx:Bool -> @+eyx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, y, x) == byx : Bool} -> @+bxh:Bool -> @+exh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, h) == bxh : Bool} -> @+byh:Bool -> @+eyh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, y, h) == byh : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, y, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, t)) : List<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, y, h <> t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, h <> t)) : List<&2, A>}

template ins_comm source · line 120 · raw

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