Convenient short forms for rewrite rule formulas

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

(IMPLIES (ANDhyp1...hypk) (eqvlhsrhs))

where *eqv* is either *lhs* is the application of some function
symbol other than

* In the special case where there is only one *hyp* term, i.e.,
*k*=1, the *hyp1**hyp1*.

* In the special case where there are no *hyp* terms, *k*=0, the

* If you build a rewrite rule from a formula that concludes with *x**x*

* If you build a rewrite rule from a formula that concludes with an

(IMPLIES hyp (AND concl1 concl2))

is propositionally equivalent to

(AND (IMPLIES hyp concl1) (IMPLIES hyp concl2)).

However, if you use an *not* do the dual transformation. Thus,

* Finally, if you build a rewrite rule from a formula that does not
conclude with an *lhs*, then ACL2 acts like you typed *lhs*

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

Use your browser's **Back Button** now to return to introduction-to-rewrite-rules-part-1.