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