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 | ⊦ mkinode(m, md, boolvar, m0, m1) = mkinode(m2, md0, boolvar0, m3, m4) ↔ m = m2 ∧ md = md0 ∧ (boolvar ↔ boolvar0) ∧ m0 = m3 ∧ m1 = m4 | An Axiom |
| case | ⊦ mkinode(inode.ino, inode.meta, inode.directory, inode.nlink, inode.size) = inode | An Axiom |
| elim | ⊦ (((m = inode.ino ∧ md = inode.meta) ∧ (boolvar ↔ inode.directory)) ∧ m0 = inode.nlink) ∧ m1 = inode.size ↔ inode = mkinode(m, md, boolvar, m0, m1) | An Axiom |
| gen | 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-05 | ⊦ (inode.size:= m1).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-10 | ⊦ (inode.size:= m1).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-15 | ⊦ (inode.size:= m1).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-20 | ⊦ (inode.size:= m1).nlink = inode.nlink | 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-25 | ⊦ (inode.size:= m1).size = m1 | An Axiom |
| upd-05 | ⊦ mkinode(m, md, boolvar, m0, m1).ino:= m2 = mkinode(m2, md, boolvar, m0, m1) | An Axiom |
| upd-06 | ⊦ mkinode(m, md, boolvar, m0, m1).meta:= md0 = mkinode(m, md0, boolvar, m0, m1) | An Axiom |
| upd-07 | ⊦ mkinode(m, md, boolvar, m0, m1).directory:= boolvar0 = mkinode(m, md, boolvar0, m0, m1) | An Axiom |
| upd-08 | ⊦ mkinode(m, md, boolvar, m0, m1).nlink:= m3 = mkinode(m, md, boolvar, m3, m1) | An Axiom |
| upd-09 | ⊦ mkinode(m, md, boolvar, m0, m1).size:= m4 = mkinode(m, md, boolvar, m0, m4) | An Axiom |
| sel-05 | ⊦ mkinode(m, md, boolvar, m0, m1).ino = m | An Axiom |
| sel-06 | ⊦ mkinode(m, md, boolvar, m0, m1).meta = md | An Axiom |
| sel-07 | ⊦ mkinode(m, md, boolvar, m0, m1).directory ↔ boolvar | An Axiom |
| sel-08 | ⊦ mkinode(m, md, boolvar, m0, m1).nlink = m0 | An Axiom |
| sel-09 | ⊦ mkinode(m, md, boolvar, m0, m1).size = m1 | An Axiom |