		Search-engine friendly clone of the ACL2 documentation.

Truth

Index-move-up

Signature
(index-move-up 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-up

(defun index-move-up (m n x)
  (declare (xargs :guard (and (natp m) (natp n) (natp x))))
  (declare (xargs :guard (<= m n)))
  (let ((__function__ 'index-move-up))
    (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-swap next m x)))
      (index-move-up next n x))))

Theorem: natp-of-index-move-up

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

Theorem: index-move-up-redef

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

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

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

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

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

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

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

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

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

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

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

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

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