		Search-engine friendly clone of the ACL2 documentation.

Fty-pseudo-term-utilities

Fty-remove-equal-formals-actuals

FTY version of remove-equal-formals-actuals.

Signature
(fty-remove-equal-formals-actuals formals actuals) → (mv new-formals new-actuals)
Arguments: formals — Guard (symbol-listp formals).; actuals — Guard (pseudo-term-listp actuals).
Returns: new-formals — Type (symbol-listp new-formals), given (symbol-listp formals).; new-actuals — Type (pseudo-term-listp new-actuals).

Definitions and Theorems

Function: fty-remove-equal-formals-actuals

(defun fty-remove-equal-formals-actuals (formals actuals)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-term-listp actuals))))
  (declare (xargs :guard (= (len formals) (len actuals))))
  (let ((__function__ 'fty-remove-equal-formals-actuals))
    (declare (ignorable __function__))
    (remove-equal-formals-actuals formals
                                  (pseudo-term-list-fix actuals))))

Theorem: symbol-listp-of-fty-remove-equal-formals-actuals.new-formals

(defthm symbol-listp-of-fty-remove-equal-formals-actuals.new-formals
 (implies (symbol-listp formals)
          (b* (((mv ?new-formals ?new-actuals)
                (fty-remove-equal-formals-actuals formals actuals)))
            (symbol-listp new-formals)))
 :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-fty-remove-equal-formals-actuals.new-actuals

(defthm
  pseudo-term-listp-of-fty-remove-equal-formals-actuals.new-actuals
  (b* (((mv ?new-formals ?new-actuals)
        (fty-remove-equal-formals-actuals formals actuals)))
    (pseudo-term-listp new-actuals))
  :rule-classes :rewrite)

Theorem: true-listp-of-fty-remove-equal-formals-actuals.new-formals

(defthm true-listp-of-fty-remove-equal-formals-actuals.new-formals
  (b* (((mv ?new-formals ?new-actuals)
        (fty-remove-equal-formals-actuals formals actuals)))
    (true-listp new-formals))
  :rule-classes :type-prescription)

Theorem: true-listp-of-fty-remove-equal-formals-actuals.new-actuals

(defthm true-listp-of-fty-remove-equal-formals-actuals.new-actuals
  (b* (((mv ?new-formals ?new-actuals)
        (fty-remove-equal-formals-actuals formals actuals)))
    (true-listp new-actuals))
  :rule-classes :type-prescription)

Theorem: len-of-fty-remove-equal-formals-actuals.new-formals-is-new-actuals

(defthm
 len-of-fty-remove-equal-formals-actuals.new-formals-is-new-actuals
 (b* (((mv ?new-formals ?new-actuals)
       (fty-remove-equal-formals-actuals formals actuals)))
   (equal (len new-formals)
          (len new-actuals))))

Theorem: len-of-fty-remove-equal-formals-actuals.new-actuals-is-new-formals

(defthm
 len-of-fty-remove-equal-formals-actuals.new-actuals-is-new-formals
 (b* (((mv ?new-formals ?new-actuals)
       (fty-remove-equal-formals-actuals formals actuals)))
   (equal (len new-actuals)
          (len new-formals))))

Theorem: pseudo-term-list-count-of-remove-equal-formals-actuals

(defthm pseudo-term-list-count-of-remove-equal-formals-actuals
  (b* (((mv & new-actuals)
        (remove-equal-formals-actuals formals actuals)))
    (implies (pseudo-term-listp actuals)
             (<= (pseudo-term-list-count new-actuals)
                 (pseudo-term-list-count actuals))))
  :rule-classes :linear)

Theorem: pseudo-term-list-count-of-fty-remove-equal-formals-actuals

(defthm pseudo-term-list-count-of-fty-remove-equal-formals-actuals
  (b* (((mv ?new-formals ?new-actuals)
        (fty-remove-equal-formals-actuals formals actuals)))
    (<= (pseudo-term-list-count new-actuals)
        (pseudo-term-list-count actuals)))
  :rule-classes :linear)