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,
|
| 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-ass,
and-com,
|
| and-combine | proved | all subs proved
| and-com,
and-ass,
and,
precise-and,
precise-split-l,
sep-com,
|
| wand-intro-lifted | proved | all subs proved
| Imp1,
wand-intro,
Imp,
|
| sep-partial-mp-2 | proved | all subs proved
| sep-partial-mp,
split-union,
sep-com,
sep-ass,
sep-split-interactive,
|
| true-true | proved | all subs proved
| trueH,
true-emp,
|
| septract-given | proved | all subs proved
| precise-split-l,
septract,
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,
|
| sep-partial-mp | proved | all subs proved
| sep-com,
sep-ass,
split-union,
sep,
wand,
|
| wand-intro | proved | all subs proved
| sep-com,
sep-ass,
split-union,
wand,
|
| 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-disj | proved | all subs proved
| precise,
trueH,
precise-same,
sep-com,
sep-ass,
true-elim,
sep,
|
| adjunction | proved | all subs proved
| sep-com,
sep-ass,
split-union,
wand,
sep,
imp,
|
| eq-frame | proved | all subs proved
| sep-com,
sep-ass,
emp-sep,
|
| Imp2 | proved | all subs proved
| sep-com,
sep-ass,
split-union,
Imp1,
sep,
|
| sep-inj3 | proved | all subs proved
| sep-com,
sep-ass,
|
| Frame | proved | all subs proved
| sep-com,
sep-ass,
split-union,
wand,
Imp,
|
| sharing-weaken | proved | all subs proved
| sep,
sep-com,
sep-ass,
sharing,
sharing-com,
sharing-ass,
|
| imp-mono | proved | all subs proved
| sep-com,
sep-ass,
split-union,
sep,
|
| true-sharing | proved | all subs proved
| sep,
sep-com,
sep-ass,
prop,
sharing,
sharing-com,
sharing-ass,
true,
|
| wand-flatten | proved | all subs proved
| sep-com,
sep-ass,
split-union,
sep,
wand,
|
| stability | proved | all subs proved
| septract,
split-union,
sep-com,
this,
sep,
Imp,
|
| Eq-P | proved | all subs proved
| sep-com,
sep-ass,
emp-sep,
|
| Imp-frame | proved | all subs proved
| sep-com,
sep-ass,
emp-sep,
Imp,
|
| Imp-p | proved | all subs proved
| and-com,
and-ass,
prop,
and,
Imp,
p-Imp,
|
| wand-shift-p | proved | all subs proved
| sep-com,
wand-shift,
split-union,
sep,
sep-ass,
|
| p-Imp | proved | all subs proved
| and-com,
and-ass,
prop,
and,
Imp,
|
| precise-and | proved | all subs proved
| precise-same,
and-com,
and-ass,
and,
precise,
|
| sep-com | proved | all subs proved
| sep-ass,
split-union,
sep,
|
| And-prop-inj | proved | all subs proved
| and-com,
and-ass,
prop,
and,
|
| sep-mp-p | proved | all subs proved
| sep-mp,
split-union,
sep,
sep-ass,
|
| contract-wand | proved | all subs proved
| sep-mp,
and-com,
and-ass,
and,
|
| and-weaken | proved | all subs proved
| and-com,
and-ass,
and,
imp,
|
| and-weaken-this | proved | all subs proved
| imp,
and-com,
and-ass,
and,
|
| false-and | proved | all subs proved
| prop,
false,
and-com,
and-ass,
and,
|
| true-and | proved | all subs proved
| and-com,
and-ass,
prop,
and,
true,
|
| sharing-and | proved | all subs proved
| sharing,
sharing-com,
sharing-ass,
|
| sharing-sep-true | proved | all subs proved
| prop,
sep,
sharing,
sharing-com,
sharing-ass,
true,
|
| sharing-ass | proved | all subs proved
| sharing-ass-aux2,
sharing-ass-aux1,
|
| and-com | proved | all subs proved
| and-ass,
and,
|
| true-elim | proved | all subs proved
| prop,
split-union,
sep,
true,
|
| sep-ass | proved | all subs proved
| split-union,
sep,
|
| wand-same-emp-lifted | proved | all subs proved
| wand-same-emp,
emp,
Imp,
|
| wand-elim-lifted | proved | all subs proved
| Imp1,
wand-elim,
Imp,
|
| sep-inj2-imp | proved | all subs proved
| split-union,
sep,
Imp,
|
| or-com | proved | all subs proved
| or-ass,
or,
|
| wand-same-emp-p | proved | all subs proved
| wand-same-emp,
sep,
|
| introduce-sharing | proved | all subs proved
| sep,
wand,
this,
split-union,
sharing,
|
| precise-sep | proved | all subs proved
| precise-same,
sep,
precise,
|
| wand-shift | proved | all subs proved
| wand,
sep,
|
| sharing-ass-aux1 | proved | all subs proved
| sharing,
|
| sharing-ass-aux2 | proved | all subs proved
| sharing,
|
| sep-split-interactive | proved | all subs proved
| sep,
|
| sharing-com | proved | all subs proved
| sharing,
|
| or-ass | proved | all subs proved
| or,
|
| emp-sep | proved | all subs proved
| emp,
sep,
|
| sep-mp | proved | all subs proved
| wand,
sep,
|
| wand-elim | proved | all subs proved
| wand,
sep,
|
| Imp1 | proved | all subs proved
| Imp,
|
| split-union | proved | all subs proved
| sep,
|
| wand-same-emp | proved | all subs proved
| wand,
|
| precise-same | proved | all subs proved
| precise,
|
| trueH | proved | all subs proved
| prop,
true,
|
| and-ass | proved | all subs proved
| and,
|
| precise-this | proved | all subs proved
| this,
precise,
|
| ite-same | proved | all subs proved
| ite,
|
| wand-empty | proved | all subs proved
| emp,
wand,
|
| imp-cases | proved | all subs proved
| prop,
imp,
|
| Imp-from-eq | proved | all subs proved
| Imp,
|
| falseH | proved | all subs proved
| prop,
false,
|
| false-sep | proved | all subs proved
| prop,
sep,
false,
|
| Imp-trans | proved | all subs proved
| Imp,
|
| sep-mp-subset | proved | all subs proved
| wand,
sep,
Imp,
|
| this-emp | proved | all subs proved
| this,
emp,
|
| true-rev | proved | all subs proved
| true,
|
| ite-true | proved | all subs proved
| ite,
|
| false-rev | proved | all subs proved
| false,
|
| imp-proptrue | proved | all subs proved
| prop,
imp,
true,
|
| precise-emp | proved | all subs proved
| emp,
precise,
|
| wand-dual | proved | all subs proved
| wand,
septract,
not,
|
| septract-dual | proved | all subs proved
| septract,
wand,
not,
|
| imp-propfalse | proved | all subs proved
| prop,
imp,
true,
false,
|
| false-Imp | proved | all subs proved
| prop,
false,
Imp,
|
| Imp-refl | proved | all subs proved
| Imp,
|
| ite-false | proved | all subs proved
| ite,
|
| imp-ite | proved | all subs proved
| prop,
imp,
ite,
|
| true-elims | proved | all subs proved
| prop,
sharing,
true,
|
| precise-alt-def | proved | all subs proved
| precise,
|
| sharing-emp | proved | all subs proved
| emp,
sharing,
|
| not | axiom | | |
| septract | axiom | | |
| sharing | axiom | | |
| or | axiom | | |
| true | axiom | | |
| false | axiom | | |
| imp | axiom | | |
| prop | axiom | | |
| wand | axiom | | |
| ite | axiom | | |
| Imp | axiom | | |
| emp | axiom | | |
| sep | axiom | | |
| and | axiom | | |
| precise | axiom | | |
| this | axiom | | |