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

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:
owns-one-none	proved	all subs proved	owns-none, owns-one,
rely-alloc	proved	all subs proved	rely,
owns-one-map	proved	all subs proved	owns-one,
rely-reuse	proved	all subs proved	rely,
rely-owns-one	proved	all subs proved	owns-one, rely,
rely-map-write-known	proved	all subs proved	rely,
rely-trans	proved	all subs proved	rely,
owns-none-one	proved	all subs proved	owns-one, owns-none,
rely-map-write-unknown	proved	all subs proved	rely,
rely-transfer-owner	proved	all subs proved	rely,
owns-none-one2	proved	all subs proved	owns-one, owns-none,
rely-refl	proved	all subs proved	rely,
rely-owned-in-rs	proved	all subs proved	rely,
rely-owned-unchgd	proved	all subs proved	rely,
rely-owns-none	proved	all subs proved	rely, owns-none,
owns-one	axiom
owns-none	axiom
rely	axiom