|
|
|---|
|
|
|
|---|
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.
Theorem:
(defthm if*-when-true (implies a (equal (if* a b c) b)))
Theorem:
(defthm if*-when-false (implies (not a) (equal (if* a b c) c)))
Theorem:
(defthm if*-when-same (equal (if* a b b) b))