		Search-engine friendly clone of the ACL2 documentation.

Truth

Index-swap

Signature
(index-swap n m x) → swap
Arguments: n — first element to swap.
Guard (natp n).; m — second element to swap.
Guard (natp m).; x — index to apply the swap to.
Guard (natp x).
Returns: swap — Type (natp swap).

Definitions and Theorems

Function: index-swap

(defun index-swap (n m x)
       (declare (xargs :guard (and (natp n) (natp m) (natp x))))
       (let ((__function__ 'index-swap))
            (declare (ignorable __function__))
            (b* ((x (lnfix x))
                 (n (lnfix n))
                 (m (lnfix m)))
                (cond ((eql x n) m)
                      ((eql x m) n)
                      (t x)))))

Theorem: natp-of-index-swap

(defthm natp-of-index-swap
        (b* ((swap (index-swap n m x)))
            (natp swap))
        :rule-classes :type-prescription)

Theorem: index-swap-commute

(defthm index-swap-commute
        (equal (index-swap m n x)
               (index-swap n m x))
        :rule-classes ((:rewrite :loop-stopper ((n m)))))

Theorem: index-swap-inverse

(defthm index-swap-inverse
        (equal (index-swap n m (index-swap n m x))
               (nfix x)))

Theorem: index-swap-n

(defthm index-swap-n
        (equal (index-swap n m n) (nfix m)))

Theorem: index-swap-m

(defthm index-swap-m
        (equal (index-swap n m m) (nfix n)))

Theorem: index-swap-unaffected

(defthm index-swap-unaffected
        (implies (and (not (nat-equiv n x))
                      (not (nat-equiv m x)))
                 (equal (index-swap n m x) (nfix x))))

Theorem: index-swap-self

(defthm index-swap-self
        (equal (index-swap n n x) (nfix x)))

Theorem: index-swap-unique

(defthm index-swap-unique
        (iff (equal (index-swap n m x)
                    (index-swap n m y))
             (equal (nfix x) (nfix y))))

Theorem: index-swap-of-nfix-n

(defthm index-swap-of-nfix-n
        (equal (index-swap (nfix n) m x)
               (index-swap n m x)))

Theorem: index-swap-nat-equiv-congruence-on-n

(defthm index-swap-nat-equiv-congruence-on-n
        (implies (nat-equiv n n-equiv)
                 (equal (index-swap n m x)
                        (index-swap n-equiv m x)))
        :rule-classes :congruence)

Theorem: index-swap-of-nfix-m

(defthm index-swap-of-nfix-m
        (equal (index-swap n (nfix m) x)
               (index-swap n m x)))

Theorem: index-swap-nat-equiv-congruence-on-m

(defthm index-swap-nat-equiv-congruence-on-m
        (implies (nat-equiv m m-equiv)
                 (equal (index-swap n m x)
                        (index-swap n m-equiv x)))
        :rule-classes :congruence)

Theorem: index-swap-of-nfix-x

(defthm index-swap-of-nfix-x
        (equal (index-swap n m (nfix x))
               (index-swap n m x)))

Theorem: index-swap-nat-equiv-congruence-on-x

(defthm index-swap-nat-equiv-congruence-on-x
        (implies (nat-equiv x x-equiv)
                 (equal (index-swap n m x)
                        (index-swap n m x-equiv)))
        :rule-classes :congruence)