		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

No-trivial-pairsp

Check if an alist has no pairs with equal key and value.

Signature
(no-trivial-pairsp alist) → yes/no
Arguments: alist — Guard (alistp alist).
Returns: yes/no — Type (booleanp yes/no).

This is a constraint satisfied by function substitutions; see fun-substp. A pair that substitutes a function with itself would have no effect, so such pairs are useless.

Definitions and Theorems

Function: no-trivial-pairsp

(defun no-trivial-pairsp (alist)
  (declare (xargs :guard (alistp alist)))
  (let ((__function__ 'no-trivial-pairsp))
    (declare (ignorable __function__))
    (if (endp alist)
        t
      (let ((pair (car alist)))
        (and (not (equal (car pair) (cdr pair)))
             (no-trivial-pairsp (cdr alist)))))))

Theorem: booleanp-of-no-trivial-pairsp

(defthm booleanp-of-no-trivial-pairsp
  (b* ((yes/no (no-trivial-pairsp alist)))
    (booleanp yes/no))
  :rule-classes :rewrite)