		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-rsh

Signature
(lhs-rsh sh x) → rsh
Arguments: sh — Guard (natp sh).; x — Guard (lhs-p x).
Returns: rsh — Type (lhs-p rsh).

Definitions and Theorems

Function: lhs-rsh

(defun lhs-rsh (sh x)
 (declare (xargs :guard (and (natp sh) (lhs-p x))))
 (let ((__function__ 'lhs-rsh))
   (declare (ignorable __function__))
   (b*
     (((when (zp sh)) (lhs-fix x))
      ((when (atom x)) nil)
      ((lhrange xf) (car x))
      ((when (<= xf.w sh))
       (lhs-rsh (- sh xf.w) (cdr x)))
      (newatom
           (lhatom-case
                xf.atom
                :z (lhatom-z)
                :var (lhatom-var xf.atom.name (+ xf.atom.rsh sh)))))
     (lhs-cons (lhrange (- xf.w sh) newatom)
               (cdr x)))))

Theorem: lhs-p-of-lhs-rsh

(defthm lhs-p-of-lhs-rsh
  (b* ((rsh (lhs-rsh sh x))) (lhs-p rsh))
  :rule-classes :rewrite)

Theorem: lhs-rsh-of-nfix-sh

(defthm lhs-rsh-of-nfix-sh
  (equal (lhs-rsh (nfix sh) x)
         (lhs-rsh sh x)))

Theorem: lhs-rsh-nat-equiv-congruence-on-sh

(defthm lhs-rsh-nat-equiv-congruence-on-sh
  (implies (nat-equiv sh sh-equiv)
           (equal (lhs-rsh sh x)
                  (lhs-rsh sh-equiv x)))
  :rule-classes :congruence)

Theorem: lhs-rsh-of-lhs-fix-x

(defthm lhs-rsh-of-lhs-fix-x
  (equal (lhs-rsh sh (lhs-fix x))
         (lhs-rsh sh x)))

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

(defthm lhs-rsh-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs-rsh sh x)
                  (lhs-rsh sh x-equiv)))
  :rule-classes :congruence)

Theorem: lhs-rsh-correct

(defthm lhs-rsh-correct
  (equal (lhs-eval (lhs-rsh sh x) env)
         (4vec-rsh (2vec (nfix sh))
                   (lhs-eval x env))))

Theorem: lhs-rsh-correct-zero

(defthm lhs-rsh-correct-zero
  (equal (lhs-eval-zx (lhs-rsh sh x) env)
         (4vec-rsh (2vec (nfix sh))
                   (lhs-eval-zx x env))))

Theorem: lhs-width-of-lhs-rsh

(defthm lhs-width-of-lhs-rsh
  (<= (lhs-width (lhs-rsh sh x))
      (nfix (- (lhs-width x) (nfix sh))))
  :rule-classes :linear)

Theorem: lhs-rsh-of-lhs-cons

(defthm lhs-rsh-of-lhs-cons
  (lhs-norm-equiv (lhs-rsh sh (lhs-cons x y))
                  (lhs-rsh sh (cons x y))))

Theorem: lhs-rsh-of-lhs-norm-x-under-lhs-norm-equiv

(defthm lhs-rsh-of-lhs-norm-x-under-lhs-norm-equiv
  (lhs-norm-equiv (lhs-rsh sh (lhs-norm x))
                  (lhs-rsh sh x)))

Theorem: lhs-rsh-lhs-norm-equiv-congruence-on-x-under-lhs-norm-equiv

(defthm lhs-rsh-lhs-norm-equiv-congruence-on-x-under-lhs-norm-equiv
  (implies (lhs-norm-equiv x x-equiv)
           (lhs-norm-equiv (lhs-rsh sh x)
                           (lhs-rsh sh x-equiv)))
  :rule-classes :congruence)

Theorem: len-of-lhs-rsh

(defthm len-of-lhs-rsh
  (<= (len (lhs-rsh sh x)) (len x))
  :rule-classes :linear)