[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,
lsucc-01provedall subs proved ltwo-05, lls, two-pot-zero, add, pot2-def, lemma-ax2, Log2def,
ltwo-03provedall subs proved ltwo-05, lls, two-pot-zero, add, pot2-def, lemma-ax2, Log2def,
ltwo-04provedall subs proved pot2-def, one-01, Log2def,
ltwo-05provedall subs proved lls-01, succ-02,
one-01provedall subs proved Pot2-zero, pot-01,
laddprovedall subs proved lls-02,
potmonleqprovedall subs proved potmon,
power-of-2provedall subs proved 2-pot-mod-01,
power-of-2-01provedall subs proved 2-pot-mod-01,
2-pot-mod-01provedall subs proved 2-pot-mod,
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,
llsprovedall subs proved Log2def, pot-mon, potex, two-pot-zero, pot2-def,
lls-02provedall subs proved Log2def, pot-mon, two-pot-zero, pot2-def, potex,
inj-02provedall subs proved pot2-def, lemma-ax2, inj,
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,
two-pot-zeroprovedall subs proved pot-zero,
potexprovedall subs proved Pot2-zero, zero, lemma-ax2,
pot-monprovedall subs proved rec-01, pot-zero, Pot-zero,
injprovedall subs proved lemma-ax2, one, Pot2-zero,
pot2-defprovedall subs proved add, lemma-ax2, Pot2-zero,
2-pot-modprovedall subs proved add,
pot-zero-01provedall subs proved zero-01,
twoprovedall subs proved add,
zero-01provedall subs proved rec-01,
pot-zeroprovedall subs proved rec-01, Pot-zero,
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,
multprovedall subs proved rec-01, Pot-zero,
pot-twoprovedall subs proved one-01-01, rec-01,
recprovedall subs proved lemma-ax2,
succ-03provedall subs proved lemma-ax2, Pot2-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