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

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:
dll_to_bst_correct	proved	all subs proved	dll_to_bst_rec_correct, dll-size-correct, dll_to_bst,
dll_to_bst_iter_correct	proved	all subs proved	dll_to_bst_rec_correct, dll-size-iter-correct, dll_to_bst_iter,
dll-size-iter-correct	proved	all subs proved	size_iter,
dll-size-correct	proved	all subs proved	size,
dll_to_bst_rec_correct	proved	all subs proved	dll_to_bst_rec,
dll_to_bst_iter	axiom
size	axiom
size_iter	axiom
dll_to_bst_rec	axiom
dll_to_bst	axiom