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

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:
lexicographic-total	proved	all subs proved	array-exists-first-neq, lexicographic,
array-exists-first-neq	proved	all subs proved	ls-at-subarray,
suffix-same	proved	all subs proved	ls-at-subarray, suffix,
suffix-end	proved	all subs proved	suffix,
lexicographic-trans	proved	all subs proved	ls-at-subarray, lexicographic,
lexicographic-suffix-next	proved	all subs proved	ls-at-subarray, lexicographic, suffix,
lexicographic-irrefl	proved	all subs proved	lexicographic,
lexicographic-emparray	proved	all subs proved	lexicographic,
suffix	axiom
lexicographic	axiom
ls-at-subarray	proved	all subs proved