Theorem refin-not-02

• 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-short,
• Used spec theorems:
  • Used simplifier rules:
    • javavalue/test-129
    • javavalue/test-128
    • javavalue/test-127
    • javavalue/test-126
    • javavalue/test-125
    • javavalue/test-124
    • javavalue/test-122
    • javavalue/test-172
    • javavalue/test-205
    • javavalue/test-204
    • javavalue/test-203
    • javavalue/test-292
    • javavalue/test-121
    • javavalue/test-96
    • javavalue/test-95
    • javavalue/test-81
    • javavalue/test-123
    • javavalue/test-80