Theorem refin-not-03

• 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-bool,
• Used spec theorems:
  • Used simplifier rules:
    • javavalue/test-106
    • javavalue/test-105
    • javavalue/test-51
    • javavalue/test-42
    • javavalue/test-135
    • javavalue/test-84
    • javavalue/test-22
    • javavalue/test-174
    • javavalue/test-211
    • javavalue/test-210
    • javavalue/test-209
    • javavalue/test-294
    • javavalue/test-13
    • javavalue/test-14
    • javavalue/test-134
    • javavalue/test-133
    • javavalue/test-03
    • javavalue/test-15