		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-bitproj

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

Definitions and Theorems

Function: lhs-bitproj

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

Theorem: lhbit-p-of-lhs-bitproj

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

Theorem: lhs-bitproj-of-nfix-idx

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

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

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

Theorem: lhs-bitproj-of-lhs-fix-x

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

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

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

Theorem: lhs-bitproj-correct

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

Theorem: lhs-bitproj-of-lhs-cons

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

Theorem: lhs-bitproj-of-lhs-concat

(defthm lhs-bitproj-of-lhs-concat
  (equal (lhs-bitproj idx (lhs-concat w x y))
         (if (< (nfix idx) (nfix w))
             (lhs-bitproj idx x)
           (lhs-bitproj (- (nfix idx) (nfix w))
                        y))))

Theorem: lhs-bitproj-of-lhs-rsh

(defthm lhs-bitproj-of-lhs-rsh
  (equal (lhs-bitproj idx (lhs-rsh sh x))
         (lhs-bitproj (+ (nfix idx) (nfix sh))
                      x)))

Theorem: lhs-bitproj-of-lhs-norm-x

(defthm lhs-bitproj-of-lhs-norm-x
  (equal (lhs-bitproj idx (lhs-norm x))
         (lhs-bitproj idx x)))

Theorem: lhs-bitproj-lhs-norm-equiv-congruence-on-x

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