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: |
|---|---|---|
| inj | ⊦ mkinode(m, md, boolvar, m0, m1, m2) = mkinode(m3, md0, boolvar0, m4, m5, m6) ↔ m = m3 ∧ md = md0 ∧ (boolvar ↔ boolvar0) ∧ m0 = m4 ∧ m1 = m5 ∧ m2 = m6 | An Axiom |
| case | ⊦ mkinode(inode.ino, inode.meta, inode.directory, inode.nlink, inode.nsubdirs, inode.size) = inode | An Axiom |
| elim | ⊦ ((((m = inode.ino ∧ md = inode.meta) ∧ (boolvar ↔ inode.directory)) ∧ m0 = inode.nlink) ∧ m1 = inode.nsubdirs) ∧ m2 = inode.size ↔ inode = mkinode(m, md, boolvar, m0, m1, m2) | An Axiom |
| gen | inode freely generated by mkinode; | An Axiom |
| updsel-01 | ⊦ (inode.ino:= m).ino = m | An Axiom |
| updsel-02 | ⊦ (inode.meta:= md).ino = inode.ino | An Axiom |
| updsel-03 | ⊦ (inode.directory:= boolvar).ino = inode.ino | An Axiom |
| updsel-04 | ⊦ (inode.nlink:= m0).ino = inode.ino | An Axiom |
| updsel-06 | ⊦ (inode.ino:= m).meta = inode.meta | An Axiom |
| updsel-07 | ⊦ (inode.meta:= md).meta = md | An Axiom |
| updsel-08 | ⊦ (inode.directory:= boolvar).meta = inode.meta | An Axiom |
| updsel-09 | ⊦ (inode.nlink:= m0).meta = inode.meta | An Axiom |
| updsel-11 | ⊦ (inode.ino:= m).directory ↔ inode.directory | An Axiom |
| updsel-12 | ⊦ (inode.meta:= md).directory ↔ inode.directory | An Axiom |
| updsel-13 | ⊦ (inode.directory:= boolvar).directory ↔ boolvar | An Axiom |
| updsel-14 | ⊦ (inode.nlink:= m0).directory ↔ inode.directory | An Axiom |
| updsel-16 | ⊦ (inode.ino:= m).nlink = inode.nlink | An Axiom |
| updsel-17 | ⊦ (inode.meta:= md).nlink = inode.nlink | An Axiom |
| updsel-18 | ⊦ (inode.directory:= boolvar).nlink = inode.nlink | An Axiom |
| updsel-19 | ⊦ (inode.nlink:= m0).nlink = m0 | An Axiom |
| updsel-21 | ⊦ (inode.ino:= m).size = inode.size | An Axiom |
| updsel-22 | ⊦ (inode.meta:= md).size = inode.size | An Axiom |
| updsel-23 | ⊦ (inode.directory:= boolvar).size = inode.size | An Axiom |
| updsel-24 | ⊦ (inode.nlink:= m0).size = inode.size | An Axiom |
| updsel-26 | ⊦ (inode.nsubdirs:= m1).ino = inode.ino | An Axiom |
| updsel-27 | ⊦ (inode.size:= m2).ino = inode.ino | An Axiom |
| updsel-28 | ⊦ (inode.nsubdirs:= m1).meta = inode.meta | An Axiom |
| updsel-29 | ⊦ (inode.size:= m2).meta = inode.meta | An Axiom |
| updsel-30 | ⊦ (inode.nsubdirs:= m1).directory ↔ inode.directory | An Axiom |
| updsel-31 | ⊦ (inode.size:= m2).directory ↔ inode.directory | An Axiom |
| updsel-32 | ⊦ (inode.nsubdirs:= m1).nlink = inode.nlink | An Axiom |
| updsel-33 | ⊦ (inode.size:= m2).nlink = inode.nlink | An Axiom |
| updsel-34 | ⊦ (inode.ino:= m).nsubdirs = inode.nsubdirs | An Axiom |
| updsel-35 | ⊦ (inode.size:= m2).nsubdirs = inode.nsubdirs | An Axiom |
| updsel-36 | ⊦ (inode.meta:= md).nsubdirs = inode.nsubdirs | An Axiom |
| updsel-37 | ⊦ (inode.nsubdirs:= m1).nsubdirs = m1 | An Axiom |
| updsel-38 | ⊦ (inode.directory:= boolvar).nsubdirs = inode.nsubdirs | An Axiom |
| updsel-39 | ⊦ (inode.nlink:= m0).nsubdirs = inode.nsubdirs | An Axiom |
| updsel-40 | ⊦ (inode.nsubdirs:= m1).size = inode.size | An Axiom |
| updsel-41 | ⊦ (inode.size:= m2).size = m2 | An Axiom |
| upd-01 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino:= m3 = mkinode(m3, md, boolvar, m0, m1, m2) | An Axiom |
| upd-02 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta:= md0 = mkinode(m, md0, boolvar, m0, m1, m2) | An Axiom |
| upd-03 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory:= boolvar0 = mkinode(m, md, boolvar0, m0, m1, m2) | An Axiom |
| upd-04 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).nlink:= m4 = mkinode(m, md, boolvar, m4, m1, m2) | An Axiom |
| upd-10 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs:= m5 = mkinode(m, md, boolvar, m0, m5, m2) | An Axiom |
| upd-11 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).size:= m6 = mkinode(m, md, boolvar, m0, m1, m6) | An Axiom |
| sel-01 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m | An Axiom |
| sel-02 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md | An Axiom |
| sel-03 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar | An Axiom |
| sel-04 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).nlink = m0 | An Axiom |
| sel-10 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs = m1 | An Axiom |
| sel-11 | ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2 | An Axiom |