		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Matchstate-measure

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

Definitions and Theorems

Function: matchstate-measure

(defun matchstate-measure (x st)
  (declare (xargs :guard (and (stringp x) (matchstate-p st))))
  (let ((__function__ 'matchstate-measure))
    (declare (ignorable __function__))
    (nfix (- (strlen x) (matchstate->index st)))))

Theorem: natp-of-matchstate-measure

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

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

(defthm matchstate-measure-of-str-fix-x
  (equal (matchstate-measure (acl2::str-fix x)
                             st)
         (matchstate-measure x st)))

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

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

Theorem: matchstate-measure-of-matchstate-fix-st

(defthm matchstate-measure-of-matchstate-fix-st
  (equal (matchstate-measure x (matchstate-fix st))
         (matchstate-measure x st)))

Theorem: matchstate-measure-matchstate-equiv-congruence-on-st

(defthm matchstate-measure-matchstate-equiv-congruence-on-st
  (implies (matchstate-equiv st st-equiv)
           (equal (matchstate-measure x st)
                  (matchstate-measure x st-equiv)))
  :rule-classes :congruence)