[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/addex is used by potmonleq,
nat-basic/c is used by add,
nat-basic/succ is used by lemma-ax2,
nat-basic/a is used by zero-01, zero, succ-03, succ-02, rec, potmonleq, potex, pot2-def, pot-mon, one, lzer, ltwo-03, lsucc-01, lpot, log2-elim, lls-02, lls-01, lls, ladd, inj, div-eq-zero, add, 2-pot-mod,
nat-basic/add-base is used by add,
nat-basic/c is used by zero-01, zero, succ-03, succ-02, rec, potmonleq, potex, pot2-def, pot-mon, one, lzer, ltwo-03, lsucc-01, lpot, log2-elim, lls-02, lls-01, lls, ladd, inj, div-eq-zero, add, 2-pot-mod,
nat-basic/eq-01 is used by inj,
nat-basic/f is used by potmonleq, potex, lzer, ltwo-03, lsucc-01, log2-elim, lls-02, lls-01, lls, ladd-01, ladd, div-eq-zero,
nat-basic/l-02 is used by potex, ladd,
nat-basic/less-zero is used by pot-mon,
nat-basic/ls-02 is used by potmonleq,
nat-basic/neq-01 is used by potmonleq,
nat-basic/one is used by pot-mon,
nat-basic/one-01 is used by pot-mon, lzer,
nat-basic/one-06 is used by succ-03,
nat-basic/oz is used by potex, pot-mon, lzer, 2-pot-mod,
nat-basic/refl-nat is used by potex, lsucc-01, lpot, lls-02, lls-01, lls,
nat-basic/s-04 is used by potex, pot-mon, lls-02, lls,
nat-basic/succ is used by zero-01, zero, succ-03, rec-01, potex, pot2-def, pot-zero, pot-mon, one, mult, lzer, ltwo-03, lsucc-01, lpot, log2-elim, lls-02, lls-01, lls, inj, add, 2-pot-mod,
nat-basic/z-02 is used by div-eq-zero,

Used from specification nat

nat/le-def is used by lzer, ltwo-03,
nat/lels is used by ltwo-03, lsucc-01,
nat/anti is used by potmonleq,
nat/elim-pred-c is used by pot-mon, pot-01,
nat/eq-02 is used by log2-elim,
nat/eqle-one is used by potex,
nat/fle is used by potex, lsucc-01, lls-02,
nat/fle-01 is used by potex, lzer, lsucc-01, log2-elim, lls-02, lls-01, lls,
nat/l-num-05 is used by lzer,
nat/le-add is used by potmonleq,
nat/le-def is used by potex, pot-mon, lsucc-01, lpot, log2-elim,
nat/le-ls-simp is used by potex, log2-elim,
nat/le-num-02 is used by potex,
nat/le-one is used by potex,
nat/lels is used by potmonleq, potex, lpot, lls-02, lls-01, lls, div-eq-zero,
nat/lels-02 is used by potmonleq,
nat/lels-03 is used by potmonleq, potex,
nat/lep is used by log2-elim,
nat/lep-02 is used by potex,
nat/ler is used by potmonleq, lls-02, lls,
nat/les is used by potex,
nat/let is used by lls-02,
nat/lez-01 is used by lls-02, lls-01,
nat/ls-01 is used by pot-mon, log2-elim,
nat/ls-le-simp is used by ltwo-03, div-eq-zero,
nat/pred-03 is used by pot-01,
nat/succ-01 is used by potex,

Used from specification nat-mult

nat-mult/le is used by ltwo-03,
nat-mult/mult-a is used by power-of-2-01, potex,
nat-mult/two-02 is used by two,
nat-mult/two-succ-04 is used by lsucc-01,
nat-mult/le2-04 is used by lsucc-01,
nat-mult/ls is used by ltwo-03, lls-01,
nat-mult/ls-01 is used by potex,
nat-mult/ls-02 is used by pot-mon,
nat-mult/ls-07 is used by potex,
nat-mult/ls2-03 is used by potex,
nat-mult/mult-a is used by zero-01, zero, succ-03, succ-02, rec, power-of-2-01, potex, pot2-def, pot-zero, pot-mon, one-01-01, one, mult, ltwo-03, lsucc-01, lpot, log2-elim, lls-01, inj, div-eq-zero, add, 2-pot-mod,
nat-mult/mult-base is used by zero-01, div-eq-zero,
nat-mult/mult-c is used by zero-01, zero, succ-03, succ-02, rec, power-of-2-01, power-of-2, potex, pot2-def, pot-zero, pot-mon, one-01-01, one, mult, ltwo-03, lsucc-01, lpot, log2-elim, lls-01, inj, div-eq-zero, add, 2-pot-mod,
nat-mult/numeral-36 is used by log2-elim,
nat-mult/one is used by one-01-01, log2-elim, add,
nat-mult/one-01 is used by pot-mon, one, inj,
nat-mult/rsucc-02 is used by potex,
nat-mult/two-02 is used by rec, log2-elim,
nat-mult/two-succ-05 is used by succ-03,
nat-mult/two-zero-01 is used by zero, succ-03, potex, ltwo-03, lsucc-01, log2-elim, lls-01,
nat-mult/twole is used by lpot,
nat-mult/zero-01 is used by pot-zero,
nat-mult/zero-02 is used by succ-02, rec, power-of-2-01, pot2-def, mult, inj, add,
nat-mult/zero-06 is used by pot-mon,

Used from specification nat-div

nat-div/mult-02 is used by power-of-2-01, power-of-2,
nat-div/div-elim is used by div-eq-zero,
nat-div/mod-mult-01 is used by 2-pot-mod,
nat-div/zero-01 is used by div-eq-zero,