		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-rest-aux

Signature
(lhs-rest-aux w prev x) → rest
Arguments: w — Guard (posp w).; prev — Guard (lhatom-p prev).; x — Guard (lhs-p x).
Returns: rest — Type (lhs-p rest).

Definitions and Theorems

Function: lhs-rest-aux

(defun lhs-rest-aux (w prev x)
 (declare (xargs :guard (and (posp w)
                             (lhatom-p prev)
                             (lhs-p x))))
 (let ((__function__ 'lhs-rest-aux))
   (declare (ignorable __function__))
   (if (and (consp x)
            (lhrange-combinable-dec w prev (lhrange->atom (car x))))
       (lhs-rest-aux (+ (pos-fix w) (lhrange->w (car x)))
                     prev (cdr x))
     (lhs-fix x))))

Theorem: lhs-p-of-lhs-rest-aux

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

Theorem: lhs-rest-aux-of-pos-fix-w

(defthm lhs-rest-aux-of-pos-fix-w
  (equal (lhs-rest-aux (pos-fix w) prev x)
         (lhs-rest-aux w prev x)))

Theorem: lhs-rest-aux-pos-equiv-congruence-on-w

(defthm lhs-rest-aux-pos-equiv-congruence-on-w
  (implies (pos-equiv w w-equiv)
           (equal (lhs-rest-aux w prev x)
                  (lhs-rest-aux w-equiv prev x)))
  :rule-classes :congruence)

Theorem: lhs-rest-aux-of-lhatom-fix-prev

(defthm lhs-rest-aux-of-lhatom-fix-prev
  (equal (lhs-rest-aux w (lhatom-fix prev) x)
         (lhs-rest-aux w prev x)))

Theorem: lhs-rest-aux-lhatom-equiv-congruence-on-prev

(defthm lhs-rest-aux-lhatom-equiv-congruence-on-prev
  (implies (lhatom-equiv prev prev-equiv)
           (equal (lhs-rest-aux w prev x)
                  (lhs-rest-aux w prev-equiv x)))
  :rule-classes :congruence)

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

(defthm lhs-rest-aux-of-lhs-fix-x
  (equal (lhs-rest-aux w prev (lhs-fix x))
         (lhs-rest-aux w prev x)))

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

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

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

(defthm lhs-rest-aux-in-terms-of-lhs-norm
  (lhs-norm-equiv (lhs-rest-aux w prev x)
                  (cdr (lhs-cons (lhrange w prev)
                                 (lhs-norm x)))))