## ELIM

make a destructor elimination rule
```Major Section:  RULE-CLASSES
```

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. An example `:``corollary` formula from which an `:elim` rule might be built is:

```Example:
(implies (consp x)                      when (car v) or (cdr v) appears
(equal (cons (car x) (cdr x))  in a conjecture, and v is a
x))                     variable, consider replacing v by
(cons a b), for two new variables
a and b.

General Form:
(implies hyp (equiv lhs x))
```

where `equiv` is a known equivalence relation See defequiv, `x` is a variable symbol and `lhs` contains one or more terms (called ``destructor terms'') of the form `(fn v1 ... vn)`, where `fn` is a function symbol and the `vi` are distinct variable symbols, `v1`, ..., `vn` include all the variable symbols in the formula, no `fn` occurs in `lhs` in more than one destructor term, and all occurrences of `x` in `lhs` are inside destructor terms.

To use an `:elim` rule, the theorem prover waits until a conjecture has been maximally simplified. If it then finds an instance of some destructor term `(fn v1 ... vn)` in the conjecture, where the instance for `x` is some variable symbol, `vi`, and every occurrence of `vi` outside the destructor terms is in an `equiv`-hittable position, then it instantiates the `:elim` formula as indicated by the destructor term matched, splits the conjecture into two goals, according to whether the instantiated hypothesis, `hyp`, holds, and in the case that it does, generalizes all the instantiated destructor terms in the conjecture to new variables and then replaces `vi` in the conjecture by the generalized instantiated `lhs`. An occurrence of `vi` is ```equiv`-hittable'' if sufficient congruence rules (see defcong) have been proved to establish that the propositional value of the clause is not altered by replacing that occurrence of `vi` by some `equiv`-equivalent term.

If an `:elim` rule is not applied when you think it should have been, and the rule uses an equivalence relation, `equiv`, other than `equal`, it is most likely that there is an occurrence of the variable that is not `equiv`-hittable. Easy occurrences to overlook are those in in the governing hypotheses. If you see an unjustified occurrence of the variable, you must prove the appropriate congruence rule to allow the `:elim` to fire.

At the moment, the best description of how ACL2 `:elim` rules are used may be found in the discussion of ``ELIM Rules,'' pp 247 of A Computational Logic Handbook.