[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 subdirs
⊦ str ∈ subdirs(ino, dirs) ↔ ino ∈ dirs ∧ str ∈ dirs[ino].entries ∧ dirs[ino].entries[str] ∈ dirs
Type: An axiom
Validity: The proof is valid.
Features: s, ls, ss, lss,
Comment:
Used by:
afs-cons-init
,
subdirs-add-entry
,
subdirs-alloc
,
subdirs-dec-size
,
subdirs-del-entry
,
subdirs-del-mod-size
,
subdirs-delete-orphans
,
subdirs-inc-size
,
subdirs-modmeta
,
subdirs-put
,
subdirs-putother
,
subdirs-write
,
Used by units in proved state:
afs-asm
,
Proof exists?: No