Theorem newrefs-three

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 28
• Proof steps: 36
• Used lemmas: instore-02, newref-new, instore-01, newref-notin, newref-in, instore, newref-jvmref, newref-def, newrefs-one-01, newrefs-rec-01, newrefsnew,
• Used spec theorems:
  • store/javastore/in-neq
• Used simplifier rules:
  • refkey/inj
  • refkey/inj-01
  • store/javastore/In-insert
  • list/references/a
  • list/references/app-01
  • list/references/c
  • list/references/Two