### PRACTICE-FORMULATING-STRONG-RULES-4

rules suggested by `(SUBSETP (APPEND (FOO A) (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 (APPEND (FOO A) (BAR B)) (MUM C))

When is `(append x y)`

a subset of `z`

? When everything in
`x`

is in `z`

and everything in `y`

is in `z`

. We would
make it a rewrite rule:

(defthm subsetp-append-1-strong
(equal (subsetp (append x y) z)
(and (subsetp x z)
(subsetp y z))))

We put the ```-1-`

'' in the name because there is a comparable
theorem for when the `append`

is in the second argument of the `subsetp`

;
see practice-formulating-strong-rules-5.

This strong rule is better than the conditional rule;

(defthm subsetp-append-1-weak
(implies (and (subsetp x z)
(subsetp y z))
(subsetp (append x y) z)))

for all the usual reasons.
Use your browser's **Back Button** now to return to
practice-formulating-strong-rules.