		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Soutcome-result-renamevarp

Variable renaming relation over statement outcome results.

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

Either they are both (possibly different) errors, or they are related statement outcomes.

Definitions and Theorems

Function: soutcome-result-renamevarp

(defun soutcome-result-renamevarp (old new ren)
  (declare (xargs :guard (and (soutcome-resultp old)
                              (soutcome-resultp new)
                              (renamingp ren))))
  (let ((__function__ 'soutcome-result-renamevarp))
    (declare (ignorable __function__))
    (b* ((old (soutcome-result-fix old))
         (new (soutcome-result-fix new)))
      (or (and (reserrp old) (reserrp new))
          (and (not (reserrp old))
               (not (reserrp new))
               (soutcome-renamevarp old new ren))))))

Theorem: booleanp-of-soutcome-result-renamevarp

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

Theorem: soutcome-result-renamevarp-to-soutcome-renamevarp

(defthm soutcome-result-renamevarp-to-soutcome-renamevarp
  (implies (and (soutcome-resultp x)
                (soutcome-resultp y)
                (not (reserrp x))
                (not (reserrp y)))
           (equal (soutcome-result-renamevarp x y ren)
                  (soutcome-renamevarp x y ren))))

Theorem: soutcome-result-renamevarp-of-errors-not-error

(defthm soutcome-result-renamevarp-of-errors-not-error
  (implies (and (reserrp x) (reserrp y))
           (soutcome-result-renamevarp x y ren)))

Theorem: soutcome-result-renamevarp-of-soutcome-result-fix-old

(defthm soutcome-result-renamevarp-of-soutcome-result-fix-old
  (equal (soutcome-result-renamevarp (soutcome-result-fix old)
                                     new ren)
         (soutcome-result-renamevarp old new ren)))

Theorem: soutcome-result-renamevarp-soutcome-result-equiv-congruence-on-old

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

Theorem: soutcome-result-renamevarp-of-soutcome-result-fix-new

(defthm soutcome-result-renamevarp-of-soutcome-result-fix-new
  (equal (soutcome-result-renamevarp old (soutcome-result-fix new)
                                     ren)
         (soutcome-result-renamevarp old new ren)))

Theorem: soutcome-result-renamevarp-soutcome-result-equiv-congruence-on-new

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

Theorem: soutcome-result-renamevarp-of-renaming-fix-ren

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

Theorem: soutcome-result-renamevarp-renaming-equiv-congruence-on-ren

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