Theorem at-dels-ro-data

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: s, ls,
• Comment:
• Used by: del-commute-dels, del-del-again, del-merge-dels, del-put-again, dels-ignore-data, notin-dels,
• Used by units in proved state: aubifs-inv,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 4
• Used lemmas: datakeys-set, dels-with-data,
• Used spec theorems:
  • Used simplifier rules:
    • store+set/node-index/Diff-get
    • store+set/node-index/Diff-mems-get
    • key/test-09
    • key/sel-03