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