		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Lstate-match-renamevarp

Value matching part of the variable renaming relation over local states.

The full relation is defined in lstate-renamevarp, as consisting of three conditions. This quantified function expresses one of these conditions. The condition is that every pair of variables in the renaming have the same value (if any) in the old and new local states. Note that this allows the local states to have no values for some variable pairs in the renaming, so long as they both do not have it; or they both have it, and it is the same value in that case.

Definitions and Theorems

Theorem: lstate-match-renamevarp-necc

(defthm lstate-match-renamevarp-necc
 (implies
    (lstate-match-renamevarp old new ren)
    (implies (member-equal (cons old-var new-var)
                           (renaming->list ren))
             (equal (cdr (omap::assoc old-var (lstate-fix old)))
                    (cdr (omap::assoc new-var (lstate-fix new)))))))

Theorem: booleanp-of-lstate-match-renamevarp

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

Theorem: lstate-match-renamevarp-of-lstate-fix-old

(defthm lstate-match-renamevarp-of-lstate-fix-old
  (equal (lstate-match-renamevarp (lstate-fix old)
                                  new ren)
         (lstate-match-renamevarp old new ren)))

Theorem: lstate-match-renamevarp-lstate-equiv-congruence-on-old

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

Theorem: lstate-match-renamevarp-of-lstate-fix-new

(defthm lstate-match-renamevarp-of-lstate-fix-new
  (equal (lstate-match-renamevarp old (lstate-fix new)
                                  ren)
         (lstate-match-renamevarp old new ren)))

Theorem: lstate-match-renamevarp-lstate-equiv-congruence-on-new

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

Theorem: lstate-match-renamevarp-of-renaming-fix-ren

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

Theorem: lstate-match-renamevarp-renaming-equiv-congruence-on-ren

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

Theorem: lstate-match-renamevarp-rewrite

(defthm lstate-match-renamevarp-rewrite
  (implies (and (lstate-match-renamevarp old new ren)
                (lstatep old)
                (lstatep new)
                (member-equal (cons old-var new-var)
                              (renaming->list ren)))
           (equal (cdr (omap::assoc old-var old))
                  (cdr (omap::assoc new-var new)))))

Theorem: lstate-match-renamevarp-of-nil

(defthm lstate-match-renamevarp-of-nil
  (lstate-match-renamevarp nil nil (renaming nil)))