		Search-engine friendly clone of the ACL2 documentation.

Fgl-bitvector

First/rest/end

Deconstruct a signed bit vector.

Signature
(first/rest/end x) → (mv * * *)
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: first/rest/end

(defun first/rest/end (x)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard t))
  (let ((__function__ 'first/rest/end))
    (declare (ignorable __function__))
    (mbe :logic (mv (car x) (scdr x) (s-endp x))
         :exec (cond ((atom x) (mv nil x t))
                     ((atom (cdr x)) (mv (car x) x t))
                     (t (mv (car x) (cdr x) nil))))))

Theorem: first/rest/end-of-list-fix-x

(defthm first/rest/end-of-list-fix-x
  (equal (first/rest/end (list-fix x))
         (first/rest/end x)))

Theorem: first/rest/end-list-equiv-congruence-on-x

(defthm first/rest/end-list-equiv-congruence-on-x
  (implies (acl2::list-equiv x x-equiv)
           (equal (first/rest/end x)
                  (first/rest/end x-equiv)))
  :rule-classes :congruence)