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: |
|---|---|---|
| free-known | (r => o * P)(H) ⊦ ⟪free(r; H)⟫ P(H) | A Proof Obligation |
| free-unknown | (r =>_ * P)(H) ⊦ ⟪free(r; H)⟫ P(H) | A Proof Obligation |
| alloc | P(H) ⊦ ⟪alloc(; r, H)⟫ (r =>_ * P)(H) | A Proof Obligation |
| write-unknown | (r =>_ * P)(H) ⊦ ⟪write(r, o; H)⟫ (r => o * P)(H) | A Proof Obligation |
| write-known | (r => o0 * P)(H) ⊦ ⟪write(r, o1; H)⟫ (r => o1 * P)(H) | A Proof Obligation |
| read-unknown | (r =>_ * P)(H) ⊦ ⟪read(r, H; o)⟫ true | A Proof Obligation |
| read-known | (r => o0 * P)(H) ⊦ ⟪read(r, H; o1)⟫ o0 = o1 | A Proof Obligation |