• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
        • Litp
          • Lit-negate-cond
          • Lit-negate
          • Make-lit
          • Lit-equiv
          • Lit->var
          • Lit->neg
          • Maybe-litp
          • Lit-list
          • Lit-fix
          • Lit-list-list
            • Lit-list-list-fix
            • Lit-list-list-equiv
            • Lit-list-listp
              • Lit-list-listp-basics
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Lit-list-listp

Lit-list-listp-basics

Basic theorems about lit-list-listp, generated by deflist.

Definitions and Theorems

Theorem: lit-list-listp-of-cons

(defthm lit-list-listp-of-cons
        (equal (lit-list-listp (cons acl2::a acl2::x))
               (and (lit-listp acl2::a)
                    (lit-list-listp acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: lit-list-listp-of-cdr-when-lit-list-listp

(defthm lit-list-listp-of-cdr-when-lit-list-listp
        (implies (lit-list-listp (double-rewrite acl2::x))
                 (lit-list-listp (cdr acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: lit-list-listp-when-not-consp

(defthm lit-list-listp-when-not-consp
        (implies (not (consp acl2::x))
                 (equal (lit-list-listp acl2::x)
                        (not acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: lit-listp-of-car-when-lit-list-listp

(defthm lit-listp-of-car-when-lit-list-listp
        (implies (lit-list-listp acl2::x)
                 (iff (lit-listp (car acl2::x))
                      (or (consp acl2::x) (lit-listp nil))))
        :rule-classes ((:rewrite)))

Theorem: true-listp-when-lit-list-listp-compound-recognizer

(defthm true-listp-when-lit-list-listp-compound-recognizer
        (implies (lit-list-listp acl2::x)
                 (true-listp acl2::x))
        :rule-classes :compound-recognizer)