		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-rulename-events

Generate the events for a rule name.

Signature
(deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos 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 — Guard (rulenamep rulename).; alt — Guard (alternationp alt).; info — Guard (deftreeops-rulename-infop info).; prefix — Guard (common-lisp::symbolp prefix).; rulename-infos — Information about all the rule names.
Guard (deftreeops-rulename-info-alistp rulename-infos).; charval-infos — Information about all the character value notations.
Guard (deftreeops-charval-info-alistp charval-infos).; 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-events-aux1

(defun deftreeops-gen-rulename-events-aux1 (alt conc-matchp)
 (declare (xargs :guard (and (alternationp alt)
                             (common-lisp::symbolp conc-matchp))))
 (let ((__function__ 'deftreeops-gen-rulename-events-aux1))
  (declare (ignorable __function__))
  (cond
   ((endp alt) nil)
   (t (cons (cons conc-matchp
                  (cons 'cstss
                        (cons (pretty-print-concatenation (car alt))
                              'nil)))
            (deftreeops-gen-rulename-events-aux1 (cdr alt)
                                                 conc-matchp))))))

Theorem: true-listp-of-deftreeops-gen-rulename-events-aux1

(defthm true-listp-of-deftreeops-gen-rulename-events-aux1
  (b* ((disjuncts
            (deftreeops-gen-rulename-events-aux1 alt conc-matchp)))
    (true-listp disjuncts))
  :rule-classes :rewrite)

Function: deftreeops-gen-rulename-events-aux2

(defun deftreeops-gen-rulename-events-aux2
       (alt alt-kind conc-infos rulename-infos
            charval-infos conc-matchp)
 (declare
   (xargs
        :guard (and (alternationp alt)
                    (natp alt-kind)
                    (deftreeops-conc-info-listp conc-infos)
                    (deftreeops-rulename-info-alistp rulename-infos)
                    (deftreeops-charval-info-alistp charval-infos)
                    (common-lisp::symbolp conc-matchp))))
 (declare (xargs :guard (equal (len conc-infos) (len alt))))
 (let ((__function__ 'deftreeops-gen-rulename-events-aux2))
  (declare (ignorable __function__))
  (b*
   (((when (endp alt)) (mv nil nil nil))
    (conc (car alt))
    ((deftreeops-conc-info conc-info)
     (car conc-infos))
    ((unless (and (consp conc) (endp (cdr conc))))
     (raise "Internal error: non-singleton concatenation ~x0."
            conc)
     (mv nil nil nil))
    (rep (car conc))
    ((unless (equal (repetition->range rep)
                    (make-repeat-range :min 1
                                       :max (nati-finite 1))))
     (raise "Internal error: non-singleton repetition ~x0."
            rep)
     (mv nil nil nil))
    (elem (repetition->element rep))
    (conjunct
         (cons 'iff
               (cons (cons conc-matchp
                           (cons '(tree-nonleaf->branches cst)
                                 (cons (pretty-print-element elem)
                                       'nil)))
                     (cons conc-info.discriminant-term 'nil))))
    ((unless (and (consp conc-info.rep-infos)
                  (endp (cdr conc-info.rep-infos))))
     (raise
      "Internal error:
                   non-singleton list of repetition information ~x0."
      conc-info.rep-infos)
     (mv nil nil nil))
    ((deftreeops-rep-info rep-info)
     (car conc-info.rep-infos))
    (rules (list conc-info.matching-thm
                 rep-info.matching-thm))
    (lemma-instance
     (cond
      ((element-case elem :rulename)
       (b*
        ((rulename (element-rulename->get elem))
         (rulename-info (cdr (assoc-equal rulename rulename-infos)))
         ((unless rulename-info)
          (raise "Internal error: no information for rule name ~x0."
                 rulename)))
        (if
         (= alt-kind 1)
         (cons
          ':instance
          (cons
              (deftreeops-rulename-info->rulename-thm rulename-info)
              '((cst (nth 0
                          (nth 0 (tree-nonleaf->branches cst)))))))
         (cons
          ':instance
          (cons
            (deftreeops-rulename-info->nonleaf-thm rulename-info)
            '((cst (nth 0
                        (nth 0 (tree-nonleaf->branches cst))))))))))
      ((element-case elem :char-val)
       (b*
        ((charval (element-char-val->get elem))
         (charval-info (cdr (assoc-equal charval charval-infos)))
         ((unless charval-info)
          (raise
           "Internal error: no information for ~
                           character value notation ~x0."
           charval)))
        (cons
         ':instance
         (cons
             (deftreeops-charval-info->leafterm-thm charval-info)
             '((cst (nth 0
                         (nth 0 (tree-nonleaf->branches cst)))))))))
      (t (raise "Internal error: found element ~x0."
                elem))))
    ((mv more-conjuncts
         more-rules more-lemma-instances)
     (deftreeops-gen-rulename-events-aux2
          (cdr alt)
          alt-kind (cdr conc-infos)
          rulename-infos
          charval-infos conc-matchp)))
   (mv (cons conjunct more-conjuncts)
       (append rules more-rules)
       (cons lemma-instance more-lemma-instances)))))

Theorem: true-listp-of-deftreeops-gen-rulename-events-aux2.conjuncts

(defthm true-listp-of-deftreeops-gen-rulename-events-aux2.conjuncts
  (b* (((mv ?conjuncts ?rules ?lemma-instances)
        (deftreeops-gen-rulename-events-aux2
             alt alt-kind conc-infos rulename-infos
             charval-infos conc-matchp)))
    (true-listp conjuncts))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-deftreeops-gen-rulename-events-aux2.rules

(defthm symbol-listp-of-deftreeops-gen-rulename-events-aux2.rules
  (b* (((mv ?conjuncts ?rules ?lemma-instances)
        (deftreeops-gen-rulename-events-aux2
             alt alt-kind conc-infos rulename-infos
             charval-infos conc-matchp)))
    (symbol-listp rules))
  :rule-classes :rewrite)

Theorem: true-listp-of-deftreeops-gen-rulename-events-aux2.lemma-instances

(defthm
  true-listp-of-deftreeops-gen-rulename-events-aux2.lemma-instances
  (b* (((mv ?conjuncts ?rules ?lemma-instances)
        (deftreeops-gen-rulename-events-aux2
             alt alt-kind conc-infos rulename-infos
             charval-infos conc-matchp)))
    (true-listp lemma-instances))
  :rule-classes :rewrite)

Function: deftreeops-gen-rulename-events-aux3

(defun deftreeops-gen-rulename-events-aux3
       (alt conc-infos i rulename-infos)
 (declare
  (xargs
     :guard (and (alternationp alt)
                 (deftreeops-conc-info-listp conc-infos)
                 (posp i)
                 (deftreeops-rulename-info-alistp rulename-infos))))
 (declare (xargs :guard (equal (len conc-infos) (len alt))))
 (let ((__function__ 'deftreeops-gen-rulename-events-aux3))
  (declare (ignorable __function__))
  (b*
   (((when (endp alt)) (mv nil nil nil))
    (conc (car alt))
    ((deftreeops-conc-info conc-info)
     (car conc-infos))
    ((unless (and (consp conc) (endp (cdr conc))))
     (raise "Internal error: non-singleton concatenation ~x0."
            conc)
     (mv nil nil nil))
    (rep (car conc))
    ((unless (equal (repetition->range rep)
                    (make-repeat-range :min 1
                                       :max (nati-finite 1))))
     (raise "Internal error: non-singleton repetition ~x0."
            rep)
     (mv nil nil nil))
    (elem (repetition->element rep))
    ((unless (element-case elem :rulename))
     (raise "Internal error: element ~x0 is not a rule name."
            elem)
     (mv nil nil nil))
    (rulename (element-rulename->get elem))
    (cond-arm (cons conc-info.discriminant-term
                    (cons i 'nil)))
    (disjunct (cons 'equal
                    (cons 'number (cons i 'nil))))
    (rep-infos (deftreeops-conc-info->rep-infos conc-info))
    ((unless (and (consp rep-infos)
                  (endp (cdr rep-infos))))
     (raise
      "Internal error:
                   non-singleton list of repetition information ~x0."
      rep-infos)
     (mv nil nil nil))
    ((deftreeops-rep-info rep-info)
     (car rep-infos))
    (rulename-info (cdr (assoc-equal rulename rulename-infos)))
    ((unless rulename-info)
     (raise "Internal error: no information for rule name ~x0."
            rulename)
     (mv nil nil nil))
    (rules
        (list (deftreeops-rulename-info->nonleaf-thm rulename-info)
              (deftreeops-rulename-info->rulename-thm rulename-info)
              conc-info.matching-thm
              rep-info.matching-thm))
    ((mv more-cond-arms
         more-disjuncts more-rules)
     (deftreeops-gen-rulename-events-aux3 (cdr alt)
                                          (cdr conc-infos)
                                          (1+ i)
                                          rulename-infos)))
   (mv (cons cond-arm more-cond-arms)
       (cons disjunct more-disjuncts)
       (append rules more-rules)))))

Theorem: true-listp-of-deftreeops-gen-rulename-events-aux3.cond-arms

(defthm true-listp-of-deftreeops-gen-rulename-events-aux3.cond-arms
  (b* (((mv ?cond-arms ?disjuncts ?rules)
        (deftreeops-gen-rulename-events-aux3
             alt conc-infos i rulename-infos)))
    (true-listp cond-arms))
  :rule-classes :rewrite)

Theorem: true-listp-of-deftreeops-gen-rulename-events-aux3.disjuncts

(defthm true-listp-of-deftreeops-gen-rulename-events-aux3.disjuncts
  (b* (((mv ?cond-arms ?disjuncts ?rules)
        (deftreeops-gen-rulename-events-aux3
             alt conc-infos i rulename-infos)))
    (true-listp disjuncts))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-deftreeops-gen-rulename-events-aux3.rules

(defthm symbol-listp-of-deftreeops-gen-rulename-events-aux3.rules
  (b* (((mv ?cond-arms ?disjuncts ?rules)
        (deftreeops-gen-rulename-events-aux3
             alt conc-infos i rulename-infos)))
    (symbol-listp rules))
  :rule-classes :rewrite)

Function: deftreeops-gen-rulename-events

(defun deftreeops-gen-rulename-events
       (rulename alt info prefix
                 rulename-infos charval-infos print)
 (declare
   (xargs
        :guard (and (rulenamep rulename)
                    (alternationp alt)
                    (deftreeops-rulename-infop info)
                    (common-lisp::symbolp prefix)
                    (deftreeops-rulename-info-alistp rulename-infos)
                    (deftreeops-charval-info-alistp charval-infos)
                    (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-rulename-events))
  (declare (ignorable __function__))
  (b*
   (((deftreeops-rulename-info info) info)
    (rulename-string (rulename->get rulename))
    (alt-string (pretty-print-alternation alt))
    (matchp (deftreeops-match-pred prefix))
    (alt-matchp (deftreeops-alt-match-pred prefix))
    (conc-matchp (deftreeops-conc-match-pred prefix))
    ((unless (equal (len info.conc-infos) (len alt)))
     (raise "Internal error: ~x0 and ~x1 have different lengths."
            info.conc-infos alt)
     (mv nil nil nil
         nil nil nil nil nil nil nil nil nil))
    (alt-singletonp (and (consp alt) (endp (cdr alt))))
    ((mv conc-matching-thm-events
         check-conc-fn-equiv-thm-events
         get-tree-list-list-fn-events
         rep-matching-thm-events
         get-tree-list-fn-events
         get-tree-fn-events event-alist)
     (deftreeops-gen-conc-list-events
          alt info.conc-infos
          info.conc-equivs-thm info.check-conc-fn
          info.nonleaf-thm info.match-thm
          alt-singletonp rulename prefix print))
    (nonleaf-thm-event
     (cons
      'defruled
      (cons
       info.nonleaf-thm
       (cons
          (cons 'implies
                (cons (cons matchp
                            (cons 'cst (cons rulename-string 'nil)))
                      '((equal (tree-kind cst) :nonleaf))))
          (cons ':in-theory
                (cons (cons 'quote
                            (cons (cons matchp
                                        '(tree-nonleaf-when-match-rulename/group/option
                                              (:e element-kind)
                                              (:e member-equal)))
                                  'nil))
                      'nil))))))
    (nonleaf-thm-events
     (cons
      nonleaf-thm-event
      (and
         (evmac-input-print->= print :result)
         (cons (cons 'cw-event
                     (cons '"Theorem ~x0.~%"
                           (cons (cons 'quote
                                       (cons info.nonleaf-thm 'nil))
                                 'nil)))
               'nil))))
    (rulename-thm-event
     (cons
      'defruled
      (cons
       info.rulename-thm
       (cons
        (cons
         'implies
         (cons
          (cons matchp
                (cons 'cst (cons rulename-string 'nil)))
          (cons (cons 'equal
                      (cons '(tree-nonleaf->rulename? cst)
                            (cons (cons 'rulename
                                        (cons rulename-string 'nil))
                                  'nil)))
                'nil)))
        (cons
            ':in-theory
            (cons (cons 'quote
                        (cons (cons matchp
                                    '(tree-rulename-when-match-rulename
                                          (:e element-kind)
                                          (:e element-rulename->get)
                                          (:e rulename)))
                              'nil))
                  'nil))))))
    (rulename-thm-events
     (cons
      rulename-thm-event
      (and
        (evmac-input-print->= print :result)
        (cons (cons 'cw-event
                    (cons '"Theorem ~x0.~%"
                          (cons (cons 'quote
                                      (cons info.rulename-thm 'nil))
                                'nil)))
              'nil))))
    (match-thm-event
     (cons
      'defruled
      (cons
       info.match-thm
       (cons
        (cons 'implies
              (cons (cons matchp
                          (cons 'cst (cons rulename-string 'nil)))
                    (cons (cons alt-matchp
                                (cons '(tree-nonleaf->branches cst)
                                      (cons alt-string 'nil)))
                          'nil)))
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
                (cons matchp
                      (cons alt-matchp
                            '(tree-branches-match-alt-when-match-rulename
                                  tree-terminatedp (:e element-kind)
                                  (:e element-rulename->get)
                                  (:e lookup-rulename))))
                'nil))
          (cons ':use
                (cons info.nonleaf-thm 'nil))))))))
    (match-thm-events
     (cons
      match-thm-event
      (and
       (evmac-input-print->= print :result)
       (cons
          (cons 'cw-event
                (cons '"Theorem ~x0.~%"
                      (cons (cons 'quote (cons info.match-thm 'nil))
                            'nil)))
          'nil))))
    (concs-thm-event
     (cons
      'defruled
      (cons
       info.concs-thm
       (cons
        (cons
         'implies
         (cons
          (cons alt-matchp
                (cons 'cstss (cons alt-string 'nil)))
          (cons
           (cons
              'or
              (deftreeops-gen-rulename-events-aux1 alt conc-matchp))
           'nil)))
        (cons
         ':do-not
         (cons
          ''(preprocess)
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               alt-matchp
               (cons
                conc-matchp
                '(tree-list-list-match-alternation-p-when-atom-alternation
                  tree-list-list-match-alternation-p-of-cons-alternation)))
              'nil))
            'nil))))))))
    (concs-thm-events
     (cons
      concs-thm-event
      (and
       (evmac-input-print->= print :result)
       (cons
          (cons 'cw-event
                (cons '"Theorem ~x0.~%"
                      (cons (cons 'quote (cons info.concs-thm 'nil))
                            'nil)))
          'nil))))
    (conc-equivs-thm-event?
     (and
      info.conc-equivs-thm
      (b* (((mv conjuncts rules lemma-instances)
            (deftreeops-gen-rulename-events-aux2
                 alt info.alt-kind
                 info.conc-infos rulename-infos
                 charval-infos conc-matchp)))
       (cons
        (cons
         'defruled
         (cons
          info.conc-equivs-thm
          (cons
           (cons
                'implies
                (cons (cons matchp
                            (cons 'cst (cons rulename-string 'nil)))
                      (cons (cons 'and conjuncts) 'nil)))
           (cons
            ':in-theory
            (cons
             (cons 'quote
                   (cons (append (if (= info.alt-kind 1)
                                     '((:e rulename))
                                   nil)
                                 (cons info.match-thm rules))
                         'nil))
             (cons
              ':use
              (cons
               (cons
                (cons
                     ':instance
                     (cons info.concs-thm
                           '((cstss (tree-nonleaf->branches cst)))))
                lemma-instances)
               'nil)))))))
        'nil))))
    (conc-equivs-thm-events
     (and
      conc-equivs-thm-event?
      (append
       conc-equivs-thm-event?
       (and
        (evmac-input-print->= print :result)
        (cons
           (cons 'cw-event
                 (cons '"Theorem ~x0.~%"
                       (cons (cons 'quote
                                   (cons info.conc-equivs-thm 'nil))
                             'nil)))
           'nil)))))
    (check-conc-fn-event?
     (and
      info.check-conc-fn
      (b* (((mv cond-arms disjuncts rules)
            (deftreeops-gen-rulename-events-aux3
                 alt info.conc-infos 1 rulename-infos)))
       (cons
        (cons
         'define
         (cons
          info.check-conc-fn
          (cons
           '((cst treep))
           (cons
            ':guard
            (cons
             (cons matchp
                   (cons 'cst (cons rulename-string 'nil)))
             (cons
              ':returns
              (cons
               (cons
                'number
                (cons
                 'posp
                 (cons
                  ':hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons (cons info.check-conc-fn '((:e posp)))
                              'nil))
                       'nil)))
                    'nil)
                   'nil))))
               (cons
                (cons 'cond
                      (append cond-arms
                              '((t (prog2$ (acl2::impossible) 1)))))
                (cons
                 ':guard-hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                      (cons
                       'quote
                       (cons
                        (cons
                         'acl2::true-listp-of-nth-when-true-list-listp
                         (cons
                          '(:t tree-nonleaf->branches)
                          (cons
                           'true-list-listp-of-tree-nonleaf->branches
                           (cons
                            'treep-of-nth-when-tree-listp
                            (cons
                             'tree-listp-of-nth-when-tree-list-listp
                             (cons
                              'tree-list-listp-of-tree-nonleaf->branches
                              (cons
                               '(:e rulename)
                               (cons
                                '(:e nfix)
                                (cons
                                 info.nonleaf-thm
                                 (cons
                                      info.match-thm rules))))))))))
                        'nil))
                      (cons
                       ':use
                       (cons
                        (cons
                         (cons
                          ':instance
                          (cons
                           info.concs-thm
                           '((cstss (tree-nonleaf->branches cst)))))
                         'nil)
                        'nil)))))
                   'nil)
                  (cons
                   '///
                   (cons
                    (cons
                     'more-returns
                     (cons
                      (cons
                       'number
                       (cons
                        (cons 'or disjuncts)
                        (cons
                         ':name
                         (cons
                          (packn-pos
                           (list info.check-conc-fn '-possibilities)
                           info.check-conc-fn)
                          (cons
                           ':rule-classes
                           (cons
                            (cons
                             (cons
                              ':forward-chaining
                              (cons
                               ':trigger-terms
                               (cons
                                (cons
                                    (cons info.check-conc-fn '(cst))
                                    'nil)
                                'nil)))
                             'nil)
                            (cons
                             ':hints
                             (cons
                              (cons
                               (cons
                                '"Goal"
                                (cons
                                 ':in-theory
                                 (cons
                                  (cons
                                   'quote
                                   (cons
                                      (cons info.check-conc-fn 'nil)
                                      'nil))
                                  'nil)))
                               'nil)
                              'nil))))))))
                      'nil))
                    (cons
                     (cons
                      'fty::deffixequiv
                      (cons
                       info.check-conc-fn
                       (cons
                        ':hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'quote
                              (cons
                               (cons
                                   info.check-conc-fn
                                   '(tree-nonleaf->branches$inline-tree-equiv-congruence-on-x
                                         tree-fix-under-tree-equiv))
                               'nil))
                             'nil)))
                          'nil)
                         'nil))))
                     check-conc-fn-equiv-thm-events)))))))))))))
        'nil))))
    (check-conc-fn-events
     (and
      check-conc-fn-event?
      (append
       check-conc-fn-event?
       (and
        (evmac-input-print->= print :result)
        (cons
             (cons 'cw-event
                   (cons '"Theorem ~x0.~%"
                         (cons (cons 'quote
                                     (cons info.check-conc-fn 'nil))
                               'nil)))
             'nil))))))
   (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
       (append event-alist
               (list (cons info.nonleaf-thm nonleaf-thm-event))
               (list (cons info.rulename-thm rulename-thm-event))
               (list (cons info.match-thm match-thm-event))
               (list (cons info.concs-thm concs-thm-event))
               (and conc-equivs-thm-event?
                    (list (cons info.conc-equivs-thm
                                (car conc-equivs-thm-event?))))
               (and check-conc-fn-event?
                    (list (cons info.check-conc-fn
                                (car check-conc-fn-event?)))))))))

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

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            rulename-infos charval-infos print)))
   (pseudo-event-form-listp nonleaf-thm-events))
 :rule-classes :rewrite)

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

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            rulename-infos charval-infos print)))
   (pseudo-event-form-listp rulename-thm-events))
 :rule-classes :rewrite)

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

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            rulename-infos charval-infos print)))
   (pseudo-event-form-listp match-thm-events))
 :rule-classes :rewrite)

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

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            rulename-infos charval-infos print)))
   (pseudo-event-form-listp concs-thm-events))
 :rule-classes :rewrite)

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

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            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-events.check-conc-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            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-events.get-tree-list-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            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-events.conc-matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            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-events.rep-matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            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-events.get-tree-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            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-events.get-tree-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            rulename-infos charval-infos print)))
   (pseudo-event-form-listp get-tree-fn-events))
 :rule-classes :rewrite)

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

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-rulename-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-events
            rulename alt info prefix
            rulename-infos charval-infos print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)