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

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:
odd-addprovedall subs proved even, odd-01, modd-02, pot2-even-02, div2-elim,
even-addprovedall subs proved even, odd-01, modd-02, pot2-odd-02, div2-elim,
odd-multprovedall subs proved even, odd-01, modd-02, pot2-even-02, div2-elim,
modd-02provedall subs proved meven-02, oe-02,
meven-03provedall subs proved oex, eo-02,
eo-02provedall subs proved even, oex,
oe-02provedall subs proved even, oex,
meven-02provedall subs proved oex, eo-01,
div2-elimprovedall subs proved oex,
even-multprovedall subs proved even, oex, eo-01,
max-ls-self1provedall subs proved max-c, max-a, max-ls-self2,
modd-03provedall subs proved oex,
max-neq1provedall subs proved max-c, max-a, Max-left, max-neq2,
div2-oddprovedall subs proved even, odd-01, pot2-odd-02,
odd-div2provedall subs proved oex,
min-neq1provedall subs proved min-c, min-a, Min-left, min-neq2,
min-zero1provedall subs proved min-c, min-a, min-zero2,
otwo-02provedall subs proved oex,
min-ls-self1provedall subs proved min-c, min-a, min-ls-self2,
min-ls-self2provedall subs proved Min-right, min-c, min-a, Min-left,
min-zero2provedall subs proved Min-right, min-c, min-a, Min-left,
min-neq2provedall subs proved min-c, min-a, Min-left, Min-right,
max-neq2provedall subs proved max-c, max-a, Max-left, Max-right,
pot2-odd-02provedall subs proved even, odd-01,
max-ls-self2provedall subs proved Max-right, max-c, max-a, Max-left,
eo-01provedall subs proved even, odd-01,
oexprovedall subs proved even, odd-01,
min-ls-bothprovedall subs proved Min-right, min-c, min-a, Min-left,
oe-01provedall subs proved even, odd-01,
eoprovedall subs proved even, odd-01,
oddprovedall subs proved odd-01, Odd-new, zero-02,
ozeroprovedall subs proved even, odd-01,
div2-odd-01provedall subs proved even, odd-01, pot2-even-02,
max-ls-bothprovedall subs proved Max-right, max-c, max-a, Max-left,
zero-02provedall subs proved even, Even-new,
max-cprovedall subs proved Max-right, max-a, Max-left,
min-cprovedall subs proved Min-right, min-a, Min-left,
pot2-even-02provedall subs proved even,
odd-01provedall subs proved even, Odd-new,
two-02provedall subs proved even,
div2-evenprovedall subs proved even,
two-03provedall subs proved even,
min-iprovedall subs proved Min-right, min-a, Min-left,
plusprovedall subs proved even,
min-distrprovedall subs proved Min-right, min-a, Min-left,
max-distrprovedall subs proved Max-right, max-a, Max-left,
zero-01provedall subs proved even, Even-new,
even-div2provedall subs proved even,
max-iprovedall subs proved Max-right, max-a, Max-left,
div2-elim-01provedall subs proved even,
max-aprovedall subs proved Max-right, Max-left,
min-aprovedall subs proved Min-right, Min-left,
evenprovedall subs proved Even-new,
Even-newaxiom
Odd-newaxiom
Max-leftaxiom
Max-rightaxiom
Min-leftaxiom
Min-rightaxiom