		Search-engine friendly clone of the ACL2 documentation.

General-memory-utils

Disjoint-p$

Signature
(disjoint-p$ x y) → *
Arguments: x — Guard (true-listp x).; y — Guard (true-listp y).

Definitions and Theorems

Function: disjoint-p$

(defun disjoint-p$ (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (let ((__function__ 'disjoint-p$))
    (declare (ignorable __function__))
    (disjoint-p x y)))

Theorem: rewrite-disjoint-p$-to-disjoint-p

(defthm rewrite-disjoint-p$-to-disjoint-p
  (equal (disjoint-p$ x y)
         (disjoint-p x y)))