		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Driverlist->svex

Signature
(driverlist->svex x) → value
Arguments: x — Guard (driverlist-p x).
Returns: value — Type (svex-p value).

Definitions and Theorems

Function: driverlist->svex

(defun driverlist->svex (x)
  (declare (xargs :guard (driverlist-p x)))
  (declare (xargs :guard (drivestrength-ordered-p x)))
  (let ((__function__ 'driverlist->svex))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (svex-z))
         (strength1 (driver->strength (car x)))
         (vals1 (driverlist-values-of-strength x strength1))
         (rest1 (driverlist-rest-after-strength x strength1))
         (res1 (svexlist-resolve vals1))
         ((when (atom rest1)) res1))
      (svcall* override
               res1 (driverlist->svex rest1)))))

Theorem: svex-p-of-driverlist->svex

(defthm svex-p-of-driverlist->svex
  (b* ((value (driverlist->svex x)))
    (svex-p value))
  :rule-classes :rewrite)

Theorem: vars-of-driverlist->svex

(defthm vars-of-driverlist->svex
  (implies (not (member v (driverlist-vars x)))
           (not (member v (svex-vars (driverlist->svex x))))))

Theorem: driverlist->svex-of-driverlist-fix-x

(defthm driverlist->svex-of-driverlist-fix-x
  (equal (driverlist->svex (driverlist-fix x))
         (driverlist->svex x)))

Theorem: driverlist->svex-driverlist-equiv-congruence-on-x

(defthm driverlist->svex-driverlist-equiv-congruence-on-x
  (implies (driverlist-equiv x x-equiv)
           (equal (driverlist->svex x)
                  (driverlist->svex x-equiv)))
  :rule-classes :congruence)