[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 persistence-refine

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:
refine-sync	proved	all subs proved	fwd-in-istore-lpt, fwd-in-gstore-lpt,
refine-add-ind	proved	all subs proved	fwd-in-istore-lpt,
refine-add-gnds	proved	all subs proved	fwd-in-gstore-lpt,
recovery	proved	all subs proved	fwd-in-gstore-lpt,
refine-commit	proved	all subs proved	fwd-in-gstore-lpt,
refine-allocate-ind	proved	all subs proved	fwd-in-gstore-lpt, fwd-in-istore-lpt,
refine-deallocate-gnd	proved	all subs proved	fwd-in-istore-lpt, fwd-in-gstore-lpt,
refine-allocate-gnd	proved	all subs proved	fwd-in-gstore-lpt,
refine-get-iblock-refsize	proved	all subs proved	fwd-in-istore-lpt,
refine-get-gblock-refsize	proved	all subs proved	fwd-in-gstore-lpt,
refine-set-iblock-refsize	proved	all subs proved	fwd-in-istore-lpt,
refine-set-gblock-refsize	proved	all subs proved	fwd-in-gstore-lpt,
refine-read-gblock-nodes	proved	all subs proved	fwd-in-gstore-lpt,
refine-read-ind	proved	all subs proved	fwd-in-istore-lpt,
refine-read-gnd	proved	all subs proved	fwd-in-gstore-lpt,
fwd-in-istore-lpt	proved	all subs proved
fwd-in-gstore-lpt	proved	all subs proved