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