		Search-engine friendly clone of the ACL2 documentation.

Renamings

Renaming-new

Set of new variables in a renaming.

Signature
(renaming-new ren) → vars
Arguments: ren — Guard (renamingp ren).
Returns: vars — Type (identifier-setp vars).

Definitions and Theorems

Function: renaming-new

(defun renaming-new (ren)
  (declare (xargs :guard (renamingp ren)))
  (let ((__function__ 'renaming-new))
    (declare (ignorable __function__))
    (mergesort (strip-cdrs (renaming->list ren)))))

Theorem: identifier-setp-of-renaming-new

(defthm identifier-setp-of-renaming-new
  (b* ((vars (renaming-new ren)))
    (identifier-setp vars))
  :rule-classes :rewrite)

Theorem: new-var-in-renaming-new-when-in-renaming

(defthm new-var-in-renaming-new-when-in-renaming
  (implies (member-equal (cons old-var new-var)
                         (renaming->list ren))
           (in new-var (renaming-new ren)))
  :rule-classes :forward-chaining)

Theorem: renaming-new-of-renaming-fix-ren

(defthm renaming-new-of-renaming-fix-ren
  (equal (renaming-new (renaming-fix ren))
         (renaming-new ren)))

Theorem: renaming-new-renaming-equiv-congruence-on-ren

(defthm renaming-new-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (renaming-new ren)
                  (renaming-new ren-equiv)))
  :rule-classes :congruence)