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: |
|---|---|---|
| inj | ⊦ mkdentry(str, m) = mkdentry(str0, m0) ↔ str = str0 ∧ m = m0 | An Axiom |
| case | ⊦ dent = mkdentry(dent.name, dent.ino) ∨ dent = negdentry(dent.name) | An Axiom |
| elim | ⊦ dent.dentry? → (str = dent.name ∧ m = dent.ino ↔ dent = mkdentry(str, m)) | An Axiom |
| gen | An Axiom | |
| inj-01 | ⊦ negdentry(str) = negdentry(str0) ↔ str = str0 | An Axiom |
| test-01 | ⊦ negdentry(str).negdentry? | An Axiom |
| test-02 | ⊦ mkdentry(str, m).dentry? | An Axiom |
| test-03 | ⊦ ¬ mkdentry(str, m).negdentry? | An Axiom |
| test-04 | ⊦ ¬ negdentry(str).dentry? | An Axiom |
| upd-03 | ⊦ mkdentry(str, m).ino:= m0 = mkdentry(str, m0) | An Axiom |
| upd-04 | ⊦ mkdentry(str, m).name:= str0 = mkdentry(str0, m) | An Axiom |
| upd-05 | ⊦ negdentry(str).name:= str0 = negdentry(str0) | An Axiom |
| sel-03 | ⊦ negdentry(str).name = str | An Axiom |
| sel-04 | ⊦ mkdentry(str, m).name = str | An Axiom |
| sel-05 | ⊦ mkdentry(str, m).ino = m | An Axiom |
| disj | ⊦ mkdentry(str, m) ≠ negdentry(str0) | An Axiom |
| elim-02 | ⊦ dent.negdentry? → (str = dent.name ↔ dent = negdentry(str)) | An Axiom |
| ex-03 | ⊦ dent.dentry? ↔ (∃ str, m. dent = mkdentry(str, m)) | An Axiom |
| ex-04 | ⊦ dent.negdentry? ↔ (∃ str. dent = negdentry(str)) | An Axiom |
| updsel-01 | ⊦ (dent.name:= str).name = str | An Axiom |
| updsel-02 | ⊦ dent.dentry? → (dent.ino:= m).ino = m | An Axiom |