[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification nat-basic

nat-basic/a is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, keyset-eq-empty, div2-mult4-add-k, div2-mult2-add-k,
nat-basic/add-base is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-bubble-up,
nat-basic/c is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, keyset-eq-empty, div2-mult4-add-k, div2-mult2-add-k,
nat-basic/eq-01 is used by prepost-update, prepost-bubble-up, div2-mult4-add-k, div2-mult2-add-k,
nat-basic/f is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat-basic/l is used by prepost-update, prepost-remove, prepost-insert, prepost-bubble-down,
nat-basic/l-01 is used by prepost-next2pot, prepost-bubble-down,
nat-basic/l-02 is used by prepost-remove,
nat-basic/lf is used by prepost-resize, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat-basic/lf-01 is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat-basic/lf-02 is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat-basic/ls-02 is used by prepost-remove, prepost-extract-min,
nat-basic/neq-04 is used by prepost-remove,
nat-basic/nls-fst is used by prepost-insert, prepost-bubble-down,
nat-basic/one is used by prepost-remove, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat-basic/one-01 is used by prepost-remove, prepost-extract-min, prepost-bubble-up,
nat-basic/one-02 is used by prepost-extract-min, prepost-bubble-up,
nat-basic/one-03 is used by prepost-remove, prepost-extract-min,
nat-basic/one-06 is used by prepost-remove, prepost-bubble-up,
nat-basic/oz is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, keyset-eq-empty,
nat-basic/ref is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-down,
nat-basic/s-04 is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat-basic/succ is used by prepost-resize, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, keyset-eq-empty, div2-mult4-add-k,
nat-basic/succ-03 is used by prepost-remove, prepost-insert,
nat-basic/trans is used by prepost-resize, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat-basic/twols-02 is used by prepost-bubble-up,
nat-basic/z-01 is used by prepost-next2pot,
nat-basic/zero is used by prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-bubble-up,
nat-basic/zero-01 is used by prepost-resize, prepost-extract-min,

Used from specification bin-min-heap

bin-min-heap/elim is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, keyset-eq-empty, key-set-in,
bin-min-heap/inj is used by prepost-insert,
bin-min-heap/sel-01 is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-empty, prepost-bubble-up, prepost-bubble-down,
bin-min-heap/sel-02 is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-empty, prepost-bubble-up, prepost-bubble-down,
bin-min-heap/upd-01 is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-extract-min,
bin-min-heap/upd-02 is used by prepost-remove, prepost-insert, prepost-extract-min,
bin-min-heap/updsel-02 is used by prepost-bubble-up, prepost-bubble-down,
bin-min-heap/updsel-03 is used by prepost-bubble-up, prepost-bubble-down,

Used from specification nat

nat/le-addex is used by prepost-resize, prepost-bubble-up,
nat/add-01 is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-bubble-up, prepost-bubble-down,
nat/add-num-01 is used by prepost-bubble-down,
nat/add-num-03 is used by prepost-update, prepost-remove, prepost-insert, prepost-bubble-down,
nat/elim-pred-c is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up,
nat/elim-sub is used by prepost-next2pot, prepost-bubble-down,
nat/eqle-one is used by prepost-remove, prepost-insert,
nat/fle is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-get-min, prepost-bubble-up, prepost-bubble-down,
nat/fle-01 is used by prepost-update, prepost-resize, prepost-remove, prepost-bubble-up, prepost-bubble-down,
nat/ge is used by prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-extract-min, prepost-bubble-up,
nat/gr-def is used by prepost-resize,
nat/l-num-01 is used by prepost-bubble-down,
nat/l-num-02 is used by prepost-bubble-down,
nat/l-num-03 is used by prepost-bubble-down,
nat/l-num-06 is used by prepost-resize,
nat/le-add is used by prepost-next2pot,
nat/le-def is used by prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat/le-ls-simp is used by prepost-update, prepost-resize, prepost-remove, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat/le-num-04 is used by prepost-bubble-up,
nat/lels is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat/lels-02 is used by prepost-resize, prepost-remove, prepost-extract-min, prepost-bubble-up,
nat/lels-03 is used by prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-extract-min, prepost-bubble-down,
nat/lep is used by prepost-remove, prepost-next2pot, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat/lep-02 is used by prepost-remove, prepost-next2pot,
nat/ler is used by prepost-remove,
nat/les is used by prepost-remove,
nat/let is used by prepost-update, prepost-resize, prepost-remove, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat/lez is used by prepost-insert,
nat/lez-01 is used by prepost-remove,
nat/ls is used by prepost-next2pot,
nat/ls-01 is used by prepost-remove, prepost-extract-min, prepost-bubble-down,
nat/ls-02 is used by prepost-remove, prepost-bubble-up,
nat/ls-03 is used by prepost-remove, prepost-extract-min,
nat/ls-le-simp is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
nat/not-zero is used by prepost-remove, prepost-extract-min, prepost-bubble-up,
nat/sub-base is used by prepost-resize,
nat/succ-01 is used by prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, keyset-eq-empty,
nat/zero-02 is used by prepost-remove, prepost-extract-min, prepost-bubble-up,

Used from specification set-union

set-union/keyindex-set/delsw is used by prepost-remove, prepost-extract-min,
set-union/keyindex-set/del-addeq-05 is used by prepost-remove, prepost-extract-min,
set-union/keyindex-set/del-e-01 is used by prepost-extract-min,
set-union/keyindex-set/del-e-02 is used by prepost-remove,
set-union/keyindex-set/del-in-03 is used by prepost-remove,
set-union/keyindex-set/del-neq-02 is used by prepost-remove, prepost-extract-min,
set-union/keyindex-set/delete-insert is used by prepost-remove, prepost-extract-min,

Used from specification set-basic

set-basic/keyindex-set/In-empty is used by prepost-remove,
set-basic/keyindex-set/In-insert is used by prepost-remove, prepost-insert, prepost-extract-min,
set-basic/keyindex-set/Size-empty is used by prepost-get-min, prepost-extract-min,
set-basic/keyindex-set/in-04 is used by prepost-extract-min,
set-basic/keyindex-set/ne is used by prepost-remove, prepost-insert, prepost-extract-min, keyset-eq-empty,
set-basic/keyindex-set/ne-01 is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min,
set-basic/keyindex-set/size-one-01 is used by prepost-remove, prepost-extract-min,
set-basic/keyindex-set/size-zero is used by prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min,
set-basic/keyindex-set/size-zero-01 is used by prepost-update, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min,

Used from specification key-index

key-index/elim is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
key-index/inj is used by prepost-update, prepost-remove, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
key-index/sel-01 is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-bubble-up,
key-index/sel-02 is used by prepost-update, prepost-resize, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
key-index/upd-02 is used by prepost-update,

Used from specification index-array

index-array/id-idx-refl is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
index-array/id-idx-write is used by prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
index-array/id-idx-write-left is used by prepost-remove, prepost-insert, prepost-extract-min,

Used from specification bin-min-heap-inv

bin-min-heap-inv/heap-order is used by prepost-update, prepost-resize, prepost-bubble-up, prepost-bubble-down,
bin-min-heap-inv/heap-order-add-smaller is used by prepost-insert,
bin-min-heap-inv/heap-order-min is used by prepost-get-min, prepost-extract-min,
bin-min-heap-inv/heap-order-overwrite-children-at is used by prepost-remove, prepost-extract-min,
bin-min-heap-inv/heap-order-overwrite-children-ok is used by prepost-update, prepost-bubble-down,
bin-min-heap-inv/heap-order-overwrite-parent-ok is used by prepost-bubble-up,
bin-min-heap-inv/heap-order-overwrite0 is used by prepost-bubble-up,
bin-min-heap-inv/heap-order-pull-down-parent is used by prepost-remove,
bin-min-heap-inv/heap-order-pull-up-child is used by prepost-update, prepost-remove, prepost-extract-min,
bin-min-heap-inv/key-index-in-keyset-array-extract is used by prepost-remove,
bin-min-heap-inv/key-set-extract-index is used by prepost-update, prepost-remove, prepost-get-min, prepost-extract-min, key-set-in,
bin-min-heap-inv/key-set-write-nodups is used by prepost-remove, prepost-extract-min,
bin-min-heap-inv/keyset-subarray-eq is used by prepost-insert,
bin-min-heap-inv/keyset-xchg is used by prepost-bubble-down,
bin-min-heap-inv/no-dups-idx is used by prepost-resize, prepost-remove, prepost-extract-min,
bin-min-heap-inv/no-dups-idx-xchg is used by prepost-bubble-up, prepost-bubble-down,
bin-min-heap-inv/valid-idx is used by prepost-update, prepost-resize, prepost-remove, prepost-bubble-up,
bin-min-heap-inv/valid-idx-rec is used by prepost-insert,
bin-min-heap-inv/valid-idx-xhg is used by prepost-bubble-down,
bin-min-heap-inv/2exp-size-0 is used by prepost-next2pot, prepost-get-min,
bin-min-heap-inv/2exp-size-1 is used by prepost-empty,
bin-min-heap-inv/2exp-size-mult2 is used by prepost-next2pot,
bin-min-heap-inv/heap-order-0 is used by prepost-insert, prepost-extract-min, prepost-empty,
bin-min-heap-inv/heap-order-1 is used by prepost-remove, prepost-insert, prepost-extract-min,
bin-min-heap-inv/heap-order-remove-last is used by prepost-remove, prepost-extract-min,
bin-min-heap-inv/key-index-in-keyset-array-extract is used by prepost-update, prepost-remove,
bin-min-heap-inv/key-set-1 is used by prepost-extract-min,
bin-min-heap-inv/key-set-write-last is used by prepost-insert,
bin-min-heap-inv/key-set-write-nodups is used by prepost-update,
bin-min-heap-inv/keyset-base is used by prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-empty, keyset-eq-empty,
bin-min-heap-inv/keyset-rec is used by prepost-remove, prepost-insert, prepost-extract-min, keyset-eq-empty,
bin-min-heap-inv/keyset-xchg is used by prepost-bubble-up,
bin-min-heap-inv/no-dups-idx-0 is used by prepost-insert, prepost-extract-min, prepost-empty,
bin-min-heap-inv/no-dups-idx-mvlast is used by prepost-remove, prepost-extract-min,
bin-min-heap-inv/no-dups-idx-rec is used by prepost-insert,
bin-min-heap-inv/no-dups-idx-rem1 is used by prepost-remove, prepost-extract-min,
bin-min-heap-inv/no-dups-idx-remlast is used by prepost-extract-min,
bin-min-heap-inv/no-dups-update-key is used by prepost-update,
bin-min-heap-inv/valid-idx-0 is used by prepost-insert, prepost-extract-min, prepost-empty,
bin-min-heap-inv/valid-idx-imp-1 is used by prepost-remove,
bin-min-heap-inv/valid-idx-last-valid is used by prepost-resize, prepost-remove, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
bin-min-heap-inv/valid-idx-move-last is used by prepost-remove, prepost-extract-min,
bin-min-heap-inv/valid-idx-outofbounds is used by prepost-remove,
bin-min-heap-inv/valid-idx-remlast is used by prepost-extract-min,
bin-min-heap-inv/valid-idx-update-key is used by prepost-update,
bin-min-heap-inv/valid-idx-xhg is used by prepost-bubble-up,

Used from specification array-copy

array-copy/key-index-array/at-copy is used by prepost-resize,
array-copy/key-index-array/copy-exact is used by prepost-resize,
array-copy/key-index-array/size-copy is used by prepost-resize,
array-copy/key-index-array/subarray-copy-elim-exact is used by prepost-resize,
array-copy/key-index-array/subarray-elim is used by prepost-insert,
array-copy/key-index-array/subarray-zero is used by prepost-insert,

Used from specification nat-mult

nat-mult/dist is used by prepost-bubble-down,
nat-mult/ls-08 is used by prepost-resize, prepost-remove, prepost-bubble-up, prepost-bubble-down,
nat-mult/modls is used by prepost-bubble-down,
nat-mult/mult-a is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, div2-mult4-add-k, div2-mult2-add-k,
nat-mult/mult-c is used by prepost-update, prepost-resize, prepost-remove, prepost-next2pot, prepost-extract-min, prepost-bubble-up, prepost-bubble-down, div2-mult4-add-k, div2-mult2-add-k,
nat-mult/numeral-01 is used by prepost-bubble-down,
nat-mult/numeral-06 is used by prepost-bubble-down,
nat-mult/numeral-21 is used by prepost-bubble-down,
nat-mult/numeral-23 is used by prepost-bubble-down,
nat-mult/numeral-28 is used by prepost-update, prepost-remove, prepost-bubble-down,
nat-mult/numeral-30 is used by prepost-next2pot, prepost-bubble-down,
nat-mult/one is used by prepost-update, prepost-remove, prepost-next2pot, prepost-bubble-down,
nat-mult/rsucc-02 is used by prepost-remove, prepost-bubble-down, div2-mult4-add-k,
nat-mult/two-ls-01 is used by prepost-bubble-down,
nat-mult/two-succ-05 is used by prepost-bubble-down,
nat-mult/two-zero-01 is used by prepost-resize,
nat-mult/twole is used by prepost-next2pot,
nat-mult/twols is used by prepost-update, prepost-remove, prepost-bubble-down,
nat-mult/zero-02 is used by div2-mult4-add-k,

Used from specification oelem

oelem/binheap-key/irreflexivity is used by prepost-update, prepost-remove, prepost-insert, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
oelem/binheap-key/lel is used by prepost-update, prepost-remove, prepost-get-min, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
oelem/binheap-key/ls-le is used by prepost-bubble-down,
oelem/binheap-key/nen is used by prepost-update, prepost-extract-min, prepost-bubble-down,
oelem/binheap-key/nll is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
oelem/binheap-key/nnn is used by prepost-bubble-down,
oelem/binheap-key/seq is used by prepost-extract-min,
oelem/binheap-key/transitivity is used by prepost-update, prepost-insert, prepost-bubble-up, prepost-bubble-down,

Used from specification elem-index

elem-index/elim is used by prepost-update, prepost-resize, prepost-remove,
elem-index/sel-02 is used by prepost-update, prepost-resize, prepost-remove,

Used from specification array

array/key-index-array/Put-other is used by prepost-update, prepost-bubble-up,
array/key-index-array/Put-same is used by prepost-update, prepost-remove, prepost-insert,
array/key-index-array/Size-mkarray is used by prepost-resize, prepost-empty,
array/key-index-array/Size-put is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
array/index-array-base/Size-put is used by prepost-bubble-up, prepost-bubble-down,
array/key-index-array/cgetput is used by prepost-remove, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
array/key-index-array/cngetput is used by prepost-update, prepost-remove, prepost-insert, prepost-bubble-up, prepost-bubble-down,
array/key-index-array/cngetput-num is used by prepost-extract-min, prepost-bubble-up,
array/key-index-array/cputput is used by prepost-update, prepost-remove, prepost-insert, prepost-extract-min, prepost-bubble-up, prepost-bubble-down,
array/key-index-array/ngp-06 is used by prepost-bubble-down,
array/key-index-array/put-same-content is used by prepost-remove, prepost-extract-min,

Used from specification nat-div

nat-div/div-add is used by div2-mult4-add-k,
nat-div/modex is used by div2-mult4-add-k,
nat-div/le-div-to-mult is used by prepost-resize, prepost-remove, prepost-bubble-up,
nat-div/two-ls is used by prepost-resize, prepost-bubble-up,
nat-div/two-ls-02 is used by prepost-bubble-up,
nat-div/two-neq-01 is used by prepost-update, prepost-remove, prepost-insert, prepost-bubble-up,
nat-div/two-two-01 is used by prepost-resize, prepost-bubble-up, div2-mult2-add-k,
nat-div/two-zero-01-01 is used by prepost-update, prepost-bubble-up,