		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svar-set-index

Signature
(svar-set-index x idx) → xx
Arguments: x — Guard (svar-p x).; idx — Guard (natp idx).
Returns: xx — Type (and (svar-p xx) (svar-indexedp xx)).

Definitions and Theorems

Function: svar-set-index

(defun svar-set-index (x idx)
  (declare (xargs :guard (and (svar-p x) (natp idx))))
  (let ((__function__ 'svar-set-index))
    (declare (ignorable __function__))
    (change-svar x :name (lnfix idx))))

Theorem: return-type-of-svar-set-index

(defthm return-type-of-svar-set-index
  (b* ((xx (svar-set-index x idx)))
    (and (svar-p xx) (svar-indexedp xx)))
  :rule-classes :rewrite)

Theorem: svar-index-of-svar-set-index

(defthm svar-index-of-svar-set-index
  (equal (svar-index (svar-set-index x idx))
         (nfix idx)))

Theorem: svar-set-index-of-svar-fix-x

(defthm svar-set-index-of-svar-fix-x
  (equal (svar-set-index (svar-fix x) idx)
         (svar-set-index x idx)))

Theorem: svar-set-index-svar-equiv-congruence-on-x

(defthm svar-set-index-svar-equiv-congruence-on-x
  (implies (svar-equiv x x-equiv)
           (equal (svar-set-index x idx)
                  (svar-set-index x-equiv idx)))
  :rule-classes :congruence)

Theorem: svar-set-index-of-nfix-idx

(defthm svar-set-index-of-nfix-idx
  (equal (svar-set-index x (nfix idx))
         (svar-set-index x idx)))

Theorem: svar-set-index-nat-equiv-congruence-on-idx

(defthm svar-set-index-nat-equiv-congruence-on-idx
  (implies (nat-equiv idx idx-equiv)
           (equal (svar-set-index x idx)
                  (svar-set-index x idx-equiv)))
  :rule-classes :congruence)