		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Driverlist-values-of-strength

Signature
(driverlist-values-of-strength x strength) → values
Arguments: x — Guard (driverlist-p x).; strength — Guard (natp strength).
Returns: values — Type (svexlist-p values).

Definitions and Theorems

Function: driverlist-values-of-strength

(defun driverlist-values-of-strength (x strength)
  (declare (xargs :guard (and (driverlist-p x) (natp strength))))
  (declare (xargs :guard (drivestrength-ordered-p x)))
  (let ((__function__ 'driverlist-values-of-strength))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((driver x1) (car x))
         (strength (lnfix strength))
         ((when (eql strength x1.strength))
          (cons x1.value
                (driverlist-values-of-strength (cdr x)
                                               strength))))
      nil)))

Theorem: svexlist-p-of-driverlist-values-of-strength

(defthm svexlist-p-of-driverlist-values-of-strength
  (b* ((values (driverlist-values-of-strength x strength)))
    (svexlist-p values))
  :rule-classes :rewrite)

Theorem: svex-vars-of-driverlist-values-of-strength

(defthm svex-vars-of-driverlist-values-of-strength
 (implies
  (not (member v (driverlist-vars x)))
  (not
   (member
      v
      (svexlist-vars (driverlist-values-of-strength x strength))))))

Theorem: driverlist-values-of-strength-of-driverlist-fix-x

(defthm driverlist-values-of-strength-of-driverlist-fix-x
  (equal (driverlist-values-of-strength (driverlist-fix x)
                                        strength)
         (driverlist-values-of-strength x strength)))

Theorem: driverlist-values-of-strength-driverlist-equiv-congruence-on-x

(defthm
     driverlist-values-of-strength-driverlist-equiv-congruence-on-x
  (implies (driverlist-equiv x x-equiv)
           (equal (driverlist-values-of-strength x strength)
                  (driverlist-values-of-strength x-equiv strength)))
  :rule-classes :congruence)

Theorem: driverlist-values-of-strength-of-nfix-strength

(defthm driverlist-values-of-strength-of-nfix-strength
  (equal (driverlist-values-of-strength x (nfix strength))
         (driverlist-values-of-strength x strength)))

Theorem: driverlist-values-of-strength-nat-equiv-congruence-on-strength

(defthm
     driverlist-values-of-strength-nat-equiv-congruence-on-strength
  (implies (nat-equiv strength strength-equiv)
           (equal (driverlist-values-of-strength x strength)
                  (driverlist-values-of-strength x strength-equiv)))
  :rule-classes :congruence)