[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem class
⊦ ⌊err⌋ ↔ err ≠ ESUCCESS ∧ err ≠ EEXISTS ∧ err ≠ ENOENT ∧ err ≠ EISDIR ∧ err ≠ ENOTEMPTY ∧ err ≠ ENOTDIR ∧ err ≠ EBADFD ∧ err ≠ EACCESS
Type: An axiom
Validity: The proof is valid.
Features: lws,
Comment:
Used by:
eaccess
,
ebadfd
,
ecommit
,
eexists
,
efail
,
einval
,
eio
,
eisdir
,
enoent
,
enomem
,
enospc
,
enotdir
,
enotempty
,
erofs
,
esuccess
,
euclean
,
Used by units in proved state:
Proof exists?: No