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: |
|---|---|---|
| disj-01 | ⊦ inodekey(m) ≠ datakey(m0, m1) | An Axiom |
| disj-02 | ⊦ inodekey(m) ≠ dentrykey(m0, str) | An Axiom |
| disj-03 | ⊦ datakey(m, m0) ≠ dentrykey(m1, str) | An Axiom |
| sel-01 | ⊦ dentrykey(m, str).name = str | An Axiom |
| sel-02 | ⊦ dentrykey(m, str).ino = m | An Axiom |
| sel-03 | ⊦ datakey(m, m0).ino = m | An Axiom |
| sel-04 | ⊦ inodekey(m).ino = m | An Axiom |
| sel-05 | ⊦ datakey(m, m0).part = m0 | An Axiom |
| upd-01 | ⊦ dentrykey(m, str).name:= str0 = dentrykey(m, str0) | An Axiom |
| upd-02 | ⊦ inodekey(m).ino:= m0 = inodekey(m0) | An Axiom |
| upd-03 | ⊦ datakey(m, m0).part:= m2 = datakey(m, m2) | An Axiom |
| upd-04 | ⊦ dentrykey(m, str).ino:= m0 = dentrykey(m0, str) | An Axiom |
| upd-05 | ⊦ datakey(m, m0).ino:= m1 = datakey(m1, m0) | An Axiom |
| inj-01 | ⊦ dentrykey(m, str) = dentrykey(m0, str0) ↔ m = m0 ∧ str = str0 | An Axiom |
| inj-02 | ⊦ datakey(m, m0) = datakey(m1, m2) ↔ m = m1 ∧ m0 = m2 | An Axiom |
| inj-03 | ⊦ inodekey(m) = inodekey(m0) ↔ m = m0 | An Axiom |
| case | ⊦ key = inodekey(key.ino) ∨ key = datakey(key.ino, key.part) ∨ key = dentrykey(key.ino, key.name) | An Axiom |
| gen | An Axiom | |
| elim-01 | ⊦ key.inode? → (m = key.ino ↔ key = inodekey(m)) | An Axiom |
| elim-02 | ⊦ key.data? → (m = key.ino ∧ m0 = key.part ↔ key = datakey(m, m0)) | An Axiom |
| elim-03 | ⊦ key.dentry? → (m = key.ino ∧ str = key.name ↔ key = dentrykey(m, str)) | An Axiom |
| ex-01 | ⊦ key.dentry? ↔ (∃ m, str. key = dentrykey(m, str)) | An Axiom |
| ex-02 | ⊦ key.inode? ↔ (∃ m. key = inodekey(m)) | An Axiom |
| ex-03 | ⊦ key.data? ↔ (∃ m, m0. key = datakey(m, m0)) | An Axiom |
| test-01 | ⊦ dentrykey(m, str).dentry? | An Axiom |
| test-02 | ⊦ inodekey(m).inode? | An Axiom |
| test-03 | ⊦ ¬ datakey(m, m0).dentry? | An Axiom |
| test-04 | ⊦ ¬ datakey(m, m0).inode? | An Axiom |
| test-05 | ⊦ ¬ inodekey(m).dentry? | An Axiom |
| test-06 | ⊦ ¬ dentrykey(m, str).inode? | An Axiom |
| test-07 | ⊦ ¬ dentrykey(m, str).data? | An Axiom |
| test-08 | ⊦ ¬ inodekey(m).data? | An Axiom |
| test-09 | ⊦ datakey(m, m0).data? | An Axiom |
| updsel-01 | ⊦ (key.ino:= m).ino = m | An Axiom |
| updsel-02 | ⊦ key.data? → (key.part:= m0).part = m0 | An Axiom |
| updsel-03 | ⊦ key.dentry? → (key.name:= str).name = str | An Axiom |
| disjpred-01 | ⊦ key.inode? → ¬ key.dentry? | A User Theorem |
| disjpred-02 | ⊦ key.inode? → ¬ key.data? | A User Theorem |
| disjpred-03 | ⊦ key.dentry? → ¬ key.inode? | A User Theorem |
| disjpred-04 | ⊦ key.dentry? → ¬ key.data? | A User Theorem |
| disjpred-05 | ⊦ key.data? → ¬ key.inode? | A User Theorem |
| disjpred-06 | ⊦ key.data? → ¬ key.dentry? | A User Theorem |
| inodekey-id | ⊦ key.inode? → inodekey(key.ino) = key | A User Theorem |