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 | ⊦ aP ⊗_ ∅ = emp | An Axiom |
| Sep-ins | ⊦ ¬ a ∈ s → aP ⊗_ (s ++ a) = aP(a) * aP ⊗_ s | An Axiom |
| And-emp | ⊦ aP ∧_ ∅ = true | An Axiom |
| And-ins | ⊦ ¬ a ∈ s → aP ∧_ (s ++ a) = (aP(a) ∧ aP ∧_ s) | An Axiom |
| And-discard | ⊦ s ≠ ∅ → (λ a. P) ∧_ s = P | A User Theorem |
| And-forall | ∀ a, H. a ∈ s ∧ aP0(a)(H) → aP(a)(H) ⊦ (aP0 ∧_ s)(H) → (aP ∧_ s)(H) | A User Theorem |
| And-unfold | ⊦ a ∈ s → aP ∧_ s = (aP(a) ∧ aP ∧_ (s -- a)) | A User Theorem |
| Sep-eq | ⊦ (∀ a. a ∈ s → aP(a) = aP0(a)) → aP ⊗_ s = aP0 ⊗_ s | A User Theorem |
| Sep-forall | ∀ a, H. a ∈ s ∧ aP0(a)(H) → aP(a)(H) ⊦ (aP0 ⊗_ s)(H) → (aP ⊗_ s)(H) | A User Theorem |
| Sep-unfold | ⊦ a ∈ s → aP ⊗_ s = aP(a) * aP ⊗_ (s -- a) | A User Theorem |
| precise-Sep | ∀ a. a ∈ s → precise(aP(a)) ⊦ precise(aP ⊗_ s) | A User Theorem |