		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Funenv-renamevarp

Variable renaming relation over function environments.

Signature
(funenv-renamevarp old new) → yes/no
Arguments: old — Guard (funenvp old).; new — Guard (funenvp new).
Returns: yes/no — Type (booleanp yes/no).

The two environments must have the same number of scopes, and the corresponding scopes must be related.

Definitions and Theorems

Function: funenv-renamevarp

(defun funenv-renamevarp (old new)
  (declare (xargs :guard (and (funenvp old) (funenvp new))))
  (let ((__function__ 'funenv-renamevarp))
    (declare (ignorable __function__))
    (or (and (endp old) (endp new))
        (and (consp old)
             (consp new)
             (funscope-renamevarp (car old)
                                  (car new))
             (funenv-renamevarp (cdr old)
                                (cdr new))))))

Theorem: booleanp-of-funenv-renamevarp

(defthm booleanp-of-funenv-renamevarp
  (b* ((yes/no (funenv-renamevarp old new)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: funenv-renamevarp-of-funenv-fix-old

(defthm funenv-renamevarp-of-funenv-fix-old
  (equal (funenv-renamevarp (funenv-fix old) new)
         (funenv-renamevarp old new)))

Theorem: funenv-renamevarp-funenv-equiv-congruence-on-old

(defthm funenv-renamevarp-funenv-equiv-congruence-on-old
  (implies (funenv-equiv old old-equiv)
           (equal (funenv-renamevarp old new)
                  (funenv-renamevarp old-equiv new)))
  :rule-classes :congruence)

Theorem: funenv-renamevarp-of-funenv-fix-new

(defthm funenv-renamevarp-of-funenv-fix-new
  (equal (funenv-renamevarp old (funenv-fix new))
         (funenv-renamevarp old new)))

Theorem: funenv-renamevarp-funenv-equiv-congruence-on-new

(defthm funenv-renamevarp-funenv-equiv-congruence-on-new
  (implies (funenv-equiv new new-equiv)
           (equal (funenv-renamevarp old new)
                  (funenv-renamevarp old new-equiv)))
  :rule-classes :congruence)