• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
      • Deftreeops
        • Deftreeops-implementation
          • Deftreeops-event-generation
            • Deftreeops-gen-rep-events
            • Deftreeops-gen-conc-events
            • Deftreeops-gen-rulename-events
            • Deftreeops-gen-rulename-alist-events
            • Deftreeops-gen-discriminant-terms
            • Deftreeops-gen-conc-list-events
            • Deftreeops-gen-rep-list-events
            • Deftreeops-gen-numrange-events
            • Deftreeops-gen-conc-info-list
            • Deftreeops-gen-rep-info
            • Deftreeops-gen-cst-list-list-conc-match
            • Deftreeops-gen-cst-list-list-alt-match
            • Deftreeops-gen-conc-info
            • Deftreeops-gen-all-rulename-infos+events
            • Deftreeops-gen-cst-list-rep-match
            • Deftreeops-gen-cst-list-elem-match
            • Deftreeops-gen-rulename-info-alist
            • Deftreeops-gen-cst-match
            • Deftreeops-gen-charval-events
            • Deftreeops-gen-numrange-alist-events
            • Deftreeops-gen-all-numrange-infos+events
            • Deftreeops-gen-all-charval-infos+events
            • Deftreeops-gen-everything
            • Deftreeops-gen-charval-alist-events
            • Deftreeops-gen-charval-info-alist
            • Deftreeops-gen-rulename-info
            • Deftreeops-gen-rep-info-list
            • Deftreeops-gen-numrange-info-alist
            • Deftreeops-gen-matchers
            • Deftreeops-gen-numrange-info
            • Deftreeops-gen-charval-info
            • Deftreeops-elem-match-pred
            • Deftreeops-conc-match-pred
            • Deftreeops-alt-match-pred
            • Deftreeops-rep-match-pred
            • Deftreeops-match-pred
          • Deftreeops-info
          • Deftreeops-process-inputs-and-gen-everything
          • Deftreeops-fn
          • Deftreeops-table
          • Deftreeops-input-processing
          • Deftreeops-macro-definition
        • Deftreeops-show-event
        • Deftreeops-show-info
      • Defdefparse
      • Defgrammar
      • Tree-utilities
      • Notation
      • Grammar-parser
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
      • Differences-with-paper
      • Constructor-utilities
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Deftreeops-event-generation

Deftreeops-gen-rulename-alist-events

Generate the events for all the rule names in the alist.

Signature

(deftreeops-gen-rulename-alist-events rulename-infos 
                                      charval-infos prefix print) 
 
  → 
(mv nonleaf-thm-events 
    rulename-thm-events match-thm-events 
    concs-thm-events conc-equivs-thm-events 
    check-conc-fn-events 
    get-tree-list-list-fn-events 
    conc-matching-thm-events 
    rep-matching-thm-events 
    get-tree-list-fn-events 
    get-tree-fn-events event-alist) 

Arguments

rulename-infos — Guard (deftreeops-rulename-info-alistp rulename-infos).

charval-infos — Guard (deftreeops-charval-info-alistp charval-infos).

prefix — Guard (common-lisp::symbolp prefix).

print — Guard (evmac-input-print-p print).

Returns

nonleaf-thm-events — Type (pseudo-event-form-listp nonleaf-thm-events).

rulename-thm-events — Type (pseudo-event-form-listp rulename-thm-events).

match-thm-events — Type (pseudo-event-form-listp match-thm-events).

concs-thm-events — Type (pseudo-event-form-listp concs-thm-events).

conc-equivs-thm-events — Type (pseudo-event-form-listp conc-equivs-thm-events).

check-conc-fn-events — Type (pseudo-event-form-listp check-conc-fn-events).

get-tree-list-list-fn-events — Type (pseudo-event-form-listp get-tree-list-list-fn-events).

conc-matching-thm-events — Type (pseudo-event-form-listp conc-matching-thm-events).

rep-matching-thm-events — Type (pseudo-event-form-listp rep-matching-thm-events).

get-tree-list-fn-events — Type (pseudo-event-form-listp get-tree-list-fn-events).

get-tree-fn-events — Type (pseudo-event-form-listp get-tree-fn-events).

event-alist — Type (symbol-pseudoeventform-alistp event-alist).

Definitions and Theorems

Function: deftreeops-gen-rulename-alist-events-aux

