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: |
|---|---|---|
| Extension | ⊦ stng1 = stng2 ↔ (∀ a. stng1[a] = stng2[a]) | An Axiom |
| At-same | ⊦ stng[a, d][a] = d | An Axiom |
| At-other | ⊦ a ≠ b → stng[b, d][a] = stng[a] | An Axiom |
| In-store | ⊦ a × d ∈ stng ↔ stng[a] = d | An Axiom |
| Subset | ⊦ stng1 ⊆ stng2 ↔ (∀ a. stng1[a] = stng2[a]) | An Axiom |
| ax | ⊦ a × d = a0 × d0 ↔ a = a0 ∧ d = d0 | An Axiom |
| gen | An Axiom | |
| ins | ⊦ stng[a] = d → stng[a, d] = stng | A User Theorem |
| ins-same | ⊦ stng[a, stng[a]] = stng | A User Theorem |
| ins-two | ⊦ a ≠ b → (stng[b, d0][a, d] ≠ stng[a, d][b, d0] ↔ false) | A User Theorem |
| ins-twosame | ⊦ a ≠ b → stng[b, d][a, stng[a]] = stng[b, d] | A User Theorem |
| ins3 | ⊦ stng[a, d1][b, d0][a, d] = stng[b, d0][a, d] | A User Theorem |
| insins | ⊦ stng[a, d0][a, d] = stng[a, d] | A User Theorem |
| neq | ⊦ stng ≠ stng0 ↔ (∃ a. stng[a] ≠ stng0[a]) | A User Theorem |
| rew | ⊦ a ≠ b → stng[b, d0][a, d] = stng[a, d][b, d0] | A User Theorem |
| sub-ref | ⊦ stng ⊆ stng | A User Theorem |
| sub-trans | ⊦ stng ⊆ stng0 ∧ stng0 ⊆ stng1 → stng ⊆ stng1 | A User Theorem |