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: |
|---|---|---|
| lift-aux | ⊦ (a[P])(mk(rs, f, g)) ↔ P(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a) | An Axiom |
| alloc | ⊦ r ≠ null ∧ ¬ r ∈ rs → (R[rs, f, g] ↔ (a[r =>_] * R)[rs ++ r, f, g(r ; a)]) | A User Theorem |
| and-split | ⊦ (R ∧ R0)[rs, f, g] ↔ R[rs, f, g] ∧ R0[rs, f, g] | A User Theorem |
| aux-known | ⊦ (a0[r => o] * R)[rs, f, g] ↔ (a1[r => o] * R)[rs, f, g(r ; a1)] ∧ g(r) = a0 | A User Theorem |
| aux-unknown | ⊦ (a0[r =>_] * R)[rs, f, g] ↔ (a1[r =>_] * R)[rs, f, g(r ; a1)] ∧ g(r) = a0 | A User Theorem |
| embed-and | ⊦ a[P0 ∧ P1] = (a[P0] ∧ a[P1]) | A User Theorem |
| embed-split | ⊦ a[P0 * P1] = a[P0] * a[P1] | A User Theorem |
| get-known | ⊦ (a[r => o] * R)[rs, f, g] → (g(r) ≠ a ↔ false) | A User Theorem |
| get-unknown | ⊦ (a[r =>_] * R)[rs, f, g] → (g(r) ≠ a ↔ false) | A User Theorem |
| lift-emp | ⊦ a[emp] = emp | A User Theorem |
| lift-ex-o | ⊦ a[_∃ oP] = _∃ λ o, a0. a[oP(o)] | A User Theorem |
| lift-ex-r | ⊦ a[_∃ rP] = _∃ λ r. a[rP(r)] | A User Theorem |
| lift-false | ⊦ a[false] = false | A User Theorem |
| lift-prop | ⊦ (a[⌜bv⌝ ] ∧ emp) = (⌜bv⌝ ∧ emp) | A User Theorem |
| lift-true | ⊦ a[true][rs, f, g] ↔ (∀ r. r ∈ rs → g(r) = a) | A User Theorem |
| lift-unknown | ⊦ (r ==>_ * R)[rs, f, g] ↔ (∃ a. (a[r =>_] * R)[rs, f, g]) | A User Theorem |
| map-in | ⊦ (a[r => o] * R)[rs, f, g] → r ∈ rs | A User Theorem |
| map-in0 | ⊦ a[r => o][rs, f, g] → r ∈ rs | A User Theorem |
| map-owner-known | ⊦ (a[r => o] * R)[rs, f, g] ∧ a ≠ a0 → (g(r) = a0 ↔ false) | A User Theorem |
| map-owner-unknown | ⊦ (a[r =>_] * R)[rs, f, g] ∧ a ≠ a0 → (g(r) = a0 ↔ false) | A User Theorem |
| map-same | ⊦ ¬ (a[r => o] * a0[r => o0] * R)[rs, f, g] | A User Theorem |
| map-unique | ⊦ f(r) = o ∧ (a[r => o0] * R)[rs, f, g] → o = o0 | A User Theorem |
| map2 | ⊦ (a[r => o] * R)[rs, f, g] ∧ (a[r => o0] * R0)[rs, f, g] → o = o0 | A User Theorem |
| merge-owned | ⊦ (a[P] * R)[rs, f, g] ∧ (a0[P0] * R0)[rs, f, g] ∧ a0 ≠ a → (a[P] * a0[P0] * true)[rs, f, g] | A User Theorem |
| merge-owned-rewrite | ⊦ (a[P] * true)[rs, f, g] ∧ a0 ≠ a → ((a0[P0] * true)[rs, f, g] ↔ (a[P] * a0[P0] * true)[rs, f, g]) | A User Theorem |
| mod-f-known | a ≠ a0 ⊦ (a[r => o] * R)[rs, f, g] → (g(r) = a0 ↔ false) | A User Theorem |
| mod-other-aux | ⊦ g(r) ≠ a ∧ (a[P] * R)[rs, f, g] → (¬ (a[P] * true)[rs, f, g(r ; a0)] ↔ false) | A User Theorem |
| mod-other-aux1 | ⊦ g(r) ≠ a ∧ (a[P] * R)[rs, f, g] → ((a[P] * true)[rs, f, g(r ; a0)] ↔ (a[P] * R)[rs, f, g]) | A User Theorem |
| mod-other-both | ⊦ g(r) ≠ a ∧ (a[P] * R)[rs, f, g] → (¬ (a[P] * true)[rs, f(r ; o), g(r ; a0)] ↔ false) | A User Theorem |
| mod-other-hp | ⊦ g(r) ≠ a ∧ (a[P] * R)[rs, f, g] → (¬ (a[P] * true)[rs, f(r ; o), g] ↔ false) | A User Theorem |
| mod-other-hp2 | ⊦ g(r) ≠ a ∧ g(r) ≠ a0 ∧ (a[P] * a0[P0] * R)[rs, f, g] → (¬ (a[P] * a0[P0] * true)[rs, f(r ; o), g] ↔ false) | A User Theorem |
| split-owned2 | ⊦ (a[P] * a0[P0] * a1[P1] * R)[rs, f, g] ∧ a ≠ a0 ∧ a ≠ a1 ∧ a0 ≠ a1 → (a[P] * true)[rs, f, g] ∧ (a0[P0] * a1[P1] * true)[rs, f, g] | A User Theorem |
| switch-aux | ⊦ ¬ r ∈ rs → (R[rs, f, g(r ; a)] ↔ R[rs, f, g]) | A User Theorem |
| switch-obj | ⊦ ¬ r ∈ rs → (R[rs, f(r ; o), g] ↔ R[rs, f, g]) | A User Theorem |
| write-known | ⊦ (a[r => o0] * R)[rs, f, g] ↔ (a[r => o1] * R)[rs, f(r ; o1), g] ∧ f(r) = o0 | A User Theorem |
| write-other-true | ⊦ g(r) ≠ a → ((a[P] * true)[rs, f(r ; o), g] ↔ (a[P] * true)[rs, f, g]) | A User Theorem |
| write-unknown | ⊦ (a[r =>_] * R)[rs, f, g] ↔ (a[r => o1] * R)[rs, f(r ; o1), g] | A User Theorem |