		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-rightshift

Signature
(sparseint$-rightshift shift x) → rightshift
Arguments: shift — Guard (natp shift).; x — Guard (sparseint$-p x).
Returns: rightshift — Type (sparseint$-p rightshift).

Definitions and Theorems

Function: sparseint$-rightshift

(defun sparseint$-rightshift (shift x)
 (declare (xargs :guard (and (natp shift) (sparseint$-p x))))
 (declare (xargs :guard (sparseint$-height-correctp x)))
 (let ((__function__ 'sparseint$-rightshift))
  (declare (ignorable __function__))
  (sparseint$-case
   x :leaf
   (sparseint$-leaf (logtail shift x.val))
   :concat
   (b* (((mv shift ?height)
         (sparseint$-rightshift-rec shift x (sparseint$-height x))))
     shift))))

Theorem: sparseint$-p-of-sparseint$-rightshift

(defthm sparseint$-p-of-sparseint$-rightshift
  (b* ((rightshift (sparseint$-rightshift shift x)))
    (sparseint$-p rightshift))
  :rule-classes :rewrite)

Theorem: sparseint$-height-correctp-of-sparseint$-rightshift

(defthm sparseint$-height-correctp-of-sparseint$-rightshift
  (b* ((?rightshift (sparseint$-rightshift shift x)))
    (implies (sparseint$-height-correctp x)
             (sparseint$-height-correctp rightshift))))

Theorem: sparseint$-rightshift-correct

(defthm sparseint$-rightshift-correct
  (b* ((?rightshift (sparseint$-rightshift shift x)))
    (equal (sparseint$-val rightshift)
           (logtail shift (sparseint$-val x)))))

Theorem: height-of-sparseint$-rightshift

(defthm height-of-sparseint$-rightshift
  (b* ((?rightshift (sparseint$-rightshift shift x)))
    (implies (sparseint$-height-correctp x)
             (<= (sparseint$-height rightshift)
                 (sparseint$-height x))))
  :rule-classes :linear)

Theorem: sparseint$-rightshift-of-nfix-shift

(defthm sparseint$-rightshift-of-nfix-shift
  (equal (sparseint$-rightshift (nfix shift) x)
         (sparseint$-rightshift shift x)))

Theorem: sparseint$-rightshift-nat-equiv-congruence-on-shift

(defthm sparseint$-rightshift-nat-equiv-congruence-on-shift
  (implies (nat-equiv shift shift-equiv)
           (equal (sparseint$-rightshift shift x)
                  (sparseint$-rightshift shift-equiv x)))
  :rule-classes :congruence)

Theorem: sparseint$-rightshift-of-sparseint$-fix-x

(defthm sparseint$-rightshift-of-sparseint$-fix-x
  (equal (sparseint$-rightshift shift (sparseint$-fix x))
         (sparseint$-rightshift shift x)))

Theorem: sparseint$-rightshift-sparseint$-equiv-congruence-on-x

(defthm sparseint$-rightshift-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-rightshift shift x)
                  (sparseint$-rightshift shift x-equiv)))
  :rule-classes :congruence)