[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 sorted-rec1, sorted-lt-pre, sorted-lt-post, sorted-lt-h, sorted-lt, sorted-eq-entry, sorted-all, keep-sorted,
nat-basic/add-base is used by sorted-lt-pre, sorted-lt-post, sorted-lt-h, sorted-lt, sorted-eq-entry, sorted-all,
nat-basic/c is used by sorted-rec1, sorted-lt-pre, sorted-lt-post, sorted-lt-h, sorted-lt, sorted-eq-entry, sorted-all, keep-sorted,
nat-basic/eq-02 is used by keep-sorted,
nat-basic/f is used by sorted-lt-pre, sorted-lt-post, sorted-lt-h, sorted-lt, sorted-eq-entry, sorted-entry-lt-post, sorted-branch-lt-post, sorted-all, keep-sorted,
nat-basic/l is used by sorted-all,
nat-basic/lf is used by sorted-all,
nat-basic/lf-02 is used by sorted-eq-entry,
nat-basic/nls-fst is used by sorted-all,
nat-basic/s-04 is used by sorted-lt-h, sorted-all,
nat-basic/succ is used by sorted-rec1, sorted-lt-h, sorted-all, keep-sorted,
nat-basic/trans is used by sorted-all,
nat-basic/zero is used by sorted-lt-pre, sorted-lt-post, sorted-lt-h,
nat-basic/zero-01 is used by sorted-lt-pre, sorted-lt-h,

Used from specification zbranch

zbranch/inj-01 is used by sorted-eq-entry,
zbranch/sel-02 is used by sorted-branch-lt-post,
zbranch/sel-04 is used by sorted-eq-entry, sorted-entry-lt-post,

Used from specification nat

nat/anti is used by sorted-eq-entry,
nat/fle is used by sorted-eq-entry, sorted-all,
nat/fle-01 is used by sorted-eq-entry,
nat/le-def is used by sorted-eq-entry,
nat/le-ls-simp is used by sorted-lt-h, sorted-eq-entry,
nat/lels is used by sorted-lt-h, sorted-eq-entry, sorted-all,
nat/lep-02 is used by sorted-lt-h,
nat/ler is used by sorted-eq-entry,
nat/lez is used by sorted-lt-h,
nat/lez-01 is used by sorted-lt-h,
nat/ls-add-not-01 is used by sorted-all,
nat/ls-le-simp is used by sorted-all,
nat/succ-01 is used by sorted-all,

Used from specification oelem

oelem/key-order/irreflexivity is used by sorted-lt-post, sorted-lt-h, sorted-eq-entry,
oelem/key-order/ls-le is used by sorted-lt-h,
oelem/key-order/nll is used by sorted-lt-h,
oelem/key-order/transitivity is used by sorted-lt-h,

Used from specification array

array/zbranch-array/Put-other is used by keep-sorted,
array/zbranch-array/Put-same is used by keep-sorted,
array/zbranch-array/Size-put is used by keep-sorted,
array/zbranch-array/cngetput is used by keep-sorted,