		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Matchstatelist-indices-lte

Signature
(matchstatelist-indices-lte n x) → lte
Arguments: n — Guard (natp n).; x — Guard (matchstatelist-p x).

Definitions and Theorems

Function: matchstatelist-indices-lte

(defun matchstatelist-indices-lte (n x)
  (declare (xargs :guard (and (natp n) (matchstatelist-p x))))
  (let ((__function__ 'matchstatelist-indices-lte))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (<= (matchstate->index (car x))
               (lnfix n))
           (matchstatelist-indices-lte n (cdr x))))))

Theorem: matchstatelist-indices-lte-implies-car

(defthm matchstatelist-indices-lte-implies-car
  (b* ((?lte (matchstatelist-indices-lte n x)))
    (implies (and lte (consp x))
             (<= (matchstate->index (car x))
                 (nfix n))))
  :rule-classes :linear)

Theorem: matchstatelist-indices-lte-implies-cdr

(defthm matchstatelist-indices-lte-implies-cdr
  (b* ((?lte (matchstatelist-indices-lte n x)))
    (implies lte
             (matchstatelist-indices-lte n (cdr x)))))

Theorem: matchstatelist-indices-lte-of-append

(defthm matchstatelist-indices-lte-of-append
  (iff (matchstatelist-indices-lte n (append x y))
       (and (matchstatelist-indices-lte n x)
            (matchstatelist-indices-lte n y))))

Theorem: matchstatelist-indices-lte-of-rev

(defthm matchstatelist-indices-lte-of-rev
  (iff (matchstatelist-indices-lte n (rev x))
       (matchstatelist-indices-lte n x)))

Theorem: matchstatelist-indices-lte-of-nil

(defthm matchstatelist-indices-lte-of-nil
  (matchstatelist-indices-lte n nil))

Theorem: matchstatelist-indices-lte-of-remove

(defthm matchstatelist-indices-lte-of-remove
  (implies (matchstatelist-indices-lte n x)
           (matchstatelist-indices-lte n (remove k x))))

Theorem: matchstatelist-indices-lte-of-undup

(defthm matchstatelist-indices-lte-of-undup
  (implies (matchstatelist-indices-lte n x)
           (matchstatelist-indices-lte n (undup x))))

Theorem: matchstatelist-indices-lte-of-set-difference

(defthm matchstatelist-indices-lte-of-set-difference
  (implies (matchstatelist-indices-lte n x)
           (matchstatelist-indices-lte n (set-difference$ x y))))

Theorem: matchstatelist-indices-lte-of-nfix-n

(defthm matchstatelist-indices-lte-of-nfix-n
  (equal (matchstatelist-indices-lte (nfix n) x)
         (matchstatelist-indices-lte n x)))

Theorem: matchstatelist-indices-lte-nat-equiv-congruence-on-n

(defthm matchstatelist-indices-lte-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (matchstatelist-indices-lte n x)
                  (matchstatelist-indices-lte n-equiv x)))
  :rule-classes :congruence)

Theorem: matchstatelist-indices-lte-of-matchstatelist-fix-x

(defthm matchstatelist-indices-lte-of-matchstatelist-fix-x
  (equal (matchstatelist-indices-lte n (matchstatelist-fix x))
         (matchstatelist-indices-lte n x)))

Theorem: matchstatelist-indices-lte-matchstatelist-equiv-congruence-on-x

(defthm
    matchstatelist-indices-lte-matchstatelist-equiv-congruence-on-x
  (implies (matchstatelist-equiv x x-equiv)
           (equal (matchstatelist-indices-lte n x)
                  (matchstatelist-indices-lte n x-equiv)))
  :rule-classes :congruence)