		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)