		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhrange-combine

Signature
(lhrange-combine x y) → val
Arguments: x — Guard (lhrange-p x).; y — Guard (lhrange-p y).
Returns: val — Type (iff (lhrange-p val) val).

Definitions and Theorems

Function: lhrange-combine

(defun lhrange-combine (x y)
  (declare (xargs :guard (and (lhrange-p x) (lhrange-p y))))
  (let ((__function__ 'lhrange-combine))
    (declare (ignorable __function__))
    (b* (((lhrange x) x)
         ((lhrange y) y)
         (xkind (lhatom-kind x.atom))
         (ykind (lhatom-kind y.atom))
         ((unless (eq xkind ykind)) nil)
         ((when (eq xkind :z))
          (lhrange (+ x.w y.w) (lhatom-z)))
         ((lhatom-var x.atom) x.atom)
         ((lhatom-var y.atom) y.atom)
         ((unless (and (equal x.atom.name y.atom.name)
                       (eql y.atom.rsh (+ x.w x.atom.rsh))))
          nil))
      (lhrange (+ x.w y.w) x.atom))))

Theorem: return-type-of-lhrange-combine

(defthm return-type-of-lhrange-combine
  (b* ((val (lhrange-combine x y)))
    (iff (lhrange-p val) val))
  :rule-classes :rewrite)

Theorem: lhrange-combine-of-lhrange-fix-x

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

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

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

Theorem: lhrange-combine-of-lhrange-fix-y

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

Theorem: lhrange-combine-lhrange-equiv-congruence-on-y

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

Theorem: lhrange-combine-under-iff

(defthm lhrange-combine-under-iff
  (iff (lhrange-combine x y)
       (lhatom-equiv (lhrange-nextbit x)
                     (lhrange->atom y))))

Theorem: lhrange-combine-when-combinable

(defthm lhrange-combine-when-combinable
  (implies (lhatom-equiv (lhrange-nextbit x)
                         (lhrange->atom y))
           (equal (lhrange-combine x y)
                  (lhrange (+ (lhrange->w x) (lhrange->w y))
                           (lhrange->atom x)))))

Theorem: logapps-of-logtails

(defthm logapps-of-logtails
  (implies (equal (nfix w2) (+ (nfix w1) (nfix w)))
           (equal (logapp w (logtail w1 x)
                          (logapp w3 (logtail w2 x) y))
                  (logapp (+ (nfix w) (nfix w3))
                          (logtail w1 x)
                          y))))

Theorem: logapp-of-logapp-same-width

(defthm logapp-of-logapp-same-width
  (equal (logapp w (logapp w x z) y)
         (logapp w x y)))

Theorem: lhrange-combine-correct

(defthm lhrange-combine-correct
  (implies (lhrange-combine x y)
           (equal (lhrange-eval (lhrange-combine x y) env)
                  (lhs-eval (list x y) env))))

Theorem: lhrange-combine-correct-zero

(defthm lhrange-combine-correct-zero
 (implies
      (lhrange-combine x y)
      (equal (lhatom-eval-zero (lhrange->atom (lhrange-combine x y))
                               env)
             (4vec-concat (2vec (lhrange->w x))
                          (lhatom-eval-zero (lhrange->atom x) env)
                          (lhatom-eval-zero (lhrange->atom y)
                                            env)))))

Theorem: lhrange-combine-width

(defthm lhrange-combine-width
  (implies (lhrange-combine x y)
           (equal (lhrange->w (lhrange-combine x y))
                  (+ (lhrange->w x) (lhrange->w y)))))