### PRACTICE-FORMULATING-STRONG-RULES-6

rules suggested by `(MEMBER (FOO A) (NATS-BELOW (BAR B)))`
```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) (NATS-BELOW (BAR B)))
```
The definition of `NATS-BELOW` is
```(defun nats-below (j)
(if (zp j)
'(0)
(cons j (nats-below (- j 1)))))
```
Thus, `(nats-below 7)` is `(7 6 5 4 3 2 1 0)`. So when is `k` a member of `(nats-below j)`?

The weakest version is

```(defthm member-nats-below-weak
(implies (and (natp k)
(natp j)
(<= k j))
(member k (nats-below j))))
```
But clearly we could improve this to:
```(defthm member-nats-below-weak-better
(implies (and (natp k)
(natp j))
(iff (member k (nats-below j))
(<= k j))))
```
or even
```(defthm member-nats-below-weak-better
(implies (natp j)
(iff (member k (nats-below j))
(and (natp k)
(<= k j)))))
```
Clearly though, we'd like to get rid of the `(natp j)` hypothesis and the neatest plausible version is:
```(defthm member-nats-below-weak-neatest
(iff (member k (nats-below j))
(and (natp j)
(natp k)
(<= k j))))

```
But it is not a theorem! For example, if `j` is `-1` and `k` is 0, then the left-hand side above returns `t`, because `(nats-below j)` is `(0)`, but the right-hand side is `nil`.

But this suggests a strategy for dealing with necessary hypotheses, like `(natp j)`. We can move them into an `IF` on the right-hand side! Something like this might be a useful rewrite rule:

```(iff (member k (nats-below j))
(if (natp j)
(and (natp k)
(<= k j))
...)).
```
We know, from `member-nats-below-weak-better`, that if `(natp j)` is true, the `member` is equivalent to `(and (natp k) (<= k j))`. So now consider what we know if `(natp j)` is false. If we can think of some term it's equivalent to nd that term is simpler than the `member` expression, we have a strong rule.

But by inspection of the definition of `nats-below`, we see that when `(natp j)` is false, `(nats-below j)` is the list `(0)` because `(zp j)` is t. That is, `nats-below` treats all non-natural arguments like they were `0`. Thus, when `(natp j)` is false, `(member k (nats-below j))` is `(member k '(0))`, which is `(equal k 0)`.

So the strong version is

```(defthm member-nats-below-strong
(iff (member k (nats-below j))
(if (natp j)
(and (natp k)
(<= k j))
(equal k 0))))
```
This is a great :`rewrite` rule. It gets rid of the `member` and `nats-below` and introduces arithmetic.

This example illustrates the idea of putting an `if` on the right-hand-side of the equivalence. Many users tend to limit themselves to propositional forms inside `iff` or to simple expressions inside of `equal`. But it is quite natural to use `if` to express what the answer is: if `j` is a natural, then `k` is in `(nats-below j)` precisely if `k` is a natural less than or equal to `j`; if `j` is not a natural, then `k` is in `(nats-below j)` precisely if `k` is `0`.

Use `if` to lay out the cases you must consider, if you can think of a simpler, equivalent expression for every possible case.

Use your browser's Back Button now to return to practice-formulating-strong-rules.