Theorem insert-inter-notin-dom-nodes

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 4
• Used lemmas: in-nodes,
• Used spec theorems:
  • set-basic/address-store/Extension
  • set-union/address-store/Intersect
• Used simplifier rules:
  • set-basic/address-store/In-insert
  • store+set/address-store/Dom
  • set-union/address-store/Intersect
  • set-union/address-store/int-a
  • set-union/address-store/int-c