[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	and-com, and-ass, prop, and, sep-com, sep-ass, emp-sep, prop-shift,
prop-shift	proved	all subs proved	sep-com, sep-ass, and-com, and-ass, prop-sep, prop, and,
true-true	proved	all subs proved	trueH, true-emp,
septract-given	proved	all subs proved	precise-split-l, septract, Imp,
precise-split-r	proved	all subs proved	precise-split-l, sep-com, sep-ass, split-union,
and-split	proved	all subs proved	and, split-union, precise-split-l, sep, sep-com, sep-ass, and-imp, and-com, and-ass,
and-combine	proved	all subs proved	and-com, and-ass, and, precise-and, precise-split-l, sep-com,
Imp-p	proved	all subs proved	and-com, and-ass, prop, and, Imp, p-Imp,
true-emp	proved	all subs proved	sep-com, sep-ass, emp-sep, true-elim,
prop-sep	proved	all subs proved	and-com, and-ass, prop, and, sep-com, sep-ass, split-union, 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,
precise-and	proved	all subs proved	precise-same, and-com, and-ass, and, precise,
p-Imp	proved	all subs proved	and-com, and-ass, prop, and, Imp,
wand-shift-p	proved	all subs proved	sep-com, wand-shift, split-union, sep, sep-ass,
wand-flatten	proved	all subs proved	sep-com, sep-ass, split-union, sep, wand,
true-and	proved	all subs proved	and-com, and-ass, trueH, and,
stability	proved	all subs proved	septract, split-union, sep-com, this, sep, Imp,
sep-partial-mp-2	proved	all subs proved	sep-partial-mp, split-union, sep-com, sep-ass, sep-split-interactive,
sep-mp-p	proved	all subs proved	sep-mp, split-union, sep, sep-ass,
sep-inj3	proved	all subs proved	sep-com, sep-ass,
precise-disj	proved	all subs proved	precise, trueH, precise-same, sep-com, sep-ass, true-elim, sep,
imp-mono	proved	all subs proved	sep-com, sep-ass, split-union, sep,
false-and	proved	all subs proved	prop, false, and-com, and-ass, and,
eq-frame	proved	all subs proved	sep-com, sep-ass, emp-sep,
contract-wand	proved	all subs proved	sep-mp, and-com, and-ass, and,
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-com, sep-ass, emp-sep,
And-prop-inj	proved	all subs proved	and-com, and-ass, prop, and,
sep-partial-mp	proved	all subs proved	split-union, sep, wand,
true-elim	proved	all subs proved	trueH, split-union, sep,
sep-ass	proved	all subs proved	split-union, sep,
sep-com	proved	all subs proved	split-union, sep,
and-com	proved	all subs proved	and-ass, and,
wand-same-emp-p	proved	all subs proved	wand-same-emp, sep,
true-rev	proved	all subs proved	trueH, prop,
true-elims	proved	all subs proved	trueH, sharing,
sep-inj2-imp	proved	all subs proved	split-union, sep, Imp,
precise-sep	proved	all subs proved	precise-same, sep, precise,
or-com	proved	all subs proved	or-ass, or,
introduce-sharing	proved	all subs proved	sep, wand, this, split-union, sharing,
imp-proptrue	proved	all subs proved	trueH, imp,
imp-propfalse	proved	all subs proved	prop, trueH, imp, false,
wand-shift	proved	all subs proved	wand, sep,
wand-same-emp	proved	all subs proved	wand,
sep-split-interactive	proved	all subs proved	sep,
precise-same	proved	all subs proved	precise,
or-ass	proved	all subs proved	or,
trueH	proved	all subs proved	prop, true,
sep-mp	proved	all subs proved	wand, sep,
split-union	proved	all subs proved	sep,
emp-sep	proved	all subs proved	emp, sep,
and-ass	proved	all subs proved	and,
wand-dual	proved	all subs proved	wand, septract, not,
this-emp	proved	all subs proved	this, emp,
sharing-emp	proved	all subs proved	emp, sharing,
sharing-com	proved	all subs proved	sharing,
septract-dual	proved	all subs proved	septract, wand, not,
sep-mp-subset	proved	all subs proved	wand, sep, Imp,
precise-this	proved	all subs proved	this, precise,
precise-emp	proved	all subs proved	emp, precise,
precise-alt-def	proved	all subs proved	precise,
ite-true	proved	all subs proved	ite,
ite-same	proved	all subs proved	ite,
ite-false	proved	all subs proved	ite,
imp-ite	proved	all subs proved	prop, imp, ite,
imp-cases	proved	all subs proved	prop, imp,
falseH	proved	all subs proved	prop, false,
false-sep	proved	all subs proved	prop, sep, false,
false-rev	proved	all subs proved	false,
false-Imp	proved	all subs proved	prop, false, Imp,
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,
true	axiom
not	axiom
septract	axiom
precise	axiom
or	axiom
sharing	axiom
this	axiom
ite	axiom
false	axiom
emp	axiom
imp	axiom
sep	axiom
Imp	axiom
wand	axiom
and	axiom
prop	axiom