		Search-engine friendly clone of the ACL2 documentation.

Fairness-criteria

Clone-p

Is clone a clone of c in xs?

Signature
(clone-p clone c xs) → *
Arguments: clone — Candidate in xs who is a possible clone of candidate c.
Guard (natp clone).; c — Candidate in xs.
Guard (natp c).; xs — Guard (irv-ballot-p xs).

Definitions and Theorems

Function: clone-p

(defun clone-p (clone c xs)
  (declare (xargs :guard (and (natp clone)
                              (natp c)
                              (irv-ballot-p xs))))
  (declare (xargs :guard (not (equal clone c))))
  (let ((__function__ 'clone-p))
    (declare (ignorable __function__))
    (if (endp xs)
        t
      (and (adjacent-p clone c (car xs))
           (clone-p clone c (cdr xs))))))

Theorem: clone-p-reflexive

(defthm clone-p-reflexive
  (implies (clone-p c clone xs)
           (clone-p clone c xs)))

Theorem: eliminate-candidate-preserves-clone-p

(defthm eliminate-candidate-preserves-clone-p
  (implies (and (clone-p clone c xs)
                (not (equal id c))
                (not (equal id clone))
                (irv-ballot-p xs))
           (clone-p clone c (eliminate-candidate id xs))))

Subtopics

Adjacent-p