Theorem modify-sym

• Type: A user defined theorem
• Validity: The proof is INVALID because - the proof was set to invalid (continue/load proof to restore) - the proof was set to invalid (continue/load proof to restore) - the proof was set to invalid (continue/load proof to restore) - the proof was set to invalid (continue/load proof to restore) - the proof was set to invalid (continue/load proof to restore) - the proof was set to invalid (continue/load proof to restore) - the goal has changed
• Features:
• Comment:
• Used by: modify+-sym,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: No
• Interactions: 11
• Proof steps: 23
• Used lemmas: modify+, modify,
• Used spec theorems:
  • rtc/rtc-heap/rtc
  • heap/write-again
• Used simplifier rules:
  • rtc/rtc-heap/rtc1
  • Unknown/Unknown
  • heap/del-new
  • heap/in-write-strong
  • Unknown/Unknown