		Search-engine friendly clone of the ACL2 documentation.

Reasoning-about-page-tables

Find-first-arg-of-disjoint-p$-candidates

Signature
(find-first-arg-of-disjoint-p$-candidates var calls) → *

Definitions and Theorems

Function: find-first-arg-of-disjoint-p$-candidates

(defun find-first-arg-of-disjoint-p$-candidates (var calls)
 (declare (xargs :guard t))
 (let ((__function__ 'find-first-arg-of-disjoint-p$-candidates))
  (declare (ignorable __function__))
  (if (atom calls)
      nil
   (b* ((one-call (car calls))
        ((unless (and (true-listp one-call)
                      (equal 3 (len one-call))))
         nil)
        (term-1 (nth 1 one-call)))
    (cons
     (list (cons var term-1))
     (find-first-arg-of-disjoint-p$-candidates var (cdr calls)))))))