### PRACTICE-FORMULATING-STRONG-RULES-3

rules suggested by `(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))`
```Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER
```

What rules come to mind when looking at the following subterm of a Key Checkpoint? Think of strong rules (see strong-rewrite-rules).

```(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))
```

Since `(append x y)` contains all the members of `x` and all the members of `y`, `e` is a member of `(append x y)` precisely when `e` is a member of `x` or of `y`. So a strong statement of this is:

```(defthm member-append-strong-false
(equal (member e (append x y))
(or (member e x)
(member e y))))
```

However, this is not a theorem because `member` is not Boolean. `(Member e x)`, for example, returns the first tail of `x` that starts with `e`, or else `nil`. To see an example of this formula that evaluates to `nil`, let

```e = 3
x = '(1 2 3)
y = '(4 5 6).
```
Then the left-hand side, `(member e (append x y))` evaluates to `(3 4 5 6)` while the right-hand side evaluates to `(3)`.

However, the two sides are propositionally equivalent (both either `nil` or non-`nil` together). So this is a useful :`rewrite` rule:

```(defthm member-append-strong
(iff (member e (append x y))
(or (member e x)
(member e y)))).
```
It tells the system that whenever it encounters an instance of `(MEMBER e (APPEND x y))` in a propositional occurrence (where only its truthvalue is relevant), it should be replaced by this disjunction of `(MEMBER e x)` and `(MEMBER e y)`.

The following two formulas are true but provide much weaker rules and we would not add them:

```(implies (member e x) (member e (append x y)))

(implies (member e y) (member e (append x y)))
```
because they each cause the system to backchain upon seeing `(MEMBER e (APPEND x y))` expressions and will not apply unless one of the two side-conditions can be established.

There is a rewrite rule that is even stronger than `member-append-strong`. It is suggested by the counterexample, above, for the `EQUAL` version of the rule.

```(defthm member-append-really-strong
(equal (member e (append x y))
(if (member e x)
(append (member e x) y)
(member e y))))
```
While `member-append-strong` only rewrites `member-append` expressions occurring propositionally, the `-really-strong` version rewrites every occurrence.

However, this rule will be more useful than `member-append-strong` only if you have occurrences of `member` in non-propositional places. For example, suppose you encountered a term like:

```(CONS (MEMBER e (APPEND x y)) z).
```
Then the `-strong` rule does not apply but the `-really-strong` rule does.

Furthermore, the `-really-strong` rule, by itself, is not quite as good as the `-strong` rule in propositional settings! For example, if you have proved the `-really-strong` rule, you'll notice that the system still has to use induction to prove

```(IMPLIES (MEMBER E A)
(MEMBER E (APPEND B A))).
```
The `-really-strong` rule would rewrite it to
```(IMPLIES (MEMBER E A)
(IF (MEMBER E A)
(APPEND (MEMBER E A) B)
(MEMBER E B)))
```
which would further simplify to
```(IMPLIES (MEMBER E A)
(APPEND (MEMBER E A) B))
```
What lemma does this suggest? The answer is the rather odd:
```(implies x (append x y))
```
which rewrites propositional occurrences of `(APPEND x y)` to `T` if `x` is non-`nil`. This is an inductive fact about `append`.

A problem with the `-really-strong` rule is that it transforms even propositional occurrences of `member` into mixed propositional and non-propositional occurrences.

```(defthm member-append-really-strong
(equal (member e (append x y))      ; <-- even if this is a propositional occurrence
(if (member e x)
(append (member e x) y)  ; <-- the member in here is not!
(member e y))))
```
So if you are using the `-really-strong` lemma in a situation in which all your `member` expressions are used propositionally, you'll suddenly find yourself confronted with non-propositional uses of `member`.

Our advice is not to use the `-really-strong` version unless your application is inherently using `member` in a non-propositional way.
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}