[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
,
Proof step 6 from proof abs-fold-del (
previous step
)
⊦ str ∈ entries ∧ p ∈ tree ∧ tree[p] = dnode(md, sdt) ∧ ((abs|(tree, ROOT_INO, p, ino0) * ino0 => mkdir(# entries - 1, md, m0, m1, entries -- str) * abs(sdt -- str, entries -- str) * D))(dirs) → ((abs(tree -- (p + str '), ROOT_INO) * D))(dirs)
Lemma
abs-fold-del-p