		Search-engine friendly clone of the ACL2 documentation.

System-level-marking-view-proof-utilities

Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux

Signature
(find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux vars calls) → *
Arguments: vars — Guard (true-listp vars).

Definitions and Theorems

Function: find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux

(defun find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux (vars calls)
 (declare (xargs :guard (true-listp vars)))
 (declare (xargs :guard (equal (len vars) 2)))
 (let
  ((__function__ 'find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux))
  (declare (ignorable __function__))
  (if (atom calls)
      nil
    (b* ((one-call (car calls))
         ((unless (and (true-listp one-call)
                       (equal 3 (len one-call))))
          nil)
         (mv-nth-term-1 (nth 1 one-call))
         ((unless (and (true-listp mv-nth-term-1)
                       (equal 3 (len mv-nth-term-1))))
          nil)
         (term-1 (nth 2 mv-nth-term-1))
         ((unless (and (true-listp term-1)
                       (equal 5 (len term-1))))
          nil)
         ((list n-var addr-var) vars))
      (cons (list (cons n-var (nth 1 term-1))
                  (cons addr-var (nth 2 term-1)))
            (find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
                 vars (cdr calls)))))))