### PRACTICE-FORMULATING-STRONG-RULES-5

rules suggested by `(SUBSETP (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).

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

When is `x` a subset of `(append y z)`? Clearly it is if `x` is a subset of `y` or `x` is a subset of `z`. We could write that:

```(defthm subsetp-append-2-weak
(implies (or (subsetp x y)
(subsetp x z))
(subsetp x (append y z))))
```
The rule generated from this is: ``if you ever encounter (an instance of) `(SUBSETP x (APPEND y z))`, backchain to the `or` above and try to establish it. If you can establish it, replace the target by `T`.''

This does not fully characterize the situation though. For example, `'(1 2 3 4)` is a subset of `(append '(1 3) '(2 4))` without being a subset of either argument of the `append`.

However, no obvious equivalence comes to mind -- indeed, to express any of the ideas floating around here requires defining and introducing more functions, which is not recommended unless those functions are already in the problem.

For example, if you defined the concept of ```set-minus`'' so that `(set-minus x y)` consists of those elements of `x` not in `y`, then you could prove:

```(defthm subset-append-2-strong-but-messy
(equal (subsetp x (append y z))
(and (subsetp (set-minus x z) y)
(subsetp (set-minus x y) z))))
```
But this rewrite rule would ``trade'' `append` away and introduce `set-minus`. That might be a good strategy if `set-minus` were already in the problem. But if it were not, it might not be. We wouldn't recommend this rule unless it were helpful in normalizing the expressions in the problem.

We recommend sticking with the weak version of the rule,

```(defthm subsetp-append-2-weak
(implies (or (subsetp x y)
(subsetp x z))
(subsetp x (append y z)))).
```
This illustrates the fact that sometimes there is no strong version of a rule!