		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)