Theorem refin-not-01

• 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-byte,
• Used spec theorems:
  • Used simplifier rules:
    • javavalue/test-72
    • javavalue/test-71
    • javavalue/test-63
    • javavalue/test-62
    • javavalue/test-54
    • javavalue/test-53
    • javavalue/test-44
    • javavalue/test-171
    • javavalue/test-202
    • javavalue/test-201
    • javavalue/test-200
    • javavalue/test-291
    • javavalue/test-41
    • javavalue/test-40
    • javavalue/test-37
    • javavalue/test-36
    • javavalue/test-45
    • javavalue/test-33