		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-check-nonrec-conditions

Check whether nonrec? satisfies the conditions for nonrec<x1,...,xn> described in the documentation.

Signature
(tailrec-check-nonrec-conditions combine-nonrec nonrec? r q) → (mv yes/no combine)
Arguments: combine-nonrec — Guard (pseudo-termp combine-nonrec).; nonrec? — Candidate nonrec<x1,...,xn> to check.
Guard (pseudo-termp nonrec?).; r — Guard (symbolp r).; q — Guard (symbolp q).
Returns: yes/no — Type (booleanp yes/no).; combine — The pseudo-termp combine<q,r> described in the documentation, if yes/no is t; otherwise nil.

The conditions are that r does not occur in nonrec? and that replacing every occurrence of nonrec? in combine<nonrec<x1,...,xn>,r> with q yields a term whose only free variables are q and r.

Definitions and Theorems

Function: tailrec-check-nonrec-conditions

(defun tailrec-check-nonrec-conditions (combine-nonrec nonrec? r q)
  (declare (xargs :guard (and (pseudo-termp combine-nonrec)
                              (pseudo-termp nonrec?)
                              (symbolp r)
                              (symbolp q))))
  (let ((__function__ 'tailrec-check-nonrec-conditions))
    (declare (ignorable __function__))
    (if (member-eq r (all-vars nonrec?))
        (mv nil nil)
      (let ((combine (subst-expr1 q nonrec? combine-nonrec)))
        (if (set-equiv (all-vars combine)
                       (list q r))
            (mv t combine)
          (mv nil nil))))))

Theorem: booleanp-of-tailrec-check-nonrec-conditions.yes/no

(defthm booleanp-of-tailrec-check-nonrec-conditions.yes/no
  (b*
    (((mv ?yes/no ?combine)
      (tailrec-check-nonrec-conditions combine-nonrec nonrec? r q)))
    (booleanp yes/no))
  :rule-classes :rewrite)