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

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:
ltwo-03provedall subs proved pot-mon, ltwo-05, lls, two-pot-zero, add, pot2-def, lemma-ax2, Log2def,
lsucc-01provedall subs proved ltwo-05, lls, two-pot-zero, add, pot2-def, lemma-ax2, Log2def,
ltwo-05provedall subs proved lls-01, succ-02,
lpotprovedall subs proved zero, lemma-ax2, potmonleq, Log2def,
ladd-01provedall subs proved ladd,
lls-01provedall subs proved Log2def, potmon, zero, potex, lemma-ax2,
llsprovedall subs proved Log2def, potmon, lemma-ax2, potex, zero,
potmonleqprovedall subs proved potmon,
laddprovedall subs proved lls-02,
power-of-2-01provedall subs proved 2-pot-mod-01,
power-of-2provedall subs proved 2-pot-mod-01,
lzerprovedall subs proved Pot2-zero, Log2def, zero, lemma-ax2, potex, lone,
2-pot-mod-01provedall subs proved 2-pot-mod,
loneprovedall subs proved one-01, Pot2-zero, Log2def,
potmonprovedall subs proved pot-mon, pot2-def,
lls-02provedall subs proved Log2def, pot-mon, two-pot-zero, pot2-def, potex,
pot2-addprovedall subs proved add, pot2-def,
ltwo-04provedall subs proved pot2-def, one-01, Log2def,
inj-02provedall subs proved lemma-ax2, inj,
one-01provedall subs proved Pot2-zero, pot-01,
pot2-defprovedall subs proved add, lemma-ax2, Pot2-zero,
two-pot-zeroprovedall subs proved pot-zero,
pot-monprovedall subs proved rec-01, pot-zero, Pot-zero,
potexprovedall subs proved Pot2-zero, zero, lemma-ax2,
injprovedall subs proved lemma-ax2, one, Pot2-zero,
2-pot-modprovedall subs proved add,
twoprovedall subs proved add,
pot-zero-01provedall subs proved zero-01,
zero-01provedall subs proved rec-01,
pot-zeroprovedall subs proved rec-01, Pot-zero,
pot-01provedall subs proved lemma-ax2,
succ-02provedall subs proved lemma-ax2,
zeroprovedall subs proved lemma-ax2, Pot2-zero,
oneprovedall subs proved lemma-ax2, Pot2-zero,
addprovedall subs proved rec-01, Pot-zero,
succ-03provedall subs proved lemma-ax2, Pot2-zero,
recprovedall subs proved lemma-ax2,
pot-twoprovedall subs proved one-01-01, rec-01,
multprovedall subs proved rec-01, Pot-zero,
one-01-01provedall subs proved Pot-zero, Pot-succ,
lemma-ax2provedall subs proved Pot2-succ,
rec-01provedall subs proved Pot-succ,
Pot-succaxiom
Log2defaxiom
Pot2-succaxiom
Pot2-zeroaxiom
Pot-zeroaxiom