		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscope-update-subscope?

Signature
(vl-elabscope-update-subscope? key val x) → new-x
Arguments: key — Guard (vl-elabkey-p key).; val — Guard (vl-elabscope-p val).; x — Guard (vl-elabscope-p x).
Returns: new-x — Type (vl-elabscope-p new-x).

Definitions and Theorems

Function: vl-elabscope-update-subscope?

(defun vl-elabscope-update-subscope? (key val x)
  (declare (xargs :guard (and (vl-elabkey-p key)
                              (vl-elabscope-p val)
                              (vl-elabscope-p x))))
  (let ((__function__ 'vl-elabscope-update-subscope?))
    (declare (ignorable __function__))
    (if (hons-equal (vl-elabscope-subscope key x)
                    (vl-elabscope-fix val))
        (vl-elabscope-fix x)
      (vl-elabscope-update-subscope key val x))))

Theorem: vl-elabscope-p-of-vl-elabscope-update-subscope?

(defthm vl-elabscope-p-of-vl-elabscope-update-subscope?
  (b* ((new-x (vl-elabscope-update-subscope? key val x)))
    (vl-elabscope-p new-x))
  :rule-classes :rewrite)

Theorem: vl-elabscope-update-subscope?-of-vl-elabkey-fix-key

(defthm vl-elabscope-update-subscope?-of-vl-elabkey-fix-key
  (equal (vl-elabscope-update-subscope? (vl-elabkey-fix key)
                                        val x)
         (vl-elabscope-update-subscope? key val x)))

Theorem: vl-elabscope-update-subscope?-vl-elabkey-equiv-congruence-on-key

(defthm
   vl-elabscope-update-subscope?-vl-elabkey-equiv-congruence-on-key
  (implies (vl-elabkey-equiv key key-equiv)
           (equal (vl-elabscope-update-subscope? key val x)
                  (vl-elabscope-update-subscope? key-equiv val x)))
  :rule-classes :congruence)

Theorem: vl-elabscope-update-subscope?-of-vl-elabscope-fix-val

(defthm vl-elabscope-update-subscope?-of-vl-elabscope-fix-val
  (equal (vl-elabscope-update-subscope? key (vl-elabscope-fix val)
                                        x)
         (vl-elabscope-update-subscope? key val x)))

Theorem: vl-elabscope-update-subscope?-vl-elabscope-equiv-congruence-on-val

(defthm
 vl-elabscope-update-subscope?-vl-elabscope-equiv-congruence-on-val
 (implies (vl-elabscope-equiv val val-equiv)
          (equal (vl-elabscope-update-subscope? key val x)
                 (vl-elabscope-update-subscope? key val-equiv x)))
 :rule-classes :congruence)

Theorem: vl-elabscope-update-subscope?-of-vl-elabscope-fix-x

(defthm vl-elabscope-update-subscope?-of-vl-elabscope-fix-x
 (equal (vl-elabscope-update-subscope? key val (vl-elabscope-fix x))
        (vl-elabscope-update-subscope? key val x)))

Theorem: vl-elabscope-update-subscope?-vl-elabscope-equiv-congruence-on-x

(defthm
   vl-elabscope-update-subscope?-vl-elabscope-equiv-congruence-on-x
  (implies (vl-elabscope-equiv x x-equiv)
           (equal (vl-elabscope-update-subscope? key val x)
                  (vl-elabscope-update-subscope? key val x-equiv)))
  :rule-classes :congruence)