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: |
|---|---|---|
| rely | ⊦ rely(a, rs0, f0, g0, rs1, f1, g1) ↔ (∀ r. (g0(r) = a ∧ r ∈ rs0 ↔ g1(r) = a ∧ r ∈ rs1) ∧ (g0(r) = a ∧ r ∈ rs0 → f0(r) = f1(r))) | An Axiom |
| owns-one | ⊦ owns-one(a, r, rs, g) ↔ r ≠ null ∧ r ∈ rs ∧ g(r) = a ∧ (∀ r0. r0 ∈ rs ∧ r0 ≠ r → g(r0) ≠ a) | An Axiom |
| owns-none | ⊦ owns-none(a, rs, g) ↔ (∀ r. r ∈ rs → g(r) ≠ a) | An Axiom |
| owns-none-one | ⊦ owns-none(a, rs, g) ∧ r ∈ rs ∧ r ≠ null → owns-one(a, r, rs, g(r ; a)) | A User Theorem |
| owns-none-one2 | ⊦ owns-none(a, rs, g) ∧ ¬ r ∈ rs ∧ r ≠ null → owns-one(a, r, rs ++ r, g(r ; a)) | A User Theorem |
| owns-one-map | ⊦ owns-one(a, r, rs, g) → (∀ f. ∃ o. (a[r => o] * true)[rs, f, g]) | A User Theorem |
| owns-one-none | ⊦ a ≠ a0 ∧ owns-one(a, r, rs, g) → owns-none(a, rs, g(r ; a0)) | A User Theorem |
| rely-alloc | ⊦ ¬ r ∈ rs ∧ a0 ≠ a → (¬ rely(a, rs, f, g, rs ++ r, f, g(r ; a0)) ↔ false) | A User Theorem |
| rely-map-write-known | ⊦ (a[r => o] * R)[rs, f, g] ∧ a ≠ a0 → (¬ rely(a0, rs, f, g, rs, f(r ; o0), g) ↔ false) | A User Theorem |
| rely-map-write-unknown | ⊦ (a[r =>_] * R)[rs, f, g] ∧ a ≠ a0 → (¬ rely(a0, rs, f, g, rs, f(r ; o), g) ↔ false) | A User Theorem |
| rely-owned-in-rs | ⊦ rely(a, rs, f, g, rs0, f0, g0) ∧ g(r) = a ∧ r ∈ rs → g0(r) = a ∧ r ∈ rs0 | A User Theorem |
| rely-owned-unchgd | ⊦ rely(a, rs, f, g, rs0, f0, g0) → ((a[P] * true)[rs, f, g] ↔ (a[P] * true)[rs0, f0, g0]) | A User Theorem |
| rely-owns-none | ⊦ rely(a, rs, f, g, rs0, f0, g0) → (owns-none(a, rs, g) ↔ owns-none(a, rs0, g0)) | A User Theorem |
| rely-owns-one | ⊦ rely(a, rs, f, g, rs0, f0, g0) → (owns-one(a, r, rs, g) ↔ owns-one(a, r, rs0, g0)) | A User Theorem |
| rely-refl | ⊦ rely(a, rs, f, g, rs, f, g) | A User Theorem |
| rely-reuse | ⊦ g(r) ≠ a ∧ a0 ≠ a → (¬ rely(a, rs, f, g, rs ++ r, f, g(r ; a0)) ↔ false) | A User Theorem |
| rely-trans | ⊦ rely(a, rs, f, g, rs0, f0, g0) ∧ rely(a, rs0, f0, g0, rs1, f1, g1) → rely(a, rs, f, g, rs1, f1, g1) | A User Theorem |
| rely-transfer-owner | ⊦ g(r) ≠ a ∧ a ≠ a0 → (¬ rely(a, rs, f, g, rs, f, g(r ; a0)) ↔ false) | A User Theorem |