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