		Search-engine friendly clone of the ACL2 documentation.

Truth

Index-move-down

Signature
(index-move-down m n x) → perm-idx
Arguments: m — Guard (natp m).; n — Guard (natp n).; x — Guard (natp x).
Returns: perm-idx — Type (natp perm-idx).

Definitions and Theorems

Function: index-move-down

(defun index-move-down (m n x)
  (declare (xargs :guard (and (natp m) (natp n) (natp x))))
  (declare (xargs :guard (<= m n)))
  (let ((__function__ 'index-move-down))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (nfix n) (nfix m)))
                     :exec (eql n m)))
          (lnfix x))
         (next (1+ (lnfix m)))
         (x (lnfix x))
         (x (index-move-down next n x)))
      (index-swap next m x))))

Theorem: natp-of-index-move-down

(defthm natp-of-index-move-down
  (b* ((perm-idx (index-move-down m n x)))
    (natp perm-idx))
  :rule-classes :type-prescription)

Theorem: index-move-down-redef

(defthm index-move-down-redef
  (equal (index-move-down m n x)
         (b* ((x (nfix x)) (m (nfix m)) (n (nfix n)))
           (cond ((<= n m) x)
                 ((< x m) x)
                 ((< x n) (1+ x))
                 ((eql x n) m)
                 (t x)))))

Theorem: index-move-up-of-index-move-down

(defthm index-move-up-of-index-move-down
  (equal (index-move-up n m (index-move-down n m x))
         (nfix x)))

Theorem: index-move-down-of-index-move-up

(defthm index-move-down-of-index-move-up
  (equal (index-move-down n m (index-move-up n m x))
         (nfix x)))

Theorem: index-move-down-of-nfix-m

(defthm index-move-down-of-nfix-m
  (equal (index-move-down (nfix m) n x)
         (index-move-down m n x)))

Theorem: index-move-down-nat-equiv-congruence-on-m

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

Theorem: index-move-down-of-nfix-n

(defthm index-move-down-of-nfix-n
  (equal (index-move-down m (nfix n) x)
         (index-move-down m n x)))

Theorem: index-move-down-nat-equiv-congruence-on-n

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

Theorem: index-move-down-of-nfix-x

(defthm index-move-down-of-nfix-x
  (equal (index-move-down m n (nfix x))
         (index-move-down m n x)))

Theorem: index-move-down-nat-equiv-congruence-on-x

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