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