[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,
ltwo-04provedall subs proved pot2-def, one-01, Log2def,
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,
ladd-01provedall subs proved ladd,
ltwo-05provedall subs proved lls-01, succ-02,
one-01provedall subs proved Pot2-zero, pot-01,
laddprovedall subs proved lls-02,
power-of-2-01provedall subs proved 2-pot-mod-01,
power-of-2provedall subs proved 2-pot-mod-01,
potmonleqprovedall subs proved potmon,
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,
pot2-addprovedall subs proved add, pot2-def,
lpotprovedall subs proved two-pot-zero, pot-mon, lemma-ax2, Log2def, pot2-def,
inj-02provedall subs proved pot2-def, lemma-ax2, inj,
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,
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,
zeroprovedall subs proved lemma-ax2, Pot2-zero,
succ-02provedall subs proved lemma-ax2,
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