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: |
|---|---|---|
| ex1 | ⊦ (_∃ rP)(H) ↔ (∃ r. rP(r)(H)) | An Axiom |
| ex2 | ⊦ (_∃ rrP)(H) ↔ (∃ r0, r1. rrP(r0, r1)(H)) | An Axiom |
| maplet | ⊦ (r => o)(H) ↔ ¬ ¬ (H = (∅ ++ r)[r, o] ∧ r ≠ null) | An Axiom |
| mapex | ⊦ r =>_ = _∃ λ o. r => o | An Axiom |
| ex3 | ⊦ (_∃ oP)(H) ↔ (∃ o. oP(o)(H)) | An Axiom |
| mapornull | ⊦ r =>? = ((r = null ⊃ emp; r =>_)) | An Axiom |
| at-eq | ⊦ (r => o0 * P)(H) → (H[r] = o1 ↔ o0 = o1) | A User Theorem |
| at-rw | ⊦ (r => o0 * P)(H) → H[r] = o0 | A User Theorem |
| eq-objs | ⊦ (r => o0 * P0)(H) ∧ (r => o1 * P1)(H) → o0 = o1 | A User Theorem |
| ex1-shift | ⊦ (_∃ rP * P)(H) ↔ (∃ r. (rP(r) * P)(H)) | A User Theorem |
| ex1-shiftw | ⊦ (_∃ rP -* P)(H) ↔ (∀ r. (rP(r) -* P)(H)) | A User Theorem |
| ex2-shift | ⊦ (_∃ rrP * P)(H) ↔ (∃ r0, r1. (rrP(r0, r1) * P)(H)) | A User Theorem |
| ex2-shiftw | ⊦ (_∃ rrP -* P)(H) ↔ (∀ r0, r1. (rrP(r0, r1) -* P)(H)) | A User Theorem |
| ex3-shift | ⊦ (_∃ oP * P)(H) ↔ (∃ o. (oP(o) * P)(H)) | A User Theorem |
| ex3-shiftw | ⊦ (_∃ oP -* P)(H) ↔ (∀ o. (oP(o) -* P)(H)) | A User Theorem |
| map-del | ⊦ (r => o * P)(H) ↔ P(H -- r) ∧ r ∈ H ∧ H[r] = o | A User Theorem |
| map-in | ⊦ (r => o * P)(H) → r ∈ H | A User Theorem |
| map-in0 | ⊦ (r => o)(H) → r ∈ H | A User Theorem |
| map-null | ⊦ null => o = ⌜false⌝ | A User Theorem |
| map-put | ⊦ (r =>_ * P)(H) ↔ (r => o1 * P)(H[r, o1]) ∧ r ∈ H | A User Theorem |
| map-put-rw | r ∈ H ⊦ (r => o * P)(H) → (¬ (r => o0 * P)(H[r, o1]) ↔ o0 ≠ o1) | A User Theorem |
| map-putex | r ∈ H ⊦ (r => o0 * P)(H[r, o1]) ↔ ¬ ¬ (o0 = o1 ∧ (r =>_ * P)(H)) | A User Theorem |
| map-putex-simp | r ∈ H ⊦ ¬ (r => o0 * P)(H[r, o1]) ↔ ¬ (o0 = o1 ∧ (r =>_ * P)(H)) | A User Theorem |
| map-same | ⊦ r => o0 * r => o1 = false | A User Theorem |
| map-write | r ∈ H ⊦ (r => o0 * P)(H[r, o1]) → o0 = o1 | A User Theorem |
| mapex-and | ⊦ (r =>_ ∧ r => o) = r => o | A User Theorem |
| mapex-del | ⊦ (r =>_ * P)(H) → P(H -- r) | A User Theorem |
| mapex-elim | ⊦ (r => o * P)(H) → (r =>_ * P)(H) | A User Theorem |
| mapex-in | ⊦ (r =>_ * P)(H) → r ∈ H | A User Theorem |
| mapex-new | ¬ r ∈ H, r ≠ null ⊦ P(H) ↔ (r =>_ * P)(H ++ r) | A User Theorem |
| mapex-new-rw | ¬ r ∈ H, r ≠ null ⊦ ¬ (r =>_ * P)(H ++ r) ↔ ¬ P(H) | A User Theorem |
| mapex-null | ⊦ null =>_ = ⌜false⌝ | A User Theorem |
| mapex-put | r ∈ H ⊦ (r =>_ * P)(H[r, o]) ↔ (r => o * P)(H[r, o]) | A User Theorem |
| mapex-put-rw | r ∈ H ⊦ (r =>_ * P)(H) → (¬ (r => o0 * P)(H[r, o1]) ↔ o0 ≠ o1) | A User Theorem |
| mapornull-emp | ⊦ null =>? = emp | A User Theorem |
| mapornull-ex | ⊦ r ≠ null → r =>? = r =>_ | A User Theorem |
| precise-map | ⊦ precise(r => o) | A User Theorem |
| precise-mapex | ⊦ precise(r =>_) | A User Theorem |
| precise-mapornull | ⊦ precise(r =>?) | A User Theorem |