Theorem in-in-adr

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: ss, lss,
• Comment:
• Used by: at-diff, at-write-app, at-write-refsize, at-write-same, in-dealloc, in-write-same,
• Used by units in proved state: apersistence-asm, ablock-nodes,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 3
• Used lemmas: in,
• Used spec theorems:
  • Used simplifier rules:
    • address-data/sel-03
    • address-data/sel-04
    • address-data/sel-05
    • ablock/sel-02