#### MUTUAL-RECURSION-PROOF-EXAMPLE

a small proof about mutually recursive functions
```Major Section:  TUTORIAL5-MISCELLANEOUS-EXAMPLES
```

Sometimes one wants to reason about mutually recursive functions. Although this is possible in ACL2, it can be a bit awkward. This example is intended to give some ideas about how one can go about such proofs.

For an introduction to mutual recursion in ACL2, see mutual-recursion.

We begin by defining two mutually recursive functions: one that collects the variables from a term, the other that collects the variables from a list of terms. We actually imagine the term argument to be a `pseudo-termp`; see pseudo-termp.

```(mutual-recursion

(defun free-vars1 (term ans)
(cond ((atom term)
(add-to-set-eq term ans))
((fquotep term) ans)
(t (free-vars1-lst (fargs term) ans))))

(defun free-vars1-lst (lst ans)
(cond ((atom lst) ans)
(t (free-vars1-lst (cdr lst)
(free-vars1 (car lst) ans)))))

)
```
The idea of the following function is that it suggests a proof by induction in two cases, according to the top-level `if` structure of the body. In one case, `(atom x)` is true, and the theorem to be proved should be proved under no additional hypotheses except for `(atom x)`. In the other case, `(not (atom x))` is assumed together with three instances of the theorem to be proved, one for each recursive call in this case. So, one instance substitutes `(car x)` for `x`; one substitutes `(cdr x)` for `x`; and the third substitutes `(cdr x)` for `x` and `(free-vars1 (car x) ans)` for `ans`. If you think about how you would go about a hand proof of the theorem to follow, you'll come up with a similar scheme.
```(defun symbol-listp-free-vars1-induction (x ans)
(if (atom x)
; then we just make sure x and ans aren't considered irrelevant
(list x ans)
(list (symbol-listp-free-vars1-induction (car x) ans)
(symbol-listp-free-vars1-induction (cdr x) ans)
(symbol-listp-free-vars1-induction
(cdr x)
(free-vars1 (car x) ans)))))
```
We now prove the two theorems together as a conjunction, because the inductive hypotheses for one are sometimes needed in the proof of the other (even when you do this proof on paper!).
```(defthm symbol-listp-free-vars1
(and (implies (and (pseudo-termp x)
(symbol-listp ans))
(symbol-listp (free-vars1 x ans)))
(implies (and (pseudo-term-listp x)
(symbol-listp ans))
(symbol-listp (free-vars1-lst x ans))))
:hints
(("Goal" :induct (symbol-listp-free-vars1-induction x ans))))
```
The above works, but let's try for a more efficient proof, which avoids cluttering the proof with irrelevant (false) inductive hypotheses.
```(ubt 'symbol-listp-free-vars1-induction)

(defun symbol-listp-free-vars1-induction (flg x ans)

; Flg is non-nil (or t) if we are ``thinking'' of a single term.

(if (atom x)
(list x ans)
(if flg
(symbol-listp-free-vars1-induction nil (cdr x) ans)
(list (symbol-listp-free-vars1-induction t (car x) ans)
(symbol-listp-free-vars1-induction
nil
(cdr x)
(free-vars1 (car x) ans))))))
```
We now state the theorem as a conditional, so that it can be proved nicely using the induction scheme that we have just coded. The prover will not store an `if` term as a rewrite rule, but that's OK (as long as we tell it not to try), because we're going to derive the corollaries of interest later and make them into rewrite rules.
```(defthm symbol-listp-free-vars1-flg
(if flg
(implies (and (pseudo-termp x)
(symbol-listp ans))
(symbol-listp (free-vars1 x ans)))
(implies (and (pseudo-term-listp x)
(symbol-listp ans))
(symbol-listp (free-vars1-lst x ans))))
:hints
(("Goal" :induct (symbol-listp-free-vars1-induction flg x ans)))
:rule-classes nil)
```
And finally, we may derive the theorems we are interested in as immediate corollaries.
```(defthm symbol-listp-free-vars1
(implies (and (pseudo-termp x)
(symbol-listp ans))
(symbol-listp (free-vars1 x ans)))
:hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
(flg t)))))

(defthm symbol-listp-free-vars1-lst
(implies (and (pseudo-term-listp x)
(symbol-listp ans))
(symbol-listp (free-vars1-lst x ans)))
:hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
(flg nil)))))
```