		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-safety

Varset-new

Variables in scope for the new code in variable renaming.

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

This explicates the fact that, as mentioned in renaming-variables, the values of a renaming alist are the variables in scope for the old code.

Also see varset-old.

Definitions and Theorems

Function: varset-new

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

Theorem: identifier-setp-of-varset-new

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

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

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

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

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