		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhatom-bitproj

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

Definitions and Theorems

Function: lhatom-bitproj

(defun lhatom-bitproj (idx x)
  (declare (xargs :guard (and (natp idx) (lhatom-p x))))
  (let ((__function__ 'lhatom-bitproj))
    (declare (ignorable __function__))
    (lhatom-case x
                 :z (lhbit-z)
                 :var (lhbit-var x.name (+ (lnfix idx) x.rsh)))))

Theorem: lhbit-p-of-lhatom-bitproj

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

Theorem: lhatom-bitproj-of-nfix-idx

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

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

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

Theorem: lhatom-bitproj-of-lhatom-fix-x

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

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

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

Theorem: lhatom-bitproj-correct

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