		Search-engine friendly clone of the ACL2 documentation.

Bvec

Bfr-snorm

Signature
(bfr-snorm v) → vv
Arguments: v — Guard (true-listp v).
Returns: vv — Type (true-listp vv).

Definitions and Theorems

Function: bfr-snorm

(defun bfr-snorm (v)
  (declare (xargs :guard (true-listp v)))
  (let ((__function__ 'bfr-snorm))
    (declare (ignorable __function__))
    (if (atom v) '(nil) (llist-fix v))))

Theorem: true-listp-of-bfr-snorm

(defthm true-listp-of-bfr-snorm
  (b* ((vv (bfr-snorm v)))
    (true-listp vv))
  :rule-classes :type-prescription)

Theorem: s-endp-of-bfr-snorm

(defthm s-endp-of-bfr-snorm
  (equal (s-endp (bfr-snorm v))
         (s-endp v)))

Theorem: scdr-of-bfr-snorm

(defthm scdr-of-bfr-snorm
  (equal (scdr (bfr-snorm v))
         (bfr-snorm (scdr v))))

Theorem: car-of-bfr-snorm

(defthm car-of-bfr-snorm
  (equal (car (bfr-snorm v)) (car v)))

Theorem: bfr-list->s-of-bfr-snorm

(defthm bfr-list->s-of-bfr-snorm
  (equal (bfr-list->s (bfr-snorm v) env)
         (bfr-list->s v env)))

Theorem: bfr-snorm-of-list-fix

(defthm bfr-snorm-of-list-fix
  (equal (bfr-snorm (list-fix x))
         (bfr-snorm x)))