Theorem entries-dom2

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: forward, localforward,
• Comment:
• Used by: abs-dir-h, abs-has-rootpath-h, abs-nlinks-h, abs-paths-eq, abs-tree, absc-path, entries-unfold, path-fid, path-split-wand, path-unfold,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 3
• Used lemmas: entries-dom,
• Used spec theorems:
  • Used simplifier rules: