		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Matchstatelist-measure

Signature
(matchstatelist-measure x sts) → meas
Arguments: x — Guard (stringp x).; sts — Guard (matchstatelist-p sts).
Returns: meas — Type (natp meas).

Definitions and Theorems

Function: matchstatelist-measure

(defun matchstatelist-measure (x sts)
  (declare (xargs :guard (and (stringp x)
                              (matchstatelist-p sts))))
  (let ((__function__ 'matchstatelist-measure))
    (declare (ignorable __function__))
    (if (atom sts)
        0
      (max (matchstate-measure x (car sts))
           (matchstatelist-measure x (cdr sts))))))

Theorem: natp-of-matchstatelist-measure

(defthm natp-of-matchstatelist-measure
  (b* ((meas (matchstatelist-measure x sts)))
    (natp meas))
  :rule-classes :type-prescription)

Theorem: matchstatelist-measure-gte-car

(defthm matchstatelist-measure-gte-car
  (b* ((?meas (matchstatelist-measure x sts)))
    (implies (consp sts)
             (<= (matchstate-measure x (car sts))
                 meas)))
  :rule-classes :linear)

Theorem: matchstatelist-measure-gte-cdr

(defthm matchstatelist-measure-gte-cdr
  (b* ((?meas (matchstatelist-measure x sts)))
    (implies (consp sts)
             (<= (matchstatelist-measure x (cdr sts))
                 meas)))
  :rule-classes :linear)

Theorem: matchstatelist-measure-of-append

(defthm matchstatelist-measure-of-append
  (equal (matchstatelist-measure x (append a b))
         (max (matchstatelist-measure x a)
              (matchstatelist-measure x b))))

Theorem: matchstatelist-measure-of-nil

(defthm matchstatelist-measure-of-nil
  (equal (matchstatelist-measure x nil)
         0))

Theorem: matchstatelist-measure-of-rev

(defthm matchstatelist-measure-of-rev
  (equal (matchstatelist-measure x (rev sts))
         (matchstatelist-measure x sts)))

Theorem: matchstatelist-meassure-of-matches-add-backref

(defthm matchstatelist-meassure-of-matches-add-backref
 (equal
     (matchstatelist-measure x (matches-add-backref name start sts))
     (matchstatelist-measure x sts)))

Theorem: matchstatelist-measure-of-remove

(defthm matchstatelist-measure-of-remove
  (<= (matchstatelist-measure x (remove k sts))
      (matchstatelist-measure x sts))
  :rule-classes :linear)

Theorem: matchstatelist-measure-of-set-diff

(defthm matchstatelist-measure-of-set-diff
  (<= (matchstatelist-measure x (set-difference$ sts y))
      (matchstatelist-measure x sts))
  :rule-classes :linear)

Theorem: matchstatelist-measure-of-remove-strong-1

(defthm matchstatelist-measure-of-remove-strong-1
  (implies (< (matchstatelist-measure x y)
              (matchstate-measure x k))
           (equal (matchstatelist-measure x (remove k y))
                  (matchstatelist-measure x y))))

Theorem: matchstatelist-measure-of-remove-strong-2

(defthm matchstatelist-measure-of-remove-strong-2
  (implies (< (matchstate-measure x k)
              (matchstatelist-measure x y))
           (equal (matchstatelist-measure x (remove k y))
                  (matchstatelist-measure x y))))

Theorem: matchstatelist-measure-of-undup

(defthm matchstatelist-measure-of-undup
  (equal (matchstatelist-measure x (undup sts))
         (matchstatelist-measure x sts)))

Theorem: undup-equiv-implies-equal-matchstatelist-measure-2

(defthm undup-equiv-implies-equal-matchstatelist-measure-2
  (implies (undup-equiv sts sts-equiv)
           (equal (matchstatelist-measure x sts)
                  (matchstatelist-measure x sts-equiv)))
  :rule-classes (:congruence))

Theorem: matchstatelist-measure-of-str-fix-x

(defthm matchstatelist-measure-of-str-fix-x
  (equal (matchstatelist-measure (acl2::str-fix x)
                                 sts)
         (matchstatelist-measure x sts)))

Theorem: matchstatelist-measure-streqv-congruence-on-x

(defthm matchstatelist-measure-streqv-congruence-on-x
  (implies (acl2::streqv x x-equiv)
           (equal (matchstatelist-measure x sts)
                  (matchstatelist-measure x-equiv sts)))
  :rule-classes :congruence)

Theorem: matchstatelist-measure-of-matchstatelist-fix-sts

(defthm matchstatelist-measure-of-matchstatelist-fix-sts
  (equal (matchstatelist-measure x (matchstatelist-fix sts))
         (matchstatelist-measure x sts)))

Theorem: matchstatelist-measure-matchstatelist-equiv-congruence-on-sts

(defthm
      matchstatelist-measure-matchstatelist-equiv-congruence-on-sts
  (implies (matchstatelist-equiv sts sts-equiv)
           (equal (matchstatelist-measure x sts)
                  (matchstatelist-measure x sts-equiv)))
  :rule-classes :congruence)