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