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: |
|---|---|---|
| updsel-01 | ⊦ (ad.meta:= md).meta = md | An Axiom |
| inj | ⊦ mkdir(m, md, m0, m1, entries) = mkdir(m2, md0, m3, m4, entries0) ↔ m = m2 ∧ md = md0 ∧ m0 = m3 ∧ m1 = m4 ∧ entries = entries0 | An Axiom |
| case | ⊦ mkdir(ad.size, ad.meta, ad.nlink, ad.nsubdirs, ad.entries) = ad | An Axiom |
| elim | ⊦ (((m = ad.size ∧ md = ad.meta) ∧ m0 = ad.nlink) ∧ m1 = ad.nsubdirs) ∧ entries = ad.entries ↔ ad = mkdir(m, md, m0, m1, entries) | An Axiom |
| gen | abstract-dir freely generated by mkdir; | An Axiom |
| updsel-06 | ⊦ (ad.entries:= entries).meta = ad.meta | An Axiom |
| updsel-07 | ⊦ (ad.size:= m).nlink = ad.nlink | An Axiom |
| updsel-09 | ⊦ (ad.entries:= entries).entries = entries | An Axiom |
| updsel-10 | ⊦ (ad.entries:= entries).nlink = ad.nlink | An Axiom |
| updsel-12 | ⊦ (ad.meta:= md).entries = ad.entries | An Axiom |
| updsel-02 | ⊦ (ad.size:= m).size = m | An Axiom |
| updsel-03 | ⊦ (ad.meta:= md).size = ad.size | An Axiom |
| updsel-04 | ⊦ (ad.nlink:= m0).size = ad.size | An Axiom |
| updsel-13 | ⊦ (ad.entries:= entries).size = ad.size | An Axiom |
| updsel-14 | ⊦ (ad.size:= m).meta = ad.meta | An Axiom |
| updsel-15 | ⊦ (ad.nlink:= m0).meta = ad.meta | An Axiom |
| updsel-16 | ⊦ (ad.nsubdirs:= m1).nlink = ad.nlink | An Axiom |
| updsel-17 | ⊦ (ad.nlink:= m0).nlink = m0 | An Axiom |
| updsel-18 | ⊦ (ad.size:= m).entries = ad.entries | An Axiom |
| updsel-19 | ⊦ (ad.nlink:= m0).entries = ad.entries | An Axiom |
| updsel-05 | ⊦ (ad.nsubdirs:= m1).size = ad.size | An Axiom |
| updsel-08 | ⊦ (ad.nsubdirs:= m1).meta = ad.meta | An Axiom |
| updsel-11 | ⊦ (ad.meta:= md).nlink = ad.nlink | An Axiom |
| updsel-20 | ⊦ (ad.size:= m).nsubdirs = ad.nsubdirs | An Axiom |
| updsel-21 | ⊦ (ad.meta:= md).nsubdirs = ad.nsubdirs | An Axiom |
| updsel-22 | ⊦ (ad.nlink:= m0).nsubdirs = ad.nsubdirs | An Axiom |
| updsel-23 | ⊦ (ad.nsubdirs:= m1).nsubdirs = m1 | An Axiom |
| updsel-24 | ⊦ (ad.entries:= entries).nsubdirs = ad.nsubdirs | An Axiom |
| updsel-25 | ⊦ (ad.nsubdirs:= m1).entries = ad.entries | An Axiom |
| upd-03 | ⊦ mkdir(m, md, m0, m1, entries).size:= m2 = mkdir(m2, md, m0, m1, entries) | An Axiom |
| upd-04 | ⊦ mkdir(m, md, m0, m1, entries).meta:= md0 = mkdir(m, md0, m0, m1, entries) | An Axiom |
| upd-05 | ⊦ mkdir(m, md, m0, m1, entries).nlink:= m3 = mkdir(m, md, m3, m1, entries) | An Axiom |
| upd-08 | ⊦ mkdir(m, md, m0, m1, entries).nsubdirs:= m4 = mkdir(m, md, m0, m4, entries) | An Axiom |
| upd-09 | ⊦ mkdir(m, md, m0, m1, entries).entries:= entries0 = mkdir(m, md, m0, m1, entries0) | An Axiom |
| sel-03 | ⊦ mkdir(m, md, m0, m1, entries).size = m | An Axiom |
| sel-04 | ⊦ mkdir(m, md, m0, m1, entries).meta = md | An Axiom |
| sel-05 | ⊦ mkdir(m, md, m0, m1, entries).nlink = m0 | An Axiom |
| sel-08 | ⊦ mkdir(m, md, m0, m1, entries).nsubdirs = m1 | An Axiom |
| sel-09 | ⊦ mkdir(m, md, m0, m1, entries).entries = entries | An Axiom |