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

Lemma dependency for Specification nat-mult

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
square-even-01provedall subs proved mult-c, mult-a, rsucc-01, square-even,
sqleprovedall subs proved ls-08, mult-c, mult-a, zero-06, sqp,
sqpprovedall subs proved mult-c, mult-a, mult-le-01,
square-evenprovedall subs proved rdist, dist, modeq, ex-two, mult-c, mult-a, rsucc-01,
le2-03provedall subs proved mult-c, mult-a, ls2-02,
sqr-09provedall subs proved mult-c, mult-a, mult-le-01,
ex-twoprovedall subs proved mult-c, mult-a, two-succ-05, two-02,
mult-le-01provedall subs proved sqls, sqr-08, mult-c, mult-a, one-01, sqzero, sqle-02, le-succ,
ls2-02provedall subs proved mult-c, mult-a, ls-03-num,
two-succ-04provedall subs proved mult-c, mult-a, modls,
mult-eq-succ-01provedall subs proved mult-c, mult-a, mult-eq-succ-02, mult-eq-succ,
le2-04provedall subs proved mult-c, mult-a, modls,
le-succprovedall subs proved zero-01, mult-c, mult-a, one, modp,
mult-eq-succprovedall subs proved zero, mult-le, mult-c, mult-a, one, rsucc-01,
modlsprovedall subs proved modp, modeq-01, ls, mult-c, mult-a, zero-01,
two-succ-05provedall subs proved mult-c, mult-a, modeq-01,
ls-03-numprovedall subs proved mult-c, mult-a, zero, ls-03,
sqr-06provedall subs proved mult-c, mult-a, mult-le,
ls-09provedall subs proved mult-c, mult-a, ls-03, zero,
sqr-02provedall subs proved mult-c, mult-a, ls-04, sqr-01,
sqle-02provedall subs proved mult-c, mult-a, le-05,
sqr-08provedall subs proved mult-c, mult-a, ls-04, sqr-03, sqzero, le-04,
mult-eq-succ-02provedall subs proved one, zero, mod-neq-02, mult-c, mult-a,
sqr-01provedall subs proved leone, mult-c, mult-a, ls-04, sqzero,
modpprovedall subs proved zero-01, rsucc-01, mult-c, mult-a, le-05, zero,
modeq-01provedall subs proved mult-c, mult-a, zero-02, mod-neq-02,
ls-03provedall subs proved mult-c, mult-a, zero, ls-10,
mult-leprovedall subs proved mult-c, mult-a, ls-04, zero-01, leone,
square-eq-02provedall subs proved square-eq-03,
twole-01provedall subs proved mult-c, mult-a, le-02,
coef-22provedall subs proved coef-16, mult-c, mult-a, zero,
sqle-01provedall subs proved mult-c, mult-a, le-05,
sqrprovedall subs proved mult-c, mult-a, sqr-05,
square-le-01provedall subs proved mult-c, mult-a, succ, dist, rsucc-01, square-le,
square-eq-01provedall subs proved mult-c, mult-a, succ, dist, rsucc-01, square-eq,
ls-05provedall subs proved mult-c, mult-a, le-05,
le2-02provedall subs proved mult-c, mult-a, le-05,
mod-neq-03provedall subs proved mod-neq-02, mult-c, mult-a, rsucc-01, modeq,
nonumsimp-mod-neqprovedall subs proved mult-c, mult-a, mod-neq, rsucc-01,
twole-02provedall subs proved mult-c, mult-a, twols,
square-injectprovedall subs proved zero-02, mult-c, mult-a, coef-21, numeral-24, succ, dist, rsucc-01, square-interval,
square-intervalprovedall subs proved coef-18, numeral-20, mult-c, mult-a, succ, dist, rsucc-01, coef-21, numeral-24, square-ls,
twolsprovedall subs proved mult-c, mult-a, ls-01,
sqlsprovedall subs proved sqr-07, ls-07, mult-c, mult-a, sqzero,
mod-neqprovedall subs proved mult-c, mult-a, rsucc-01, modls-01,
le-04provedall subs proved leone, one, mult-c, mult-a, zero,
sqr-03provedall subs proved sqr-07, mult-c, mult-a, sqzero,
square-eqprovedall subs proved mult-c, mult-a, rsucc-01, square-ls,
mod-neq-02provedall subs proved mult-c, mult-a, ls-01, zero-01, coef-04, numeral-08, numeral-07,
ls-04provedall subs proved leone, mult-c, mult-a, one, zero-06,
square-leprovedall subs proved mult-c, mult-a, rsucc-01, square-ls,
sqr-05provedall subs proved mult-c, mult-a, ls-01,
coef-16provedall subs proved mult-c, mult-a, ls-01, ls-08,
le-02provedall subs proved mult-c, mult-a, ls-01,
ls-10provedall subs proved mult-c, mult-a, ls-01,
square-eq-03provedall subs proved mult-c, mult-a, dist, square-ls-05,
le-05provedall subs proved mult-c, mult-a, ls-01, zero,
twoleprovedall subs proved mult-c, mult-a, leone,
square-ls-01provedall subs proved mult-c, mult-a, rsucc-01, square-ls,
mod-neq-01provedall subs proved modls-01,
two-03provedall subs proved modls-01, zero, twoeq, mult-c, mult-a,
square-le-03provedall subs proved square-ls-05,
square-ls-03provedall subs proved square-ls-05,
modls-02provedall subs proved modls-01,
square-ls-02provedall subs proved mult-c, mult-a, succ, dist, rsucc-01, square-ls,
twoeqf-02provedall subs proved mult-c, mult-a, twoeqf,
twoeqfprovedall subs proved mult-c, mult-a, two-zero-01, two-02,
square-ls-05provedall subs proved zero, le, ls-06, ls, square-le-02, mult-c, mult-a, dist,
ls-01provedall subs proved coef-18, rsucc-01, mult-c, mult-a, zero,
sqr-07provedall subs proved one, numeral-20, two-02, rsucc-01, mult-c, mult-a,
modls-01provedall subs proved mult-c, mult-a, mod-nle,
square-lsprovedall subs proved ls, square-less, le-num, two-02, succ, dist, mult-c, mult-a, rsucc-01,
leoneprovedall subs proved coef-18, zero-06, one, mult-c, mult-a, zero, rsucc-01,
mod-nle-01provedall subs proved mult-c, mod-nle,
twoeqf-01provedall subs proved mult-c, mult-a, two-zero-01, two-02,
mod-nlsprovedall subs proved mod-nle,
square-ls-04provedall subs proved two-02, rsucc-01, square-less, square-le-02, mult-c, mult-a, sqzero,
threeprovedall subs proved zero-06, succ, two-02, rsucc-01, threeeq, one, zero, mult-c, mult-a,
nonumsimp-mod-neq-05provedall subs proved one, numeral-19, two-02, zero-06, zero, mult-c, mult-a, rsucc-01,
square-twoprovedall subs proved le-num, two-zero-01, twoeq, coef-18, mult-c, mult-a, coef-17,
twoeqf-03provedall subs proved two-02,
mod-neq-05provedall subs proved mult-c, mult-a, rsucc-01, mod-neq-04,
nonumsimp-twoeqprovedall subs proved two-02, mult-c, mult-a, one, numeral-19,
mod-neq-04provedall subs proved mult-c, mult-a, modeq,
coef-18provedall subs proved mult-c, mult-a, one, coef-05,
square-le-02provedall subs proved square-less, mult-c, mult-a, ls-06,
two-02provedall subs proved mult-c, mult-a, one, numeral-25,
mod-nleprovedall subs proved ls, modls-03, mult-c, mult-a, modeq,
threelsprovedall subs proved ls2-03, rsucc-01, mult-c, mult-a,
coef-15provedall subs proved mult-c, mult-a, one, coef-05,
succ-01provedall subs proved mult-c, mult-a, zero, modeq,
numeral-25provedall subs proved rsucc-01, mult-c, mult-a, coef-17,
coef-05provedall subs proved mult-c, mult-a, coef-08, zero, dist, le,
numeral-19provedall subs proved rsucc-01, mult-c, mult-a, coef-17,
coef-21provedall subs proved mult-c, mult-a, one, coef-08,
modeqprovedall subs proved coef-17, rsucc-01, mult-c, mult-a, zero-01, ls-08, zero,
square-lessprovedall subs proved ls-06, ls, le, mult-c, mult-a, sqzero,
ls2-03provedall subs proved mult-c, mult-a, two-one-01, zero-06,
coef-23provedall subs proved mult-c, mult-a, one, coef-08,
le-sameprovedall subs proved one, mult-base, coef-17, mult-c, mult-a, zero-01,
coef-19provedall subs proved mult-c, mult-a, one, coef-06,
two-one-01provedall subs proved mult-c, mult-a, one-01,
numeral-07provedall subs proved coef-01, dist, mult-c, mult-a, coef-04,
coef-06provedall subs proved mult-c, mult-a, zero, coef-03,
threeeqprovedall subs proved one-01, rsucc-01, mult-c, mult-a,
coef-17provedall subs proved mult-c, mult-a, one, coef-04,
ls-06provedall subs proved mult-c, mult-a, zero-06, zero, ls,
coef-08provedall subs proved mult-c, mult-a, zero, coef-03,
coef-11provedall subs proved mult-c, mult-a, one, coef-03,
le-rewprovedall subs proved mult-c, mult-a, ls, le,
coef-20provedall subs proved mult-c, mult-a, one, coef-07,
coef-14provedall subs proved mult-c, mult-a, one, coef-04,
numeral-01provedall subs proved dist, mult-c, mult-a, coef-04,
dist-subprovedall subs proved mult-c, mult-a, zero-02, dist-sub-04,
le-03provedall subs proved mult-c, mult-a, rsucc-01, le, rsucc,
coef-13provedall subs proved mult-c, mult-a, one, coef-03,
mult-sub-lessprovedall subs proved mult-c, mult-a, zero-02, dist-sub-04,
two-ls-01provedall subs proved mult-c, mult-a, ls,
twoeqprovedall subs proved mult-c, mult-a, one-02,
rsuccprovedall subs proved mult-c, mult-a, eq-01, rsucc-01,
succprovedall subs proved mult-c, mult-a, eq-01, rsucc-01,
one-01provedall subs proved one, rsucc-01, zero, mult-c, mult-a,
dist-sub-04provedall subs proved mult-c, mult-a, zero-02, dist,
coef-07provedall subs proved mult-c, mult-a, zero, coef-02,
lsprovedall subs proved mult-c, mult-a, ls-02, zero-01,
coef-03provedall subs proved mult-c, mult-a, coef-02, zero, dist, ls-02,
coef-04provedall subs proved mult-c, mult-a, zero, coef-01,
two-succ-03provedall subs proved mult-c, mult-a, eq-01, rsucc-01,
nonumsimp-lstwoprovedall subs proved mult-c, mult-a, one, numeral-24, dist, rsucc-01,
dist-mergeprovedall subs proved mult-c, mult-a, coef-01, dist,
nonumsimp-twonleprovedall subs proved mult-c, mult-a, one, numeral-27,
nonumsimp-twoleprovedall subs proved mult-c, mult-a, one, numeral-32,
dist-sub-01provedall subs proved mult-c, mult-a, zero-02, rsucc-01,
coef-10provedall subs proved mult-c, mult-a, one, coef-02,
succ-mergeprovedall subs proved mult-c, mult-a, eq-01, rsucc-01,
nonumsimp-twoeq-01provedall subs proved mult-c, mult-a, one, numeral-28,
dist-sub-03provedall subs proved mult-c, mult-a, zero-02, dist,
coef-12provedall subs proved mult-c, mult-a, one, coef-02,
coef-09provedall subs proved mult-c, mult-a, one, coef-01,
nonumsimp-succprovedall subs proved mult-c, mult-a, eq-01, rsucc-01,
mult-ineq-ltprovedall subs proved mult-c, mult-a, ls-02,
ls-02provedall subs proved mult-c, mult-a, le,
one-02provedall subs proved mult-c, mult-a, zero, zero-03,
coef-02provedall subs proved mult-c, mult-a, zero, dist, le,
le-numprovedall subs proved mult-c, mult-a, le,
coef-01provedall subs proved mult-c, mult-a, zero, dist, eq,
zero-02provedall subs proved mult-c, mult-a, zero, eq,
eq-01provedall subs proved mult-c, mult-a, rsucc-01, eq,
oneprovedall subs proved zero-03, rsucc-01, mult-c, mult-a,
twols-01provedall subs proved zero-06, rsucc-01, two-zero-01, mult-c, mult-a,
zero-04provedall subs proved mult-c, mult-a, zero, eq,
neqoneprovedall subs proved mult-c, mult-a, zero, zero-03,
mult-ineq-leprovedall subs proved mult-c, mult-a, le,
eqprovedall subs proved rsucc-01, mult-c, mult-a, zero-06, zero,
ls-07provedall subs proved zero-06, rsucc-01, mult-c, mult-a, zero,
sqzeroprovedall subs proved mult-c, mult-a, zero-06,
zero-03provedall subs proved zero-01, rsucc-01, zero-06, mult-c, mult-a, zero,
two-zero-01provedall subs proved mult-c, mult-a, zero-06,
leprovedall subs proved numeral-05, mult-c, mult-a, zero-06, numeral-03,
two-les-01provedall subs proved mult-c, mult-a, numeral-33,
numeral-10provedall subs proved zero-06, rsucc-01, zero, mult-c, mult-a, zero-01,
zero-numprovedall subs proved mult-c, mult-a, zero, zero-06,
numeral-17provedall subs proved zero-06, rsucc-01, zero, mult-c, mult-a, zero-01,
modls-03provedall subs proved rsucc-01, mult-c, mult-a, ls-08, zero,
numeral-08provedall subs proved mult-c, mult-a, dist,
numeral-03provedall subs proved mult-c, mult-a, dist,
numeral-05provedall subs proved mult-c, mult-a, dist,
numeral-33provedall subs proved mult-c, mult-a, ls-08,
zero-06provedall subs proved mult-c, mult-a, zero, zero-01,
numeral-16provedall subs proved mult-c, mult-a, dist,
numeral-04provedall subs proved mult-c, mult-a, dist,
nonumsimp-addls-01provedall subs proved mult-c, mult-a, dist,
numeral-18provedall subs proved mult-c, mult-a, dist,
numeral-12provedall subs proved mult-c, mult-a, dist,
numeral-06provedall subs proved mult-c, mult-a, dist,
numeral-15provedall subs proved mult-c, mult-a, dist,
addleprovedall subs proved addle-01, mult-c, mult-a,
numeral-09provedall subs proved mult-c, mult-a, dist,
numeral-29provedall subs proved mult-c, mult-a, ls-08,
numeral-11provedall subs proved mult-c, mult-a, dist,
le-01provedall subs proved mult-c, mult-a, ls-08,
addle-01provedall subs proved rsucc-01, mult-c, mult-a, zero,
numeral-28provedall subs proved mult-c, mult-a, rsucc-01,
ls-08provedall subs proved rsucc-01, mult-c, mult-a, zero,
numeral-20provedall subs proved mult-c, mult-a, rsucc-01,
numeral-32provedall subs proved mult-c, mult-a, rsucc-01,
numeral-27provedall subs proved mult-c, mult-a, rsucc-01,
numeral-24provedall subs proved mult-c, mult-a, rsucc-01,
distprovedall subs proved rsucc-01, mult-c, mult-a, zero,
zero-01provedall subs proved rsucc-01, mult-c, mult-a, zero,
dist-sub-02provedall subs proved mult-c, mult-a, rsucc-01,
two-succ-06provedall subs proved rsucc-01, mult-c, mult-a,
zero-05provedall subs proved mult-c, mult-a, zero, rsucc-01,
numeral-36provedall subs proved mult-c, mult-a, rsucc-01,
nonumsimp-eqsuccprovedall subs proved mult-c, mult-a, rsucc-01,
numeral-30provedall subs proved mult-c, mult-a, rsucc-01,
numeral-21provedall subs proved mult-c, mult-a, rsucc-01,
nonumsimp-twolsprovedall subs proved mult-c, mult-a, rsucc-01,
lssucc-01provedall subs proved mult-c, mult-a, rsucc-01,
lssuccprovedall subs proved mult-c, mult-a, rsucc-01,
square-oneprovedall subs proved mult-c, mult-a,
numeral-35provedall subs proved mult-c, mult-a, rsucc-01,
numeral-23provedall subs proved mult-c, mult-a, rsucc-01,
numeral-26provedall subs proved mult-c, mult-a, rsucc-01,
mult-cprovedall subs proved rsucc-01, rsucc-02, mult-a, zero, mult-base,
zeroprovedall subs proved rsucc-02, mult-a,
rsucc-01provedall subs proved rsucc-02, mult-a, mult-base,
mult-aprovedall subs proved rdist, rsucc-02, mult-base,
rdistprovedall subs proved rsucc-02, mult-base,
rsucc-02provedall subs proved mult-rec,
fourprovedall subs proved four-01,
four-01provedall subs proved
mult-recaxiom
mult-baseaxiom