• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Miscellaneous
    • Output-controls
    • Bdd
      • If*
        • Std/basic/if*
      • Bdd-algorithm
      • Bdd-introduction
      • Show-bdd
      • Obdd
    • Macros
    • Installation
    • Mailing-lists
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/basic
• If*

Std/basic/if*

Rules about if*.

These rules are unrelated to the special status of if* in BDD reasoning. These rules are useful when if* is used as a more controllable version of the built-in if, e.g. so that ACL2 does not do unwanted case splits.

Definitions and Theorems

Theorem: if*-when-true

(defthm if*-when-true
  (implies a (equal (if* a b c) b)))

Theorem: if*-when-false

(defthm if*-when-false
  (implies (not a) (equal (if* a b c) c)))

Theorem: if*-when-same

(defthm if*-when-same
  (equal (if* a b b) b))