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: |
|---|---|---|
| gen | error freely generated by ESUCCESS, EFAIL, ENOMEM, ENOSPC, EIO, EEXISTS, ENOENT, EISDIR, ENOTDIR, ENOTEMPTY, EBADFD, EACCESS, EINVAL, ECOMMIT, EROFS, EUCLEAN ; | An Axiom |
| case | ⊦ err = ESUCCESS ∨ err = EFAIL ∨ err = ENOMEM ∨ err = ENOSPC ∨ err = EIO ∨ err = EEXISTS ∨ err = ENOENT ∨ err = EISDIR ∨ err = ENOTDIR ∨ err = ENOTEMPTY ∨ err = EBADFD ∨ err = EACCESS ∨ err = EINVAL ∨ err = ECOMMIT ∨ err = EROFS ∨ err = EUCLEAN | An Axiom |
| disj-01 | ⊦ EBADFD ≠ EACCESS | An Axiom |
| disj-02 | ⊦ ENOTDIR ≠ EACCESS | An Axiom |
| disj-03 | ⊦ ENOTDIR ≠ EBADFD | An Axiom |
| disj-04 | ⊦ EISDIR ≠ EACCESS | An Axiom |
| disj-05 | ⊦ EISDIR ≠ EBADFD | An Axiom |
| disj-06 | ⊦ EISDIR ≠ ENOTDIR | An Axiom |
| disj-07 | ⊦ ENOENT ≠ EACCESS | An Axiom |
| disj-08 | ⊦ ENOENT ≠ EBADFD | An Axiom |
| disj-09 | ⊦ ENOENT ≠ ENOTDIR | An Axiom |
| disj-10 | ⊦ ENOENT ≠ EISDIR | An Axiom |
| disj-11 | ⊦ EEXISTS ≠ EACCESS | An Axiom |
| disj-12 | ⊦ EEXISTS ≠ EBADFD | An Axiom |
| disj-13 | ⊦ EEXISTS ≠ ENOTDIR | An Axiom |
| disj-14 | ⊦ EEXISTS ≠ EISDIR | An Axiom |
| disj-15 | ⊦ EEXISTS ≠ ENOENT | An Axiom |
| disj-16 | ⊦ ENOSPC ≠ EACCESS | An Axiom |
| disj-17 | ⊦ ENOSPC ≠ EBADFD | An Axiom |
| disj-18 | ⊦ ENOSPC ≠ ENOTDIR | An Axiom |
| disj-19 | ⊦ ENOSPC ≠ EISDIR | An Axiom |
| disj-20 | ⊦ ENOSPC ≠ ENOENT | An Axiom |
| disj-21 | ⊦ ENOSPC ≠ EEXISTS | An Axiom |
| disj-22 | ⊦ ENOMEM ≠ EACCESS | An Axiom |
| disj-23 | ⊦ ENOMEM ≠ EBADFD | An Axiom |
| disj-24 | ⊦ ENOMEM ≠ ENOTDIR | An Axiom |
| disj-25 | ⊦ ENOMEM ≠ EISDIR | An Axiom |
| disj-26 | ⊦ ENOMEM ≠ ENOENT | An Axiom |
| disj-27 | ⊦ ENOMEM ≠ EEXISTS | An Axiom |
| disj-28 | ⊦ ENOMEM ≠ ENOSPC | An Axiom |
| disj-29 | ⊦ ESUCCESS ≠ EACCESS | An Axiom |
| disj-30 | ⊦ ESUCCESS ≠ EBADFD | An Axiom |
| disj-31 | ⊦ ESUCCESS ≠ ENOTDIR | An Axiom |
| disj-32 | ⊦ ESUCCESS ≠ EISDIR | An Axiom |
| disj-33 | ⊦ ESUCCESS ≠ ENOENT | An Axiom |
| disj-34 | ⊦ ESUCCESS ≠ EEXISTS | An Axiom |
| disj-35 | ⊦ ESUCCESS ≠ ENOSPC | An Axiom |
| disj-36 | ⊦ ESUCCESS ≠ ENOMEM | An Axiom |
| disj-37 | ⊦ EFAIL ≠ EACCESS | An Axiom |
| disj-38 | ⊦ EFAIL ≠ EBADFD | An Axiom |
| disj-39 | ⊦ EFAIL ≠ ENOTDIR | An Axiom |
| disj-40 | ⊦ EFAIL ≠ EISDIR | An Axiom |
| disj-41 | ⊦ EFAIL ≠ ENOENT | An Axiom |
| disj-42 | ⊦ EFAIL ≠ EEXISTS | An Axiom |
| disj-43 | ⊦ EFAIL ≠ ENOSPC | An Axiom |
| disj-44 | ⊦ EFAIL ≠ ENOMEM | An Axiom |
| disj-45 | ⊦ ESUCCESS ≠ EFAIL | An Axiom |
| disj-46 | ⊦ ENOTEMPTY ≠ EACCESS | An Axiom |
| disj-47 | ⊦ ENOTEMPTY ≠ EBADFD | An Axiom |
| disj-48 | ⊦ ENOTDIR ≠ ENOTEMPTY | An Axiom |
| disj-49 | ⊦ EISDIR ≠ ENOTEMPTY | An Axiom |
| disj-50 | ⊦ ENOENT ≠ ENOTEMPTY | An Axiom |
| disj-51 | ⊦ EEXISTS ≠ ENOTEMPTY | An Axiom |
| disj-52 | ⊦ ENOSPC ≠ ENOTEMPTY | An Axiom |
| disj-53 | ⊦ ENOMEM ≠ ENOTEMPTY | An Axiom |
| disj-54 | ⊦ EFAIL ≠ ENOTEMPTY | An Axiom |
| disj-55 | ⊦ ESUCCESS ≠ ENOTEMPTY | An Axiom |
| disj-56 | ⊦ EIO ≠ EACCESS | An Axiom |
| disj-57 | ⊦ EIO ≠ EBADFD | An Axiom |
| disj-58 | ⊦ EIO ≠ ENOTEMPTY | An Axiom |
| disj-59 | ⊦ EIO ≠ ENOTDIR | An Axiom |
| disj-60 | ⊦ EIO ≠ EISDIR | An Axiom |
| disj-61 | ⊦ EIO ≠ ENOENT | An Axiom |
| disj-62 | ⊦ EIO ≠ EEXISTS | An Axiom |
| disj-63 | ⊦ ENOSPC ≠ EIO | An Axiom |
| disj-64 | ⊦ ENOMEM ≠ EIO | An Axiom |
| disj-65 | ⊦ EFAIL ≠ EIO | An Axiom |
| disj-66 | ⊦ ESUCCESS ≠ EIO | An Axiom |
| disj-67 | ⊦ EACCESS ≠ EINVAL | An Axiom |
| disj-68 | ⊦ EBADFD ≠ EINVAL | An Axiom |
| disj-69 | ⊦ ENOTEMPTY ≠ EINVAL | An Axiom |
| disj-70 | ⊦ ENOTDIR ≠ EINVAL | An Axiom |
| disj-71 | ⊦ EISDIR ≠ EINVAL | An Axiom |
| disj-72 | ⊦ ENOENT ≠ EINVAL | An Axiom |
| disj-73 | ⊦ EEXISTS ≠ EINVAL | An Axiom |
| disj-74 | ⊦ EIO ≠ EINVAL | An Axiom |
| disj-75 | ⊦ ENOSPC ≠ EINVAL | An Axiom |
| disj-76 | ⊦ ENOMEM ≠ EINVAL | An Axiom |
| disj-77 | ⊦ EFAIL ≠ EINVAL | An Axiom |
| disj-78 | ⊦ ESUCCESS ≠ EINVAL | An Axiom |
| disj-79 | ⊦ EINVAL ≠ ECOMMIT | An Axiom |
| disj-80 | ⊦ EACCESS ≠ ECOMMIT | An Axiom |
| disj-81 | ⊦ EBADFD ≠ ECOMMIT | An Axiom |
| disj-82 | ⊦ ENOTEMPTY ≠ ECOMMIT | An Axiom |
| disj-83 | ⊦ ENOTDIR ≠ ECOMMIT | An Axiom |
| disj-84 | ⊦ EISDIR ≠ ECOMMIT | An Axiom |
| disj-85 | ⊦ ENOENT ≠ ECOMMIT | An Axiom |
| disj-86 | ⊦ EEXISTS ≠ ECOMMIT | An Axiom |
| disj-87 | ⊦ EIO ≠ ECOMMIT | An Axiom |
| disj-88 | ⊦ ENOSPC ≠ ECOMMIT | An Axiom |
| disj-89 | ⊦ ENOMEM ≠ ECOMMIT | An Axiom |
| disj-90 | ⊦ EFAIL ≠ ECOMMIT | An Axiom |
| disj-91 | ⊦ ESUCCESS ≠ ECOMMIT | An Axiom |
| disj-92 | ⊦ EROFS ≠ EUCLEAN | An Axiom |
| disj-93 | ⊦ ECOMMIT ≠ EUCLEAN | An Axiom |
| disj-94 | ⊦ ECOMMIT ≠ EROFS | An Axiom |
| disj-95 | ⊦ EINVAL ≠ EUCLEAN | An Axiom |
| disj-96 | ⊦ EINVAL ≠ EROFS | An Axiom |
| disj-97 | ⊦ EACCESS ≠ EUCLEAN | An Axiom |
| disj-98 | ⊦ EACCESS ≠ EROFS | An Axiom |
| disj-99 | ⊦ EBADFD ≠ EUCLEAN | An Axiom |
| disj-100 | ⊦ EBADFD ≠ EROFS | An Axiom |
| disj-101 | ⊦ ENOTEMPTY ≠ EUCLEAN | An Axiom |
| disj-102 | ⊦ ENOTEMPTY ≠ EROFS | An Axiom |
| disj-103 | ⊦ ENOTDIR ≠ EUCLEAN | An Axiom |
| disj-104 | ⊦ ENOTDIR ≠ EROFS | An Axiom |
| disj-105 | ⊦ EISDIR ≠ EUCLEAN | An Axiom |
| disj-106 | ⊦ EISDIR ≠ EROFS | An Axiom |
| disj-107 | ⊦ ENOENT ≠ EUCLEAN | An Axiom |
| disj-108 | ⊦ ENOENT ≠ EROFS | An Axiom |
| disj-109 | ⊦ EEXISTS ≠ EUCLEAN | An Axiom |
| disj-110 | ⊦ EEXISTS ≠ EROFS | An Axiom |
| disj-111 | ⊦ EIO ≠ EUCLEAN | An Axiom |
| disj-112 | ⊦ EIO ≠ EROFS | An Axiom |
| disj-113 | ⊦ ENOSPC ≠ EUCLEAN | An Axiom |
| disj-114 | ⊦ ENOSPC ≠ EROFS | An Axiom |
| disj-115 | ⊦ ENOMEM ≠ EUCLEAN | An Axiom |
| disj-116 | ⊦ ENOMEM ≠ EROFS | An Axiom |
| disj-117 | ⊦ EFAIL ≠ EUCLEAN | An Axiom |
| disj-118 | ⊦ EFAIL ≠ EROFS | An Axiom |
| disj-119 | ⊦ ESUCCESS ≠ EUCLEAN | An Axiom |
| disj-120 | ⊦ ESUCCESS ≠ EROFS | An Axiom |