[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 map-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:
true-trueprovedall subs proved trueH, true-emp,
prop-empprovedall subs proved and-com, and-ass, prop, and, sep-com, sep-ass, emp-sep, prop-shift,
prop-shiftprovedall subs proved and-com, and-ass, prop-sep, prop, and,
true-empprovedall subs proved sep-com, sep-ass, emp-sep, true-elim,
precise-disjprovedall subs proved precise, prop, precise-same, sep-com, sep-ass, sep, true,
adjunctionprovedall subs proved sep-com, sep-ass, split-union, wand, sep, imp,
Imp2provedall subs proved sep-com, sep-ass, split-union, Imp1, sep,
precise-split-rprovedall subs proved precise-split-l, sep-com,
Frameprovedall subs proved sep-com, sep-ass, split-union, wand, Imp,
and-splitprovedall subs proved and, split-union, precise-split-l, sep, and-imp, and-ass, and-com,
sharing-weakenprovedall subs proved sharing, sep, sep-com, sep-ass,
and-combineprovedall subs proved and-com, and-ass, and, precise-and, precise-split-l, sep-com,
true-sharingprovedall subs proved sep, sep-com, sep-ass, prop, sharing, sharing-com, sharing-ass, true,
wand-flattenprovedall subs proved sep-com, sep-ass, split-union, sep, wand,
stabilityprovedall subs proved septract, split-union, sep-com, this, sep, Imp,
sep-partial-mp-2provedall subs proved sep-partial-mp, split-union, sep-com, sep-ass, sep-split-interactive,
Eq-Pprovedall subs proved sep-com, sep-ass, emp-sep,
Imp-frameprovedall subs proved sep-com, sep-ass, emp-sep, Imp,
Imp-pprovedall subs proved and-com, and-ass, prop, and, Imp, p-Imp,
wand-shift-pprovedall subs proved sep-com, wand-shift, split-union, sep, sep-ass,
prop-sepprovedall subs proved and-com, and-ass, prop, and, split-union, sep,
p-Impprovedall subs proved and-com, and-ass, prop, and, Imp,
precise-andprovedall subs proved precise-same, and-com, and-ass, and, precise,
and-impprovedall subs proved split-union, and-com, and-ass, and, sep,
sep-comprovedall subs proved sep-ass, split-union, sep,
sep-mp-pprovedall subs proved sep-mp, split-union, sep, sep-ass,
contract-wandprovedall subs proved sep-mp, and-com, and-ass, and,
and-weakenprovedall subs proved and-com, and-ass, and, imp,
and-weaken-thisprovedall subs proved imp, and-com, and-ass, and,
false-andprovedall subs proved prop, false, and-com, and-ass, and,
true-andprovedall subs proved and-com, and-ass, prop, and, true,
sharing-andprovedall subs proved sharing, sharing-com, sharing-ass,
sharing-sep-trueprovedall subs proved prop, sep, sharing, sharing-com, sharing-ass, true,
septract-givenprovedall subs proved precise-split-l, septract, Imp,
true-elimprovedall subs proved prop, split-union, sep, true,
sharing-assprovedall subs proved sharing-ass-aux2, sharing-ass-aux1,
and-comprovedall subs proved and-ass, and,
precise-split-lprovedall subs proved sep, precise, split-union,
sep-assprovedall subs proved split-union, sep,
eq-frameprovedall subs proved emp-sep,
sep-inj2-impprovedall subs proved split-union, sep, Imp,
or-comprovedall subs proved or-ass, or,
imp-monoprovedall subs proved split-union, sep,
wand-same-emp-pprovedall subs proved wand-same-emp, sep,
introduce-sharingprovedall subs proved sep, wand, this, split-union, sharing,
precise-sepprovedall subs proved precise-same, sep, precise,
wand-shiftprovedall subs proved wand, sep,
trueHprovedall subs proved prop, true,
sharing-ass-aux1provedall subs proved sharing,
sharing-ass-aux2provedall subs proved sharing,
sep-split-interactiveprovedall subs proved sep,
sep-partial-mpprovedall subs proved sep, wand,
sharing-comprovedall subs proved sharing,
wand-same-empprovedall subs proved wand,
or-assprovedall subs proved or,
Imp1provedall subs proved Imp,
emp-sepprovedall subs proved emp, sep,
sep-mpprovedall subs proved wand, sep,
split-unionprovedall subs proved sep,
precise-sameprovedall subs proved precise,
and-assprovedall subs proved and,
precise-thisprovedall subs proved this, precise,
ite-sameprovedall subs proved ite,
imp-casesprovedall subs proved prop, imp,
And-prop-injprovedall subs proved prop, and,
Imp-from-eqprovedall subs proved Imp,
falseHprovedall subs proved prop, false,
false-sepprovedall subs proved prop, sep, false,
Imp-transprovedall subs proved Imp,
sep-mp-subsetprovedall subs proved wand, sep, Imp,
this-empprovedall subs proved this, emp,
true-revprovedall subs proved true,
ite-trueprovedall subs proved ite,
false-revprovedall subs proved false,
imp-proptrueprovedall subs proved prop, imp, true,
precise-empprovedall subs proved emp, precise,
wand-dualprovedall subs proved wand, septract, not,
septract-dualprovedall subs proved septract, wand, not,
imp-propfalseprovedall subs proved prop, imp, true, false,
false-Impprovedall subs proved prop, false, Imp,
Imp-reflprovedall subs proved Imp,
ite-falseprovedall subs proved ite,
imp-iteprovedall subs proved prop, imp, ite,
true-elimsprovedall subs proved prop, sharing, true,
precise-alt-defprovedall subs proved precise,
sharing-empprovedall subs proved emp, sharing,
notaxiom
septractaxiom
sharingaxiom
oraxiom
empaxiom
falseaxiom
Impaxiom
wandaxiom
impaxiom
iteaxiom
trueaxiom
sepaxiom
propaxiom
andaxiom
preciseaxiom
thisaxiom