		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modinsts-nodups-p

Signature
(elab-modinsts-nodups-p x) → *

Definitions and Theorems

Function: elab-modinsts-nodups-p

(defun elab-modinsts-nodups-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'elab-modinsts-nodups-p))
    (declare (ignorable __function__))
    (and (elab-modinst-list-p x)
         (no-duplicatesp-equal (elab-modinst-list-names x)))))

Theorem: elab-modinsts-nodups-p-implies-elab-modinst-list-p

(defthm elab-modinsts-nodups-p-implies-elab-modinst-list-p
  (implies (elab-modinsts-nodups-p x)
           (elab-modinst-list-p x)))

Theorem: elab-modinsts-nodups-p-of-append

(defthm elab-modinsts-nodups-p-of-append
  (implies (and (elab-modinsts-nodups-p a)
                (elab-modinsts-nodups-p b)
                (not (intersection$ (elab-modinst-list-names a)
                                    (elab-modinst-list-names b))))
           (elab-modinsts-nodups-p (append a b))))

Theorem: elab-modinsts-nodups-p-of-cons

(defthm elab-modinsts-nodups-p-of-cons
  (equal (elab-modinsts-nodups-p (cons a b))
         (and (elab-modinst$cp a)
              (elab-modinsts-nodups-p b)
              (not (member (nth *elab-modinst$c->instname* a)
                           (elab-modinst-list-names b))))))