[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 transitivity,
nat-basic/c is used by transitivity,
nat-basic/f is used by transitivity,
nat-basic/l-02 is used by transitivity,
nat-basic/lf is used by transitivity,
nat-basic/lf-01 is used by transitivity,
nat-basic/lf-02 is used by transitivity,
nat-basic/ls-02 is used by transitivity,
nat-basic/neq-01 is used by totality,
nat-basic/ref is used by transitivity, irreflexivity,
nat-basic/succ is used by transitivity,
nat-basic/trans is used by transitivity,

Used from specification string-less

string-less/val-total is used by totality,
string-less/Irreflexivity is used by irreflexivity,
string-less/Transitivity is used by transitivity,

Used from specification nat

nat/anti is used by totality,
nat/fle is used by transitivity,
nat/fle-01 is used by transitivity,
nat/le-ls-simp is used by transitivity,
nat/lels is used by totality, transitivity,
nat/lels-02 is used by totality, transitivity,
nat/ler is used by totality,
nat/ls-le-simp is used by transitivity,

Used from specification key

key/disj-01 is used by totality,
key/disj-02 is used by totality,
key/disj-03 is used by totality,
key/disjpred-03 is used by transitivity,
key/disjpred-04 is used by transitivity,
key/disjpred-05 is used by transitivity,
key/disjpred-06 is used by transitivity,
key/inj-01 is used by totality,
key/inj-02 is used by totality,
key/inj-03 is used by totality,
key/sel-01 is used by totality, transitivity, irreflexivity,
key/sel-02 is used by totality, transitivity, irreflexivity,
key/sel-03 is used by totality, transitivity, irreflexivity,
key/sel-04 is used by totality, transitivity, irreflexivity,
key/sel-05 is used by totality, transitivity, irreflexivity,
key/test-01 is used by totality, transitivity, irreflexivity,
key/test-02 is used by transitivity, irreflexivity,
key/test-03 is used by totality, transitivity,
key/test-04 is used by totality, transitivity,
key/test-05 is used by totality, transitivity,
key/test-06 is used by totality, transitivity,
key/test-07 is used by totality, transitivity, irreflexivity,
key/test-08 is used by totality, transitivity,
key/test-09 is used by totality, transitivity, irreflexivity,

Used from specification key-order-def

key-order-def/datakey-less is used by transitivity, irreflexivity,
key-order-def/dentrykey-less is used by transitivity, irreflexivity,
key-order-def/inode-less is used by transitivity, irreflexivity,
key-order-def/datakey-less is used by totality, transitivity,
key-order-def/dentrykey-less is used by totality, transitivity,
key-order-def/inode-less is used by totality, transitivity,