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