		Search-engine friendly clone of the ACL2 documentation.

Clause-indices

Collect indices of all identifiers used throughout a clause.

Signature
(clause-indices clause) → *
Arguments: clause — Guard (lit-listp clause).

Definitions and Theorems

Function: clause-indices

(defun clause-indices (clause)
  (declare (xargs :guard (lit-listp clause)))
  (let ((__function__ 'clause-indices))
    (declare (ignorable __function__))
    (if (atom clause)
        nil
      (cons (lit->var (car clause))
            (clause-indices (cdr clause))))))

Theorem: clause-indices-when-atom

(defthm clause-indices-when-atom
  (implies (atom clause)
           (equal (clause-indices clause) nil)))

Theorem: clause-indices-of-cons

(defthm clause-indices-of-cons
  (equal (clause-indices (cons lit clause))
         (cons (lit->var lit)
               (clause-indices clause))))

Theorem: clause-indices-of-lit-list-fix-clause

(defthm clause-indices-of-lit-list-fix-clause
  (equal (clause-indices (lit-list-fix clause))
         (clause-indices clause)))

Theorem: clause-indices-lit-list-equiv-congruence-on-clause

(defthm clause-indices-lit-list-equiv-congruence-on-clause
  (implies (lit-list-equiv clause clause-equiv)
           (equal (clause-indices clause)
                  (clause-indices clause-equiv)))
  :rule-classes :congruence)