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: |
|---|---|---|
| at-mk | ⊦ r ∈ rs → (mk(rs, f)[r]) = f(r) | An Axiom |
| in-mk | ⊦ r ∈ mk(rs, f) ↔ r ∈ rs | An Axiom |
| apply | ⊦ P[rs, f] ↔ P(mk(rs, f)) | An Axiom |
| at-rw | ⊦ (r => o * P)[rs, f] → (f(r) ≠ o ↔ false) | A User Theorem |
| at-rw0 | ⊦ (r => o)[rs, f] → (f(r) ≠ o ↔ false) | A User Theorem |
| at-unil | ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f0) ∪ mk(rs1, f1))[r] = f0(r) | A User Theorem |
| at-unir | ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f0) ∪ mk(rs1, f1))[r] = f1(r) | A User Theorem |
| del | ⊦ mk(rs -- r, f) = mk(rs, f) -- r | A User Theorem |
| disj | ⊦ mk(rs0, f0) ⊥ mk(rs1, f1) ↔ rs0 ∩ rs1 = ∅ | A User Theorem |
| emp | ⊦ mk(∅, f) = ∅ | A User Theorem |
| ex1-shift | ⊦ (_∃ rP * P)[rs, f] ↔ (∃ r. (rP(r) * P)[rs, f]) | A User Theorem |
| ex2-shift | ⊦ (_∃ rrP * P)[rs, f] ↔ (∃ r0, r1. (rrP(r0, r1) * P)[rs, f]) | A User Theorem |
| ex3-shift | ⊦ (_∃ oP * P)[rs, f] ↔ (∃ o. (oP(o) * P)[rs, f]) | A User Theorem |
| in-uni | ⊦ rs0 ∩ rs1 = ∅ → (r ∈ mk(rs0, f0) ∪ mk(rs1, f1) ↔ ¬ ¬ (r ∈ rs0 ∨ r ∈ rs1)) | A User Theorem |
| map-del | ⊦ (r => o * P)[rs, f] ↔ P[rs -- r, f] ∧ r ∈ rs ∧ f(r) = o | A User Theorem |
| map-in | ⊦ (r => o * P)[rs, f] → r ∈ rs | A User Theorem |
| map-in0 | ⊦ (r => o)[rs, f] → r ∈ rs | A User Theorem |
| map-put | ⊦ (r =>_ * P)[rs, f] ↔ (r => o1 * P)[rs, f(r ; o1)] ∧ r ∈ rs | A User Theorem |
| map-putrev | r ∈ rs ⊦ (r => o0 * P)[rs, f(r ; o1)] ↔ ¬ ¬ (o0 = o1 ∧ (r =>_ * P)[rs, f]) | A User Theorem |
| mapex-del | ⊦ (r =>_ * P)[rs, f] → P[rs -- r, f] | A User Theorem |
| mapex-elim | ⊦ (r => o * P)[rs, f] → (r =>_ * P)[rs, f] | A User Theorem |
| mapex-in | ⊦ (r =>_ * P)[rs, f] → r ∈ rs | A User Theorem |
| mapex-in0 | ⊦ (r =>_)[rs, f] → r ∈ rs | A User Theorem |
| mapex-new | ¬ r ∈ rs, r ≠ null ⊦ P[rs, f] ↔ (r =>_ * P)[rs ++ r, f] | A User Theorem |
| mapex-put | r ∈ rs ⊦ (r =>_ * P)[rs, f(r ; o)] ↔ (r => o * P)[rs, f(r ; o)] | A User Theorem |
| mk-exists | ⊦ ∃ rs, f. H = mk(rs, f) | A User Theorem |
| mk-ext | ⊦ P0 = P1 ↔ (∀ rs, f. P0[rs, f] ↔ P1[rs, f]) | A User Theorem |
| prop | ⊦ ⌜bv⌝ [rs, f] ↔ bv | A User Theorem |
| prop-emp | ⊦ ((⌜bv⌝ ∧ emp) * P)[rs, f] ↔ ¬ ¬ (bv ∧ P[rs, f]) | A User Theorem |
| prop-false | ⊦ ¬ false[rs, f] | A User Theorem |
| prop-sep | ⊦ ((⌜bv⌝ ∧ P0) * P1)[rs, f] ↔ bv ∧ (P0 * P1)[rs, f] | A User Theorem |
| prop-true | ⊦ true[rs, f] | A User Theorem |
| sep | ⊦ (P0 * P1)[rs, f] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ P0[rs0, f] ∧ P1[rs1, f]) | A User Theorem |
| split-uni | ⊦ P0[rs0, f] ∧ P1[rs1, f] ∧ rs0 ∩ rs1 = ∅ → (¬ (P0 * P1)[rs0 ∪ rs1, f] ↔ false) | A User Theorem |
| true-elim | ⊦ (P0 * P)[rs, f] → (true * P)[rs, f] | A User Theorem |
| true-emp | ⊦ P[rs, f] → (true * P)[rs, f] | A User Theorem |
| uni | ⊦ rs0 ∩ rs1 = ∅ → mk(rs0 ∪ rs1, f) = mk(rs0, f) ∪ mk(rs1, f) | A User Theorem |
| write | ⊦ r ∈ rs → mk(rs, f(r ; o)) = (mk(rs, f)[r, o]) | A User Theorem |