		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Matches-remove-zero-length

Signature
(matches-remove-zero-length start-index matches) → new-matches
Arguments: start-index — Guard (natp start-index).; matches — Guard (matchstatelist-p matches).
Returns: new-matches — Type (matchstatelist-p new-matches).

Definitions and Theorems

Function: matches-remove-zero-length

(defun matches-remove-zero-length (start-index matches)
 (declare (xargs :guard (and (natp start-index)
                             (matchstatelist-p matches))))
 (let ((__function__ 'matches-remove-zero-length))
  (declare (ignorable __function__))
  (if (atom matches)
      nil
   (if (< (lnfix start-index)
          (matchstate->index (car matches)))
       (cons (matchstate-fix (car matches))
             (matches-remove-zero-length start-index (cdr matches)))
     (matches-remove-zero-length start-index (cdr matches))))))

Theorem: matchstatelist-p-of-matches-remove-zero-length

(defthm matchstatelist-p-of-matches-remove-zero-length
  (b*
    ((new-matches (matches-remove-zero-length start-index matches)))
    (matchstatelist-p new-matches))
  :rule-classes :rewrite)

Theorem: matchstatelist-measure-of-matches-remove-zero-length

(defthm matchstatelist-measure-of-matches-remove-zero-length
  (b*
   ((?new-matches (matches-remove-zero-length start-index matches)))
   (implies (< (nfix start-index) (strlen x))
            (< (matchstatelist-measure x new-matches)
               (- (strlen x) (nfix start-index)))))
  :rule-classes :linear)

Theorem: matchstatelist-measure-of-matches-remove-zero-length-of-matchstate->index

(defthm
 matchstatelist-measure-of-matches-remove-zero-length-of-matchstate->index
 (b*
   ((new-matches (matches-remove-zero-length (matchstate->index st)
                                             matches)))
   (implies (< (matchstate->index st) (strlen x))
            (< (matchstatelist-measure x new-matches)
               (matchstate-measure x st))))
 :rule-classes :linear)

Theorem: matchstatelist-measure-of-matches-remove-zero-length-of-matchstate->index-weak

(defthm
 matchstatelist-measure-of-matches-remove-zero-length-of-matchstate->index-weak
 (b*
   ((new-matches (matches-remove-zero-length (matchstate->index st)
                                             matches)))
   (<= (matchstatelist-measure x new-matches)
       (matchstate-measure x st)))
 :rule-classes :linear)

Theorem: matches-remove-zero-length-of-nil

(defthm matches-remove-zero-length-of-nil
  (equal (matches-remove-zero-length start-index nil)
         nil))

Theorem: matches-remove-zero-length-preserves-gte

(defthm matches-remove-zero-length-preserves-gte
  (b*
   ((?new-matches (matches-remove-zero-length start-index matches)))
   (implies (matchstatelist-indices-gte n matches)
            (matchstatelist-indices-gte n new-matches))))

Theorem: matches-remove-zero-length-preserves-lte

(defthm matches-remove-zero-length-preserves-lte
  (b*
   ((?new-matches (matches-remove-zero-length start-index matches)))
   (implies (matchstatelist-indices-lte n matches)
            (matchstatelist-indices-lte n new-matches))))

Theorem: matches-remove-zero-length-of-nfix-start-index

(defthm matches-remove-zero-length-of-nfix-start-index
  (equal (matches-remove-zero-length (nfix start-index)
                                     matches)
         (matches-remove-zero-length start-index matches)))

Theorem: matches-remove-zero-length-nat-equiv-congruence-on-start-index

(defthm
     matches-remove-zero-length-nat-equiv-congruence-on-start-index
 (implies
     (acl2::nat-equiv start-index start-index-equiv)
     (equal (matches-remove-zero-length start-index matches)
            (matches-remove-zero-length start-index-equiv matches)))
 :rule-classes :congruence)

Theorem: matches-remove-zero-length-of-matchstatelist-fix-matches

(defthm matches-remove-zero-length-of-matchstatelist-fix-matches
  (equal (matches-remove-zero-length start-index
                                     (matchstatelist-fix matches))
         (matches-remove-zero-length start-index matches)))

Theorem: matches-remove-zero-length-matchstatelist-equiv-congruence-on-matches

(defthm
 matches-remove-zero-length-matchstatelist-equiv-congruence-on-matches
 (implies
     (matchstatelist-equiv matches matches-equiv)
     (equal (matches-remove-zero-length start-index matches)
            (matches-remove-zero-length start-index matches-equiv)))
 :rule-classes :congruence)