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