• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
      • Symbol-symbol-alistp
      • String-string-alistp
      • Symbol-string-alistp
      • Symbol-pseudoterm-alistp
      • String-symbollist-alistp
      • Symbol-pos-alistp
      • Cons-pos-alistp
      • Symbol-symbollist-alistp
      • Symbol-truelist-alistp
      • Keyword-symbol-alistp
      • String-stringlist-alistp
      • Keyword-truelist-alistp
      • Symbol-nat-alistp
      • String-symbol-alistp
      • Keyword-to-keyword-value-list-alistp
      • Std/typed-alists/symbol-alistp
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/typed-alists

Std/typed-alists/symbol-alistp

Theorems about the built-in symbol-alistp.

Definitions and Theorems

Theorem: symbol-alistp-of-append

(defthm symbol-alistp-of-append
        (equal (symbol-alistp (append x y))
               (and (symbol-alistp (true-list-fix x))
                    (symbol-alistp y))))

Theorem: alistp-when-symbol-alistp

(defthm alistp-when-symbol-alistp
        (implies (symbol-alistp x) (alistp x)))