		Search-engine friendly clone of the ACL2 documentation.

Remove-unused-vars

Remove-unused-vars-aux

Signature
(remove-unused-vars-aux formals actuals body-vars) → (mv remaining-formals remaining-actuals)
Arguments: formals — Guard (symbol-listp formals).; actuals — Guard (pseudo-term-listp actuals).; body-vars — Guard (symbol-listp body-vars).
Returns: remaining-formals — Type (symbol-listp remaining-formals), given (symbol-listp formals).; remaining-actuals — Type (pseudo-term-listp remaining-actuals), given (pseudo-term-listp actuals).

Definitions and Theorems

Function: remove-unused-vars-aux

(defun remove-unused-vars-aux (formals actuals body-vars)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-term-listp actuals)
                              (symbol-listp body-vars))))
  (declare (xargs :guard (= (len formals) (len actuals))))
  (let ((__function__ 'remove-unused-vars-aux))
    (declare (ignorable __function__))
    (b* (((when (endp formals)) (mv nil nil))
         (formal (car formals))
         (actual (car actuals))
         ((unless (member-eq formal body-vars))
          (remove-unused-vars-aux (cdr formals)
                                  (cdr actuals)
                                  body-vars))
         ((mv formals actuals)
          (remove-unused-vars-aux (cdr formals)
                                  (cdr actuals)
                                  body-vars)))
      (mv (cons formal formals)
          (cons actual actuals)))))

Theorem: symbol-listp-of-remove-unused-vars-aux.remaining-formals

(defthm symbol-listp-of-remove-unused-vars-aux.remaining-formals
 (implies (symbol-listp formals)
          (b* (((mv ?remaining-formals ?remaining-actuals)
                (remove-unused-vars-aux formals actuals body-vars)))
            (symbol-listp remaining-formals)))
 :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-remove-unused-vars-aux.remaining-actuals

(defthm
      pseudo-term-listp-of-remove-unused-vars-aux.remaining-actuals
 (implies (pseudo-term-listp actuals)
          (b* (((mv ?remaining-formals ?remaining-actuals)
                (remove-unused-vars-aux formals actuals body-vars)))
            (pseudo-term-listp remaining-actuals)))
 :rule-classes :rewrite)

Theorem: true-listp-of-remove-unused-vars-aux.remaining-formals

(defthm true-listp-of-remove-unused-vars-aux.remaining-formals
  (b* (((mv ?remaining-formals ?remaining-actuals)
        (remove-unused-vars-aux formals actuals body-vars)))
    (true-listp remaining-formals))
  :rule-classes :type-prescription)

Theorem: true-listp-of-remove-unused-vars-aux.remaining-actuals

(defthm true-listp-of-remove-unused-vars-aux.remaining-actuals
  (b* (((mv ?remaining-formals ?remaining-actuals)
        (remove-unused-vars-aux formals actuals body-vars)))
    (true-listp remaining-actuals))
  :rule-classes :type-prescription)

Theorem: acl2-count-of-remove-unused-vars-aux-remaining-formals

(defthm acl2-count-of-remove-unused-vars-aux-remaining-formals
  (b* (((mv ?remaining-formals ?remaining-actuals)
        (remove-unused-vars-aux formals actuals body-vars)))
    (<= (acl2-count remaining-formals)
        (acl2-count formals)))
  :rule-classes :linear)

Theorem: acl2-count-of-remove-unused-vars-aux-remaining-actuals

(defthm acl2-count-of-remove-unused-vars-aux-remaining-actuals
 (implies (= (len formals) (len actuals))
          (b* (((mv ?remaining-formals ?remaining-actuals)
                (remove-unused-vars-aux formals actuals body-vars)))
            (<= (acl2-count remaining-actuals)
                (acl2-count actuals))))
 :rule-classes :linear)

Theorem: same-len-of-remove-unused-vars-aux

(defthm same-len-of-remove-unused-vars-aux
  (b* (((mv remaining-formals remaining-actuals)
        (remove-unused-vars-aux formals actuals body-vars)))
    (implies (equal (len formals) (len actuals))
             (equal (len remaining-formals)
                    (len remaining-actuals)))))