Theorem abs-dirs-del-dir

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: s,
• Comment:
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 3
• Used lemmas: at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
• Used spec theorems:
  • Used simplifier rules:
    • heap/dir-heap/at-del
    • key/inj-03
    • heap/dir-heap/in-del
    • store/node-index/Del-in
    • key/disj-02
    • store/node-index/Del-at-strong