[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

Used from specification set-union

set-union/keyindex-set/del-in is used by key-set-write-nodups,
set-union/keyindex-set/Delete is used by key-set-write-nodups,
set-union/keyindex-set/del-addeq-05 is used by key-set-write-nodups,
set-union/keyindex-set/del-e-01 is used by key-set-write-nodups,

Used from specification nat

nat/anti is used by keyset-size-bound0,
nat/add-01 is used by heap-order-remove-last, heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite0, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-min, heap-order-add-smaller, heap-order-add-parent-key,
nat/add-num-03 is used by heap-order-pull-up-child, heap-order-add-parent-key,
nat/anti is used by no-dups-keyset-size, keyset-xchg, keyset-overwrite-add, key-set-write-nodups, key-set-extract-index,
nat/elim-pred-c is used by heap-order-remove-last, heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite0, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-min, heap-order-add-smaller, heap-order-add-parent-key, 2exp-size-mult2,
nat/eqle-one is used by no-dups-keyset-size, keyset-size-bound0,
nat/fle is used by valid-idx-xhg, valid-idx-update-key, valid-idx-remlast, valid-idx-outofbounds, valid-idx-move-last, valid-idx-last-valid, keyset-xchg, keyset-size-bound, keyset-overwrite-add, key-set-write-nodups, key-index-in-keyset-array-extract, heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite0, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-min,
nat/fle-01 is used by valid-idx-rec, no-dups-keyset-size, no-dups-idx-rec, keyset-size-bound0, keyset-size-bound, key-set-write-other, key-set-extract-index, heap-order-min, heap-order-add-smaller, heap-order-add-parent-key,
nat/l-num-05 is used by heap-order-overwrite-children-ok,
nat/le-def is used by keyset-size-bound0, keyset-size-bound,
nat/le-ls-simp is used by valid-idx-xhg, valid-idx-remlast, valid-idx-move-last,
nat/lels is used by valid-idx-xhg, valid-idx-remlast, valid-idx-rec, valid-idx-move-last, no-dups-keyset-size, no-dups-idx-xchg, no-dups-idx-rec, keyset-xchg, keyset-size-bound0, keyset-size-bound, keyset-overwrite-add, key-set-write-other, key-set-write-nodups, key-set-write-last, key-set-extract-index, heap-order-pull-up-child, heap-order-min, heap-order-add-smaller, heap-order-add-parent-key,
nat/lels-02 is used by valid-idx-rec, no-dups-keyset-size, no-dups-idx-rec, keyset-xchg, keyset-subarray-eq-add, keyset-overwrite-add, key-set-write-nodups, heap-order-add-smaller, heap-order-add-parent-key,
nat/lels-03 is used by valid-idx-remlast, valid-idx-rec, valid-idx-outofbounds, valid-idx-move-last, valid-idx-imp-1, no-dups-keyset-size, no-dups-idx-rec, keyset-xchg, keyset-subarray-eq, keyset-overwrite-add, key-set-write-other, key-set-write-nodups, key-set-extract-index, heap-order-min,
nat/lep-02 is used by heap-order-add-parent-key,
nat/ler is used by valid-idx-rec, no-dups-keyset-size, no-dups-idx-rec, keyset-xchg, key-set-write-nodups, key-set-write-last, heap-order-add-smaller, heap-order-add-parent-key,
nat/lez is used by valid-idx-0, keyset-xchg, keyset-overwrite-add, key-set-write-nodups,
nat/ls-add-not-01 is used by keyset-size-bound,
nat/ls-le-simp is used by valid-idx-xhg, no-dups-keyset-size, no-dups-idx-xchg, keyset-xchg, keyset-size-bound0, keyset-overwrite-add, key-set-write-other, key-set-write-nodups, key-set-write-last,
nat/succ-01 is used by valid-idx-remlast, valid-idx-rec, valid-idx-outofbounds, valid-idx-move-last, valid-idx-imp-1, no-dups-keyset-size, keyset-xchg, keyset-subarray-eq, keyset-size-bound0, keyset-overwrite-add, key-set-write-other, key-set-write-nodups, key-set-extract-index, heap-order-min, heap-order-add-smaller, heap-order-add-parent-key,

Used from specification nat-pot

nat-pot/Pot2-zero is used by 2exp-size-mult2,
nat-pot/inj-02 is used by 2exp-size-mult2,
nat-pot/lemma-ax2 is used by 2exp-size-mult2,
nat-pot/one is used by 2exp-size-1,
nat-pot/zero is used by 2exp-size-0,

Used from specification set-basic

set-basic/keyindex-set/Size-insert is used by no-dups-keyset-size, keyset-size-bound,
set-basic/keyindex-set/ext-rec is used by key-set-write-nodups,
set-basic/keyindex-set/sw is used by keyset-overwrite-add, key-set-write-nodups,
set-basic/keyindex-set/In-empty is used by key-set-extract-index,
set-basic/keyindex-set/In-insert is used by key-set-write-nodups, key-set-extract-index,
set-basic/keyindex-set/Size-empty is used by no-dups-keyset-size, keyset-size-bound,
set-basic/keyindex-set/eq is used by no-dups-keyset-size, keyset-subarray-eq-add, keyset-size-bound,
set-basic/keyindex-set/eq-04 is used by keyset-overwrite-add,
set-basic/keyindex-set/in-05 is used by keyset-subarray-eq-add,
set-basic/keyindex-set/ne is used by key-set-write-nodups,
set-basic/keyindex-set/ne-01 is used by valid-idx-outofbounds, no-dups-keyset-size, no-dups-idx-rec, keyset-size-bound, key-set-write-nodups, key-set-extract-index, key-index-in-keyset-array-extract,
set-basic/keyindex-set/size-zero-01 is used by valid-idx-outofbounds, no-dups-keyset-size, no-dups-idx-rec, key-set-write-nodups, key-set-extract-index, key-index-in-keyset-array-extract,

Used from specification key-index

Used from specification array-copy

array-copy/key-index-array/subarray-at is used by keyset-subarray-eq,
array-copy/key-index-array/size-subarray is used by keyset-subarray-eq,
array-copy/key-index-array/subarray-elim is used by keyset-subarray-eq-add, keyset-subarray-eq,

Used from specification oelem

oelem/binheap-key/irreflexivity is used by heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-add-parent-key,
oelem/binheap-key/lel is used by heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-add-smaller, heap-order-add-parent-key,
oelem/binheap-key/nen is used by heap-order-pull-up-child, heap-order-overwrite0, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at,
oelem/binheap-key/nll is used by heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite0, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-min,
oelem/binheap-key/nnn is used by heap-order-pull-up-child, heap-order-overwrite0, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-min,
oelem/binheap-key/transitivity is used by heap-order-pull-up-child,

Used from specification nat-mult

nat-mult/ls-08 is used by heap-order-add-parent-key,
nat-mult/mult-a is used by heap-order-pull-up-child, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-add-parent-key, 2exp-size-mult2,
nat-mult/mult-c is used by heap-order-pull-up-child, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-add-parent-key, 2exp-size-mult2,
nat-mult/numeral-28 is used by heap-order-add-parent-key,
nat-mult/one is used by heap-order-add-parent-key,
nat-mult/one-01 is used by 2exp-size-mult2,
nat-mult/rsucc-02 is used by heap-order-pull-up-child, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-add-parent-key,
nat-mult/two-zero-01 is used by heap-order-pull-up-child,
nat-mult/zero-02 is used by 2exp-size-mult2,

Used from specification elem-index

elem-index/elim is used by valid-idx-xhg, valid-idx-update-key, valid-idx-remlast, valid-idx-rec, valid-idx-move-last, valid-idx-imp-1,
elem-index/inj is used by valid-idx-xhg, valid-idx-remlast, valid-idx-move-last,
elem-index/sel-02 is used by valid-idx-update-key, valid-idx-rec, valid-idx-outofbounds, valid-idx-move-last, valid-idx-imp-1, key-index-in-keyset-array-extract,
elem-index/upd-02 is used by valid-idx-xhg, valid-idx-remlast, valid-idx-move-last,
elem-index/updsel-04 is used by valid-idx-rec,

Used from specification array

array/key-index-array/Extension is used by keyset-subarray-eq,
array/key-index-array/Put-other is used by heap-order-overwrite-children-ok, heap-order-add-parent-key,
array/key-index-array/cputput-reverse is used by keyset-xchg,
array/index-array-base/Put-other is used by valid-idx-xhg, valid-idx-remlast, valid-idx-rec, valid-idx-move-last,
array/key-index-array/Put-other is used by valid-idx-xhg, valid-idx-update-key, valid-idx-remlast, valid-idx-rec, valid-idx-move-last, no-dups-update-key, no-dups-idx-xchg, no-dups-idx-remlast, no-dups-idx-rec, no-dups-idx-mvlast, keyset-xchg, keyset-overwrite-add, key-set-write-nodups, heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite0, heap-order-overwrite-parent-ok, heap-order-overwrite-children-at, heap-order-add-smaller,
array/key-index-array/Put-same is used by valid-idx-xhg, valid-idx-update-key, valid-idx-remlast, valid-idx-rec, valid-idx-move-last, no-dups-update-key, no-dups-idx-xchg, no-dups-idx-remlast, no-dups-idx-rec, no-dups-idx-mvlast, keyset-xchg, keyset-overwrite-add, key-set-write-nodups, key-set-write-last, heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-add-smaller, heap-order-add-parent-key,
array/index-array-base/Put-same is used by valid-idx-xhg, valid-idx-remlast, valid-idx-rec, valid-idx-move-last,
array/key-index-array/Size-put is used by valid-idx-xhg, valid-idx-update-key, valid-idx-remlast, valid-idx-rec, valid-idx-move-last, no-dups-update-key, no-dups-idx-xchg, no-dups-idx-remlast, no-dups-idx-rec, no-dups-idx-mvlast, keyset-xchg, keyset-overwrite-add, key-set-write-other, key-set-write-nodups, key-set-write-last,
array/index-array-base/Size-put is used by valid-idx-xhg, valid-idx-remlast, valid-idx-rec, valid-idx-move-last,
array/index-array-base/cgetput is used by valid-idx-xhg,
array/key-index-array/cgetput is used by valid-idx-xhg, no-dups-idx-xchg, keyset-xchg, heap-order-overwrite0,
array/key-index-array/cngetput is used by heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-add-smaller, heap-order-add-parent-key,
array/index-array-base/ngp-06 is used by valid-idx-xhg, valid-idx-remlast,
array/key-index-array/ngp-07 is used by valid-idx-rec, no-dups-idx-rec, key-set-write-other,

Used from specification nat-div

nat-div/div-two-mult is used by heap-order-pull-up-child, heap-order-overwrite-children-at,
nat-div/div-elim is used by heap-order-overwrite-children-ok, heap-order-add-parent-key,
nat-div/mod-eq-02 is used by heap-order-pull-up-child, heap-order-overwrite-children-at,
nat-div/mult-02 is used by heap-order-pull-up-child, heap-order-overwrite-children-at,
nat-div/two-ls-02 is used by heap-order-min, heap-order-add-smaller,
nat-div/two-ls-04 is used by heap-order-pull-up-child, heap-order-overwrite-children-at,
nat-div/two-neq-01 is used by heap-order-pull-up-child, heap-order-pull-down-parent, heap-order-overwrite-parent-ok, heap-order-overwrite-children-ok, heap-order-overwrite-children-at, heap-order-add-parent-key,
nat-div/two-odd-01 is used by heap-order-pull-up-child, heap-order-overwrite-children-at,
nat-div/two-two-01 is used by heap-order-pull-up-child,
nat-div/two-zero-01-01 is used by heap-order-overwrite0, heap-order-overwrite-children-at, heap-order-min,