• 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
        • Fresh-logical-name-with-$s-suffix
        • Irrelevant-formals-info
        • Std/system/function-queries
        • Std/system/term-queries
        • Std/system/term-transformations
        • Std/system/enhanced-utilities
        • Install-not-normalized-event-lst
        • Install-not-normalized-event
        • Std/system/term-function-recognizers
        • Pseudo-tests-and-call-listp
        • Genvar$
        • Std/system/event-name-queries
        • Maybe-pseudo-event-formp
        • Add-suffix-to-fn-or-const
        • Chk-irrelevant-formals-ok
        • Std/system/good-atom-listp
        • Pseudo-tests-and-callp
        • Table-alist+
        • Add-suffix-to-fn-or-const-lst
        • Known-packages+
        • Add-suffix-to-fn-lst
        • Unquote-term
        • Event-landmark-names
        • Add-suffix-lst
        • Std/system/theorem-queries
        • Unquote-term-list
        • Std/system/macro-queries
        • Pseudo-event-landmark-listp
        • Pseudo-command-landmark-listp
        • Install-not-normalized$
        • Rune-disabledp
        • Known-packages
        • Std/system/partition-rest-and-keyword-args
        • Rune-enabledp
        • Included-books
        • Std/system/pseudo-event-formp
          • Std/system/plist-worldp-with-formals
          • Std/system/w
          • Std/system/geprops
          • Std/system/arglistp
          • Std/system-extensions
          • Std/system/constant-queries
        • Std/basic
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Std/system

    Std/system/pseudo-event-formp

    Theorems about pseudo-event-formp.

    Definitions and Theorems

    Theorem: booleanp-of-pseudo-event-formp

    (defthm booleanp-of-pseudo-event-formp
            (booleanp (pseudo-event-formp x)))

    Theorem: pseudo-event-formp-of-cons

    (defthm pseudo-event-formp-of-cons
            (equal (pseudo-event-formp (cons a b))
                   (and (symbolp a) (true-listp b))))