Theorem del-put-again

• 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: 7
• Proof steps: 16
• Used lemmas: at-dels-ro-data, at-dels-ro-nodata, in-dels-ro,
• Used spec theorems:
  • store/node-index/k-Extension
  • store/node-index/At-other
  • store/node-index/In-insert
• Used simplifier rules:
  • set-basic/node-index/size-zero-01
  • set-basic/node-index/ne-01
  • key/elim-02
  • key/test-09
  • key/disj-01