Theorem refin-not-09

• 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-break,
• Used spec theorems:
  • Used simplifier rules:
    • javavalue/test-114
    • javavalue/test-113
    • javavalue/test-61
    • javavalue/test-70
    • javavalue/test-160
    • javavalue/test-97
    • javavalue/test-67
    • javavalue/test-193
    • javavalue/test-280
    • javavalue/test-279
    • javavalue/test-278
    • javavalue/test-321
    • javavalue/test-48
    • javavalue/test-47
    • javavalue/test-159
    • javavalue/test-158
    • javavalue/test-50
    • javavalue/test-46