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