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: |
|---|---|---|
| class | ⊦ ⌊err⌋ ↔ err ≠ ESUCCESS ∧ err ≠ EEXISTS ∧ err ≠ ENOENT ∧ err ≠ EISDIR ∧ err ≠ ENOTEMPTY ∧ err ≠ ENOTDIR ∧ err ≠ EBADFD ∧ err ≠ EACCESS | An Axiom |
| fail-or-success | An Axiom | |
| fail | An Axiom | |
| eaccess | ⊦ ¬ ⌊EACCESS⌋ | A User Theorem |
| ebadfd | ⊦ ¬ ⌊EBADFD⌋ | A User Theorem |
| ecommit | ⊦ ⌊ECOMMIT⌋ | A User Theorem |
| eexists | ⊦ ¬ ⌊EEXISTS⌋ | A User Theorem |
| efail | ⊦ ⌊EFAIL⌋ | A User Theorem |
| einval | ⊦ ⌊EINVAL⌋ | A User Theorem |
| eio | ⊦ ⌊EIO⌋ | A User Theorem |
| eisdir | ⊦ ¬ ⌊EISDIR⌋ | A User Theorem |
| enoent | ⊦ ¬ ⌊ENOENT⌋ | A User Theorem |
| enospc | ⊦ ⌊ENOSPC⌋ | A User Theorem |
| enotdir | ⊦ ¬ ⌊ENOTDIR⌋ | A User Theorem |
| enotempty | ⊦ ¬ ⌊ENOTEMPTY⌋ | A User Theorem |
| esuccess | ⊦ ¬ ⌊ESUCCESS⌋ | A User Theorem |
| fail-or-success-prepost | ⊦ ⟪fail_or_success#(; err)⟫ (⌊err⌋ ∨ err = ESUCCESS) | A User Theorem |
| fail-prepost | ⊦ ⟪fail#(; err)⟫ ⌊err⌋ | A User Theorem |
| not-esuccess | ⊦ ⌊err⌋ → err ≠ ESUCCESS | A User Theorem |