[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 3 from proof abs-tree (
previous step
)
⊦ tree0 = tree1 ↔ (∀ p. (p ∈ tree0 ↔ p ∈ tree1) ∧ (p ∈ tree0 → (tree0[p].dir? ↔ tree1[p].dir?) ∧ (tree0[p].dir? ⊃ tree0[p].meta = tree1[p].meta;tree0[p].fid = tree1[p].fid)))
A spec-lemma