[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-basic1

nat-basic1/f is used by sorted-sub-merge, sorted-sub-less1, sorted-sub-entire, sorted-sub-change-above, sorted-exchange, sorted-1, sorted-0,
nat-basic1/lf is used by sorted-sub-merge, sorted-sub-less1, sorted-sub-entire, sorted-sub-change-above, sorted-exchange, sorted-0,
nat-basic1/lf-01 is used by sorted-exchange,
nat-basic1/lf-02 is used by sorted-exchange,
nat-basic1/ls-02 is used by sorted-sub-less1, sorted-sub-change-above, sorted-exchange, sorted-0,
nat-basic1/one is used by sorted-exchange,
nat-basic1/ref-1 is used by sorted-sub-merge, sorted-last2, sorted-exchange,
nat-basic1/trans-1 is used by sorted-sub-merge, sorted-sub-less1, sorted-sub-entire, sorted-sub-change-above, sorted-exchange, sorted-0,

Used from specification order

order/reflexive is used by sorted-exchange,
order/transitive is used by sorted-sub-merge, sorted-exchange,
order/total-2nle is used by sorted-exchange,

Used from specification array

array/Put-other is used by sorted-exchange,
array/Put-same is used by sorted-exchange,
array/Size-put is used by sorted-exchange,
array/cgetput is used by sorted-exchange,
array/cngetput is used by sorted-sub-change-above, sorted-exchange,

Used from specification nat

nat/anti is used by sorted-sub-merge,
nat/anti is used by sorted-sub-merge, sorted-exchange,
nat/eqle-one is used by sorted-exchange,
nat/fle is used by sorted-sub-merge, sorted-sub-change-above, sorted-exchange, sorted-1, sorted-0,
nat/fle-01 is used by sorted-sub-merge, sorted-sub-less1, sorted-sub-change-above, sorted-exchange, sorted-1, sorted-0,
nat/ge is used by sorted-sub-change-above,
nat/l-num-04 is used by sorted-exchange,
nat/le-add is used by sorted-sub-merge, sorted-exchange,
nat/le-ls-simp is used by sorted-sub-merge, sorted-exchange,
nat/lels is used by sorted-sub-merge, sorted-exchange, sorted-1,
nat/lels-01 is used by sorted-sub-merge,
nat/lels-02 is used by sorted-sub-merge, sorted-exchange,
nat/lels-03 is used by sorted-sub-merge, sorted-exchange,
nat/ler is used by sorted-sub-merge, sorted-exchange,
nat/les is used by sorted-sub-merge, sorted-exchange,
nat/let is used by sorted-1,
nat/lez is used by sorted-sub-merge, sorted-sub-entire, sorted-last2,
nat/ls-le-simp is used by sorted-sub-merge, sorted-sub-change-above, sorted-exchange, sorted-1,
nat/succ-01 is used by sorted-sub-merge, sorted-exchange,

Used from specification nat-basic2

nat-basic2/addex is used by sorted-exchange,
nat-basic2/a is used by sorted-sub-merge, sorted-sub-less1, sorted-last2, sorted-exchange, sorted-1,
nat-basic2/c is used by sorted-sub-merge, sorted-sub-less1, sorted-last2, sorted-exchange, sorted-1,
nat-basic2/eq is used by sorted-exchange,
nat-basic2/l is used by sorted-last2, sorted-exchange,
nat-basic2/l-02 is used by sorted-exchange,
nat-basic2/neq-01 is used by sorted-exchange,
nat-basic2/s is used by sorted-sub-merge, sorted-sub-less1, sorted-last2, sorted-exchange, sorted-1,
nat-basic2/succ is used by sorted-sub-merge, sorted-sub-less1, sorted-sub-entire, sorted-exchange,
nat-basic2/succ-03 is used by sorted-exchange,