Lift deftreeops-gen-rep-events to lists.
(deftreeops-gen-rep-list-events conc infos i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix) → (mv matching-thm-events get-tree-list-fn-events get-tree-fn-events)
Function:
(defun deftreeops-gen-rep-list-events (conc infos i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix) (declare (xargs :guard (and (concatenationp conc) (deftreeops-rep-info-listp infos) (posp i) (common-lisp::symbolp get-tree-list-list-fn) (common-lisp::symbolp get-tree-list-list-fn-match-thm) (common-lisp::symbolp conc-matching-thm) (common-lisp::symbolp check-conc-fn) (rulenamep rulename) (common-lisp::symbolp prefix)))) (declare (xargs :guard (equal (len infos) (len conc)))) (let ((__function__ 'deftreeops-gen-rep-list-events)) (declare (ignorable __function__)) (b* (((when (endp conc)) (mv nil nil nil)) ((mv matching-thm-event? get-tree-list-fn-event? get-tree-fn-event?) (deftreeops-gen-rep-events (car conc) (car infos) i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix)) ((mv more-matching-thm-events more-get-tree-list-fn-events more-get-tree-fn-events) (deftreeops-gen-rep-list-events (cdr conc) (cdr infos) i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (mv (append matching-thm-event? more-matching-thm-events) (append get-tree-list-fn-event? more-get-tree-list-fn-events) (append get-tree-fn-event? more-get-tree-fn-events)))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.matching-thm-events (b* (((mv ?matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events) (deftreeops-gen-rep-list-events conc infos i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (pseudo-event-form-listp matching-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.get-tree-list-fn-events (b* (((mv ?matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events) (deftreeops-gen-rep-list-events conc infos i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (pseudo-event-form-listp get-tree-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.get-tree-fn-events (b* (((mv ?matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events) (deftreeops-gen-rep-list-events conc infos i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (pseudo-event-form-listp get-tree-fn-events)) :rule-classes :rewrite)