		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-decomp-aux

Signature
(lhs-decomp-aux w prev x) → (mv * *)
Arguments: w — Guard (posp w).; prev — Guard (lhatom-p prev).; x — Guard (lhs-p x).

Definitions and Theorems

Function: lhs-decomp-aux

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

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

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

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

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

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

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

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

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

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

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

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

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