		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-decomp

Signature
(lhs-decomp x) → (mv * *)
Arguments: x — Guard (lhs-p x).

Definitions and Theorems

Function: lhs-decomp

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

Theorem: lhs-vars-of-decomp-redef

(defthm lhs-vars-of-decomp-redef
  (set-equiv (lhs-vars x)
             (b* (((mv first rest) (lhs-decomp x))
                  ((unless first) nil))
               (append (lhatom-vars (lhrange->atom first))
                       (lhs-vars rest))))
  :rule-classes ((:definition :install-body nil)))

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

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

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

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