### SPECIAL-CASES-FOR-REWRITE-RULES

convenient short forms for rewrite rule formulas
```Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER
```

In principle, every rewrite rule is made from a formula of this shape:

```(IMPLIES (AND hyp1 ... hypk)
(eqv lhs rhs))
```
where eqv is either `EQUAL` or `IFF` and the result of expanding any abbreviations in lhs is the application of some function symbol other than `IF`.

* In the special case where there is only one hyp term, i.e., k=1, the `(AND `hyp1`)` can be written hyp1.

* In the special case where there are no hyp terms, k=0, the `(AND)` term is logically just `T` and the whole `IMPLIES` can be dropped; such a formula may be written as an unconditional `EQUAL` or `IFF` term.

* If you build a rewrite rule from a formula that concludes with `(NOT `x`)`, it is treated as though it were `(EQUAL `x` NIL)`, which is logically equivalent to what you typed.

* If you build a rewrite rule from a formula that concludes with an `AND`, ACL2 will build a rewrite rule for each conjunct of the `AND`. This is because

```(IMPLIES hyp (AND concl1 concl2))
```
is propositionally equivalent to
```(AND (IMPLIES hyp concl1)
(IMPLIES hyp concl2)).
```
However, if you use an `OR`-expression as a hypothesis, ACL2 does not do the dual transformation. Thus, `(IMPLIES (OR hyp1 hyp2) concl)` generates one rewrite rule.

* Finally, if you build a rewrite rule from a formula that does not conclude with an `EQUAL`, an `IFF`, a `NOT`, or an `AND,` but with some other term, say, lhs, then ACL2 acts like you typed `(IFF `lhs` T)`, which is logically equivalent to what you typed.

Thus, regardless of what you type, every rule has k hypotheses. For unconditional rules, k is 0 and the hypotheses are vacuously true. Whether or not you write an `EQUAL` or an `IFF` in the conclusion, every rule is either an equality or a propositional equivalence, every rule has a left-hand side, and every rule has a right-hand side.