		Search-engine friendly clone of the ACL2 documentation.

Intersectp-equal-theorems

Some theorems about the built-in function intersectp.

Theorem: intersectp-append-left

(defthm intersectp-append-left
  (equal (intersectp-equal (append x y) z)
         (or (intersectp-equal x z)
             (intersectp-equal y z))))

Theorem: intersectp-append-right

(defthm intersectp-append-right
  (equal (intersectp-equal x (append y z))
         (or (intersectp-equal x y)
             (intersectp-equal x z))))