[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 4 from proof btree-sub-clean-next (
previous step
)
⊦ btree-sub-clean(r, n, zh) ↔ r ∈ zh ∧ ( ¬ zh[r].leaf → (∀ n0. n0 < zh[r].usedsize ∧ n0 < n ∧ zh[r].zbranches[n0].branch? ∧ zh[r].zbranches[n0].child ∈ zh → ¬ zh[zh[r].zbranches[n0].child].dirty))
Lemma
btree-sub-clean