		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)