Theorem refin-not-07

• 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-type,
• Used spec theorems:
  • Used simplifier rules:
    • javavalue/test-112
    • javavalue/test-111
    • javavalue/test-79
    • javavalue/test-94
    • javavalue/test-144
    • javavalue/test-92
    • javavalue/test-90
    • javavalue/test-191
    • javavalue/test-274
    • javavalue/test-273
    • javavalue/test-272
    • javavalue/test-319
    • javavalue/test-89
    • javavalue/test-88
    • javavalue/test-143
    • javavalue/test-142
    • javavalue/test-91
    • javavalue/test-87