		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Driverlist-rest-after-strength

Signature
(driverlist-rest-after-strength x strength) → rest
Arguments: x — Guard (driverlist-p x).; strength — Guard (natp strength).
Returns: rest — Type (driverlist-p rest).

Definitions and Theorems

Function: driverlist-rest-after-strength

(defun driverlist-rest-after-strength (x strength)
  (declare (xargs :guard (and (driverlist-p x) (natp strength))))
  (declare (xargs :guard (drivestrength-ordered-p x)))
  (let ((__function__ 'driverlist-rest-after-strength))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((driver x1) (car x))
         (strength (lnfix strength))
         ((when (< x1.strength strength))
          (driverlist-fix x)))
      (driverlist-rest-after-strength (cdr x)
                                      strength))))

Theorem: driverlist-p-of-driverlist-rest-after-strength

(defthm driverlist-p-of-driverlist-rest-after-strength
  (b* ((rest (driverlist-rest-after-strength x strength)))
    (driverlist-p rest))
  :rule-classes :rewrite)

Theorem: vars-of-driverlist-rest-after-strength

(defthm vars-of-driverlist-rest-after-strength
 (implies
  (not (member v (driverlist-vars x)))
  (not (member v
               (driverlist-vars
                    (driverlist-rest-after-strength x strength))))))

Theorem: len-of-driverlist-rest-after-strength

(defthm len-of-driverlist-rest-after-strength
 (implies
  (consp x)
  (<
   (len
      (driverlist-rest-after-strength x (driver->strength (car x))))
   (len x)))
 :rule-classes :linear)

Theorem: drivestrength-ordered-p-of-driverlist-rest-after-strength

(defthm drivestrength-ordered-p-of-driverlist-rest-after-strength
  (implies (drivestrength-ordered-p x)
           (drivestrength-ordered-p
                (driverlist-rest-after-strength x strength))))

Theorem: driverlist-rest-after-strength-of-driverlist-fix-x

(defthm driverlist-rest-after-strength-of-driverlist-fix-x
  (equal (driverlist-rest-after-strength (driverlist-fix x)
                                         strength)
         (driverlist-rest-after-strength x strength)))

Theorem: driverlist-rest-after-strength-driverlist-equiv-congruence-on-x

(defthm
    driverlist-rest-after-strength-driverlist-equiv-congruence-on-x
 (implies (driverlist-equiv x x-equiv)
          (equal (driverlist-rest-after-strength x strength)
                 (driverlist-rest-after-strength x-equiv strength)))
 :rule-classes :congruence)

Theorem: driverlist-rest-after-strength-of-nfix-strength

(defthm driverlist-rest-after-strength-of-nfix-strength
  (equal (driverlist-rest-after-strength x (nfix strength))
         (driverlist-rest-after-strength x strength)))

Theorem: driverlist-rest-after-strength-nat-equiv-congruence-on-strength

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