		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Netassigns-vars

Signature
(netassigns-vars x) → vars
Arguments: x — Guard (netassigns-p x).
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: netassigns-vars

(defun netassigns-vars (x)
  (declare (xargs :guard (netassigns-p x)))
  (let ((__function__ 'netassigns-vars))
    (declare (ignorable __function__))
    (b* ((x (netassigns-fix x))
         ((when (atom x)) nil))
      (cons (caar x)
            (append (driverlist-vars (cdar x))
                    (netassigns-vars (cdr x)))))))

Theorem: svarlist-p-of-netassigns-vars

(defthm svarlist-p-of-netassigns-vars
  (b* ((vars (netassigns-vars x)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: netassigns-vars-of-acons

(defthm netassigns-vars-of-acons
  (equal (netassigns-vars (cons (cons a b) c))
         (cons (svar-fix a)
               (append (driverlist-vars b)
                       (netassigns-vars c)))))

Theorem: netassigns-vars-of-append

(defthm netassigns-vars-of-append
  (equal (netassigns-vars (append a b))
         (append (netassigns-vars a)
                 (netassigns-vars b))))

Theorem: member-lookup-in-netassigns

(defthm member-lookup-in-netassigns
 (implies
  (and (not (member v (netassigns-vars x)))
       (netassigns-p x))
  (not (member v
               (driverlist-vars (cdr (hons-assoc-equal name x)))))))

Theorem: netassign-vars-of-remove-assoc

(defthm netassign-vars-of-remove-assoc
 (implies
    (and (not (member v (netassigns-vars x)))
         (netassigns-p x))
    (not (member v
                 (netassigns-vars (acl2::hons-remove-assoc k x))))))

Theorem: netassign-vars-of-fast-alist-clean

(defthm netassign-vars-of-fast-alist-clean
  (implies (and (not (member v (netassigns-vars x)))
                (netassigns-p x))
           (not (member v
                        (netassigns-vars (fast-alist-clean x))))))

Theorem: netassigns-vars-of-netassigns-fix-x

(defthm netassigns-vars-of-netassigns-fix-x
  (equal (netassigns-vars (netassigns-fix x))
         (netassigns-vars x)))

Theorem: netassigns-vars-netassigns-equiv-congruence-on-x

(defthm netassigns-vars-netassigns-equiv-congruence-on-x
  (implies (netassigns-equiv x x-equiv)
           (equal (netassigns-vars x)
                  (netassigns-vars x-equiv)))
  :rule-classes :congruence)