Theorem refin-not

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 2
• Used lemmas: refin-int,
• Used spec theorems:
  • Used simplifier rules:
    • javavalue/test-102
    • javavalue/test-101
    • javavalue/test-30
    • javavalue/test-26
    • javavalue/test-32
    • javavalue/test-82
    • javavalue/test-07
    • javavalue/test-170
    • javavalue/test-199
    • javavalue/test-198
    • javavalue/test-197
    • javavalue/test-290
    • javavalue/test-23
    • javavalue/test-24
    • javavalue/test-29
    • javavalue/test-28
    • javavalue/test-01
    • javavalue/test-25