		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhrange-combinable

Signature
(lhrange-combinable x y) → *
Arguments: x — Guard (lhrange-p x).; y — Guard (lhatom-p y).

Definitions and Theorems

Function: lhrange-combinable

(defun lhrange-combinable (x y)
 (declare (xargs :guard (and (lhrange-p x) (lhatom-p y))))
 (let ((__function__ 'lhrange-combinable))
  (declare (ignorable __function__))
  (mbe :logic
       (equal (lhatom-fix y)
              (lhrange-nextbit x))
       :exec
       (b* (((lhrange x) x)
            (xkind (lhatom-kind x.atom))
            (ykind (lhatom-kind y)))
         (and (eq xkind ykind)
              (or (eq xkind :z)
                  (and (equal (lhatom-var->name x.atom)
                              (lhatom-var->name y))
                       (eql (lhatom-var->rsh y)
                            (+ (lhatom-var->rsh x.atom) x.w)))))))))

Theorem: lhrange-combinable-of-lhrange-fix-x

(defthm lhrange-combinable-of-lhrange-fix-x
  (equal (lhrange-combinable (lhrange-fix x) y)
         (lhrange-combinable x y)))

Theorem: lhrange-combinable-lhrange-equiv-congruence-on-x

(defthm lhrange-combinable-lhrange-equiv-congruence-on-x
  (implies (lhrange-equiv x x-equiv)
           (equal (lhrange-combinable x y)
                  (lhrange-combinable x-equiv y)))
  :rule-classes :congruence)

Theorem: lhrange-combinable-of-lhatom-fix-y

(defthm lhrange-combinable-of-lhatom-fix-y
  (equal (lhrange-combinable x (lhatom-fix y))
         (lhrange-combinable x y)))

Theorem: lhrange-combinable-lhatom-equiv-congruence-on-y

(defthm lhrange-combinable-lhatom-equiv-congruence-on-y
  (implies (lhatom-equiv y y-equiv)
           (equal (lhrange-combinable x y)
                  (lhrange-combinable x y-equiv)))
  :rule-classes :congruence)