conjoin

(in-package "ACL2")

(defsection std/system/conjoin
  :parents (std/system/term-transformations)
  :short "Theorems about @(tsee conjoin) and @(tsee conjoin2)."
  (defthm pseudo-termp-of-conjoin
    (implies (pseudo-term-listp terms)
      (pseudo-termp (conjoin terms))))
  (defthm pseudo-termp-of-conjoin2
    (implies (and (pseudo-termp term1) (pseudo-termp term2))
      (pseudo-termp (conjoin2 term1 term2)))))