This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| sep | ⊦ (P0 * P1)(H) ↔ (∃ H0, H1. H0 ⊥ H1 ∧ H = H0 ∪ H1 ∧ P0(H0) ∧ P1(H1)) | An Axiom |
| imp | ⊦ (P0 → P1)(H) ↔ ¬ ¬ (P0(H) → P1(H)) | An Axiom |
| or | ⊦ (P0 ∨ P1)(H) ↔ ¬ ¬ (P0(H) ∨ P1(H)) | An Axiom |
| and | ⊦ (P0 ∧ P1)(H) ↔ ¬ ¬ (P0(H) ∧ P1(H)) | An Axiom |
| not | ⊦ (¬ P0)(H) ↔ ¬ P0(H) | An Axiom |
| prop | ⊦ ⌜bv⌝ (H) ↔ bv | An Axiom |
| emp | ⊦ emp(H) ↔ H = ∅ | An Axiom |
| precise | ⊦ precise(P) ↔ (∀ H, H0, H1, H2. P(H) ∧ P(H0) ∧ H ⊥ H1 ∧ H0 ⊥ H2 ∧ H ∪ H1 = H0 ∪ H2 → H = H0) | An Axiom |
| false | ⊦ false = ⌜false⌝ | An Axiom |
| true | ⊦ true = ⌜true⌝ | An Axiom |
| wand | ⊦ (P0 -* P1)(H) ↔ (∀ H1. H1 ⊥ H ∧ P0(H1) → P1(H1 ∪ H)) | An Axiom |
| Imp | ⊦ P0 ⊆ P1 ↔ (∀ H. P0(H) → P1(H)) | An Axiom |
| septract | ⊦ (P0 -⊗ P1)(H) ↔ (∃ H0, H1. H0 ⊥ H ∧ H1 = H0 ∪ H ∧ P0(H0) ∧ P1(H1)) | An Axiom |
| this | ⊦ {H} (H0) ↔ H = H0 | An Axiom |
| sharing | ⊦ (P0 ⊗ P1)(H) ↔ (∃ H0, H1, H2. H0 ⊥ H2 ∧ H0 ⊥ H1 ∧ H1 ⊥ H2 ∧ H = H0 ∪ H1 ∪ H2 ∧ P0(H0 ∪ H2) ∧ P1(H1 ∪ H2)) | An Axiom |
| Eq-P | ⊦ P0 = P1 ↔ (∀ P, H. (P0 * P)(H) ↔ (P1 * P)(H)) | A User Theorem |
| Frame | ⊦ P0 ⊆ P1 -* P1 * P0 | A User Theorem |
| Imp-frame | ∀ P. P * P0 ⊆ P * P1 ⊦ P0 ⊆ P1 | A User Theorem |
| Imp-from-eq | ⊦ P0 = P1 ↔ P0 ⊆ P1 ∧ P1 ⊆ P0 | A User Theorem |
| Imp-refl | ⊦ P ⊆ P | A User Theorem |
| Imp-trans | ⊦ P0 ⊆ P1 ∧ P1 ⊆ P2 → P0 ⊆ P2 | A User Theorem |
| Imp1 | ⊦ P0 ⊆ P1 ∧ P0(H) → P1(H) | A User Theorem |
| Imp2 | ⊦ P0 ⊆ P1 ∧ (P * P0)(H) → (P * P1)(H) | A User Theorem |
| adjunction | ⊦ (∀ H. (P0 → P1 -* P2)(H)) ↔ (∀ H. (P0 * P1 → P2)(H)) | A User Theorem |
| and-ass | ⊦ ((P0 ∧ P1) ∧ P2) = (P0 ∧ P1 ∧ P2) | A User Theorem |
| and-com | ⊦ (P0 ∧ P1) = (P1 ∧ P0) | A User Theorem |
| and-combine | precise(P0) ⊦ H ⊥ H0 ∧ P0(H0) ∧ P1(H0) → ((P * (P0 ∧ P1))(H ∪ H0) ↔ P(H)) | A User Theorem |
| and-imp | ⊦ (P * (P1 ∧ P2))(H) → (P * P1)(H) | A User Theorem |
| and-split | precise(P) ⊦ (P * (P0 ∧ P1))(H) ↔ (P * P0)(H) ∧ (P * P1)(H) | A User Theorem |
| and-weaken | ∀ H. (P1 → P0)(H) ⊦ (P0 ∧ P1) = P1 | A User Theorem |
| and-weaken-this | (P1 → P0)(H) ⊦ (P0 ∧ P1)(H) ↔ P1(H) | A User Theorem |
| emp-sep | ⊦ emp * P = P | A User Theorem |
| eq-frame | ∀ P. P * P0 = P * P1 ⊦ P0 = P1 | A User Theorem |
| false-and | ⊦ (false ∧ P) = false | A User Theorem |
| false-rev | ⊦ ⌜false⌝ = false | A User Theorem |
| false-sep | ⊦ false * P = false | A User Theorem |
| falseH | ⊦ ¬ false(H) | A User Theorem |
| imp-cases | ⊦ bv → (⌜bv⌝ → P) = P | A User Theorem |
| imp-mono | ∀ H. P(H) → P0(H), (P * P1)(H0) ⊦ (P0 * P1)(H0) | A User Theorem |
| imp-propfalse | ⊦ (false → P) = true | A User Theorem |
| imp-proptrue | ⊦ (true → P) = P | A User Theorem |
| introduce-sharing | ⊦ (P0 ⊗ P1)(H) ↔ (∃ P. ((P -* P0) * (P -* P1) * P)(H)) | A User Theorem |
| or-ass | ⊦ ((P0 ∨ P1) ∨ P2) = (P0 ∨ P1 ∨ P2) | A User Theorem |
| or-com | ⊦ (P0 ∨ P1) = (P1 ∨ P0) | A User Theorem |
| precise-and | ⊦ precise(P0) → precise(P0 ∧ P1) | A User Theorem |
| precise-disj | precise(P0), precise(P1) ⊦ (P0 * P1 * true)(H0 ∪ H2) ∧ H0 ∪ H2 = H1 ∪ H3 ∧ H0 ⊥ H2 ∧ H1 ⊥ H3 ∧ P0(H0) ∧ P1(H1) → H0 ⊥ H1 | A User Theorem |
| precise-emp | ⊦ precise(emp) | A User Theorem |
| precise-same | precise(P) ⊦ P(H0) ∧ P(H1) ∧ H0 ⊥ H ∧ H1 ⊥ H2 → (H0 ∪ H = H1 ∪ H2 ↔ ¬ ¬ (H0 = H1 ∧ H = H2)) | A User Theorem |
| precise-sep | ⊦ precise(P0) ∧ precise(P1) → precise(P0 * P1) | A User Theorem |
| precise-split-l | precise(P0) ⊦ P0(H0) ∧ H0 ⊥ H1 → ((P0 * P1)(H0 ∪ H1) ↔ P1(H1)) | A User Theorem |
| precise-split-r | precise(P1) ⊦ P1(H1) ∧ H0 ⊥ H1 → ((P0 * P1)(H0 ∪ H1) ↔ P0(H0)) | A User Theorem |
| precise-this | ⊦ precise({H} ) | A User Theorem |
| prop-emp | ⊦ ((⌜bv⌝ ∧ emp) * P)(H) ↔ ¬ ¬ (bv ∧ P(H)) | A User Theorem |
| prop-sep | ⊦ ((⌜bv⌝ ∧ P0) * P1)(H) ↔ bv ∧ (P0 * P1)(H) | A User Theorem |
| prop-shift | ⊦ (⌜bv⌝ ∧ P0) * P1 = (⌜bv⌝ ∧ P0 * P1) | A User Theorem |
| sep-Mp | ⊦ P0 * (P0 -* P1) ⊆ P1 | A User Theorem |
| sep-ass | ⊦ (P0 * P1) * P2 = P0 * P1 * P2 | A User Theorem |
| sep-com | ⊦ P0 * P1 = P1 * P0 | A User Theorem |
| sep-mp | ⊦ (P0 * (P0 -* P1))(H) → P1(H) | A User Theorem |
| sep-split-interactive | ⊦ ∀ P0. (P * P0)(H) → (∃ H0, H1. H0 ⊥ H1 ∧ H0 ∪ H1 = H ∧ P(H0) ∧ P0(H1)) | A User Theorem |
| septract-given | ⊦ precise(P0) → P0 -⊗ P0 * P1 ⊆ P1 | A User Theorem |
| sharing-com | ⊦ P0 ⊗ P1 = P1 ⊗ P0 | A User Theorem |
| sharing-emp | ⊦ P ⊗ emp = P | A User Theorem |
| split-union | ⊦ P0(H0) ∧ P1(H1) ∧ H0 ⊥ H1 → (¬ (P0 * P1)(H0 ∪ H1) ↔ false) | A User Theorem |
| stability | (P0 * {H} )(H0), (P1 * {H} )(H1), (P0 -⊗ P) * P1 ⊆ P ⊦ P(H0) → P(H1) | A User Theorem |
| this-emp | ⊦ {∅} = emp | A User Theorem |
| true-and | ⊦ (true ∧ P) = P | A User Theorem |
| true-elim | ⊦ (P0 * P)(H) → (true * P)(H) | A User Theorem |
| true-elims | ⊦ (P0 ⊗ P)(H) → (true ⊗ P)(H) | A User Theorem |
| true-emp | ⊦ P(H) → (true * P)(H) | A User Theorem |
| true-rev | ⊦ ⌜true⌝ = true | A User Theorem |
| true-true | ⊦ true * true = true | A User Theorem |
| trueH | ⊦ true(H) | A User Theorem |
| wand-dual | ⊦ P0 -⊗ P1 = ¬ (P0 -* ¬ P1) | A User Theorem |
| wand-same-emp | ⊦ (P -* P)(∅) | A User Theorem |
| wand-same-emp-p | ⊦ P0(H) → (¬ ((P -* P) * P0)(H) ↔ false) | A User Theorem |
| wand-shift | ⊦ (P0 * (P1 -* P2))(H) → (¬ (P1 -* P0 * P2)(H) ↔ false) | A User Theorem |