[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

nat/le-def is used by 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/eqle-one is used by potex,
nat/fle is used by potex, ltwo-03, lsucc-01, lls-02,
nat/fle-01 is used by potex, lzer, ltwo-03, lsucc-01, lls-02, lls-01, lls,
nat/l-num-05 is used by lzer,
nat/le-add is used by potmonleq,
nat/le-ls-simp is used by potex,
nat/le-num-02 is used by potex,
nat/le-one is used by potex,
nat/lels is used by potmonleq, potex, lsucc-01, lpot, lls-02, lls-01, div-eq-zero,
nat/lels-01 is used by potex, pot-mon, lsucc-01,
nat/lels-02 is used by potmonleq,
nat/lels-03 is used by potmonleq, potex,
nat/lep is used by lzer,
nat/lep-02 is used by potex,
nat/ler is used by potmonleq, lpot, lls-02,
nat/les is used by potex,
nat/let is used by lls-02,
nat/lez-01 is used by lls-02,
nat/ls-01 is used by pot-mon,
nat/ls-le-simp is used by div-eq-zero,
nat/pred-03 is used by pot-01,
nat/succ-01 is used by potex,

Used from specification nat-basic2

nat-basic2/addex is used by potmonleq,
nat-basic2/c is used by add,
nat-basic2/succ is used by lemma-ax2,
nat-basic2/a is used by zero-01, zero, succ-03, succ-02, rec, potmonleq, potex, pot2-def, pot-two, pot-mon, pot-01, one, lzer, ltwo-03, lsucc-01, lpot, lls-02, lls-01, lls, ladd, inj-02, inj, div-eq-zero, add, 2-pot-mod,
nat-basic2/add-base is used by div-eq-zero, add,
nat-basic2/c is used by zero-01, zero, succ-03, succ-02, rec, potmonleq, potex, pot2-def, pot-two, pot-mon, pot-01, one, lzer, ltwo-03, lsucc-01, lpot, lls-02, lls-01, lls, ladd, inj-02, inj, div-eq-zero, add, 2-pot-mod,
nat-basic2/eq-01 is used by inj,
nat-basic2/l is used by lsucc-01,
nat-basic2/l-02 is used by potex, ladd,
nat-basic2/one-03 is used by succ-03,
nat-basic2/oz is used by potex, pot-mon, pot-01, 2-pot-mod,
nat-basic2/s is used by potex, pot-mon, lls-02,
nat-basic2/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, lls-02, lls-01, lls, inj, add, 2-pot-mod,
nat-basic2/z-01 is used by lzer,

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/le-05 is used by lls-01,
nat-mult/le2-04 is used by lsucc-01,
nat-mult/ls is used by ltwo-03,
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/modeq-01 is used by succ-03,
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, pot-01, one-01-01, one-01, one, mult, lzer, ltwo-03, lsucc-01, lpot, lls-01, lls, inj, div-eq-zero, add, 2-pot-mod,
nat-mult/mult-base is used by zero-01,
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, pot-01, one-01-01, one-01, one, mult, lzer, ltwo-03, lsucc-01, lpot, lls-01, lls, inj, div-eq-zero, add, 2-pot-mod,
nat-mult/one is used by one-01-01, 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,
nat-mult/two-ls-01 is used by lls-01,
nat-mult/two-zero-01 is used by succ-03, potex, lzer, ltwo-03, lsucc-01, lls-01, lls,
nat-mult/twole is used by lpot,
nat-mult/zero is used by div-eq-zero,
nat-mult/zero-01 is used by lsucc-01,
nat-mult/zero-02 is used by succ-02, rec, power-of-2-01, pot2-def, pot-01, mult, inj, add,
nat-mult/zero-06 is used by zero, pot-zero, pot-mon,

Used from specification nat-basic1

nat-basic1/f is used by potmonleq, potex, lzer, ltwo-03, lsucc-01, lls-02, lls-01, lls, ladd-01, ladd,
nat-basic1/lf-01 is used by potex, lls-01, lls,
nat-basic1/lf-02 is used by lls-01, lls,
nat-basic1/ls-02 is used by potmonleq, lls-01, lls,
nat-basic1/neq-01 is used by potmonleq,
nat-basic1/one is used by pot-mon,
nat-basic1/one-01 is used by pot-mon, lzer,
nat-basic1/ref-1 is used by potex, ltwo-03, lsucc-01, lls-02,
nat-basic1/zero-01 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,