[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, 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,
two-le-02provedall subs proved mult-02, two-le-03,
square-injprovedall subs proved square-inject,
div-two-multprovedall subs proved mod-add, div-succ-01, mod2-succ, mult-02, mod-eq-02,
square-injectprovedall subs proved square-even-02, mult-div,
mult-02provedall subs proved mult-div,
mod-neqprovedall subs proved mod-succ-06, mod-ls, mod-succ-02,
mod-by6provedall subs proved mod-mult-01, mod-add, modex, mod-once,
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,
mod2-succprovedall subs proved mod-mult-01, mod-once, div-elim, mod-succ-02,
two-ls-04provedall subs proved two-mdiv2-02, modex,
two-le-03provedall subs proved two-mdiv2-02, modex,
mult-divprovedall subs proved div-mult, modex,
mod-succ-06provedall subs proved mod-succ, mod-succ-01,
mod-addprovedall subs proved mod-mult, modex,
square-even-03provedall subs proved mod-once, square-even-01,
two-ls-05provedall subs proved two-mdiv2-02, modex,
exmultprovedall subs proved modex,
mod-mod-01provedall subs proved mod-mult-01, modex,
two-oddprovedall subs proved mod-mult-01, mod-eq-02,
mod-modprovedall subs proved mod-mult-01, modex,
ls-succprovedall subs proved le-succ,
div-addprovedall subs proved div-mult, mult, modex,
le-succprovedall subs proved div-elim, le-div-to-mult,
mod-eq-02provedall subs proved mod-eq-01,
mod-succprovedall subs proved mod-mult-01, div-elim,
square-even-01provedall subs proved mod-once, square-even,
mod-succ-02provedall subs proved mod-succ-01,
modexprovedall subs proved div-elim, mod-mult-01,
square-even-02provedall subs proved square-even,
two-succprovedall subs proved two-ls-02,
ls-01provedall subs proved div-elim, le-div-to-mult,
two-leprovedall subs proved two-ls-02,
two-ls-01provedall subs proved two-ls,
two-paddprovedall subs proved le-div-to-mult,
two-ls-03provedall subs proved le-div-to-mult,
mod-sameprovedall subs proved mod-ls-03, mod-ls,
nummult-le-01provedall subs proved le-div-to-mult,
two-loup-08provedall subs proved div-elim, two-ls-02, two-zero-01-01,
mult-01provedall subs proved div-mult,
mod-leprovedall subs proved mod-ls-01,
two-le-01provedall subs proved le-div-to-mult,
modulo-between-equal3provedall subs proved modulo-between-equal, mod-once,
leprovedall subs proved cond-01, le-div-to-mult,
modulo-between-equal2provedall subs proved modulo-between-equal,
two-loup-01provedall subs proved le-div-to-mult,
two-le-04provedall subs proved le-div-to-mult,
div-succprovedall subs proved div-mult, add, div-elim,
div-leprovedall subs proved zero, le-div-to-mult,
mod-succ-05provedall subs proved mod-ls-01, mod-mult, div-elim,
div-le-01provedall subs proved zero, le-div-to-mult,
mod-le-02provedall subs proved mod-ls-03,
mod-le-01provedall subs proved mod-ls-02,
div-succ-01provedall subs proved zero-01, mult, div-elim,
mod-ls-02provedall subs proved div-elim,
mod-succ-01provedall subs proved mod-eq, div-elim,
mod-eq-01provedall subs proved mod-eq, mod-mult, div-elim,
modulo-between-equalprovedall subs proved mod-ls, div-elim,
square-evenprovedall subs proved div-elim,
mod-ls-01provedall subs proved div-elim,
div-multprovedall subs proved div-elim,
two-zero-01-01provedall subs proved div-elim,
mod-ls-03provedall subs proved div-elim,
two-mdiv2-02provedall subs proved div-elim,
two-lsprovedall subs proved div-elim,
le-div-to-multprovedall subs proved div-elim,
mod-mult-01provedall subs proved mod-zero-01, mod-mult,
two-ls-02provedall subs proved div-elim,
two-neqprovedall subs proved div-elim,
two-loupprovedall subs proved div-elim,
two-neq-02provedall subs proved div-elim,
two-neq-01provedall subs proved div-elim,
mod-eq-mod-plus-1provedall subs proved div-elim, mod-one, mod-once,
square-nlsprovedall subs proved div-elim,
two-loup-13provedall subs proved div-elim,
two-odd-01provedall 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,
modsucc-neqprovedall 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-02provedall subs proved div-elim,
two-loup-04provedall subs proved div-elim,
two-loup-05provedall subs proved div-elim,
two-ppredprovedall subs proved div-elim,
two-eqprovedall subs proved div-elim,
lsprovedall subs proved div-elim,
two-peqprovedall subs proved div-elim, two-zero-01, two-one-01,
mod-succ-04provedall subs proved div-elim,
mod-multprovedall subs proved mod-once,
two-mdiv2-03provedall subs proved mult,
div-elimprovedall subs proved zero-01, mult, mod-ls, Moddef,
two-threeprovedall subs proved two-rec,
two-two-01provedall subs proved mult,
mod-recprovedall subs proved mod-once,
div-two-addprovedall subs proved mult,
mod-succ-03provedall subs proved mod-one-01, mod-once,
two-twosucc-02provedall subs proved mult,
multprovedall subs proved add,
mod-onceprovedall subs proved cond-01, add, rax,
two-recprovedall subs proved add,
recprovedall subs proved add,
mod-zero-01provedall subs proved mod-eq,
mod-one-01provedall subs proved mod-eq,
addprovedall subs proved ls-03, ls-02, le-01,
modsucc-lessprovedall subs proved mod-eq, mod-zero,
mod-le-04provedall subs proved mod-le-03, mod-eq,
leq-modsuccprovedall subs proved mod-zero, mod-eq,
ls-03provedall subs proved ls-02, Divdef,
cond-01provedall subs proved cond,
mod-zeroprovedall subs proved one, Moddef,
mod-eqprovedall subs proved zero-01, Moddef,
mod-lsprovedall subs proved mod-le-03,
mod-oneprovedall subs proved one-01, Moddef,
mod-nlsprovedall subs proved mod-le-03,
div-oneprovedall subs proved zero-01,
le-01provedall subs proved Divdef,
oneprovedall subs proved Divdef,
zeroprovedall subs proved Divdef,
raxprovedall subs proved Moddef,
ls-02provedall subs proved Divdef,
condprovedall subs proved Moddef,
mod-le-03provedall subs proved Divdef, Moddef,
zero-01provedall subs proved Divdef,
one-01provedall 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