		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-first-aux

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

Definitions and Theorems

Function: lhs-first-aux

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

Theorem: return-type-of-lhs-first-aux

(defthm return-type-of-lhs-first-aux
  (b* ((first (lhs-first-aux w prev x)))
    (iff (lhrange-p first) first))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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

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

(defthm lhs-first-aux-in-terms-of-lhs-norm
  (equal (lhs-first-aux w prev x)
         (car (lhs-cons (lhrange w prev)
                        (lhs-norm x)))))