Filtering...

flatten-ands-in-lit

books/std/system/flatten-ands-in-lit

Included Books

constructors pseudo-term-listp
other
(in-package "ACL2")
include-book
(include-book "xdoc/constructors" :dir :system)
local
(local (include-book "std/typed-lists/pseudo-term-listp" :dir :system))
other
(defsection std/system/flatten-ands-in-lit
  :parents (std/system/term-transformations)
  :short (topstring "Theorems about "
    (seetopic "system-utilities"
      "@('flatten-ands-in-lit')")
    ".")
  (defthm pseudo-term-listp-of-flatten-ands-in-lit
    (implies (pseudo-termp term)
      (pseudo-term-listp (flatten-ands-in-lit term)))))
in-theory
(in-theory (disable flatten-ands-in-lit))