[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 olist-sort

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:
combine-ordered-sublists	proved	all subs proved	emptyp, Ordered, perm, ordered-perm-sort,
ordered-perm-sort	proved	all subs proved	sperm, eq,
two-01	proved	all subs proved	one, rec,
two	proved	all subs proved	one, rec,
sort-02	proved	all subs proved	rec, sort,
size-01	proved	all subs proved	size, rec,
ole	proved	all subs proved	ins-02, appins,
one	proved	all subs proved	empty, rec,
sort	proved	all subs proved	ins, rec, empty,
size	proved	all subs proved	rec, empty,
eq	proved	all subs proved	rec, empty,
ins-02	proved	all subs proved	Ordered, perm-01, rec,
emptyp	proved	all subs proved	rec, empty,
sort-append-three	proved	all subs proved	sperm,
sort-append	proved	all subs proved	sperm,
ins-01	proved	all subs proved	rec,
del1	proved	all subs proved	Ordered, rec, empty,
ins	proved	all subs proved	Ordered, perm,
sperm	proved	all subs proved	Ordered, perm, Perm,
appins	proved	all subs proved	Ordered, perm,
perm-01	proved	all subs proved	perm,
rec	proved	all subs proved	Ordered, perm,
sort-01	proved	all subs proved	Ordered, perm,
empty	proved	all subs proved	Perm,
perm	proved	all subs proved	Perm,
in	proved	all subs proved	Perm,
Perm	axiom
Ordered	axiom