pseudo-term-listp

(in-package "ACL2")

(defsection std/typed-lists/pseudo-term-listp
  :parents (pseudo-termp)
  :short "Lemmas about lists of @(see pseudo-termp)s, available in the @(see
std/typed-lists) library."
  :long "<p>Most of these are generated automatically with @(see
std::deflist).</p>"
  (deflist pseudo-term-listp
    (x)
    (pseudo-termp x)
    :true-listp t
    :elementp-of-nil t
    :already-definedp t
    :parents nil)
  (defthm pseudo-term-listp-of-remove-equal
    (implies (pseudo-term-listp x)
      (pseudo-term-listp (remove-equal a x))))
  (defthm pseudo-term-listp-of-remove1-equal
    (implies (pseudo-term-listp x)
      (pseudo-term-listp (remove1-equal a x))))
  (defthm pseudo-term-listp-of-make-list-ac
    (equal (pseudo-term-listp (make-list-ac n x ac))
      (and (pseudo-term-listp ac) (or (pseudo-termp x) (zp n)))))
  (defthm pseudo-term-listp-when-symbol-listp
    (implies (symbol-listp syms) (pseudo-term-listp syms)))
  (defthmd true-listp-when-pseudo-term-listp
    (implies (pseudo-term-listp x) (true-listp x))))