		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-rest

Signature
(lhs-rest x) → rest
Arguments: x — Guard (lhs-p x).
Returns: rest — Type (lhs-p rest).

Definitions and Theorems

Function: lhs-rest

(defun lhs-rest (x)
  (declare (xargs :guard (lhs-p x)))
  (let ((__function__ 'lhs-rest))
    (declare (ignorable __function__))
    (mbe :logic
         (if (or (atom x) (atom (cdr x)))
             nil
           (if (lhrange-combine (car x) (cadr x))
               (lhs-rest (cdr x))
             (lhs-fix (cdr x))))
         :exec
         (if (consp x)
             (if (and (consp (cdr x))
                      (lhrange-combinable (car x)
                                          (lhrange->atom (cadr x))))
                 (lhs-rest-aux (+ (lhrange->w (car x))
                                  (lhrange->w (cadr x)))
                               (lhrange->atom (car x))
                               (cddr x))
               (cdr x))
           x))))

Theorem: lhs-p-of-lhs-rest

(defthm lhs-p-of-lhs-rest
  (b* ((rest (lhs-rest x))) (lhs-p rest))
  :rule-classes :rewrite)

Theorem: lhs-rest-of-lhs-fix-x

(defthm lhs-rest-of-lhs-fix-x
  (equal (lhs-rest (lhs-fix x))
         (lhs-rest x)))

Theorem: lhs-rest-lhs-equiv-congruence-on-x

(defthm lhs-rest-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs-rest x) (lhs-rest x-equiv)))
  :rule-classes :congruence)

Theorem: lhs-rest-aux-elim

(defthm lhs-rest-aux-elim
  (equal (lhs-rest-aux w prev x)
         (lhs-rest (cons (lhrange w prev) x))))

Theorem: lhs-rest-in-terms-of-lhs-norm

(defthm lhs-rest-in-terms-of-lhs-norm
  (lhs-norm-equiv (lhs-rest x)
                  (cdr (lhs-norm x))))

Theorem: lhs-normp-of-lhs-rest

(defthm lhs-normp-of-lhs-rest
  (implies (lhs-normp x)
           (lhs-normp (lhs-rest x))))

Theorem: lhs-rest-of-lhs-norm

(defthm lhs-rest-of-lhs-norm
  (equal (lhs-rest (lhs-norm x))
         (cdr (lhs-norm x))))

Theorem: len-of-lhs-rest

(defthm len-of-lhs-rest
  (implies (consp x)
           (< (len (lhs-rest x)) (len x)))
  :rule-classes :linear)

Theorem: cons-first-rest-when-first-is-car

(defthm cons-first-rest-when-first-is-car
  (implies (and (equal (car (lhs-norm x)) (car x))
                (consp (lhs-norm x)))
           (equal (cons (car x) (lhs-rest x))
                  (lhs-fix x))))

Theorem: vars-of-lhs-rest

(defthm vars-of-lhs-rest
  (implies (not (member v (lhs-vars x)))
           (not (member v (lhs-vars (lhs-rest x))))))