		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

Aig-force-sign-s

Signature
(aig-force-sign-s sign x) → new-x
Arguments: x — Guard (true-listp x).
Returns: new-x — Type (true-listp new-x).

Definitions and Theorems

Function: aig-force-sign-s

(defun aig-force-sign-s (sign x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'aig-force-sign-s))
    (declare (ignorable __function__))
    (b* (((mv first rest end)
          (gl::first/rest/end x))
         ((when end) (list sign)))
      (aig-scons first (aig-force-sign-s sign rest)))))

Theorem: true-listp-of-aig-force-sign-s

(defthm true-listp-of-aig-force-sign-s
  (b* ((new-x (aig-force-sign-s sign x)))
    (true-listp new-x))
  :rule-classes :type-prescription)

Theorem: aig-force-sign-s-correct

(defthm aig-force-sign-s-correct
  (b* nil
    (implies (equal (aig-eval (aig-sign-s x) env)
                    (aig-eval sign env))
             (equal (aig-list->s (aig-force-sign-s sign x)
                                 env)
                    (aig-list->s x env)))))

Theorem: aig-force-sign-s-of-list-fix-x

(defthm aig-force-sign-s-of-list-fix-x
  (equal (aig-force-sign-s sign (list-fix x))
         (aig-force-sign-s sign x)))

Theorem: aig-force-sign-s-list-equiv-congruence-on-x

(defthm aig-force-sign-s-list-equiv-congruence-on-x
  (implies (list-equiv x x-equiv)
           (equal (aig-force-sign-s sign x)
                  (aig-force-sign-s sign x-equiv)))
  :rule-classes :congruence)