		Search-engine friendly clone of the ACL2 documentation.

Fgl-bitvector

Scdr

Like logcdr for signed bit vectors.

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

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: 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))))

Theorem: scdr$inline-of-list-fix-v

(defthm scdr$inline-of-list-fix-v
  (equal (scdr$inline (list-fix v))
         (scdr$inline v)))

Theorem: scdr$inline-list-equiv-congruence-on-v

(defthm scdr$inline-list-equiv-congruence-on-v
  (implies (acl2::list-equiv v v-equiv)
           (equal (scdr$inline v)
                  (scdr$inline v-equiv)))
  :rule-classes :congruence)