		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhrange-bitproj

Signature
(lhrange-bitproj idx x) → bit
Arguments: idx — Guard (natp idx).; x — Guard (lhrange-p x).
Returns: bit — Type (lhbit-p bit).

Definitions and Theorems

Function: lhrange-bitproj

(defun lhrange-bitproj (idx x)
  (declare (xargs :guard (and (natp idx) (lhrange-p x))))
  (let ((__function__ 'lhrange-bitproj))
    (declare (ignorable __function__))
    (b* (((lhrange x) x) (idx (lnfix idx)))
      (if (<= x.w idx)
          (lhbit-z)
        (lhatom-bitproj idx x.atom)))))

Theorem: lhbit-p-of-lhrange-bitproj

(defthm lhbit-p-of-lhrange-bitproj
  (b* ((bit (lhrange-bitproj idx x)))
    (lhbit-p bit))
  :rule-classes :rewrite)

Theorem: lhrange-bitproj-of-nfix-idx

(defthm lhrange-bitproj-of-nfix-idx
  (equal (lhrange-bitproj (nfix idx) x)
         (lhrange-bitproj idx x)))

Theorem: lhrange-bitproj-nat-equiv-congruence-on-idx

(defthm lhrange-bitproj-nat-equiv-congruence-on-idx
  (implies (nat-equiv idx idx-equiv)
           (equal (lhrange-bitproj idx x)
                  (lhrange-bitproj idx-equiv x)))
  :rule-classes :congruence)

Theorem: lhrange-bitproj-of-lhrange-fix-x

(defthm lhrange-bitproj-of-lhrange-fix-x
  (equal (lhrange-bitproj idx (lhrange-fix x))
         (lhrange-bitproj idx x)))

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

(defthm lhrange-bitproj-lhrange-equiv-congruence-on-x
  (implies (lhrange-equiv x x-equiv)
           (equal (lhrange-bitproj idx x)
                  (lhrange-bitproj idx x-equiv)))
  :rule-classes :congruence)

Theorem: lhrange-bitproj-correct

(defthm lhrange-bitproj-correct
  (equal (lhbit-eval (lhrange-bitproj idx x) env)
         (4vec-bit-index idx (lhrange-eval x env))))

Theorem: lhrange-bitproj-of-lhrange-combine

(defthm lhrange-bitproj-of-lhrange-combine
  (implies (lhrange-combine x y)
           (equal (lhrange-bitproj idx (lhrange-combine x y))
                  (if (< (nfix idx) (lhrange->w x))
                      (lhrange-bitproj idx x)
                    (lhrange-bitproj (- (nfix idx) (lhrange->w x))
                                     y)))))

Theorem: lhatom-bitproj-of-lhrange-combine-atom

(defthm lhatom-bitproj-of-lhrange-combine-atom
  (implies
       (lhrange-combine x y)
       (equal (lhatom-bitproj idx
                              (lhrange->atom (lhrange-combine x y)))
              (if (< (nfix idx) (lhrange->w x))
                  (lhatom-bitproj idx (lhrange->atom x))
                (lhatom-bitproj (- (nfix idx) (lhrange->w x))
                                (lhrange->atom y))))))