Generate the events for all the rule names in the alist.
(deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix) → (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)
Function:
(defun deftreeops-gen-rulename-alist-events-aux (rest-rulename-infos prefix all-rulename-infos charval-infos) (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)))) (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)) ((cons rulename info) (car rest-rulename-infos)) (alt (deftreeops-rulename-info->alt info)) ((mv nonleaf-thm-event rulename-thm-event match-thm-event concs-thm-event conc-equivs-thm-event? check-conc-fn-event? get-tree-list-list-fn-events conc-matching-thm-events rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events) (deftreeops-gen-rulename-events rulename alt info prefix all-rulename-infos charval-infos)) ((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) (deftreeops-gen-rulename-alist-events-aux (cdr rest-rulename-infos) prefix all-rulename-infos charval-infos))) (mv (cons nonleaf-thm-event more-nonleaf-thm-events) (cons rulename-thm-event more-rulename-thm-events) (cons match-thm-event more-match-thm-events) (cons concs-thm-event more-concs-thm-events) (append conc-equivs-thm-event? more-conc-equivs-thm-events) (append check-conc-fn-event? 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)))))
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp nonleaf-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp rulename-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp match-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp concs-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp conc-equivs-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp check-conc-fn-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp get-tree-list-list-fn-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp conc-matching-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp rep-matching-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp get-tree-list-fn-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events-aux rest-rulename-infos prefix all-rulename-infos charval-infos))) (pseudo-event-form-listp get-tree-fn-events)) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-rulename-alist-events (rulename-infos charval-infos prefix) (declare (xargs :guard (and (deftreeops-rulename-info-alistp rulename-infos) (deftreeops-charval-info-alistp charval-infos) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-rulename-alist-events)) (declare (ignorable __function__)) (deftreeops-gen-rulename-alist-events-aux rulename-infos prefix rulename-infos charval-infos)))
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp nonleaf-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp rulename-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp match-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp concs-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp conc-equivs-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp check-conc-fn-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp get-tree-list-list-fn-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp conc-matching-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp rep-matching-thm-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp get-tree-list-fn-events)) :rule-classes :rewrite)
Theorem:
(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) (deftreeops-gen-rulename-alist-events rulename-infos charval-infos prefix))) (pseudo-event-form-listp get-tree-fn-events)) :rule-classes :rewrite)