maximum-length

(in-package "ACL2")

(in-theory (disable maximum-length))

(defthm maximum-length-of-cons
  (equal (maximum-length name (cons a x))
    (if (equal :header (car a))
      (cadr (assoc-keyword :maximum-length (cdr a)))
      (maximum-length name x)))
  :hints (("Goal" :in-theory (enable maximum-length header))))

(defthmd normalize-maximum-length-name
  (implies (syntaxp (not (equal name '':fake-name)))
    (equal (maximum-length name l)
      (maximum-length :fake-name l)))
  :hints (("Goal" :in-theory (enable maximum-length))))

(defthm maximum-length-intro
  (equal (cadr (assoc-keyword :maximum-length (cdr (header name l))))
    (maximum-length name l))
  :hints (("Goal" :in-theory (enable maximum-length))))

(theory-invariant (incompatible (:rewrite maximum-length-intro)
    (:definition maximum-length)))