		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-unmark-vars

Lift atj-unmark-var to lists.

Signature
(atj-unmark-vars vars) → (mv unmarked-vars new?s)
Arguments: vars — Guard (symbol-listp vars).
Returns: unmarked-vars — Type (symbol-listp unmarked-vars).; new?s — Type (boolean-listp new?s).

Definitions and Theorems

Function: atj-unmark-vars

(defun atj-unmark-vars (vars)
  (declare (xargs :guard (symbol-listp vars)))
  (let ((__function__ 'atj-unmark-vars))
    (declare (ignorable __function__))
    (b* (((when (endp vars)) (mv nil nil))
         ((mv var new?)
          (atj-unmark-var (car vars)))
         ((mv vars new?s)
          (atj-unmark-vars (cdr vars))))
      (mv (cons var vars)
          (cons new? new?s)))))

Theorem: symbol-listp-of-atj-unmark-vars.unmarked-vars

(defthm symbol-listp-of-atj-unmark-vars.unmarked-vars
  (b* (((mv ?unmarked-vars ?new?s)
        (atj-unmark-vars vars)))
    (symbol-listp unmarked-vars))
  :rule-classes :rewrite)

Theorem: boolean-listp-of-atj-unmark-vars.new?s

(defthm boolean-listp-of-atj-unmark-vars.new?s
  (b* (((mv ?unmarked-vars ?new?s)
        (atj-unmark-vars vars)))
    (boolean-listp new?s))
  :rule-classes :rewrite)

Theorem: len-of-atj-unmark-vars.unmarked-vars

(defthm len-of-atj-unmark-vars.unmarked-vars
  (b* (((mv ?unmarked-vars ?new?s)
        (atj-unmark-vars vars)))
    (equal (len unmarked-vars) (len vars))))

Theorem: len-of-atj-unmark-vars.new?s

(defthm len-of-atj-unmark-vars.new?s
  (b* (((mv ?unmarked-vars ?new?s)
        (atj-unmark-vars vars)))
    (equal (len new?s) (len vars))))