		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Netassigns->resolves

Signature
(netassigns->resolves x) → assigns
Arguments: x — Guard (netassigns-p x).
Returns: assigns — Type (svex-alist-p assigns).

Definitions and Theorems

Function: netassigns->resolves

(defun netassigns->resolves (x)
 (declare (xargs :guard (netassigns-p x)))
 (let ((__function__ 'netassigns->resolves))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* ((x (netassigns-fix x))
        ((when (atom x)) nil)
        ((cons name drivers) (car x))
        (value (driverlist->svex
                    (drivestrength-sort (driverlist-fix drivers)))))
     (cons (cons name value)
           (netassigns->resolves (cdr x))))
   :exec
   (if (atom x)
       nil
     (acl2::with-local-nrev
          (netassigns->resolves-nrev x acl2::nrev))))))

Theorem: svex-alist-p-of-netassigns->resolves

(defthm svex-alist-p-of-netassigns->resolves
  (b* ((assigns (netassigns->resolves x)))
    (svex-alist-p assigns))
  :rule-classes :rewrite)

Theorem: vars-of-drivestrength-insert

(defthm vars-of-drivestrength-insert
 (implies
     (and (not (member v (driverlist-vars x)))
          (not (member v (svex-vars (driver->value elt)))))
     (not (member v
                  (driverlist-vars (drivestrength-insert elt x))))))

Theorem: vars-of-drivestrength-insertsort

(defthm vars-of-drivestrength-insertsort
 (implies
     (not (member v (driverlist-vars x)))
     (not (member v
                  (driverlist-vars (drivestrength-insertsort x))))))

Theorem: vars-of-netassigns->resolves

(defthm vars-of-netassigns->resolves
 (implies
   (not (member v (netassigns-vars x)))
   (and (not (member v
                     (svex-alist-keys (netassigns->resolves x))))
        (not (member v
                     (svex-alist-vars (netassigns->resolves x)))))))

Theorem: svex-lookup-under-iff-of-netassigns->resolves

(defthm svex-lookup-under-iff-of-netassigns->resolves
  (b* ((?assigns (netassigns->resolves x)))
    (iff (svex-lookup v assigns)
         (hons-assoc-equal (svar-fix v)
                           (netassigns-fix x)))))

Theorem: netassigns->resolves-of-netassigns-fix-x

(defthm netassigns->resolves-of-netassigns-fix-x
  (equal (netassigns->resolves (netassigns-fix x))
         (netassigns->resolves x)))

Theorem: netassigns->resolves-netassigns-equiv-congruence-on-x

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