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

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:
leone-trueprovedall subs proved leone,
leone-falseprovedall subs proved leone,
leoneprovedall subs proved one-02, one-01,
one-01provedall subs proved one-02,
nottrue-02provedall subs proved nottrue,
mklist-introprovedall subs proved mklist, mklist-01,
mklist-02provedall subs proved inmklist,
last-first-01provedall subs proved nottrue,
last-firstprovedall subs proved notfalse,
mklist-01provedall subs proved
mklistprovedall subs proved
inmklistprovedall subs proved
one-02provedall subs proved
nottrueprovedall subs proved
notfalseprovedall subs proved