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