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

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:
legal-noncylic-equiv-reaches-null	proved	all subs proved	legal-nxt-1, cyclic-weak-def,
cyclic-brent-def	proved	all subs proved	cyclic-weak-def, cyclic-all-ncyclic, cyclic-def,
cyclic-weak-def	proved	all subs proved	path-nodups-subset, path-dups, cyclic-alt-def,
cyclic-floyd-def	proved	all subs proved	cyclic-def, cyclic-all-ncyclic, cyclic-ncyclic, cyclic-alt-def,
legal-nxt-2	proved	all subs proved	legal-nxt-1,
reach-n-next-legal	proved	all subs proved	legal-nxt-1,
cyclic-all-ncyclic	proved	all subs proved	cyclic-ncyclic, cyclic-all-cyclic,
path-dups	proved	all subs proved	cyclic-def,
cyclic-alt-def	proved	all subs proved	cyclic-def,
legal-nxt-1	proved	all subs proved	legal-def,
legal-def	axiom
path-nodups-subset	proved	all subs proved
cyclic-def	axiom
cyclic-all-cyclic	proved	all subs proved
cyclic-ncyclic	proved	all subs proved