		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Cstate-renamevarp

Variable renaming relation over computation states.

Signature
(cstate-renamevarp old new ren) → yes/no
Arguments: old — Guard (cstatep old).; new — Guard (cstatep new).; ren — Guard (renamingp ren).
Returns: yes/no — Type (booleanp yes/no).

The underlying local states must be related.

Definitions and Theorems

Function: cstate-renamevarp

(defun cstate-renamevarp (old new ren)
  (declare (xargs :guard (and (cstatep old)
                              (cstatep new)
                              (renamingp ren))))
  (let ((__function__ 'cstate-renamevarp))
    (declare (ignorable __function__))
    (lstate-renamevarp (cstate->local old)
                       (cstate->local new)
                       ren)))

Theorem: booleanp-of-cstate-renamevarp

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

Theorem: cstate-renamevarp-of-nil

(defthm cstate-renamevarp-of-nil
  (cstate-renamevarp (change-cstate old-cstate :local nil)
                     (change-cstate new-cstate :local nil)
                     (renaming nil)))

Theorem: cstate-renamevarp-of-cstate-fix-old

(defthm cstate-renamevarp-of-cstate-fix-old
  (equal (cstate-renamevarp (cstate-fix old)
                            new ren)
         (cstate-renamevarp old new ren)))

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

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

Theorem: cstate-renamevarp-of-cstate-fix-new

(defthm cstate-renamevarp-of-cstate-fix-new
  (equal (cstate-renamevarp old (cstate-fix new)
                            ren)
         (cstate-renamevarp old new ren)))

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

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

Theorem: cstate-renamevarp-of-renaming-fix-ren

(defthm cstate-renamevarp-of-renaming-fix-ren
  (equal (cstate-renamevarp old new (renaming-fix ren))
         (cstate-renamevarp old new ren)))

Theorem: cstate-renamevarp-renaming-equiv-congruence-on-ren

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