Lift deftreeops-gen-conc-events to lists.
(deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix) → (mv matching-thm-events check-conc-fn-equiv-thm-events get-tree-list-list-fn-events rep-matching-thmevents get-tree-list-fn-events get-tree-fn-events event-alist)
Function:
(defun deftreeops-gen-conc-list-events-aux (alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix) (declare (xargs :guard (and (alternationp alt) (deftreeops-conc-info-listp infos) (posp i) (common-lisp::symbolp conc-equivs-thm) (common-lisp::symbolp check-conc-fn) (common-lisp::symbolp nonleaf-thm) (common-lisp::symbolp alt-match-thm) (booleanp alt-singletonp) (rulenamep rulename) (common-lisp::symbolp prefix)))) (declare (xargs :guard (equal (len infos) (len alt)))) (let ((__function__ 'deftreeops-gen-conc-list-events-aux)) (declare (ignorable __function__)) (b* (((when (endp alt)) (mv nil nil nil nil nil nil nil)) ((mv matching-thm-event? check-conc-fn-equiv-thm-event? get-tree-list-list-fn-event? rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events event-alist) (deftreeops-gen-conc-events (car alt) (car infos) i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix)) ((mv more-matching-thm-events more-check-conc-fn-equiv-thm-events more-get-tree-list-list-fn-events more-rep-matching-thm-events more-get-tree-list-fn-events more-get-tree-fn-events more-event-alist) (deftreeops-gen-conc-list-events-aux (cdr alt) (cdr infos) (1+ i) conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (mv (append matching-thm-event? more-matching-thm-events) (append check-conc-fn-equiv-thm-event? more-check-conc-fn-equiv-thm-events) (append get-tree-list-list-fn-event? more-get-tree-list-list-fn-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:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.matching-thm-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events-aux alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp matching-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.check-conc-fn-equiv-thm-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events-aux alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp check-conc-fn-equiv-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-list-list-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events-aux alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp get-tree-list-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.rep-matching-thmevents (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events-aux alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp rep-matching-thmevents)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-list-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events-aux alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp get-tree-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events-aux alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp get-tree-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-conc-list-events-aux.event-alist (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events-aux alt infos i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-conc-list-events (alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix) (declare (xargs :guard (and (alternationp alt) (deftreeops-conc-info-listp infos) (common-lisp::symbolp conc-equivs-thm) (common-lisp::symbolp check-conc-fn) (common-lisp::symbolp nonleaf-thm) (common-lisp::symbolp alt-match-thm) (booleanp alt-singletonp) (rulenamep rulename) (common-lisp::symbolp prefix)))) (declare (xargs :guard (equal (len infos) (len alt)))) (let ((__function__ 'deftreeops-gen-conc-list-events)) (declare (ignorable __function__)) (deftreeops-gen-conc-list-events-aux alt infos 1 conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix)))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.matching-thm-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp matching-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.check-conc-fn-equiv-thm-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp check-conc-fn-equiv-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-list-list-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp get-tree-list-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.rep-matching-thmevents (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp rep-matching-thmevents)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-list-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp get-tree-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (pseudo-event-form-listp get-tree-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-conc-list-events.event-alist (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thmevents ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-list-events alt infos conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)