This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| sel-03 | ⊦ datanode(key, buf).data = buf | An Axiom |
| upd-02 | ⊦ datanode(key, buf).data:= buf0 = datanode(key, buf0) | An Axiom |
| upd-04 | ⊦ datanode(key, buf).key:= key0 = datanode(key0, buf) | An Axiom |
| test-12 | ⊦ ¬ datanode(key, buf).inode? | An Axiom |
| inj-02 | ⊦ datanode(key, buf) = datanode(key0, buf0) ↔ key = key0 ∧ buf = buf0 | An Axiom |
| case | ⊦ nd = inodenode(nd.key, nd.meta, nd.directory, nd.nlink, nd.nsubdirs, nd.size) ∨ nd = dentrynode(nd.key, nd.ino) ∨ nd = datanode(nd.key, nd.data) ∨ nd = truncnode(nd.key, nd.size) | An Axiom |
| gen | node freely generated by inodenode, dentrynode, datanode, truncnode; | An Axiom |
| elim-05 | ⊦ nd.data? → (key = nd.key ∧ buf = nd.data ↔ nd = datanode(key, buf)) | An Axiom |
| ex-05 | ⊦ nd.data? ↔ (∃ key, buf. nd = datanode(key, buf)) | An Axiom |
| test-19 | ⊦ ¬ datanode(key, buf).trunc? | An Axiom |
| test-22 | ⊦ datanode(key, buf).data? | An Axiom |
| sel-09 | ⊦ datanode(key, buf).key = key | An Axiom |
| updsel-01 | ⊦ (nd.key:= key).key = key | An Axiom |
| updsel-05 | ⊦ nd.data? → (nd.data:= buf).data = buf | An Axiom |
| updsel-06 | ⊦ nd.inode? → (nd.meta:= md).nlink = nd.nlink | An Axiom |
| updsel-07 | ⊦ nd.dentry? → (nd.ino:= m).ino = m | An Axiom |
| updsel-08 | ⊦ nd.inode? → (nd.meta:= md).size = nd.size | An Axiom |
| updsel-10 | ⊦ nd.inode? → (nd.directory:= boolvar).meta = nd.meta | An Axiom |
| updsel-16 | ⊦ nd.inode? → (nd.directory:= boolvar).nlink = nd.nlink | An Axiom |
| updsel-18 | ⊦ nd.inode? → (nd.directory:= boolvar).size = nd.size | An Axiom |
| updsel-20 | ⊦ nd.inode? → (nd.nlink:= m).meta = nd.meta | An Axiom |
| updsel-22 | ⊦ nd.inode? → ((nd.nlink:= m).directory ↔ nd.directory) | An Axiom |
| updsel-24 | ⊦ nd.inode? → (nd.nlink:= m).nlink = m | An Axiom |
| updsel-25 | ⊦ nd.inode? → (nd.nlink:= m).size = nd.size | An Axiom |
| updsel-03 | ⊦ nd.trunc? → (nd.size:= m).size = m | An Axiom |
| updsel-04 | ⊦ nd.inode? → ((nd.meta:= md).directory ↔ nd.directory) | An Axiom |
| updsel-12 | ⊦ nd.inode? → ((nd.directory:= boolvar).directory ↔ boolvar) | An Axiom |
| disj-04 | ⊦ datanode(key, buf) ≠ truncnode(key0, m) | An Axiom |
| test-13 | ⊦ ¬ datanode(key, buf).dentry? | An Axiom |
| elim-04 | ⊦ nd.trunc? → (key = nd.key ∧ m = nd.size ↔ nd = truncnode(key, m)) | An Axiom |
| ex-04 | ⊦ nd.trunc? ↔ (∃ key, m. nd = truncnode(key, m)) | An Axiom |
| inj-05 | ⊦ truncnode(key, m) = truncnode(key0, m0) ↔ key = key0 ∧ m = m0 | An Axiom |
| test-15 | ⊦ ¬ truncnode(key, m).inode? | An Axiom |
| test-16 | ⊦ ¬ truncnode(key, m).dentry? | An Axiom |
| test-17 | ⊦ ¬ truncnode(key, m).data? | An Axiom |
| test-18 | ⊦ truncnode(key, m).trunc? | An Axiom |
| updsel-02 | ⊦ nd.inode? → (nd.meta:= md).meta = md | An Axiom |
| upd-03 | ⊦ truncnode(key, m).key:= key0 = truncnode(key0, m) | An Axiom |
| upd-13 | ⊦ truncnode(key, m).size:= m0 = truncnode(key, m0) | An Axiom |
| sel-04 | ⊦ truncnode(key, m).key = key | An Axiom |
| sel-13 | ⊦ truncnode(key, m).size = m | An Axiom |
| elim-02 | ⊦ nd.dentry? → (key = nd.key ∧ m = nd.ino ↔ nd = dentrynode(key, m)) | An Axiom |
| ex-01 | ⊦ nd.dentry? ↔ (∃ key, m. nd = dentrynode(key, m)) | An Axiom |
| inj-01 | ⊦ dentrynode(key, m) = dentrynode(key0, m0) ↔ key = key0 ∧ m = m0 | An Axiom |
| test-01 | ⊦ ¬ dentrynode(key, m).inode? | An Axiom |
| test-02 | ⊦ dentrynode(key, m).dentry? | An Axiom |
| test-03 | ⊦ ¬ dentrynode(key, m).data? | An Axiom |
| test-14 | ⊦ ¬ dentrynode(key, m).trunc? | An Axiom |
| upd-01 | ⊦ dentrynode(key, m).key:= key0 = dentrynode(key0, m) | An Axiom |
| upd-14 | ⊦ dentrynode(key, m).ino:= m0 = dentrynode(key, m0) | An Axiom |
| sel-01 | ⊦ dentrynode(key, m).key = key | An Axiom |
| sel-14 | ⊦ dentrynode(key, m).ino = m | An Axiom |
| disj-01 | ⊦ dentrynode(key, m) ≠ truncnode(key0, m0) | An Axiom |
| disj-02 | ⊦ dentrynode(key, m) ≠ datanode(key0, buf) | An Axiom |
| elim-03 | ⊦ nd.inode? → ( ((((key = nd.key ∧ md = nd.meta) ∧ (boolvar ↔ nd.directory)) ∧ m = nd.nlink) ∧ m0 = nd.nsubdirs) ∧ m1 = nd.size ↔ nd = inodenode(key, md, boolvar, m, m0, m1)) | An Axiom |
| ex-03 | ⊦ nd.inode? ↔ (∃ key, md, boolvar, m, m0, m1. nd = inodenode(key, md, boolvar, m, m0, m1)) | An Axiom |
| inj-04 | ⊦ inodenode(key, md, boolvar, m, m0, m1) = inodenode(key0, md0, boolvar0, m2, m3, m4) ↔ key = key0 ∧ md = md0 ∧ (boolvar ↔ boolvar0) ∧ m = m2 ∧ m0 = m3 ∧ m1 = m4 | An Axiom |
| test-06 | ⊦ inodenode(key, md, boolvar, m, m0, m1).inode? | An Axiom |
| test-08 | ⊦ ¬ inodenode(key, md, boolvar, m, m0, m1).dentry? | An Axiom |
| test-09 | ⊦ ¬ inodenode(key, md, boolvar, m, m0, m1).data? | An Axiom |
| test-11 | ⊦ ¬ inodenode(key, md, boolvar, m, m0, m1).trunc? | An Axiom |
| updsel-09 | ⊦ nd.inode? → (nd.meta:= md).nsubdirs = nd.nsubdirs | An Axiom |
| updsel-11 | ⊦ nd.inode? → (nd.size:= m1).nsubdirs = nd.nsubdirs | An Axiom |
| updsel-13 | ⊦ nd.inode? → (nd.directory:= boolvar).nsubdirs = nd.nsubdirs | An Axiom |
| updsel-14 | ⊦ nd.inode? → (nd.nsubdirs:= m0).meta = nd.meta | An Axiom |
| updsel-15 | ⊦ nd.inode? → ((nd.nsubdirs:= m0).directory ↔ nd.directory) | An Axiom |
| updsel-26 | ⊦ nd.inode? → (nd.nsubdirs:= m0).nlink = nd.nlink | An Axiom |
| updsel-27 | ⊦ nd.inode? → (nd.nsubdirs:= m0).nsubdirs = m0 | An Axiom |
| updsel-28 | ⊦ nd.inode? → (nd.nsubdirs:= m0).size = nd.size | An Axiom |
| updsel-29 | ⊦ nd.inode? → (nd.size:= m1).meta = nd.meta | An Axiom |
| updsel-30 | ⊦ nd.inode? → ((nd.size:= m1).directory ↔ nd.directory) | An Axiom |
| updsel-31 | ⊦ nd.inode? → (nd.size:= m1).nlink = nd.nlink | An Axiom |
| updsel-32 | ⊦ nd.inode? → (nd.nlink:= m).nsubdirs = nd.nsubdirs | An Axiom |
| updsel-33 | ⊦ nd.inode? → (nd.size:= m1).size = m1 | An Axiom |
| upd-05 | ⊦ inodenode(key, md, boolvar, m, m0, m1).key:= key0 = inodenode(key0, md, boolvar, m, m0, m1) | An Axiom |
| upd-06 | ⊦ inodenode(key, md, boolvar, m, m0, m1).meta:= md0 = inodenode(key, md0, boolvar, m, m0, m1) | An Axiom |
| upd-12 | ⊦ inodenode(key, md, boolvar, m, m0, m1).directory:= boolvar0 = inodenode(key, md, boolvar0, m, m0, m1) | An Axiom |
| upd-15 | ⊦ inodenode(key, md, boolvar, m, m0, m1).nlink:= m2 = inodenode(key, md, boolvar, m2, m0, m1) | An Axiom |
| upd-16 | ⊦ inodenode(key, md, boolvar, m, m0, m1).nsubdirs:= m3 = inodenode(key, md, boolvar, m, m3, m1) | An Axiom |
| upd-17 | ⊦ inodenode(key, md, boolvar, m, m0, m1).size:= m4 = inodenode(key, md, boolvar, m, m0, m4) | An Axiom |
| sel-05 | ⊦ inodenode(key, md, boolvar, m, m0, m1).key = key | An Axiom |
| sel-06 | ⊦ inodenode(key, md, boolvar, m, m0, m1).meta = md | An Axiom |
| sel-11 | ⊦ inodenode(key, md, boolvar, m, m0, m1).directory ↔ boolvar | An Axiom |
| sel-15 | ⊦ inodenode(key, md, boolvar, m, m0, m1).nlink = m | An Axiom |
| sel-16 | ⊦ inodenode(key, md, boolvar, m, m0, m1).nsubdirs = m0 | An Axiom |
| sel-17 | ⊦ inodenode(key, md, boolvar, m, m0, m1).size = m1 | An Axiom |
| disj-05 | ⊦ inodenode(key, md, boolvar, m, m0, m1) ≠ truncnode(key0, m2) | An Axiom |
| disj-07 | ⊦ inodenode(key, md, boolvar, m, m0, m1) ≠ datanode(key0, buf) | An Axiom |
| disj-08 | ⊦ inodenode(key, md, boolvar, m, m0, m1) ≠ dentrynode(key0, m2) | An Axiom |