[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 dlinked-list

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:
inj-dll	proved	all subs proved	inj-dll-gen, dll,
inj-dll-gen	proved	all subs proved	dll-rec, dll-prev-null, dll-base,
dll-union	proved	all subs proved	dll-rec, dll-prev-null, dll-base,
precise-dll	proved	all subs proved	precise-dll-prev, dll,
dll-null	proved	all subs proved	dll-prev-null, dll,
dll-one	proved	all subs proved	dll-prev-one, dll,
dll-prev-one	proved	all subs proved	dll-base, dll-rec,
precise-dll-prev	proved	all subs proved	dll-rec, dll-base,
dll-prev-null	proved	all subs proved	dll-rec, dll-base,
dll-fold	proved	all subs proved	dll-rec,
ls-unfold2	proved	all subs proved	dll-rec,
ls-unfold1	proved	all subs proved	dll-rec, dll-base,
dll	axiom
dll-base	axiom
dll-rec	axiom