		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-first

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

Definitions and Theorems

Function: lhs-first

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

Theorem: lhs-norm-car-under-iff

(defthm lhs-norm-car-under-iff
  (iff (car (lhs-norm x))
       (consp (lhs-norm x))))

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

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

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

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