		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Funinfo-renamevarp

Variable renaming relation over function information.

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

An old and new function information are related by variable renaming when their inputs and outputs form a renaming under which the bodies are related by the renaming relation.

Definitions and Theorems

Function: funinfo-renamevarp

(defun funinfo-renamevarp (old new)
  (declare (xargs :guard (and (funinfop old) (funinfop new))))
  (let ((__function__ 'funinfo-renamevarp))
    (declare (ignorable __function__))
    (b* ((ren (add-vars-to-var-renaming (funinfo->inputs old)
                                        (funinfo->inputs new)
                                        (renaming nil)))
         ((when (reserrp ren)) nil)
         (ren (add-vars-to-var-renaming (funinfo->outputs old)
                                        (funinfo->outputs new)
                                        ren))
         ((when (reserrp ren)) nil))
      (not (reserrp (block-renamevar (funinfo->body old)
                                     (funinfo->body new)
                                     ren))))))

Theorem: booleanp-of-funinfo-renamevarp

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

Theorem: funinfo-renamevarp-of-funinfo-fix-old

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

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

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

Theorem: funinfo-renamevarp-of-funinfo-fix-new

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

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

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