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

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-ls-03provedall subs proved square-even-02, mod-mult-01, square-even-03, mod-once, mod-add, ls-even, ls-02, mult, two-rec, square-ls,
square-lsprovedall subs proved two-rec, square-ls-01,
square-nle-01-01provedall subs proved two-rec, square-nle-01,
div-two-multprovedall subs proved mod-add, mult-div, div-succ-01, mod2-succ, mult-02, mod-eq-02,
square-nle-01provedall subs proved div-elim, square-ls-02,
square-ls-01provedall subs proved two-rec, square-ls-02,
mod2-succprovedall subs proved mod-mult-01, mod-once, div-elim, mod-succ-02,
mod-succ-05provedall subs proved mod-succ-06,
mod-neqprovedall subs proved mod-succ-06, mod-ls, mod-succ-02,
square-ls-02provedall subs proved square-even-02, ls-even,
mod-succ-02provedall subs proved mod-succ-01,
mod-succ-06provedall subs proved mod-succ, mod-succ-01,
two-oddprovedall subs proved mod-mult-01, mod-eq-02,
ls-evenprovedall subs proved mult-02, two-ls-04,
mod-succ-01provedall subs proved mod-mult-01, mod-eq-01, div-elim,
mod-eq-02provedall subs proved mod-eq, mod-add, mod-eq-01,
two-le-02provedall subs proved mult-02, two-le-03,
square-injprovedall subs proved square-inject,
square-injectprovedall subs proved square-even-02, mult-div,
mod-eq-01provedall subs proved mod-mult, div-elim, mod-ls, mod-eq, mod-add,
mult-02provedall subs proved mult-div,
square-intervalprovedall subs proved square-even-03, mod-once, square-even-02, le-div-to-mult, two-rec, mult-div,
nummult-eqprovedall subs proved mult-div, div-mult, mod-mult-01,
mod-by6provedall subs proved mod-mult-01, mod-add, modex, mod-once,
two-le-03provedall subs proved two-mdiv2-02, modex,
square-even-03provedall subs proved mod-once, square-even-01,
two-ls-04provedall subs proved two-mdiv2-02, modex,
mult-divprovedall subs proved div-mult, modex,
mod-addprovedall subs proved mod-mult, modex,
two-ls-05provedall subs proved two-mdiv2-02, modex,
mod-mod-01provedall subs proved mod-mult-01, modex,
mod-modprovedall subs proved mod-mult-01, modex,
exmultprovedall subs proved modex,
div-addprovedall subs proved div-mult, mult, modex,
square-even-02provedall subs proved square-even,
square-even-01provedall subs proved mod-once, square-even,
mod-succprovedall subs proved mod-mult-01, div-elim,
modexprovedall subs proved div-elim, mod-mult-01,
two-succprovedall subs proved two-ls-02,
two-paddprovedall subs proved le-div-to-mult,
two-ls-03provedall subs proved le-div-to-mult,
two-ls-01provedall subs proved two-ls,
two-loup-08provedall subs proved div-elim, two-ls-02, two-zero-01-01,
two-loup-04provedall subs proved div-elim, zero-01, le-div-to-mult,
two-loup-01provedall subs proved le-div-to-mult,
two-le-04provedall subs proved le-div-to-mult,
two-le-01provedall subs proved le-div-to-mult,
two-leprovedall subs proved two-ls-02,
nummult-le-01provedall subs proved le-div-to-mult,
mult-01provedall subs proved div-mult,
mod-sameprovedall subs proved mod-ls-03, mod-ls,
mod-le-02provedall subs proved mod-ls-03,
mod-le-01provedall subs proved mod-ls-02,
mod-leprovedall subs proved mod-ls-01,
ls-succprovedall subs proved le-succ,
leprovedall subs proved cond-01, le-div-to-mult,
div-succprovedall subs proved div-mult, add, div-elim,
div-le-01provedall subs proved zero, le-div-to-mult,
div-leprovedall subs proved zero, le-div-to-mult,
two-lsprovedall subs proved div-elim,
two-zero-01-01provedall subs proved div-elim,
two-mdiv2-02provedall subs proved div-elim,
two-ls-02provedall subs proved div-elim,
square-evenprovedall subs proved div-elim,
mod-ls-03provedall subs proved div-elim,
mod-ls-02provedall subs proved div-elim,
mod-ls-01provedall subs proved div-elim,
mod-mult-01provedall subs proved mod-zero-01, mod-mult,
le-succprovedall subs proved div-elim,
div-succ-01provedall subs proved zero-01, mult, div-elim,
le-div-to-multprovedall subs proved div-elim,
div-multprovedall subs proved div-elim,
two-ppredprovedall subs proved div-elim,
two-peqprovedall subs proved div-elim, two-one-01,
two-odd-01provedall subs proved div-elim,
two-neq-02provedall subs proved div-elim,
two-neq-01provedall subs proved div-elim,
two-neqprovedall subs proved div-elim,
two-loup-13provedall subs proved div-elim,
two-loup-12provedall subs proved div-elim,
two-loup-11provedall subs proved div-elim, two-mdiv2-03,
two-loup-10provedall subs proved div-elim, two-mdiv2-03,
two-loup-09provedall subs proved div-elim,
two-loup-07provedall subs proved div-elim,
two-loup-06provedall subs proved div-elim,
two-loup-05provedall subs proved div-elim,
two-loup-02provedall subs proved div-elim,
two-loupprovedall subs proved div-elim,
two-eqprovedall subs proved div-elim,
square-nlsprovedall subs proved div-elim,
mod-succ-04provedall subs proved div-elim,
mod-rewprovedall subs proved div-elim, cond-01,
ls-01provedall subs proved div-elim,
lsprovedall subs proved div-elim,
two-mdiv2-03provedall subs proved mult,
mod-multprovedall subs proved mod-once,
div-elimprovedall subs proved zero-01, mult, mod-ls, Moddef,
two-twosucc-02provedall subs proved mult,
two-two-01provedall subs proved mult,
two-threeprovedall subs proved two-rec,
mod-succ-03provedall subs proved mod-one-01, mod-once,
mod-recprovedall subs proved mod-once,
div-two-addprovedall subs proved mult,
two-recprovedall subs proved add,
mod-onceprovedall subs proved cond-01, add, rax,
multprovedall subs proved add,
recprovedall subs proved add,
mod-one-01provedall subs proved mod-eq,
mod-zero-01provedall subs proved mod-eq,
addprovedall subs proved ls-03, ls-02, le-01,
mod-le-04provedall subs proved mod-le-03, mod-eq,
mod-eqprovedall subs proved zero-01, Moddef,
cond-01provedall subs proved cond,
mod-lsprovedall subs proved mod-le-03,
ls-03provedall subs proved ls-02, Divdef,
mod-zeroprovedall subs proved one, Moddef,
mod-oneprovedall subs proved one-01, Moddef,
mod-nlsprovedall subs proved mod-le-03,
div-oneprovedall subs proved zero-01,
oneprovedall subs proved Divdef,
one-01provedall subs proved Divdef,
raxprovedall subs proved Moddef,
mod-le-03provedall subs proved Divdef, Moddef,
zeroprovedall subs proved Divdef,
zero-01provedall subs proved Divdef,
condprovedall subs proved Moddef,
le-01provedall subs proved Divdef,
ls-02provedall subs proved Divdef,
mult-ls-01provedall subs proved Divdef,
mult-lsprovedall subs proved Divdef,
two-one-01provedall subs proved
Divdefaxiom
Moddefaxiom