[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 heap-sep

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:
prop-emp	proved	all subs proved	prop, and, and-com, and-ass, sep-com, sep-ass, emp-sep, prop-shift,
prop-shift	proved	all subs proved	prop-sep, and-imp, sep-com, sep-ass, and-com, and-ass, prop, and,
and-combine	proved	all subs proved	and, and-com, and-ass, precise-and, precise-split-l, sep-com,
and-split	proved	all subs proved	and, split-union, precise-split-l, sep, and-imp, sep-com, sep-ass, and-com, and-ass,
precise-split-r	proved	all subs proved	precise-split-l, sep-com, sep-ass, split-union,
septract-given	proved	all subs proved	precise-split-l, septract, Imp,
true-true	proved	all subs proved	true-emp, true-rev, prop, true,
precise-and	proved	all subs proved	precise-same, and-com, and-ass, and, precise,
prop-sep	proved	all subs proved	sep-com, sep-ass, split-union, and-com, and-ass, prop, and, sep,
and-imp	proved	all subs proved	sep-com, sep-ass, split-union, and-com, and-ass, and, sep,
precise-split-l	proved	all subs proved	sep, precise, sep-com, sep-ass, split-union,
true-emp	proved	all subs proved	sep-com, sep-ass, emp-sep, true-elim, true-rev, true,
true-and	proved	all subs proved	and-com, and-ass, prop, and, true,
stability	proved	all subs proved	septract, split-union, sep-com, this, sep, Imp,
precise-disj	proved	all subs proved	precise, trueH, precise-same, true-elim, sep-com, sep-ass, sep,
imp-mono	proved	all subs proved	sep-com, sep-ass, split-union, sep,
false-and	proved	all subs proved	and-com, and-ass, prop, and, false,
eq-frame	proved	all subs proved	sep-com, sep-ass, emp-sep,
and-weaken-this	proved	all subs proved	imp, and-com, and-ass, and,
and-weaken	proved	all subs proved	and-com, and-ass, and, imp,
adjunction	proved	all subs proved	sep-com, sep-ass, split-union, wand, sep, imp,
Imp2	proved	all subs proved	sep-com, sep-ass, split-union, sep, Imp,
Imp-frame	proved	all subs proved	sep-com, sep-ass, emp-sep, Imp,
Frame	proved	all subs proved	sep-com, sep-ass, split-union, wand, Imp,
Eq-P	proved	all subs proved	sep-ass, emp-sep, sep-com,
true-elim	proved	all subs proved	prop, split-union, sep, true,
and-com	proved	all subs proved	and-ass, and,
sep-com	proved	all subs proved	split-union, sep,
sep-ass	proved	all subs proved	split-union, sep,
imp-propfalse	proved	all subs proved	trueH, prop, imp, false,
imp-proptrue	proved	all subs proved	trueH, imp,
introduce-sharing	proved	all subs proved	sep, wand, this, split-union, sharing,
or-com	proved	all subs proved	or-ass, or,
precise-sep	proved	all subs proved	precise-same, sep, precise,
true-elims	proved	all subs proved	trueH, sharing,
wand-same-emp-p	proved	all subs proved	wand-same-emp, sep,
or-ass	proved	all subs proved	or,
precise-same	proved	all subs proved	precise,
and-ass	proved	all subs proved	and,
split-union	proved	all subs proved	sep,
trueH	proved	all subs proved	prop, true,
emp-sep	proved	all subs proved	emp, sep,
true-rev	proved	all subs proved	true,
wand-same-emp	proved	all subs proved	wand,
wand-shift	proved	all subs proved	wand, sep,
wand-dual	proved	all subs proved	wand, septract, not,
this-emp	proved	all subs proved	emp, this,
sharing-emp	proved	all subs proved	emp, sharing,
sharing-com	proved	all subs proved	sharing,
sep-split-interactive	proved	all subs proved	sep,
sep-mp	proved	all subs proved	wand, sep,
sep-Mp	proved	all subs proved	wand, sep, Imp,
precise-this	proved	all subs proved	this, precise,
precise-emp	proved	all subs proved	emp, precise,
imp-cases	proved	all subs proved	prop, imp,
falseH	proved	all subs proved	prop, false,
false-sep	proved	all subs proved	sep, prop, false,
false-rev	proved	all subs proved	false,
Imp1	proved	all subs proved	Imp,
Imp-trans	proved	all subs proved	Imp,
Imp-refl	proved	all subs proved	Imp,
Imp-from-eq	proved	all subs proved	Imp,
not	axiom
true	axiom
septract	axiom
precise	axiom
or	axiom
sharing	axiom
this	axiom
false	axiom
prop	axiom
emp	axiom
and	axiom
imp	axiom
sep	axiom
Imp	axiom
wand	axiom