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-emp | ⊦ adP ⊗_ ∅ = emp | An Axiom |
| Sep-ins | ⊦ ¬ a ∈ st → adP ⊗_ st[a, d] = adP(a, d) * adP ⊗_ st | An Axiom |
| And-emp | ⊦ adP ∧_ ∅ = true | An Axiom |
| And-ins | ⊦ ¬ a ∈ st → adP ∧_ st[a, d] = (adP(a, d) ∧ adP ∧_ st) | An Axiom |
| And-discard | ⊦ st ≠ ∅ → (λ a, d. P) ∧_ st = P | A User Theorem |
| And-forall | ∀ a, H. a ∈ st ∧ adP0(a, st[a])(H) → adP(a, st[a])(H) ⊦ (adP0 ∧_ st)(H) → (adP ∧_ st)(H) | A User Theorem |
| And-unfold | ⊦ a ∈ st → adP ∧_ st = (adP(a, st[a]) ∧ adP ∧_ (st -- a)) | A User Theorem |
| Sep-any | ⊦ st ≠ ∅ → ((adP ⊗_ st * P)(H) ↔ (∃ a, d, st0. ¬ a ∈ st0 ∧ st = st0[a, d] ∧ (adP(a, d) * adP ⊗_ st0 * P)(H))) | A User Theorem |
| Sep-eq | ⊦ (∀ a. a ∈ st → adP(a, st[a]) = adP0(a, st[a])) → adP ⊗_ st = adP0 ⊗_ st | A User Theorem |
| Sep-forall | ∀ a, H. a ∈ st ∧ adP0(a, st[a])(H) → adP(a, st[a])(H) ⊦ (adP0 ⊗_ st)(H) → (adP ⊗_ st)(H) | A User Theorem |
| Sep-unfold | ⊦ a ∈ st → adP ⊗_ st = adP(a, st[a]) * adP ⊗_ (st -- a) | A User Theorem |
| precise-Sep | ∀ a. a ∈ st → precise(adP(a, st[a])) ⊦ precise(adP ⊗_ st) | A User Theorem |