		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

4vmasklist-len-fix

Signature
(4vmasklist-len-fix n x) → xx
Arguments: n — Guard (natp n).; x — Guard (4vmasklist-p x).
Returns: xx — Type (4vmasklist-p xx).

Definitions and Theorems

Function: 4vmasklist-len-fix$inline

(defun 4vmasklist-len-fix$inline (n x)
  (declare (xargs :guard (and (natp n) (4vmasklist-p x))))
  (let ((__function__ '4vmasklist-len-fix))
    (declare (ignorable __function__))
    (if (zp n)
        nil
      (if (atom x)
          (cons -1 (4vmasklist-len-fix (1- n) nil))
        (cons (4vmask-fix (car x))
              (4vmasklist-len-fix (1- n) (cdr x)))))))

Theorem: 4vmasklist-p-of-4vmasklist-len-fix

(defthm 4vmasklist-p-of-4vmasklist-len-fix
  (b* ((xx (4vmasklist-len-fix$inline n x)))
    (4vmasklist-p xx))
  :rule-classes :rewrite)

Theorem: len-of-4vmasklist-len-fix

(defthm len-of-4vmasklist-len-fix
  (equal (len (4vmasklist-len-fix n x))
         (nfix n)))

Theorem: 4vmasklist-len-fix-of-cons

(defthm 4vmasklist-len-fix-of-cons
  (equal (4vmasklist-len-fix n (cons a b))
         (if (zp n)
             nil
           (cons (4vmask-fix a)
                 (4vmasklist-len-fix (1- n) b)))))

Theorem: 4vmasklist-len-fix-of-0

(defthm 4vmasklist-len-fix-of-0
  (equal (4vmasklist-len-fix 0 args) nil))

Theorem: 4vmasklist-len-fix$inline-of-nfix-n

(defthm 4vmasklist-len-fix$inline-of-nfix-n
  (equal (4vmasklist-len-fix$inline (nfix n) x)
         (4vmasklist-len-fix$inline n x)))

Theorem: 4vmasklist-len-fix$inline-nat-equiv-congruence-on-n

(defthm 4vmasklist-len-fix$inline-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (4vmasklist-len-fix$inline n x)
                  (4vmasklist-len-fix$inline n-equiv x)))
  :rule-classes :congruence)

Theorem: 4vmasklist-len-fix$inline-of-4vmasklist-fix-x

(defthm 4vmasklist-len-fix$inline-of-4vmasklist-fix-x
  (equal (4vmasklist-len-fix$inline n (4vmasklist-fix x))
         (4vmasklist-len-fix$inline n x)))

Theorem: 4vmasklist-len-fix$inline-4vmasklist-equiv-congruence-on-x

(defthm 4vmasklist-len-fix$inline-4vmasklist-equiv-congruence-on-x
  (implies (4vmasklist-equiv x x-equiv)
           (equal (4vmasklist-len-fix$inline n x)
                  (4vmasklist-len-fix$inline n x-equiv)))
  :rule-classes :congruence)

Theorem: 4veclist-mask-of-4vmasklist-len-fix

(defthm 4veclist-mask-of-4vmasklist-len-fix
  (implies (<= (len x) (nfix len))
           (equal (4veclist-mask (4vmasklist-len-fix len m)
                                 x)
                  (4veclist-mask m x))))

Theorem: 4veclist-mask-of-len-fix

(defthm 4veclist-mask-of-len-fix
 (equal
     (4veclist-mask (4vmasklist-len-fix len (cons mask1 masks))
                    args)
     (and (consp args)
          (if (zp len)
              (4veclist-fix args)
            (cons (4vec-mask mask1 (4veclist-nth-safe 0 args))
                  (4veclist-mask (4vmasklist-len-fix (1- len) masks)
                                 (cdr args)))))))

Theorem: 4veclist-mask-of-len-fix-nthcdr

(defthm 4veclist-mask-of-len-fix-nthcdr
 (equal
     (4veclist-mask (4vmasklist-len-fix len (cons mask1 masks))
                    (nthcdr n args))
     (and (consp (nthcdr n args))
          (if (zp len)
              (4veclist-fix (nthcdr n args))
            (cons (4vec-mask mask1 (4veclist-nth-safe n args))
                  (4veclist-mask (4vmasklist-len-fix (1- len) masks)
                                 (nthcdr (+ 1 (nfix n)) args)))))))