(defun deftreeops-gen-rulename-alist-events-aux
       (rest-rulename-infos prefix
                            all-rulename-infos charval-infos print)
 (declare
  (xargs
   :guard (and (deftreeops-rulename-info-alistp rest-rulename-infos)
               (common-lisp::symbolp prefix)
               (deftreeops-rulename-info-alistp all-rulename-infos)
               (deftreeops-charval-info-alistp charval-infos)
               (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-rulename-alist-events-aux))
   (declare (ignorable __function__))
   (b* (((when (endp rest-rulename-infos))
         (mv nil nil nil
             nil nil nil nil nil nil nil nil nil))
        ((cons rulename info)
         (car rest-rulename-infos))
        (alt (deftreeops-rulename-info->alt info))
        ((mv nonleaf-thm-events
             rulename-thm-events match-thm-events
             concs-thm-events conc-equivs-thm-events
             check-conc-fn-events
             get-tree-list-list-fn-events
             conc-matching-thm-events
             rep-matching-thm-events
             get-tree-list-fn-events
             get-tree-fn-events event-alist)
         (deftreeops-gen-rulename-events
              rulename alt info prefix
              all-rulename-infos charval-infos print))
        ((mv more-nonleaf-thm-events
             more-rulename-thm-events
             more-match-thm-events
             more-concs-thm-events
             more-conc-equivs-thm-events
             more-check-conc-fn-events
             more-get-tree-list-list-fn-events
             more-conc-matching-thm-events
             more-rep-matching-thm-events
             more-get-tree-list-fn-events
             more-get-tree-fn-events
             more-event-alist)
         (deftreeops-gen-rulename-alist-events-aux
              (cdr rest-rulename-infos)
              prefix all-rulename-infos
              charval-infos print)))
     (mv (append nonleaf-thm-events
                 more-nonleaf-thm-events)
         (append rulename-thm-events
                 more-rulename-thm-events)
         (append match-thm-events more-match-thm-events)
         (append concs-thm-events more-concs-thm-events)
         (append conc-equivs-thm-events
                 more-conc-equivs-thm-events)
         (append check-conc-fn-events
                 more-check-conc-fn-events)
         (append get-tree-list-list-fn-events
                 more-get-tree-list-list-fn-events)
         (append conc-matching-thm-events
                 more-conc-matching-thm-events)
         (append rep-matching-thm-events
                 more-rep-matching-thm-events)
         (append get-tree-list-fn-events
                 more-get-tree-list-fn-events)
         (append get-tree-fn-events
                 more-get-tree-fn-events)
         (append event-alist more-event-alist)))))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.nonleaf-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.nonleaf-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp nonleaf-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.rulename-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.rulename-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp rulename-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.match-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.match-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp match-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.concs-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.concs-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp concs-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.conc-equivs-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.conc-equivs-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp conc-equivs-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.check-conc-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.check-conc-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp check-conc-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.get-tree-list-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.get-tree-list-list-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp get-tree-list-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.conc-matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.conc-matching-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp conc-matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.rep-matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.rep-matching-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp rep-matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.get-tree-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.get-tree-list-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp get-tree-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.get-tree-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events-aux.get-tree-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (pseudo-event-form-listp get-tree-fn-events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-rulename-alist-events-aux.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-rulename-alist-events-aux.event-alist
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events-aux
            rest-rulename-infos
            prefix all-rulename-infos
            charval-infos print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)

Function: deftreeops-gen-rulename-alist-events

(defun deftreeops-gen-rulename-alist-events
       (rulename-infos charval-infos prefix print)
 (declare
   (xargs
        :guard (and (deftreeops-rulename-info-alistp rulename-infos)
                    (deftreeops-charval-info-alistp charval-infos)
                    (common-lisp::symbolp prefix)
                    (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-rulename-alist-events))
   (declare (ignorable __function__))
   (deftreeops-gen-rulename-alist-events-aux
        rulename-infos prefix
        rulename-infos charval-infos print)))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.nonleaf-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.nonleaf-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp nonleaf-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.rulename-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.rulename-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp rulename-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.match-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.match-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp match-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.concs-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.concs-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp concs-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.conc-equivs-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.conc-equivs-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp conc-equivs-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.check-conc-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.check-conc-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp check-conc-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.get-tree-list-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.get-tree-list-list-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp get-tree-list-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.conc-matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.conc-matching-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp conc-matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.rep-matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.rep-matching-thm-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp rep-matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.get-tree-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.get-tree-list-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp get-tree-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.get-tree-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-alist-events.get-tree-fn-events
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (pseudo-event-form-listp get-tree-fn-events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-rulename-alist-events.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-rulename-alist-events.event-alist
 (b* (((mv ?nonleaf-thm-events ?rulename-thm-events
           ?match-thm-events ?concs-thm-events
           ?conc-equivs-thm-events
           ?check-conc-fn-events
           ?get-tree-list-list-fn-events
           ?conc-matching-thm-events
           ?rep-matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rulename-alist-events
            rulename-infos
            charval-infos prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)