		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-vars-assignablep

Lift atc-var-assignablep to lists.

Signature
(atc-vars-assignablep var-list innermostp-list affect) → yes/no
Arguments: var-list — Guard (symbol-listp var-list).; innermostp-list — Guard (boolean-listp innermostp-list).; affect — Guard (symbol-listp affect).
Returns: yes/no — Type (booleanp yes/no), given (boolean-listp innermostp-list).

Definitions and Theorems

Function: atc-vars-assignablep

(defun atc-vars-assignablep (var-list innermostp-list affect)
  (declare (xargs :guard (and (symbol-listp var-list)
                              (boolean-listp innermostp-list)
                              (symbol-listp affect))))
  (declare (xargs :guard (equal (len var-list)
                                (len innermostp-list))))
  (let ((__function__ 'atc-vars-assignablep))
    (declare (ignorable __function__))
    (or (endp var-list)
        (and (atc-var-assignablep (car var-list)
                                  (car innermostp-list)
                                  affect)
             (atc-vars-assignablep (cdr var-list)
                                   (cdr innermostp-list)
                                   affect)))))

Theorem: booleanp-of-atc-vars-assignablep

(defthm booleanp-of-atc-vars-assignablep
 (implies
  (boolean-listp innermostp-list)
  (b*
   ((yes/no (atc-vars-assignablep var-list innermostp-list affect)))
   (booleanp yes/no)))
 :rule-classes :rewrite)