		Search-engine friendly clone of the ACL2 documentation.

Bvec

Scdr

Like logcdr for signed bvecs.

Signature
(scdr v) → cdr
Arguments: v — Guard (true-listp v).
Returns: cdr — Type (true-listp cdr).

See bvec. For a signed bit vector, the final bit is the sign bit, which we must implicitly extend out to infinity.

Definitions and Theorems

Function: scdr$inline

(defun scdr$inline (v)
  (declare (xargs :guard (true-listp v)))
  (let ((__function__ 'scdr))
    (declare (ignorable __function__))
    (let ((v (llist-fix v)))
      (if (atom (cdr v)) v (cdr v)))))

Theorem: true-listp-of-scdr

(defthm true-listp-of-scdr
  (b* ((cdr (scdr$inline v)))
    (true-listp cdr))
  :rule-classes :type-prescription)

Theorem: pbfr-list-depends-on-scdr

(defthm pbfr-list-depends-on-scdr
  (implies (not (pbfr-list-depends-on k p x))
           (not (pbfr-list-depends-on k p (scdr x)))))

Theorem: scdr-of-list-fix

(defthm scdr-of-list-fix
  (equal (scdr (list-fix x))
         (list-fix (scdr x))))

Theorem: scdr-count-weak

(defthm scdr-count-weak
  (<= (acl2-count (scdr v))
      (acl2-count v))
  :rule-classes :linear)

Theorem: scdr-count-strong

(defthm scdr-count-strong
  (implies (not (s-endp v))
           (< (acl2-count (scdr v))
              (acl2-count v)))
  :rule-classes :linear)

Theorem: scdr-len-strong

(defthm scdr-len-strong
  (implies (not (s-endp v))
           (< (len (scdr v)) (len v)))
  :rule-classes :linear)

Theorem: scdr-len-weak

(defthm scdr-len-weak
  (<= (len (scdr v)) (len v))
  :rule-classes :linear)

Theorem: s-endp-of-scdr

(defthm s-endp-of-scdr
  (implies (s-endp b) (s-endp (scdr b))))

Theorem: scdr-when-s-endp

(defthm scdr-when-s-endp
  (implies (s-endp x)
           (equal (scdr x) (list-fix x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))