		Search-engine friendly clone of the ACL2 documentation.

Clone-p

Adjacent-p

Signature
(adjacent-p clone c x) → *
Arguments: clone — Guard (natp clone).; c — Guard (natp c).; x — Guard (nat-listp x).

Definitions and Theorems

Function: adjacent-p

(defun adjacent-p (clone c x)
  (declare (xargs :guard (and (natp clone)
                              (natp c)
                              (nat-listp x))))
  (declare (xargs :guard (no-duplicatesp-equal x)))
  (let ((__function__ 'adjacent-p))
    (declare (ignorable __function__))
    (cond ((endp x) t)
          ((equal (car x) clone)
           (if (cdr x)
               (equal (car (cdr x)) c)
             nil))
          ((equal (car x) c)
           (if (cdr x)
               (equal (car (cdr x)) clone)
             nil))
          (t (adjacent-p clone c (cdr x))))))

Theorem: adjacent-p-of-absent-elements

(defthm adjacent-p-of-absent-elements
  (implies (and (not (member-equal c x))
                (not (member-equal clone x)))
           (adjacent-p clone c x)))

Theorem: adjacent-p-reflexive

(defthm adjacent-p-reflexive
  (implies (adjacent-p c clone x)
           (adjacent-p clone c x)))

Theorem: remove-equal-preserves-adjacent-p

(defthm remove-equal-preserves-adjacent-p
  (implies (and (adjacent-p clone c x)
                (true-listp x)
                (not (equal id c))
                (not (equal id clone)))
           (adjacent-p clone c (remove-equal id x))))