Theorem refin-not-05

• 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-string,
• Used spec theorems:
  • Used simplifier rules:
    • javavalue/test-188
    • javavalue/test-187
    • javavalue/test-186
    • javavalue/test-185
    • javavalue/test-184
    • javavalue/test-183
    • javavalue/test-181
    • javavalue/test-180
    • javavalue/test-265
    • javavalue/test-264
    • javavalue/test-263
    • javavalue/test-316
    • javavalue/test-179
    • javavalue/test-178
    • javavalue/test-177
    • javavalue/test-176
    • javavalue/test-182
    • javavalue/test-175