		Search-engine friendly clone of the ACL2 documentation.

4v-alists-agree

4v-alists-disagree-witness

Try to find a key for which two four-valued alists don't agree.

Definitions and Theorems

Function: 4v-alists-disagree-witness

(defun 4v-alists-disagree-witness (keys al1 al2)
  (declare (xargs :guard t))
  (if (atom keys)
      nil
    (if (equal (4v-lookup (car keys) al1)
               (4v-lookup (car keys) al2))
        (4v-alists-disagree-witness (cdr keys)
                                    al1 al2)
      (car keys))))

Theorem: 4v-alists-witness-correct

(defthm 4v-alists-witness-correct
  (iff (4v-alists-agree keys al1 al2)
       (let ((witness (4v-alists-disagree-witness keys al1 al2)))
         (or (not (member-equal witness keys))
             (equal (4v-lookup witness al1)
                    (4v-lookup witness al2))))))