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